FormalConjectures.WrittenOnTheWallII.Test

/-
Copyright 2025 The Formal Conjectures Authors.

Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at

    https://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/

import FormalConjecturesUtil

Testing Graph Invariants

This file contains tests for graph invariants on 5 specific concrete graphs:

HouseGraph: A graph on 5 vertices.

K4: The complete graph on 4 vertices.

PetersenGraph: The Petersen graph on 10 vertices.

C6: The cycle graph on 6 vertices.

Star5: The star graph with 5 leaves (6 vertices total).

Tests cover: independence_number, dominationNumber, average_distance, diameter, radius, girth, order, size, szeged_index, wiener_index, min_degree, max_degree, average_degree, matching_number, residue, annihilation_number, cvetkovic.

open SimpleGraphnamespace WrittenOnTheWallII.Test

House Graph: Square 0-1-2-3-0 with roof 4 connected to 2,3.

abbrev HouseGraph : SimpleGraph (Fin 5) :=
  SimpleGraph.fromEdgeSet {
    s(0, 1), s(1, 2), s(2, 3), s(3, 0),
    s(2, 4), s(3, 4)
  }

K4: Complete graph on 4 vertices.

abbrev K4 : SimpleGraph (Fin 4) := completeGraph (Fin 4)

Petersen Graph on 10 vertices.

abbrev PetersenGraph : SimpleGraph (Fin 10) :=
  SimpleGraph.fromEdgeSet {
    -- Outer Cycle
    s(0, 1), s(1, 2), s(2, 3), s(3, 4), s(4, 0),
    -- Spokes
    s(0, 5), s(1, 6), s(2, 7), s(3, 8), s(4, 9),
    -- Inner Star
    s(5, 7), s(7, 9), s(9, 6), s(6, 8), s(8, 5)
  }

C6: Cycle graph on 6 vertices.

abbrev C6 : SimpleGraph (Fin 6) := cycleGraph 6

Star5: Star graph with center 0 and 5 leaves.

abbrev Star5 : SimpleGraph (Fin 1 ⊕ Fin 5) := completeBipartiteGraph (Fin 1) (Fin 5)

instance : DecidableRel Star5.Adj := by⊢ DecidableRel Star5.Adj unfold Star5 completeBipartiteGraph⊢ DecidableRel
  { Adj := fun v w ↦ v.isLeft = true ∧ w.isRight = true ∨ v.isRight = true ∧ w.isLeft = true, symm := ⋯,
      loopless := ⋯ }.Adj; infer_instanceAll goals completed! 🐙




/-  ### House Graph Tests -/

@[category test, AMS 5]
theorem house_indep : α(HouseGraph) = 2 := by⊢ α(HouseGraph) = 2
  rw [indep_num_eq_computable⊢ HouseGraph.computable_indep_num = 2⊢ HouseGraph.computable_indep_num = 2]⊢ HouseGraph.computable_indep_num = 2; decide +nativeAll goals completed! 🐙



@[category test, AMS 5]
theorem house_dom : dominationNumber HouseGraph = 2 := by⊢ HouseGraph.dominationNumber = 2
  rw [dom_num_eq_computable⊢ HouseGraph.computable_dom_num = 2⊢ HouseGraph.computable_dom_num = 2]⊢ HouseGraph.computable_dom_num = 2; decide +nativeAll goals completed! 🐙



@[category test, AMS 5]
theorem house_avg_dist : averageDistance HouseGraph = 7/5 := by⊢ HouseGraph.averageDistance = 7 / 5
  rw [avg_dist_eq_computable,⊢ ↑HouseGraph.computable_avg_dist = 7 / 5⊢ ↑(7 / 5) = 7 / 5 show computable_avg_dist HouseGraph = (7 / 5 : ℚ) from by⊢ HouseGraph.computable_avg_dist = 7 / 5⊢ ↑(7 / 5) = 7 / 5 decide +nativeAll goals completed! 🐙⊢ ↑(7 / 5) = 7 / 5]⊢ ↑(7 / 5) = 7 / 5
  norm_numAll goals completed! 🐙



@[category test, AMS 5]
theorem house_diameter : ediam HouseGraph = 2 := by⊢ HouseGraph.ediam = 2
  rw [ediam_eq_computable HouseGraph (by⊢ HouseGraph.Connected⊢ ↑HouseGraph.computable_ediam = 2 decideAll goals completed! 🐙⊢ ↑HouseGraph.computable_ediam = 2)]⊢ ↑HouseGraph.computable_ediam = 2
  exact_mod_cast (by⊢ HouseGraph.computable_ediam = 2 decide +nativeAll goals completed! 🐙 : computable_ediam HouseGraph = 2)



@[category test, AMS 5]
theorem house_radius : radius HouseGraph = 2 := by⊢ HouseGraph.radius = 2
  rw [radius_eq_computable HouseGraph (by⊢ HouseGraph.Connected⊢ ↑HouseGraph.computable_radius = 2 decideAll goals completed! 🐙⊢ ↑HouseGraph.computable_radius = 2)]⊢ ↑HouseGraph.computable_radius = 2
  exact_mod_cast (by⊢ HouseGraph.computable_radius = 2 decide +nativeAll goals completed! 🐙 : computable_radius HouseGraph = 2)



@[category test, AMS 5]
theorem house_girth : HouseGraph.girth = 3 := by⊢ HouseGraph.girth = 3
  have hcyc : (Walk.cons (show HouseGraph.Adj 2 3 by decideAll goals completed! 🐙hcyc:(Walk.cons ⋯ (Walk.cons ⋯ (Walk.cons ⋯ Walk.nil))).IsCycle⊢ HouseGraph.girth = 3)
      (Walk.cons (show HouseGraph.Adj 3 4 by decideAll goals completed! 🐙hcyc:(Walk.cons ⋯ (Walk.cons ⋯ (Walk.cons ⋯ Walk.nil))).IsCycle⊢ HouseGraph.girth = 3)
      (Walk.cons (show HouseGraph.Adj 4 2 by decideAll goals completed! 🐙hcyc:(Walk.cons ⋯ (Walk.cons ⋯ (Walk.cons ⋯ Walk.nil))).IsCycle⊢ HouseGraph.girth = 3) Walk.nil))).IsCycle := by
    rw [Walk.isCycle_def⊢ (Walk.cons ⋯ (Walk.cons ⋯ (Walk.cons ⋯ Walk.nil))).IsTrail ∧
  Walk.cons ⋯ (Walk.cons ⋯ (Walk.cons ⋯ Walk.nil)) ≠ Walk.nil ∧
    (Walk.cons ⋯ (Walk.cons ⋯ (Walk.cons ⋯ Walk.nil))).support.tail.Nodup⊢ (Walk.cons ⋯ (Walk.cons ⋯ (Walk.cons ⋯ Walk.nil))).IsTrail ∧
  Walk.cons ⋯ (Walk.cons ⋯ (Walk.cons ⋯ Walk.nil)) ≠ Walk.nil ∧
    (Walk.cons ⋯ (Walk.cons ⋯ (Walk.cons ⋯ Walk.nil))).support.tail.Noduphcyc:(Walk.cons ⋯ (Walk.cons ⋯ (Walk.cons ⋯ Walk.nil))).IsCycle⊢ HouseGraph.girth = 3]⊢ (Walk.cons ⋯ (Walk.cons ⋯ (Walk.cons ⋯ Walk.nil))).IsTrail ∧
  Walk.cons ⋯ (Walk.cons ⋯ (Walk.cons ⋯ Walk.nil)) ≠ Walk.nil ∧
    (Walk.cons ⋯ (Walk.cons ⋯ (Walk.cons ⋯ Walk.nil))).support.tail.Noduphcyc:(Walk.cons ⋯ (Walk.cons ⋯ (Walk.cons ⋯ Walk.nil))).IsCycle⊢ HouseGraph.girth = 3
    refine ⟨?_, ?_, ?_⟩refine_1⊢ (Walk.cons ⋯ (Walk.cons ⋯ (Walk.cons ⋯ Walk.nil))).IsTrailrefine_2⊢ Walk.cons ⋯ (Walk.cons ⋯ (Walk.cons ⋯ Walk.nil)) ≠ Walk.nilrefine_3⊢ (Walk.cons ⋯ (Walk.cons ⋯ (Walk.cons ⋯ Walk.nil))).support.tail.Noduphcyc:(Walk.cons ⋯ (Walk.cons ⋯ (Walk.cons ⋯ Walk.nil))).IsCycle⊢ HouseGraph.girth = 3
    ·refine_1⊢ (Walk.cons ⋯ (Walk.cons ⋯ (Walk.cons ⋯ Walk.nil))).IsTrailhcyc:(Walk.cons ⋯ (Walk.cons ⋯ (Walk.cons ⋯ Walk.nil))).IsCycle⊢ HouseGraph.girth = 3 rw [Walk.isTrail_defrefine_1⊢ (Walk.cons ⋯ (Walk.cons ⋯ (Walk.cons ⋯ Walk.nil))).edges.Noduprefine_1⊢ (Walk.cons ⋯ (Walk.cons ⋯ (Walk.cons ⋯ Walk.nil))).edges.Noduphcyc:(Walk.cons ⋯ (Walk.cons ⋯ (Walk.cons ⋯ Walk.nil))).IsCycle⊢ HouseGraph.girth = 3]refine_1⊢ (Walk.cons ⋯ (Walk.cons ⋯ (Walk.cons ⋯ Walk.nil))).edges.Noduphcyc:(Walk.cons ⋯ (Walk.cons ⋯ (Walk.cons ⋯ Walk.nil))).IsCycle⊢ HouseGraph.girth = 3; decideAll goals completed! 🐙hcyc:(Walk.cons ⋯ (Walk.cons ⋯ (Walk.cons ⋯ Walk.nil))).IsCycle⊢ HouseGraph.girth = 3
    ·refine_2⊢ Walk.cons ⋯ (Walk.cons ⋯ (Walk.cons ⋯ Walk.nil)) ≠ Walk.nilhcyc:(Walk.cons ⋯ (Walk.cons ⋯ (Walk.cons ⋯ Walk.nil))).IsCycle⊢ HouseGraph.girth = 3 simpAll goals completed! 🐙hcyc:(Walk.cons ⋯ (Walk.cons ⋯ (Walk.cons ⋯ Walk.nil))).IsCycle⊢ HouseGraph.girth = 3
    ·refine_3⊢ (Walk.cons ⋯ (Walk.cons ⋯ (Walk.cons ⋯ Walk.nil))).support.tail.Noduphcyc:(Walk.cons ⋯ (Walk.cons ⋯ (Walk.cons ⋯ Walk.nil))).IsCycle⊢ HouseGraph.girth = 3 decidehcyc:(Walk.cons ⋯ (Walk.cons ⋯ (Walk.cons ⋯ Walk.nil))).IsCycle⊢ HouseGraph.girth = 3hcyc:(Walk.cons ⋯ (Walk.cons ⋯ (Walk.cons ⋯ Walk.nil))).IsCycle⊢ HouseGraph.girth = 3
  refine le_antisymm ?_ (three_le_girth (fun hac => hac _ hcyc))hcyc:(Walk.cons ⋯ (Walk.cons ⋯ (Walk.cons ⋯ Walk.nil))).IsCycle⊢ HouseGraph.girth ≤ 3
  simpa using girth_le_length hcycAll goals completed! 🐙



open scoped Classical in
@[category test, AMS 5]
theorem house_order : Fintype.card ↥(⊤ : Subgraph HouseGraph).verts = 5 := by⊢ Fintype.card ↑⊤.verts = 5
  rw [Fintype.card_congr SimpleGraph.Subgraph.topIso.toEquiv⊢ Fintype.card (Fin 5) = 5⊢ Fintype.card (Fin 5) = 5]⊢ Fintype.card (Fin 5) = 5
  rflAll goals completed! 🐙

@[category test, AMS 5]
theorem house_size : HouseGraph.edgeFinset.card = 6 := by⊢ HouseGraph.edgeFinset.card = 6
  decide +nativeAll goals completed! 🐙



@[category test, AMS 5]
theorem house_szeged : szegedIndex HouseGraph = 24 := by⊢ HouseGraph.szegedIndex = 24
  rw [szeged_eq_computable⊢ HouseGraph.computable_szeged_index = 24⊢ HouseGraph.computable_szeged_index = 24]⊢ HouseGraph.computable_szeged_index = 24; decide +nativeAll goals completed! 🐙



@[category test, AMS 5]
theorem house_wiener : wienerIndex HouseGraph = 14 := by⊢ HouseGraph.wienerIndex = 14
  rw [wiener_eq_computable⊢ HouseGraph.computable_wiener = 14⊢ HouseGraph.computable_wiener = 14]⊢ HouseGraph.computable_wiener = 14; decide +nativeAll goals completed! 🐙

@[category test, AMS 5]
theorem house_min_deg : HouseGraph.minDegree = 2 := by⊢ HouseGraph.minDegree = 2
  decide +nativeAll goals completed! 🐙

@[category test, AMS 5]
theorem house_max_deg : HouseGraph.maxDegree = 3 := by⊢ HouseGraph.maxDegree = 3
  decide +nativeAll goals completed! 🐙

@[category test, AMS 5]
theorem house_avg_deg : averageDegree HouseGraph = 12/5 := by⊢ HouseGraph.averageDegree = 12 / 5
  unfold averageDegree⊢ (∑ v, ↑(HouseGraph.degree v)) / ↑(Fintype.card (Fin 5)) = 12 / 5; simp [Fintype.card_fin]⊢ ∑ v, ↑(HouseGraph.degree v) = 12; decide +nativeAll goals completed! 🐙



@[category test, AMS 5]
theorem house_matching : matchingNumber HouseGraph = 2 := by⊢ HouseGraph.matchingNumber = 2
  classical
  have hbdd : BddAbove (Set.image (fun M : Subgraph HouseGraph => (M.edgeSet.toFinset.card : ℝ)) {M | M.IsMatching}) := by
    refine ⟨(Fintype.card (Fin 5) : ℝ), ?_⟩⊢ ↑(Fintype.card (Fin 5)) ∈ upperBounds ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})hbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ HouseGraph.matchingNumber = 2
    rintro x ⟨M, hM, rfl⟩M:HouseGraph.SubgraphhM:M ∈ {M | M.IsMatching}⊢ (fun M ↦ ↑M.edgeSet.toFinset.card) M ≤ ↑(Fintype.card (Fin 5))hbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ HouseGraph.matchingNumber = 2
    show (M.edgeSet.toFinset.card : ℝ) ≤ Fintype.card (Fin 5)M:HouseGraph.SubgraphhM:M ∈ {M | M.IsMatching}⊢ ↑M.edgeSet.toFinset.card ≤ ↑(Fintype.card (Fin 5))hbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ HouseGraph.matchingNumber = 2
    have hb := matching_card_bound HouseGraph M hMM:HouseGraph.SubgraphhM:M ∈ {M | M.IsMatching}hb:2 * M.edgeSet.toFinset.card ≤ Fintype.card (Fin 5)⊢ ↑M.edgeSet.toFinset.card ≤ ↑(Fintype.card (Fin 5))hbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ HouseGraph.matchingNumber = 2
    exact_mod_cast (byM:HouseGraph.SubgraphhM:M ∈ {M | M.IsMatching}hb:2 * M.edgeSet.toFinset.card ≤ Fintype.card (Fin 5)⊢ M.edgeSet.toFinset.card ≤ Fintype.card (Fin 5)hbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ HouseGraph.matchingNumber = 2 omegaAll goals completed! 🐙hbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ HouseGraph.matchingNumber = 2 : M.edgeSet.toFinset.card ≤ Fintype.card (Fin 5))hbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ HouseGraph.matchingNumber = 2
  unfold matchingNumberhbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ (have matchings := {M | M.IsMatching};
  sSup ((fun M ↦ ↑M.edgeSet.toFinset.card) '' matchings)) =
  2
  apply le_antisymmahbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ (have matchings := {M | M.IsMatching};
  sSup ((fun M ↦ ↑M.edgeSet.toFinset.card) '' matchings)) ≤
  2ahbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ 2 ≤
  have matchings := {M | M.IsMatching};
  sSup ((fun M ↦ ↑M.edgeSet.toFinset.card) '' matchings)
  ·ahbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ (have matchings := {M | M.IsMatching};
  sSup ((fun M ↦ ↑M.edgeSet.toFinset.card) '' matchings)) ≤
  2 apply csSup_le (Set.Nonempty.image _ ⟨⊥, byhbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ ⊥ ∈ {M | M.IsMatching} simp [Subgraph.IsMatching]All goals completed! 🐙⟩)
    rintro x ⟨M, hM, rfl⟩ahbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})M:HouseGraph.SubgraphhM:M ∈ {M | M.IsMatching}⊢ (fun M ↦ ↑M.edgeSet.toFinset.card) M ≤ 2
    show (M.edgeSet.toFinset.card : ℝ) ≤ 2ahbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})M:HouseGraph.SubgraphhM:M ∈ {M | M.IsMatching}⊢ ↑M.edgeSet.toFinset.card ≤ 2
    have hb := matching_card_bound HouseGraph M hMahbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})M:HouseGraph.SubgraphhM:M ∈ {M | M.IsMatching}hb:2 * M.edgeSet.toFinset.card ≤ Fintype.card (Fin 5)⊢ ↑M.edgeSet.toFinset.card ≤ 2
    simp only [Fintype.card_fin] at hbahbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})M:HouseGraph.SubgraphhM:M ∈ {M | M.IsMatching}hb:2 * M.edgeSet.toFinset.card ≤ 5⊢ ↑M.edgeSet.toFinset.card ≤ 2
    exact_mod_cast (byhbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})M:HouseGraph.SubgraphhM:M ∈ {M | M.IsMatching}hb:2 * M.edgeSet.toFinset.card ≤ 5⊢ M.edgeSet.toFinset.card ≤ 2 omegaAll goals completed! 🐙 : M.edgeSet.toFinset.card ≤ 2)
  ·ahbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ 2 ≤
  have matchings := {M | M.IsMatching};
  sSup ((fun M ↦ ↑M.edgeSet.toFinset.card) '' matchings) apply le_csSup hbddahbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ 2 ∈ (fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching}
    refine ⟨HouseGraph.subgraphOfAdj (show HouseGraph.Adj 0 1 by⊢ HouseGraph.matchingNumber = 2 decideAll goals completed! 🐙) ⊔ HouseGraph.subgraphOfAdj (show HouseGraph.Adj 2 3 by⊢ HouseGraph.matchingNumber = 2 decideAll goals completed! 🐙), ?_, ?_⟩
    ·a.refine_1hbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ HouseGraph.subgraphOfAdj ⋯ ⊔ HouseGraph.subgraphOfAdj ⋯ ∈ {M | M.IsMatching} exact (Subgraph.IsMatching.subgraphOfAdj _).sup (Subgraph.IsMatching.subgraphOfAdj _)
        (byhbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ Disjoint (HouseGraph.subgraphOfAdj ⋯).support (HouseGraph.subgraphOfAdj ⋯).support rw [support_subgraphOfAdj,hbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ Disjoint {0, 1} (HouseGraph.subgraphOfAdj ⋯).supporthbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ Disjoint {0, 1} {2, 3} support_subgraphOfAdjhbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ Disjoint {0, 1} {2, 3}hbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ Disjoint {0, 1} {2, 3}]hbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ Disjoint {0, 1} {2, 3}; simp [Set.disjoint_left]All goals completed! 🐙)
    ·a.refine_2hbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ (fun M ↦ ↑M.edgeSet.toFinset.card) (HouseGraph.subgraphOfAdj ⋯ ⊔ HouseGraph.subgraphOfAdj ⋯) = 2 simpAll goals completed! 🐙

@[category test, AMS 5]
theorem house_residue : residue HouseGraph = 2 := by⊢ HouseGraph.residue = 2
  unfold residue⊢ residueAux ((Multiset.map (fun v ↦ HouseGraph.degree v) Finset.univ.val).sort fun x1 x2 ↦ x1 ≥ x2) = 2; decide +nativeAll goals completed! 🐙

@[category test, AMS 5]
theorem house_annihilation : annihilationNumber HouseGraph = 3 := by⊢ HouseGraph.annihilationNumber = 3
  decide +nativeAll goals completed! 🐙

@[category test, AMS 5]
theorem house_cvetkovic : cvetkovic HouseGraph = 3 := by⊢ HouseGraph.cvetkovic = 3
  sorryAll goals completed! 🐙




/-  ### K4 Tests -/

@[category test, AMS 5]
theorem K4_indep : α(K4) = 1 := by⊢ α(K4) = 1
  rw [indep_num_eq_computable⊢ K4.computable_indep_num = 1⊢ K4.computable_indep_num = 1]⊢ K4.computable_indep_num = 1; decide +nativeAll goals completed! 🐙



@[category test, AMS 5]
theorem K4_dom : dominationNumber K4 = 1 := by⊢ K4.dominationNumber = 1
  rw [dom_num_eq_computable⊢ K4.computable_dom_num = 1⊢ K4.computable_dom_num = 1]⊢ K4.computable_dom_num = 1; decide +nativeAll goals completed! 🐙



@[category test, AMS 5]
theorem K4_avg_dist : averageDistance K4 = 1 := by⊢ K4.averageDistance = 1
  rw [avg_dist_eq_computable,⊢ ↑K4.computable_avg_dist = 1⊢ ↑1 = 1 show computable_avg_dist K4 = (1 : ℚ) from by⊢ K4.computable_avg_dist = 1⊢ ↑1 = 1 decide +nativeAll goals completed! 🐙⊢ ↑1 = 1]⊢ ↑1 = 1
  norm_numAll goals completed! 🐙



@[category test, AMS 5]
theorem K4_diameter : ediam K4 = 1 := by⊢ K4.ediam = 1
  rw [ediam_eq_computable K4 (by⊢ K4.Connected⊢ ↑K4.computable_ediam = 1 decideAll goals completed! 🐙⊢ ↑K4.computable_ediam = 1)]⊢ ↑K4.computable_ediam = 1
  exact_mod_cast (by⊢ K4.computable_ediam = 1 decide +nativeAll goals completed! 🐙 : computable_ediam K4 = 1)



@[category test, AMS 5]
theorem K4_radius : radius K4 = 1 := by⊢ K4.radius = 1
  rw [radius_eq_computable K4 (by⊢ K4.Connected⊢ ↑K4.computable_radius = 1 decideAll goals completed! 🐙⊢ ↑K4.computable_radius = 1)]⊢ ↑K4.computable_radius = 1
  exact_mod_cast (by⊢ K4.computable_radius = 1 decide +nativeAll goals completed! 🐙 : computable_radius K4 = 1)



@[category test, AMS 5]
theorem K4_girth : K4.girth = 3 := by⊢ K4.girth = 3
  have hcyc : (Walk.cons (show K4.Adj 0 1 by decideAll goals completed! 🐙hcyc:(Walk.cons ⋯ (Walk.cons ⋯ (Walk.cons ⋯ Walk.nil))).IsCycle⊢ K4.girth = 3)
      (Walk.cons (show K4.Adj 1 2 by decideAll goals completed! 🐙hcyc:(Walk.cons ⋯ (Walk.cons ⋯ (Walk.cons ⋯ Walk.nil))).IsCycle⊢ K4.girth = 3)
      (Walk.cons (show K4.Adj 2 0 by decideAll goals completed! 🐙hcyc:(Walk.cons ⋯ (Walk.cons ⋯ (Walk.cons ⋯ Walk.nil))).IsCycle⊢ K4.girth = 3) Walk.nil))).IsCycle := by
    rw [Walk.isCycle_def⊢ (Walk.cons ⋯ (Walk.cons ⋯ (Walk.cons ⋯ Walk.nil))).IsTrail ∧
  Walk.cons ⋯ (Walk.cons ⋯ (Walk.cons ⋯ Walk.nil)) ≠ Walk.nil ∧
    (Walk.cons ⋯ (Walk.cons ⋯ (Walk.cons ⋯ Walk.nil))).support.tail.Nodup⊢ (Walk.cons ⋯ (Walk.cons ⋯ (Walk.cons ⋯ Walk.nil))).IsTrail ∧
  Walk.cons ⋯ (Walk.cons ⋯ (Walk.cons ⋯ Walk.nil)) ≠ Walk.nil ∧
    (Walk.cons ⋯ (Walk.cons ⋯ (Walk.cons ⋯ Walk.nil))).support.tail.Noduphcyc:(Walk.cons ⋯ (Walk.cons ⋯ (Walk.cons ⋯ Walk.nil))).IsCycle⊢ K4.girth = 3]⊢ (Walk.cons ⋯ (Walk.cons ⋯ (Walk.cons ⋯ Walk.nil))).IsTrail ∧
  Walk.cons ⋯ (Walk.cons ⋯ (Walk.cons ⋯ Walk.nil)) ≠ Walk.nil ∧
    (Walk.cons ⋯ (Walk.cons ⋯ (Walk.cons ⋯ Walk.nil))).support.tail.Noduphcyc:(Walk.cons ⋯ (Walk.cons ⋯ (Walk.cons ⋯ Walk.nil))).IsCycle⊢ K4.girth = 3
    refine ⟨?_, ?_, ?_⟩refine_1⊢ (Walk.cons ⋯ (Walk.cons ⋯ (Walk.cons ⋯ Walk.nil))).IsTrailrefine_2⊢ Walk.cons ⋯ (Walk.cons ⋯ (Walk.cons ⋯ Walk.nil)) ≠ Walk.nilrefine_3⊢ (Walk.cons ⋯ (Walk.cons ⋯ (Walk.cons ⋯ Walk.nil))).support.tail.Noduphcyc:(Walk.cons ⋯ (Walk.cons ⋯ (Walk.cons ⋯ Walk.nil))).IsCycle⊢ K4.girth = 3
    ·refine_1⊢ (Walk.cons ⋯ (Walk.cons ⋯ (Walk.cons ⋯ Walk.nil))).IsTrailhcyc:(Walk.cons ⋯ (Walk.cons ⋯ (Walk.cons ⋯ Walk.nil))).IsCycle⊢ K4.girth = 3 rw [Walk.isTrail_defrefine_1⊢ (Walk.cons ⋯ (Walk.cons ⋯ (Walk.cons ⋯ Walk.nil))).edges.Noduprefine_1⊢ (Walk.cons ⋯ (Walk.cons ⋯ (Walk.cons ⋯ Walk.nil))).edges.Noduphcyc:(Walk.cons ⋯ (Walk.cons ⋯ (Walk.cons ⋯ Walk.nil))).IsCycle⊢ K4.girth = 3]refine_1⊢ (Walk.cons ⋯ (Walk.cons ⋯ (Walk.cons ⋯ Walk.nil))).edges.Noduphcyc:(Walk.cons ⋯ (Walk.cons ⋯ (Walk.cons ⋯ Walk.nil))).IsCycle⊢ K4.girth = 3; decideAll goals completed! 🐙hcyc:(Walk.cons ⋯ (Walk.cons ⋯ (Walk.cons ⋯ Walk.nil))).IsCycle⊢ K4.girth = 3
    ·refine_2⊢ Walk.cons ⋯ (Walk.cons ⋯ (Walk.cons ⋯ Walk.nil)) ≠ Walk.nilhcyc:(Walk.cons ⋯ (Walk.cons ⋯ (Walk.cons ⋯ Walk.nil))).IsCycle⊢ K4.girth = 3 simpAll goals completed! 🐙hcyc:(Walk.cons ⋯ (Walk.cons ⋯ (Walk.cons ⋯ Walk.nil))).IsCycle⊢ K4.girth = 3
    ·refine_3⊢ (Walk.cons ⋯ (Walk.cons ⋯ (Walk.cons ⋯ Walk.nil))).support.tail.Noduphcyc:(Walk.cons ⋯ (Walk.cons ⋯ (Walk.cons ⋯ Walk.nil))).IsCycle⊢ K4.girth = 3 decidehcyc:(Walk.cons ⋯ (Walk.cons ⋯ (Walk.cons ⋯ Walk.nil))).IsCycle⊢ K4.girth = 3hcyc:(Walk.cons ⋯ (Walk.cons ⋯ (Walk.cons ⋯ Walk.nil))).IsCycle⊢ K4.girth = 3
  refine le_antisymm ?_ (three_le_girth (fun hac => hac _ hcyc))hcyc:(Walk.cons ⋯ (Walk.cons ⋯ (Walk.cons ⋯ Walk.nil))).IsCycle⊢ K4.girth ≤ 3
  simpa using girth_le_length hcycAll goals completed! 🐙



open scoped Classical in
@[category test, AMS 5]
theorem K4_order : Fintype.card ↥(⊤ : Subgraph K4).verts = 4 := by⊢ Fintype.card ↑⊤.verts = 4
  rw [Fintype.card_congr SimpleGraph.Subgraph.topIso.toEquiv⊢ Fintype.card (Fin 4) = 4⊢ Fintype.card (Fin 4) = 4]⊢ Fintype.card (Fin 4) = 4
  rflAll goals completed! 🐙

@[category test, AMS 5]
theorem K4_size : K4.edgeFinset.card = 6 := by⊢ K4.edgeFinset.card = 6
  decide +nativeAll goals completed! 🐙



@[category test, AMS 5]
theorem K4_szeged : szegedIndex K4 = 6 := by⊢ K4.szegedIndex = 6
  rw [szeged_eq_computable⊢ K4.computable_szeged_index = 6⊢ K4.computable_szeged_index = 6]⊢ K4.computable_szeged_index = 6; decide +nativeAll goals completed! 🐙



@[category test, AMS 5]
theorem K4_wiener : wienerIndex K4 = 6 := by⊢ K4.wienerIndex = 6
  rw [wiener_eq_computable⊢ K4.computable_wiener = 6⊢ K4.computable_wiener = 6]⊢ K4.computable_wiener = 6; decide +nativeAll goals completed! 🐙

@[category test, AMS 5]
theorem K4_min_deg : K4.minDegree = 3 := by⊢ K4.minDegree = 3
  decide +nativeAll goals completed! 🐙

@[category test, AMS 5]
theorem K4_max_deg : K4.maxDegree = 3 := by⊢ K4.maxDegree = 3
  decide +nativeAll goals completed! 🐙

@[category test, AMS 5]
theorem K4_avg_deg : averageDegree K4 = 3 := by⊢ K4.averageDegree = 3
  unfold averageDegree⊢ (∑ v, ↑(K4.degree v)) / ↑(Fintype.card (Fin 4)) = 3; simp [Fintype.card_fin]All goals completed! 🐙



@[category test, AMS 5]
theorem K4_matching : matchingNumber K4 = 2 := by⊢ K4.matchingNumber = 2
  classical
  have hbdd : BddAbove (Set.image (fun M : Subgraph K4 => (M.edgeSet.toFinset.card : ℝ)) {M | M.IsMatching}) := by
    refine ⟨(Fintype.card (Fin 4) : ℝ), ?_⟩⊢ ↑(Fintype.card (Fin 4)) ∈ upperBounds ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})hbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ K4.matchingNumber = 2
    rintro x ⟨M, hM, rfl⟩M:K4.SubgraphhM:M ∈ {M | M.IsMatching}⊢ (fun M ↦ ↑M.edgeSet.toFinset.card) M ≤ ↑(Fintype.card (Fin 4))hbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ K4.matchingNumber = 2
    show (M.edgeSet.toFinset.card : ℝ) ≤ Fintype.card (Fin 4)M:K4.SubgraphhM:M ∈ {M | M.IsMatching}⊢ ↑M.edgeSet.toFinset.card ≤ ↑(Fintype.card (Fin 4))hbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ K4.matchingNumber = 2
    have hb := matching_card_bound K4 M hMM:K4.SubgraphhM:M ∈ {M | M.IsMatching}hb:2 * M.edgeSet.toFinset.card ≤ Fintype.card (Fin 4)⊢ ↑M.edgeSet.toFinset.card ≤ ↑(Fintype.card (Fin 4))hbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ K4.matchingNumber = 2
    exact_mod_cast (byM:K4.SubgraphhM:M ∈ {M | M.IsMatching}hb:2 * M.edgeSet.toFinset.card ≤ Fintype.card (Fin 4)⊢ M.edgeSet.toFinset.card ≤ Fintype.card (Fin 4)hbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ K4.matchingNumber = 2 omegaAll goals completed! 🐙hbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ K4.matchingNumber = 2 : M.edgeSet.toFinset.card ≤ Fintype.card (Fin 4))hbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ K4.matchingNumber = 2
  unfold matchingNumberhbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ (have matchings := {M | M.IsMatching};
  sSup ((fun M ↦ ↑M.edgeSet.toFinset.card) '' matchings)) =
  2
  apply le_antisymmahbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ (have matchings := {M | M.IsMatching};
  sSup ((fun M ↦ ↑M.edgeSet.toFinset.card) '' matchings)) ≤
  2ahbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ 2 ≤
  have matchings := {M | M.IsMatching};
  sSup ((fun M ↦ ↑M.edgeSet.toFinset.card) '' matchings)
  ·ahbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ (have matchings := {M | M.IsMatching};
  sSup ((fun M ↦ ↑M.edgeSet.toFinset.card) '' matchings)) ≤
  2 apply csSup_le (Set.Nonempty.image _ ⟨⊥, byhbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ ⊥ ∈ {M | M.IsMatching} simp [Subgraph.IsMatching]All goals completed! 🐙⟩)
    rintro x ⟨M, hM, rfl⟩ahbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})M:K4.SubgraphhM:M ∈ {M | M.IsMatching}⊢ (fun M ↦ ↑M.edgeSet.toFinset.card) M ≤ 2
    show (M.edgeSet.toFinset.card : ℝ) ≤ 2ahbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})M:K4.SubgraphhM:M ∈ {M | M.IsMatching}⊢ ↑M.edgeSet.toFinset.card ≤ 2
    have hb := matching_card_bound K4 M hMahbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})M:K4.SubgraphhM:M ∈ {M | M.IsMatching}hb:2 * M.edgeSet.toFinset.card ≤ Fintype.card (Fin 4)⊢ ↑M.edgeSet.toFinset.card ≤ 2
    simp only [Fintype.card_fin] at hbahbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})M:K4.SubgraphhM:M ∈ {M | M.IsMatching}hb:2 * M.edgeSet.toFinset.card ≤ 4⊢ ↑M.edgeSet.toFinset.card ≤ 2
    exact_mod_cast (byhbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})M:K4.SubgraphhM:M ∈ {M | M.IsMatching}hb:2 * M.edgeSet.toFinset.card ≤ 4⊢ M.edgeSet.toFinset.card ≤ 2 omegaAll goals completed! 🐙 : M.edgeSet.toFinset.card ≤ 2)
  ·ahbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ 2 ≤
  have matchings := {M | M.IsMatching};
  sSup ((fun M ↦ ↑M.edgeSet.toFinset.card) '' matchings) apply le_csSup hbddahbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ 2 ∈ (fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching}
    refine ⟨K4.subgraphOfAdj (show K4.Adj 0 1 by⊢ K4.matchingNumber = 2 decideAll goals completed! 🐙) ⊔ K4.subgraphOfAdj (show K4.Adj 2 3 by⊢ K4.matchingNumber = 2 decideAll goals completed! 🐙), ?_, ?_⟩
    ·a.refine_1hbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ K4.subgraphOfAdj ⋯ ⊔ K4.subgraphOfAdj ⋯ ∈ {M | M.IsMatching} exact (Subgraph.IsMatching.subgraphOfAdj _).sup (Subgraph.IsMatching.subgraphOfAdj _)
        (byhbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ Disjoint (K4.subgraphOfAdj ⋯).support (K4.subgraphOfAdj ⋯).support rw [support_subgraphOfAdj,hbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ Disjoint {0, 1} (K4.subgraphOfAdj ⋯).supporthbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ Disjoint {0, 1} {2, 3} support_subgraphOfAdjhbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ Disjoint {0, 1} {2, 3}hbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ Disjoint {0, 1} {2, 3}]hbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ Disjoint {0, 1} {2, 3}; simp [Set.disjoint_left]All goals completed! 🐙)
    ·a.refine_2hbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ (fun M ↦ ↑M.edgeSet.toFinset.card) (K4.subgraphOfAdj ⋯ ⊔ K4.subgraphOfAdj ⋯) = 2 simpAll goals completed! 🐙

@[category test, AMS 5]
theorem K4_residue : residue K4 = 1 := by⊢ K4.residue = 1
  unfold residue⊢ residueAux ((Multiset.map (fun v ↦ K4.degree v) Finset.univ.val).sort fun x1 x2 ↦ x1 ≥ x2) = 1; decide +nativeAll goals completed! 🐙

@[category test, AMS 5]
theorem K4_annihilation : annihilationNumber K4 = 2 := by⊢ K4.annihilationNumber = 2
  decide +nativeAll goals completed! 🐙

@[category test, AMS 5]
theorem K4_cvetkovic : cvetkovic K4 = 1 := by⊢ K4.cvetkovic = 1
  sorryAll goals completed! 🐙




/-  ### Petersen Graph Tests -/

@[category test, AMS 5]
theorem petersen_indep : α(PetersenGraph) = 4 := by⊢ α(PetersenGraph) = 4
  rw [indep_num_eq_computable⊢ PetersenGraph.computable_indep_num = 4⊢ PetersenGraph.computable_indep_num = 4]⊢ PetersenGraph.computable_indep_num = 4; decide +nativeAll goals completed! 🐙



@[category test, AMS 5]
theorem petersen_dom : dominationNumber PetersenGraph = 3 := by⊢ PetersenGraph.dominationNumber = 3
  rw [dom_num_eq_computable⊢ PetersenGraph.computable_dom_num = 3⊢ PetersenGraph.computable_dom_num = 3]⊢ PetersenGraph.computable_dom_num = 3; decide +nativeAll goals completed! 🐙



@[category test, AMS 5]
theorem petersen_avg_dist : averageDistance PetersenGraph = 5/3 := by⊢ PetersenGraph.averageDistance = 5 / 3
  rw [avg_dist_eq_computable,⊢ ↑PetersenGraph.computable_avg_dist = 5 / 3⊢ ↑(5 / 3) = 5 / 3 show computable_avg_dist PetersenGraph = (5 / 3 : ℚ) from by⊢ PetersenGraph.computable_avg_dist = 5 / 3⊢ ↑(5 / 3) = 5 / 3 decide +nativeAll goals completed! 🐙⊢ ↑(5 / 3) = 5 / 3]⊢ ↑(5 / 3) = 5 / 3
  norm_numAll goals completed! 🐙



@[category test, AMS 5]
theorem petersen_diameter : ediam PetersenGraph = 2 := by⊢ PetersenGraph.ediam = 2
  rw [ediam_eq_computable PetersenGraph (by⊢ PetersenGraph.Connected⊢ ↑PetersenGraph.computable_ediam = 2 decideAll goals completed! 🐙⊢ ↑PetersenGraph.computable_ediam = 2)]⊢ ↑PetersenGraph.computable_ediam = 2
  exact_mod_cast (by⊢ PetersenGraph.computable_ediam = 2 decide +nativeAll goals completed! 🐙 : computable_ediam PetersenGraph = 2)



@[category test, AMS 5]
theorem petersen_radius : radius PetersenGraph = 2 := by⊢ PetersenGraph.radius = 2
  rw [radius_eq_computable PetersenGraph (by⊢ PetersenGraph.Connected⊢ ↑PetersenGraph.computable_radius = 2 decideAll goals completed! 🐙⊢ ↑PetersenGraph.computable_radius = 2)]⊢ ↑PetersenGraph.computable_radius = 2
  exact_mod_cast (by⊢ PetersenGraph.computable_radius = 2 decide +nativeAll goals completed! 🐙 : computable_radius PetersenGraph = 2)

@[category test, AMS 5]
theorem petersen_girth : PetersenGraph.girth = 5 := by⊢ PetersenGraph.girth = 5
  sorryAll goals completed! 🐙



open scoped Classical in
@[category test, AMS 5]
theorem petersen_order : Fintype.card ↥(⊤ : Subgraph PetersenGraph).verts = 10 := by⊢ Fintype.card ↑⊤.verts = 10
  rw [Fintype.card_congr SimpleGraph.Subgraph.topIso.toEquiv⊢ Fintype.card (Fin 10) = 10⊢ Fintype.card (Fin 10) = 10]⊢ Fintype.card (Fin 10) = 10
  rflAll goals completed! 🐙

@[category test, AMS 5]
theorem petersen_size : PetersenGraph.edgeFinset.card = 15 := by⊢ PetersenGraph.edgeFinset.card = 15
  decide +nativeAll goals completed! 🐙



@[category test, AMS 5]
theorem petersen_szeged : szegedIndex PetersenGraph = 135 := by⊢ PetersenGraph.szegedIndex = 135
  rw [szeged_eq_computable⊢ PetersenGraph.computable_szeged_index = 135⊢ PetersenGraph.computable_szeged_index = 135]⊢ PetersenGraph.computable_szeged_index = 135; decide +nativeAll goals completed! 🐙



@[category test, AMS 5]
theorem petersen_wiener : wienerIndex PetersenGraph = 75 := by⊢ PetersenGraph.wienerIndex = 75
  rw [wiener_eq_computable⊢ PetersenGraph.computable_wiener = 75⊢ PetersenGraph.computable_wiener = 75]⊢ PetersenGraph.computable_wiener = 75; decide +nativeAll goals completed! 🐙

@[category test, AMS 5]
theorem petersen_min_deg : PetersenGraph.minDegree = 3 := by⊢ PetersenGraph.minDegree = 3
  decide +nativeAll goals completed! 🐙

@[category test, AMS 5]
theorem petersen_max_deg : PetersenGraph.maxDegree = 3 := by⊢ PetersenGraph.maxDegree = 3
  decide +nativeAll goals completed! 🐙

@[category test, AMS 5]
theorem petersen_avg_deg : averageDegree PetersenGraph = 3 := by⊢ PetersenGraph.averageDegree = 3
  unfold averageDegree⊢ (∑ v, ↑(PetersenGraph.degree v)) / ↑(Fintype.card (Fin 10)) = 3; simp [Fintype.card_fin]⊢ (∑ v, ↑(PetersenGraph.degree v)) / 10 = 3; decide +nativeAll goals completed! 🐙



@[category test, AMS 5]
theorem petersen_matching : matchingNumber PetersenGraph = 5 := by⊢ PetersenGraph.matchingNumber = 5
  classical
  have hbdd : BddAbove (Set.image (fun M : Subgraph PetersenGraph => (M.edgeSet.toFinset.card : ℝ)) {M | M.IsMatching}) := by
    refine ⟨(Fintype.card (Fin 10) : ℝ), ?_⟩⊢ ↑(Fintype.card (Fin 10)) ∈ upperBounds ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})hbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ PetersenGraph.matchingNumber = 5
    rintro x ⟨M, hM, rfl⟩M:PetersenGraph.SubgraphhM:M ∈ {M | M.IsMatching}⊢ (fun M ↦ ↑M.edgeSet.toFinset.card) M ≤ ↑(Fintype.card (Fin 10))hbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ PetersenGraph.matchingNumber = 5
    show (M.edgeSet.toFinset.card : ℝ) ≤ Fintype.card (Fin 10)M:PetersenGraph.SubgraphhM:M ∈ {M | M.IsMatching}⊢ ↑M.edgeSet.toFinset.card ≤ ↑(Fintype.card (Fin 10))hbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ PetersenGraph.matchingNumber = 5
    have hb := matching_card_bound PetersenGraph M hMM:PetersenGraph.SubgraphhM:M ∈ {M | M.IsMatching}hb:2 * M.edgeSet.toFinset.card ≤ Fintype.card (Fin 10)⊢ ↑M.edgeSet.toFinset.card ≤ ↑(Fintype.card (Fin 10))hbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ PetersenGraph.matchingNumber = 5
    exact_mod_cast (byM:PetersenGraph.SubgraphhM:M ∈ {M | M.IsMatching}hb:2 * M.edgeSet.toFinset.card ≤ Fintype.card (Fin 10)⊢ M.edgeSet.toFinset.card ≤ Fintype.card (Fin 10)hbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ PetersenGraph.matchingNumber = 5 omegaAll goals completed! 🐙hbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ PetersenGraph.matchingNumber = 5 : M.edgeSet.toFinset.card ≤ Fintype.card (Fin 10))hbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ PetersenGraph.matchingNumber = 5
  unfold matchingNumberhbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ (have matchings := {M | M.IsMatching};
  sSup ((fun M ↦ ↑M.edgeSet.toFinset.card) '' matchings)) =
  5
  apply le_antisymmahbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ (have matchings := {M | M.IsMatching};
  sSup ((fun M ↦ ↑M.edgeSet.toFinset.card) '' matchings)) ≤
  5ahbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ 5 ≤
  have matchings := {M | M.IsMatching};
  sSup ((fun M ↦ ↑M.edgeSet.toFinset.card) '' matchings)
  ·ahbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ (have matchings := {M | M.IsMatching};
  sSup ((fun M ↦ ↑M.edgeSet.toFinset.card) '' matchings)) ≤
  5 apply csSup_le (Set.Nonempty.image _ ⟨⊥, byhbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ ⊥ ∈ {M | M.IsMatching} simp [Subgraph.IsMatching]All goals completed! 🐙⟩)
    rintro x ⟨M, hM, rfl⟩ahbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})M:PetersenGraph.SubgraphhM:M ∈ {M | M.IsMatching}⊢ (fun M ↦ ↑M.edgeSet.toFinset.card) M ≤ 5
    show (M.edgeSet.toFinset.card : ℝ) ≤ 5ahbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})M:PetersenGraph.SubgraphhM:M ∈ {M | M.IsMatching}⊢ ↑M.edgeSet.toFinset.card ≤ 5
    have hb := matching_card_bound PetersenGraph M hMahbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})M:PetersenGraph.SubgraphhM:M ∈ {M | M.IsMatching}hb:2 * M.edgeSet.toFinset.card ≤ Fintype.card (Fin 10)⊢ ↑M.edgeSet.toFinset.card ≤ 5
    simp only [Fintype.card_fin] at hbahbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})M:PetersenGraph.SubgraphhM:M ∈ {M | M.IsMatching}hb:2 * M.edgeSet.toFinset.card ≤ 10⊢ ↑M.edgeSet.toFinset.card ≤ 5
    exact_mod_cast (byhbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})M:PetersenGraph.SubgraphhM:M ∈ {M | M.IsMatching}hb:2 * M.edgeSet.toFinset.card ≤ 10⊢ M.edgeSet.toFinset.card ≤ 5 omegaAll goals completed! 🐙 : M.edgeSet.toFinset.card ≤ 5)
  ·ahbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ 5 ≤
  have matchings := {M | M.IsMatching};
  sSup ((fun M ↦ ↑M.edgeSet.toFinset.card) '' matchings) apply le_csSup hbddahbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ 5 ∈ (fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching}
    refine ⟨PetersenGraph.subgraphOfAdj (show PetersenGraph.Adj 0 5 by⊢ PetersenGraph.matchingNumber = 5 decideAll goals completed! 🐙) ⊔ PetersenGraph.subgraphOfAdj (show PetersenGraph.Adj 1 6 by⊢ PetersenGraph.matchingNumber = 5 decideAll goals completed! 🐙) ⊔ PetersenGraph.subgraphOfAdj (show PetersenGraph.Adj 2 7 by⊢ PetersenGraph.matchingNumber = 5 decideAll goals completed! 🐙) ⊔ PetersenGraph.subgraphOfAdj (show PetersenGraph.Adj 3 8 by⊢ PetersenGraph.matchingNumber = 5 decideAll goals completed! 🐙) ⊔ PetersenGraph.subgraphOfAdj (show PetersenGraph.Adj 4 9 by⊢ PetersenGraph.matchingNumber = 5 decideAll goals completed! 🐙), ?_, ?_⟩
    ·a.refine_1hbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ PetersenGraph.subgraphOfAdj ⋯ ⊔ PetersenGraph.subgraphOfAdj ⋯ ⊔ PetersenGraph.subgraphOfAdj ⋯ ⊔
      PetersenGraph.subgraphOfAdj ⋯ ⊔
    PetersenGraph.subgraphOfAdj ⋯ ∈
  {M | M.IsMatching} apply Subgraph.IsMatching.supa.refine_1.hMhbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ (PetersenGraph.subgraphOfAdj ⋯ ⊔ PetersenGraph.subgraphOfAdj ⋯ ⊔ PetersenGraph.subgraphOfAdj ⋯ ⊔
    PetersenGraph.subgraphOfAdj ⋯).IsMatchinga.refine_1.hM'hbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ (PetersenGraph.subgraphOfAdj ⋯).IsMatchinga.refine_1.hdhbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ Disjoint
  (PetersenGraph.subgraphOfAdj ⋯ ⊔ PetersenGraph.subgraphOfAdj ⋯ ⊔ PetersenGraph.subgraphOfAdj ⋯ ⊔
      PetersenGraph.subgraphOfAdj ⋯).support
  (PetersenGraph.subgraphOfAdj ⋯).support
      ·a.refine_1.hMhbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ (PetersenGraph.subgraphOfAdj ⋯ ⊔ PetersenGraph.subgraphOfAdj ⋯ ⊔ PetersenGraph.subgraphOfAdj ⋯ ⊔
    PetersenGraph.subgraphOfAdj ⋯).IsMatching apply Subgraph.IsMatching.supa.refine_1.hM.hMhbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ (PetersenGraph.subgraphOfAdj ⋯ ⊔ PetersenGraph.subgraphOfAdj ⋯ ⊔ PetersenGraph.subgraphOfAdj ⋯).IsMatchinga.refine_1.hM.hM'hbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ (PetersenGraph.subgraphOfAdj ⋯).IsMatchinga.refine_1.hM.hdhbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ Disjoint (PetersenGraph.subgraphOfAdj ⋯ ⊔ PetersenGraph.subgraphOfAdj ⋯ ⊔ PetersenGraph.subgraphOfAdj ⋯).support
  (PetersenGraph.subgraphOfAdj ⋯).support
        ·a.refine_1.hM.hMhbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ (PetersenGraph.subgraphOfAdj ⋯ ⊔ PetersenGraph.subgraphOfAdj ⋯ ⊔ PetersenGraph.subgraphOfAdj ⋯).IsMatching apply Subgraph.IsMatching.supa.refine_1.hM.hM.hMhbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ (PetersenGraph.subgraphOfAdj ⋯ ⊔ PetersenGraph.subgraphOfAdj ⋯).IsMatchinga.refine_1.hM.hM.hM'hbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ (PetersenGraph.subgraphOfAdj ⋯).IsMatchinga.refine_1.hM.hM.hdhbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ Disjoint (PetersenGraph.subgraphOfAdj ⋯ ⊔ PetersenGraph.subgraphOfAdj ⋯).support (PetersenGraph.subgraphOfAdj ⋯).support
          ·a.refine_1.hM.hM.hMhbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ (PetersenGraph.subgraphOfAdj ⋯ ⊔ PetersenGraph.subgraphOfAdj ⋯).IsMatching exact (Subgraph.IsMatching.subgraphOfAdj _).sup (Subgraph.IsMatching.subgraphOfAdj _)
              (byhbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ Disjoint (PetersenGraph.subgraphOfAdj ⋯).support (PetersenGraph.subgraphOfAdj ⋯).support rw [support_subgraphOfAdj,hbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ Disjoint {0, 5} (PetersenGraph.subgraphOfAdj ⋯).supporthbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ Disjoint {0, 5} {1, 6} support_subgraphOfAdjhbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ Disjoint {0, 5} {1, 6}hbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ Disjoint {0, 5} {1, 6}]hbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ Disjoint {0, 5} {1, 6}; simp [Set.disjoint_left]All goals completed! 🐙)
          ·a.refine_1.hM.hM.hM'hbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ (PetersenGraph.subgraphOfAdj ⋯).IsMatching exact Subgraph.IsMatching.subgraphOfAdj _All goals completed! 🐙
          ·a.refine_1.hM.hM.hdhbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ Disjoint (PetersenGraph.subgraphOfAdj ⋯ ⊔ PetersenGraph.subgraphOfAdj ⋯).support (PetersenGraph.subgraphOfAdj ⋯).support apply Set.disjoint_of_subset (Subgraph.support_subset_verts _) (Subgraph.support_subset_verts _)a.refine_1.hM.hM.hdhbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ Disjoint (PetersenGraph.subgraphOfAdj ⋯ ⊔ PetersenGraph.subgraphOfAdj ⋯).verts (PetersenGraph.subgraphOfAdj ⋯).verts
            simp [Subgraph.verts_sup, subgraphOfAdj_verts, Set.disjoint_left]All goals completed! 🐙
        ·a.refine_1.hM.hM'hbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ (PetersenGraph.subgraphOfAdj ⋯).IsMatching exact Subgraph.IsMatching.subgraphOfAdj _All goals completed! 🐙
        ·a.refine_1.hM.hdhbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ Disjoint (PetersenGraph.subgraphOfAdj ⋯ ⊔ PetersenGraph.subgraphOfAdj ⋯ ⊔ PetersenGraph.subgraphOfAdj ⋯).support
  (PetersenGraph.subgraphOfAdj ⋯).support apply Set.disjoint_of_subset (Subgraph.support_subset_verts _) (Subgraph.support_subset_verts _)a.refine_1.hM.hdhbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ Disjoint (PetersenGraph.subgraphOfAdj ⋯ ⊔ PetersenGraph.subgraphOfAdj ⋯ ⊔ PetersenGraph.subgraphOfAdj ⋯).verts
  (PetersenGraph.subgraphOfAdj ⋯).verts
          simp [Subgraph.verts_sup, subgraphOfAdj_verts, Set.disjoint_left]All goals completed! 🐙
      ·a.refine_1.hM'hbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ (PetersenGraph.subgraphOfAdj ⋯).IsMatching exact Subgraph.IsMatching.subgraphOfAdj _All goals completed! 🐙
      ·a.refine_1.hdhbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ Disjoint
  (PetersenGraph.subgraphOfAdj ⋯ ⊔ PetersenGraph.subgraphOfAdj ⋯ ⊔ PetersenGraph.subgraphOfAdj ⋯ ⊔
      PetersenGraph.subgraphOfAdj ⋯).support
  (PetersenGraph.subgraphOfAdj ⋯).support apply Set.disjoint_of_subset (Subgraph.support_subset_verts _) (Subgraph.support_subset_verts _)a.refine_1.hdhbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ Disjoint
  (PetersenGraph.subgraphOfAdj ⋯ ⊔ PetersenGraph.subgraphOfAdj ⋯ ⊔ PetersenGraph.subgraphOfAdj ⋯ ⊔
      PetersenGraph.subgraphOfAdj ⋯).verts
  (PetersenGraph.subgraphOfAdj ⋯).verts
        simp [Subgraph.verts_sup, subgraphOfAdj_verts, Set.disjoint_left]All goals completed! 🐙
    ·a.refine_2hbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ (fun M ↦ ↑M.edgeSet.toFinset.card)
    (PetersenGraph.subgraphOfAdj ⋯ ⊔ PetersenGraph.subgraphOfAdj ⋯ ⊔ PetersenGraph.subgraphOfAdj ⋯ ⊔
        PetersenGraph.subgraphOfAdj ⋯ ⊔
      PetersenGraph.subgraphOfAdj ⋯) =
  5 simpAll goals completed! 🐙

@[category test, AMS 5]
theorem petersen_residue : residue PetersenGraph = 3 := by⊢ PetersenGraph.residue = 3
  unfold residue⊢ residueAux ((Multiset.map (fun v ↦ PetersenGraph.degree v) Finset.univ.val).sort fun x1 x2 ↦ x1 ≥ x2) = 3; decide +nativeAll goals completed! 🐙

@[category test, AMS 5]
theorem petersen_annihilation : annihilationNumber PetersenGraph = 5 := by⊢ PetersenGraph.annihilationNumber = 5
  decide +nativeAll goals completed! 🐙

@[category test, AMS 5]
theorem petersen_cvetkovic : cvetkovic PetersenGraph = 4 := by⊢ PetersenGraph.cvetkovic = 4
  sorryAll goals completed! 🐙




/-  ### C6 Tests -/

@[category test, AMS 5]
theorem C6_indep : α(C6) = 3 := by⊢ α(C6) = 3
  rw [indep_num_eq_computable⊢ C6.computable_indep_num = 3⊢ C6.computable_indep_num = 3]⊢ C6.computable_indep_num = 3; decide +nativeAll goals completed! 🐙



@[category test, AMS 5]
theorem C6_dom : dominationNumber C6 = 2 := by⊢ C6.dominationNumber = 2
  rw [dom_num_eq_computable⊢ C6.computable_dom_num = 2⊢ C6.computable_dom_num = 2]⊢ C6.computable_dom_num = 2; decide +nativeAll goals completed! 🐙



@[category test, AMS 5]
theorem C6_avg_dist : averageDistance C6 = 9/5 := by⊢ C6.averageDistance = 9 / 5
  rw [avg_dist_eq_computable,⊢ ↑C6.computable_avg_dist = 9 / 5⊢ ↑(9 / 5) = 9 / 5 show computable_avg_dist C6 = (9 / 5 : ℚ) from by⊢ C6.computable_avg_dist = 9 / 5⊢ ↑(9 / 5) = 9 / 5 decide +nativeAll goals completed! 🐙⊢ ↑(9 / 5) = 9 / 5]⊢ ↑(9 / 5) = 9 / 5
  norm_numAll goals completed! 🐙



@[category test, AMS 5]
theorem C6_diameter : ediam C6 = 3 := by⊢ C6.ediam = 3
  rw [ediam_eq_computable C6 (by⊢ C6.Connected⊢ ↑C6.computable_ediam = 3 decideAll goals completed! 🐙⊢ ↑C6.computable_ediam = 3)]⊢ ↑C6.computable_ediam = 3
  exact_mod_cast (by⊢ C6.computable_ediam = 3 decide +nativeAll goals completed! 🐙 : computable_ediam C6 = 3)



@[category test, AMS 5]
theorem C6_radius : radius C6 = 3 := by⊢ C6.radius = 3
  rw [radius_eq_computable C6 (by⊢ C6.Connected⊢ ↑C6.computable_radius = 3 decideAll goals completed! 🐙⊢ ↑C6.computable_radius = 3)]⊢ ↑C6.computable_radius = 3
  exact_mod_cast (by⊢ C6.computable_radius = 3 decide +nativeAll goals completed! 🐙 : computable_radius C6 = 3)

@[category test, AMS 5]
theorem C6_girth : C6.girth = 6 := by⊢ C6.girth = 6
  sorryAll goals completed! 🐙



open scoped Classical in
@[category test, AMS 5]
theorem C6_order : Fintype.card ↥(⊤ : Subgraph C6).verts = 6 := by⊢ Fintype.card ↑⊤.verts = 6
  rw [Fintype.card_congr SimpleGraph.Subgraph.topIso.toEquiv⊢ Fintype.card (Fin 6) = 6⊢ Fintype.card (Fin 6) = 6]⊢ Fintype.card (Fin 6) = 6
  rflAll goals completed! 🐙

@[category test, AMS 5]
theorem C6_size : C6.edgeFinset.card = 6 := by⊢ C6.edgeFinset.card = 6
  decide +nativeAll goals completed! 🐙



@[category test, AMS 5]
theorem C6_szeged : szegedIndex C6 = 54 := by⊢ C6.szegedIndex = 54
  rw [szeged_eq_computable⊢ C6.computable_szeged_index = 54⊢ C6.computable_szeged_index = 54]⊢ C6.computable_szeged_index = 54; decide +nativeAll goals completed! 🐙



@[category test, AMS 5]
theorem C6_wiener : wienerIndex C6 = 27 := by⊢ C6.wienerIndex = 27
  rw [wiener_eq_computable⊢ C6.computable_wiener = 27⊢ C6.computable_wiener = 27]⊢ C6.computable_wiener = 27; decide +nativeAll goals completed! 🐙

@[category test, AMS 5]
theorem C6_min_deg : C6.minDegree = 2 := by⊢ C6.minDegree = 2
  decide +nativeAll goals completed! 🐙

@[category test, AMS 5]
theorem C6_max_deg : C6.maxDegree = 2 := by⊢ C6.maxDegree = 2
  decide +nativeAll goals completed! 🐙

@[category test, AMS 5]
theorem C6_avg_deg : averageDegree C6 = 2 := by⊢ C6.averageDegree = 2
  unfold averageDegree⊢ (∑ v, ↑(C6.degree v)) / ↑(Fintype.card (Fin 6)) = 2; simp [Fintype.card_fin]⊢ (∑ v, ↑(C6.degree v)) / 6 = 2; decide +nativeAll goals completed! 🐙



@[category test, AMS 5]
theorem C6_matching : matchingNumber C6 = 3 := by⊢ C6.matchingNumber = 3
  classical
  have hbdd : BddAbove (Set.image (fun M : Subgraph C6 => (M.edgeSet.toFinset.card : ℝ)) {M | M.IsMatching}) := by
    refine ⟨(Fintype.card (Fin 6) : ℝ), ?_⟩⊢ ↑(Fintype.card (Fin 6)) ∈ upperBounds ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})hbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ C6.matchingNumber = 3
    rintro x ⟨M, hM, rfl⟩M:C6.SubgraphhM:M ∈ {M | M.IsMatching}⊢ (fun M ↦ ↑M.edgeSet.toFinset.card) M ≤ ↑(Fintype.card (Fin 6))hbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ C6.matchingNumber = 3
    show (M.edgeSet.toFinset.card : ℝ) ≤ Fintype.card (Fin 6)M:C6.SubgraphhM:M ∈ {M | M.IsMatching}⊢ ↑M.edgeSet.toFinset.card ≤ ↑(Fintype.card (Fin 6))hbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ C6.matchingNumber = 3
    have hb := matching_card_bound C6 M hMM:C6.SubgraphhM:M ∈ {M | M.IsMatching}hb:2 * M.edgeSet.toFinset.card ≤ Fintype.card (Fin 6)⊢ ↑M.edgeSet.toFinset.card ≤ ↑(Fintype.card (Fin 6))hbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ C6.matchingNumber = 3
    exact_mod_cast (byM:C6.SubgraphhM:M ∈ {M | M.IsMatching}hb:2 * M.edgeSet.toFinset.card ≤ Fintype.card (Fin 6)⊢ M.edgeSet.toFinset.card ≤ Fintype.card (Fin 6)hbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ C6.matchingNumber = 3 omegaAll goals completed! 🐙hbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ C6.matchingNumber = 3 : M.edgeSet.toFinset.card ≤ Fintype.card (Fin 6))hbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ C6.matchingNumber = 3
  unfold matchingNumberhbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ (have matchings := {M | M.IsMatching};
  sSup ((fun M ↦ ↑M.edgeSet.toFinset.card) '' matchings)) =
  3
  apply le_antisymmahbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ (have matchings := {M | M.IsMatching};
  sSup ((fun M ↦ ↑M.edgeSet.toFinset.card) '' matchings)) ≤
  3ahbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ 3 ≤
  have matchings := {M | M.IsMatching};
  sSup ((fun M ↦ ↑M.edgeSet.toFinset.card) '' matchings)
  ·ahbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ (have matchings := {M | M.IsMatching};
  sSup ((fun M ↦ ↑M.edgeSet.toFinset.card) '' matchings)) ≤
  3 apply csSup_le (Set.Nonempty.image _ ⟨⊥, byhbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ ⊥ ∈ {M | M.IsMatching} simp [Subgraph.IsMatching]All goals completed! 🐙⟩)
    rintro x ⟨M, hM, rfl⟩ahbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})M:C6.SubgraphhM:M ∈ {M | M.IsMatching}⊢ (fun M ↦ ↑M.edgeSet.toFinset.card) M ≤ 3
    show (M.edgeSet.toFinset.card : ℝ) ≤ 3ahbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})M:C6.SubgraphhM:M ∈ {M | M.IsMatching}⊢ ↑M.edgeSet.toFinset.card ≤ 3
    have hb := matching_card_bound C6 M hMahbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})M:C6.SubgraphhM:M ∈ {M | M.IsMatching}hb:2 * M.edgeSet.toFinset.card ≤ Fintype.card (Fin 6)⊢ ↑M.edgeSet.toFinset.card ≤ 3
    simp only [Fintype.card_fin] at hbahbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})M:C6.SubgraphhM:M ∈ {M | M.IsMatching}hb:2 * M.edgeSet.toFinset.card ≤ 6⊢ ↑M.edgeSet.toFinset.card ≤ 3
    exact_mod_cast (byhbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})M:C6.SubgraphhM:M ∈ {M | M.IsMatching}hb:2 * M.edgeSet.toFinset.card ≤ 6⊢ M.edgeSet.toFinset.card ≤ 3 omegaAll goals completed! 🐙 : M.edgeSet.toFinset.card ≤ 3)
  ·ahbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ 3 ≤
  have matchings := {M | M.IsMatching};
  sSup ((fun M ↦ ↑M.edgeSet.toFinset.card) '' matchings) apply le_csSup hbddahbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ 3 ∈ (fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching}
    refine ⟨C6.subgraphOfAdj (show C6.Adj 0 1 by⊢ C6.matchingNumber = 3 decideAll goals completed! 🐙) ⊔ C6.subgraphOfAdj (show C6.Adj 2 3 by⊢ C6.matchingNumber = 3 decideAll goals completed! 🐙) ⊔ C6.subgraphOfAdj (show C6.Adj 4 5 by⊢ C6.matchingNumber = 3 decideAll goals completed! 🐙), ?_, ?_⟩
    ·a.refine_1hbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ C6.subgraphOfAdj ⋯ ⊔ C6.subgraphOfAdj ⋯ ⊔ C6.subgraphOfAdj ⋯ ∈ {M | M.IsMatching} apply Subgraph.IsMatching.supa.refine_1.hMhbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ (C6.subgraphOfAdj ⋯ ⊔ C6.subgraphOfAdj ⋯).IsMatchinga.refine_1.hM'hbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ (C6.subgraphOfAdj ⋯).IsMatchinga.refine_1.hdhbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ Disjoint (C6.subgraphOfAdj ⋯ ⊔ C6.subgraphOfAdj ⋯).support (C6.subgraphOfAdj ⋯).support
      ·a.refine_1.hMhbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ (C6.subgraphOfAdj ⋯ ⊔ C6.subgraphOfAdj ⋯).IsMatching exact (Subgraph.IsMatching.subgraphOfAdj _).sup (Subgraph.IsMatching.subgraphOfAdj _)
          (byhbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ Disjoint (C6.subgraphOfAdj ⋯).support (C6.subgraphOfAdj ⋯).support rw [support_subgraphOfAdj,hbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ Disjoint {0, 1} (C6.subgraphOfAdj ⋯).supporthbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ Disjoint {0, 1} {2, 3} support_subgraphOfAdjhbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ Disjoint {0, 1} {2, 3}hbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ Disjoint {0, 1} {2, 3}]hbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ Disjoint {0, 1} {2, 3}; simp [Set.disjoint_left]All goals completed! 🐙)
      ·a.refine_1.hM'hbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ (C6.subgraphOfAdj ⋯).IsMatching exact Subgraph.IsMatching.subgraphOfAdj _All goals completed! 🐙
      ·a.refine_1.hdhbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ Disjoint (C6.subgraphOfAdj ⋯ ⊔ C6.subgraphOfAdj ⋯).support (C6.subgraphOfAdj ⋯).support apply Set.disjoint_of_subset (Subgraph.support_subset_verts _) (Subgraph.support_subset_verts _)a.refine_1.hdhbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ Disjoint (C6.subgraphOfAdj ⋯ ⊔ C6.subgraphOfAdj ⋯).verts (C6.subgraphOfAdj ⋯).verts
        simp [Subgraph.verts_sup, subgraphOfAdj_verts, Set.disjoint_left]All goals completed! 🐙
    ·a.refine_2hbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ (fun M ↦ ↑M.edgeSet.toFinset.card) (C6.subgraphOfAdj ⋯ ⊔ C6.subgraphOfAdj ⋯ ⊔ C6.subgraphOfAdj ⋯) = 3 simpAll goals completed! 🐙

@[category test, AMS 5]
theorem C6_residue : residue C6 = 2 := by⊢ C6.residue = 2
  unfold residue⊢ residueAux ((Multiset.map (fun v ↦ C6.degree v) Finset.univ.val).sort fun x1 x2 ↦ x1 ≥ x2) = 2; decide +nativeAll goals completed! 🐙

@[category test, AMS 5]
theorem C6_annihilation : annihilationNumber C6 = 3 := by⊢ C6.annihilationNumber = 3
  decide +nativeAll goals completed! 🐙

@[category test, AMS 5]
theorem C6_cvetkovic : cvetkovic C6 = 3 := by⊢ C6.cvetkovic = 3
  sorryAll goals completed! 🐙



/-  ### Star5 Tests -/

@[category test, AMS 5]
theorem Star5_indep : α(Star5) = 5 := by⊢ α(Star5) = 5
  rw [indep_num_eq_computable⊢ Star5.computable_indep_num = 5⊢ Star5.computable_indep_num = 5]⊢ Star5.computable_indep_num = 5; decide +nativeAll goals completed! 🐙



@[category test, AMS 5]
theorem Star5_dom : dominationNumber Star5 = 1 := by⊢ Star5.dominationNumber = 1
  rw [dom_num_eq_computable⊢ Star5.computable_dom_num = 1⊢ Star5.computable_dom_num = 1]⊢ Star5.computable_dom_num = 1; decide +nativeAll goals completed! 🐙



@[category test, AMS 5]
theorem Star5_avg_dist : averageDistance Star5 = 5/3 := by⊢ Star5.averageDistance = 5 / 3
  rw [avg_dist_eq_computable,⊢ ↑Star5.computable_avg_dist = 5 / 3⊢ ↑(5 / 3) = 5 / 3 show computable_avg_dist Star5 = (5 / 3 : ℚ) from by⊢ Star5.computable_avg_dist = 5 / 3⊢ ↑(5 / 3) = 5 / 3 decide +nativeAll goals completed! 🐙⊢ ↑(5 / 3) = 5 / 3]⊢ ↑(5 / 3) = 5 / 3
  norm_numAll goals completed! 🐙



@[category test, AMS 5]
theorem Star5_diameter : ediam Star5 = 2 := by⊢ Star5.ediam = 2
  rw [ediam_eq_computable Star5 (by⊢ Star5.Connected⊢ ↑Star5.computable_ediam = 2 decideAll goals completed! 🐙⊢ ↑Star5.computable_ediam = 2)]⊢ ↑Star5.computable_ediam = 2
  exact_mod_cast (by⊢ Star5.computable_ediam = 2 decide +nativeAll goals completed! 🐙 : computable_ediam Star5 = 2)



@[category test, AMS 5]
theorem Star5_radius : radius Star5 = 1 := by⊢ Star5.radius = 1
  rw [radius_eq_computable Star5 (by⊢ Star5.Connected⊢ ↑Star5.computable_radius = 1 decideAll goals completed! 🐙⊢ ↑Star5.computable_radius = 1)]⊢ ↑Star5.computable_radius = 1
  exact_mod_cast (by⊢ Star5.computable_radius = 1 decide +nativeAll goals completed! 🐙 : computable_radius Star5 = 1)



@[category test, AMS 5]
theorem Star5_girth : Star5.egirth = ⊤ := by⊢ Star5.egirth = ⊤
  rw [egirth_eq_top⊢ Star5.IsAcyclic⊢ Star5.IsAcyclic]⊢ Star5.IsAcyclic
  have key : ∀ (b : Fin 5) (c : Star5.Walk (Sum.inr b) (Sum.inr b)), ¬ c.IsCycle := by⊢ Star5.egirth = ⊤key:∀ (b : Fin 5) (c : Star5.Walk (Sum.inr b) (Sum.inr b)), ¬c.IsCycle⊢ Star5.IsAcyclic
    intro b c hcb:Fin 5c:Star5.Walk (Sum.inr b) (Sum.inr b)hc:c.IsCycle⊢ Falsekey:∀ (b : Fin 5) (c : Star5.Walk (Sum.inr b) (Sum.inr b)), ¬c.IsCycle⊢ Star5.IsAcyclic
    have h1 := c.adj_snd hc.not_nilb:Fin 5c:Star5.Walk (Sum.inr b) (Sum.inr b)hc:c.IsCycleh1:Star5.Adj (Sum.inr b) c.snd⊢ Falsekey:∀ (b : Fin 5) (c : Star5.Walk (Sum.inr b) (Sum.inr b)), ¬c.IsCycle⊢ Star5.IsAcyclic
    have h2 := c.adj_penultimate hc.not_nilb:Fin 5c:Star5.Walk (Sum.inr b) (Sum.inr b)hc:c.IsCycleh1:Star5.Adj (Sum.inr b) c.sndh2:Star5.Adj c.penultimate (Sum.inr b)⊢ Falsekey:∀ (b : Fin 5) (c : Star5.Walk (Sum.inr b) (Sum.inr b)), ¬c.IsCycle⊢ Star5.IsAcyclic
    have hs : c.snd.isLeft := by⊢ Star5.egirth = ⊤b:Fin 5c:Star5.Walk (Sum.inr b) (Sum.inr b)hc:c.IsCycleh1:Star5.Adj (Sum.inr b) c.sndh2:Star5.Adj c.penultimate (Sum.inr b)hs:c.snd.isLeft = true⊢ Falsekey:∀ (b : Fin 5) (c : Star5.Walk (Sum.inr b) (Sum.inr b)), ¬c.IsCycle⊢ Star5.IsAcyclic
      simp only [Star5, completeBipartiteGraph, Sum.isRight_inr, Sum.isLeft_inr] at h1b:Fin 5c:Star5.Walk (Sum.inr b) (Sum.inr b)hc:c.IsCycleh2:Star5.Adj c.penultimate (Sum.inr b)h1:false = true ∧ c.snd.isRight = true ∨ True ∧ c.snd.isLeft = true⊢ c.snd.isLeft = trueb:Fin 5c:Star5.Walk (Sum.inr b) (Sum.inr b)hc:c.IsCycleh1:Star5.Adj (Sum.inr b) c.sndh2:Star5.Adj c.penultimate (Sum.inr b)hs:c.snd.isLeft = true⊢ Falsekey:∀ (b : Fin 5) (c : Star5.Walk (Sum.inr b) (Sum.inr b)), ¬c.IsCycle⊢ Star5.IsAcyclic
      tautob:Fin 5c:Star5.Walk (Sum.inr b) (Sum.inr b)hc:c.IsCycleh1:Star5.Adj (Sum.inr b) c.sndh2:Star5.Adj c.penultimate (Sum.inr b)hs:c.snd.isLeft = true⊢ Falsekey:∀ (b : Fin 5) (c : Star5.Walk (Sum.inr b) (Sum.inr b)), ¬c.IsCycle⊢ Star5.IsAcyclicb:Fin 5c:Star5.Walk (Sum.inr b) (Sum.inr b)hc:c.IsCycleh1:Star5.Adj (Sum.inr b) c.sndh2:Star5.Adj c.penultimate (Sum.inr b)hs:c.snd.isLeft = true⊢ Falsekey:∀ (b : Fin 5) (c : Star5.Walk (Sum.inr b) (Sum.inr b)), ¬c.IsCycle⊢ Star5.IsAcyclic
    have hp : c.penultimate.isLeft := by⊢ Star5.egirth = ⊤b:Fin 5c:Star5.Walk (Sum.inr b) (Sum.inr b)hc:c.IsCycleh1:Star5.Adj (Sum.inr b) c.sndh2:Star5.Adj c.penultimate (Sum.inr b)hs:c.snd.isLeft = truehp:c.penultimate.isLeft = true⊢ Falsekey:∀ (b : Fin 5) (c : Star5.Walk (Sum.inr b) (Sum.inr b)), ¬c.IsCycle⊢ Star5.IsAcyclic
      simp only [Star5, completeBipartiteGraph, Sum.isRight_inr, Sum.isLeft_inr] at h2b:Fin 5c:Star5.Walk (Sum.inr b) (Sum.inr b)hc:c.IsCycleh1:Star5.Adj (Sum.inr b) c.sndhs:c.snd.isLeft = trueh2:c.penultimate.isLeft = true ∧ True ∨ c.penultimate.isRight = true ∧ false = true⊢ c.penultimate.isLeft = trueb:Fin 5c:Star5.Walk (Sum.inr b) (Sum.inr b)hc:c.IsCycleh1:Star5.Adj (Sum.inr b) c.sndh2:Star5.Adj c.penultimate (Sum.inr b)hs:c.snd.isLeft = truehp:c.penultimate.isLeft = true⊢ Falsekey:∀ (b : Fin 5) (c : Star5.Walk (Sum.inr b) (Sum.inr b)), ¬c.IsCycle⊢ Star5.IsAcyclic
      tautob:Fin 5c:Star5.Walk (Sum.inr b) (Sum.inr b)hc:c.IsCycleh1:Star5.Adj (Sum.inr b) c.sndh2:Star5.Adj c.penultimate (Sum.inr b)hs:c.snd.isLeft = truehp:c.penultimate.isLeft = true⊢ Falsekey:∀ (b : Fin 5) (c : Star5.Walk (Sum.inr b) (Sum.inr b)), ¬c.IsCycle⊢ Star5.IsAcyclicb:Fin 5c:Star5.Walk (Sum.inr b) (Sum.inr b)hc:c.IsCycleh1:Star5.Adj (Sum.inr b) c.sndh2:Star5.Adj c.penultimate (Sum.inr b)hs:c.snd.isLeft = truehp:c.penultimate.isLeft = true⊢ Falsekey:∀ (b : Fin 5) (c : Star5.Walk (Sum.inr b) (Sum.inr b)), ¬c.IsCycle⊢ Star5.IsAcyclic
    apply hc.snd_ne_penultimateb:Fin 5c:Star5.Walk (Sum.inr b) (Sum.inr b)hc:c.IsCycleh1:Star5.Adj (Sum.inr b) c.sndh2:Star5.Adj c.penultimate (Sum.inr b)hs:c.snd.isLeft = truehp:c.penultimate.isLeft = true⊢ c.snd = c.penultimatekey:∀ (b : Fin 5) (c : Star5.Walk (Sum.inr b) (Sum.inr b)), ¬c.IsCycle⊢ Star5.IsAcyclic
    obtain ⟨x, hx⟩ := Sum.isLeft_iff.mp hsb:Fin 5c:Star5.Walk (Sum.inr b) (Sum.inr b)hc:c.IsCycleh1:Star5.Adj (Sum.inr b) c.sndh2:Star5.Adj c.penultimate (Sum.inr b)hs:c.snd.isLeft = truehp:c.penultimate.isLeft = truex:Fin 1hx:c.snd = Sum.inl x⊢ c.snd = c.penultimatekey:∀ (b : Fin 5) (c : Star5.Walk (Sum.inr b) (Sum.inr b)), ¬c.IsCycle⊢ Star5.IsAcyclic
    obtain ⟨y, hy⟩ := Sum.isLeft_iff.mp hpb:Fin 5c:Star5.Walk (Sum.inr b) (Sum.inr b)hc:c.IsCycleh1:Star5.Adj (Sum.inr b) c.sndh2:Star5.Adj c.penultimate (Sum.inr b)hs:c.snd.isLeft = truehp:c.penultimate.isLeft = truex:Fin 1hx:c.snd = Sum.inl xy:Fin 1hy:c.penultimate = Sum.inl y⊢ c.snd = c.penultimatekey:∀ (b : Fin 5) (c : Star5.Walk (Sum.inr b) (Sum.inr b)), ¬c.IsCycle⊢ Star5.IsAcyclic
    rw [hx,b:Fin 5c:Star5.Walk (Sum.inr b) (Sum.inr b)hc:c.IsCycleh1:Star5.Adj (Sum.inr b) c.sndh2:Star5.Adj c.penultimate (Sum.inr b)hs:c.snd.isLeft = truehp:c.penultimate.isLeft = truex:Fin 1hx:c.snd = Sum.inl xy:Fin 1hy:c.penultimate = Sum.inl y⊢ Sum.inl x = c.penultimatekey:∀ (b : Fin 5) (c : Star5.Walk (Sum.inr b) (Sum.inr b)), ¬c.IsCycle⊢ Star5.IsAcyclic hy,b:Fin 5c:Star5.Walk (Sum.inr b) (Sum.inr b)hc:c.IsCycleh1:Star5.Adj (Sum.inr b) c.sndh2:Star5.Adj c.penultimate (Sum.inr b)hs:c.snd.isLeft = truehp:c.penultimate.isLeft = truex:Fin 1hx:c.snd = Sum.inl xy:Fin 1hy:c.penultimate = Sum.inl y⊢ Sum.inl x = Sum.inl ykey:∀ (b : Fin 5) (c : Star5.Walk (Sum.inr b) (Sum.inr b)), ¬c.IsCycle⊢ Star5.IsAcyclic Subsingleton.elim x yb:Fin 5c:Star5.Walk (Sum.inr b) (Sum.inr b)hc:c.IsCycleh1:Star5.Adj (Sum.inr b) c.sndh2:Star5.Adj c.penultimate (Sum.inr b)hs:c.snd.isLeft = truehp:c.penultimate.isLeft = truex:Fin 1hx:c.snd = Sum.inl xy:Fin 1hy:c.penultimate = Sum.inl y⊢ Sum.inl y = Sum.inl ykey:∀ (b : Fin 5) (c : Star5.Walk (Sum.inr b) (Sum.inr b)), ¬c.IsCycle⊢ Star5.IsAcyclic]key:∀ (b : Fin 5) (c : Star5.Walk (Sum.inr b) (Sum.inr b)), ¬c.IsCycle⊢ Star5.IsAcyclickey:∀ (b : Fin 5) (c : Star5.Walk (Sum.inr b) (Sum.inr b)), ¬c.IsCycle⊢ Star5.IsAcyclic
  intro v c hckey:∀ (b : Fin 5) (c : Star5.Walk (Sum.inr b) (Sum.inr b)), ¬c.IsCyclev:Fin 1 ⊕ Fin 5c:Star5.Walk v vhc:c.IsCycle⊢ False
  cases v with
  | inr b =>inrkey:∀ (b : Fin 5) (c : Star5.Walk (Sum.inr b) (Sum.inr b)), ¬c.IsCycleb:Fin 5c:Star5.Walk (Sum.inr b) (Sum.inr b)hc:c.IsCycle⊢ False exact key b c hcAll goals completed! 🐙
  | inl a =>inlkey:∀ (b : Fin 5) (c : Star5.Walk (Sum.inr b) (Sum.inr b)), ¬c.IsCyclea:Fin 1c:Star5.Walk (Sum.inl a) (Sum.inl a)hc:c.IsCycle⊢ False
    have h1 := c.adj_snd hc.not_nilinlkey:∀ (b : Fin 5) (c : Star5.Walk (Sum.inr b) (Sum.inr b)), ¬c.IsCyclea:Fin 1c:Star5.Walk (Sum.inl a) (Sum.inl a)hc:c.IsCycleh1:Star5.Adj (Sum.inl a) c.snd⊢ False
    obtain ⟨b, hb⟩ : ∃ b, c.snd = Sum.inr b := bykey:∀ (b : Fin 5) (c : Star5.Walk (Sum.inr b) (Sum.inr b)), ¬c.IsCyclea:Fin 1c:Star5.Walk (Sum.inl a) (Sum.inl a)hc:c.IsCycleh1:Star5.Adj (Sum.inl a) c.snd⊢ ∃ b, c.snd = Sum.inr binlkey:∀ (b : Fin 5) (c : Star5.Walk (Sum.inr b) (Sum.inr b)), ¬c.IsCyclea:Fin 1c:Star5.Walk (Sum.inl a) (Sum.inl a)hc:c.IsCycleh1:Star5.Adj (Sum.inl a) c.sndb:Fin 5hb:c.snd = Sum.inr b⊢ False
      rcases hsnd : c.snd with x | yinlkey:∀ (b : Fin 5) (c : Star5.Walk (Sum.inr b) (Sum.inr b)), ¬c.IsCyclea:Fin 1c:Star5.Walk (Sum.inl a) (Sum.inl a)hc:c.IsCycleh1:Star5.Adj (Sum.inl a) c.sndx:Fin 1hsnd:c.snd = Sum.inl x⊢ ∃ b, Sum.inl x = Sum.inr binrkey:∀ (b : Fin 5) (c : Star5.Walk (Sum.inr b) (Sum.inr b)), ¬c.IsCyclea:Fin 1c:Star5.Walk (Sum.inl a) (Sum.inl a)hc:c.IsCycleh1:Star5.Adj (Sum.inl a) c.sndy:Fin 5hsnd:c.snd = Sum.inr y⊢ ∃ b, Sum.inr y = Sum.inr binlkey:∀ (b : Fin 5) (c : Star5.Walk (Sum.inr b) (Sum.inr b)), ¬c.IsCyclea:Fin 1c:Star5.Walk (Sum.inl a) (Sum.inl a)hc:c.IsCycleh1:Star5.Adj (Sum.inl a) c.sndb:Fin 5hb:c.snd = Sum.inr b⊢ False
      ·inlkey:∀ (b : Fin 5) (c : Star5.Walk (Sum.inr b) (Sum.inr b)), ¬c.IsCyclea:Fin 1c:Star5.Walk (Sum.inl a) (Sum.inl a)hc:c.IsCycleh1:Star5.Adj (Sum.inl a) c.sndx:Fin 1hsnd:c.snd = Sum.inl x⊢ ∃ b, Sum.inl x = Sum.inr binlkey:∀ (b : Fin 5) (c : Star5.Walk (Sum.inr b) (Sum.inr b)), ¬c.IsCyclea:Fin 1c:Star5.Walk (Sum.inl a) (Sum.inl a)hc:c.IsCycleh1:Star5.Adj (Sum.inl a) c.sndb:Fin 5hb:c.snd = Sum.inr b⊢ False rw [hsndinlkey:∀ (b : Fin 5) (c : Star5.Walk (Sum.inr b) (Sum.inr b)), ¬c.IsCyclea:Fin 1c:Star5.Walk (Sum.inl a) (Sum.inl a)hc:c.IsCyclex:Fin 1h1:Star5.Adj (Sum.inl a) (Sum.inl x)hsnd:c.snd = Sum.inl x⊢ ∃ b, Sum.inl x = Sum.inr binlkey:∀ (b : Fin 5) (c : Star5.Walk (Sum.inr b) (Sum.inr b)), ¬c.IsCyclea:Fin 1c:Star5.Walk (Sum.inl a) (Sum.inl a)hc:c.IsCyclex:Fin 1h1:Star5.Adj (Sum.inl a) (Sum.inl x)hsnd:c.snd = Sum.inl x⊢ ∃ b, Sum.inl x = Sum.inr binlkey:∀ (b : Fin 5) (c : Star5.Walk (Sum.inr b) (Sum.inr b)), ¬c.IsCyclea:Fin 1c:Star5.Walk (Sum.inl a) (Sum.inl a)hc:c.IsCycleh1:Star5.Adj (Sum.inl a) c.sndb:Fin 5hb:c.snd = Sum.inr b⊢ False] at h1inlkey:∀ (b : Fin 5) (c : Star5.Walk (Sum.inr b) (Sum.inr b)), ¬c.IsCyclea:Fin 1c:Star5.Walk (Sum.inl a) (Sum.inl a)hc:c.IsCyclex:Fin 1h1:Star5.Adj (Sum.inl a) (Sum.inl x)hsnd:c.snd = Sum.inl x⊢ ∃ b, Sum.inl x = Sum.inr binlkey:∀ (b : Fin 5) (c : Star5.Walk (Sum.inr b) (Sum.inr b)), ¬c.IsCyclea:Fin 1c:Star5.Walk (Sum.inl a) (Sum.inl a)hc:c.IsCycleh1:Star5.Adj (Sum.inl a) c.sndb:Fin 5hb:c.snd = Sum.inr b⊢ False; simp [Star5, completeBipartiteGraph] at h1All goals completed! 🐙inlkey:∀ (b : Fin 5) (c : Star5.Walk (Sum.inr b) (Sum.inr b)), ¬c.IsCyclea:Fin 1c:Star5.Walk (Sum.inl a) (Sum.inl a)hc:c.IsCycleh1:Star5.Adj (Sum.inl a) c.sndb:Fin 5hb:c.snd = Sum.inr b⊢ False
      ·inrkey:∀ (b : Fin 5) (c : Star5.Walk (Sum.inr b) (Sum.inr b)), ¬c.IsCyclea:Fin 1c:Star5.Walk (Sum.inl a) (Sum.inl a)hc:c.IsCycleh1:Star5.Adj (Sum.inl a) c.sndy:Fin 5hsnd:c.snd = Sum.inr y⊢ ∃ b, Sum.inr y = Sum.inr binlkey:∀ (b : Fin 5) (c : Star5.Walk (Sum.inr b) (Sum.inr b)), ¬c.IsCyclea:Fin 1c:Star5.Walk (Sum.inl a) (Sum.inl a)hc:c.IsCycleh1:Star5.Adj (Sum.inl a) c.sndb:Fin 5hb:c.snd = Sum.inr b⊢ False exact ⟨y, rfl⟩inlkey:∀ (b : Fin 5) (c : Star5.Walk (Sum.inr b) (Sum.inr b)), ¬c.IsCyclea:Fin 1c:Star5.Walk (Sum.inl a) (Sum.inl a)hc:c.IsCycleh1:Star5.Adj (Sum.inl a) c.sndb:Fin 5hb:c.snd = Sum.inr b⊢ Falseinlkey:∀ (b : Fin 5) (c : Star5.Walk (Sum.inr b) (Sum.inr b)), ¬c.IsCyclea:Fin 1c:Star5.Walk (Sum.inl a) (Sum.inl a)hc:c.IsCycleh1:Star5.Adj (Sum.inl a) c.sndb:Fin 5hb:c.snd = Sum.inr b⊢ False
    have hmem : Sum.inr b ∈ c.support := hb ▸ List.mem_of_mem_tail (c.snd_mem_tail_support hc.not_nil)inlkey:∀ (b : Fin 5) (c : Star5.Walk (Sum.inr b) (Sum.inr b)), ¬c.IsCyclea:Fin 1c:Star5.Walk (Sum.inl a) (Sum.inl a)hc:c.IsCycleh1:Star5.Adj (Sum.inl a) c.sndb:Fin 5hb:c.snd = Sum.inr bhmem:Sum.inr b ∈ c.support⊢ False
    exact key b (c.rotate _ hmem) (hc.rotate hmem)All goals completed! 🐙



open scoped Classical in
@[category test, AMS 5]
theorem Star5_order : Fintype.card ↥(⊤ : Subgraph Star5).verts = 6 := by⊢ Fintype.card ↑⊤.verts = 6
  rw [Fintype.card_congr SimpleGraph.Subgraph.topIso.toEquiv⊢ Fintype.card (Fin 1 ⊕ Fin 5) = 6⊢ Fintype.card (Fin 1 ⊕ Fin 5) = 6]⊢ Fintype.card (Fin 1 ⊕ Fin 5) = 6
  rflAll goals completed! 🐙

@[category test, AMS 5]
theorem Star5_size : Star5.edgeFinset.card = 5 := by⊢ Star5.edgeFinset.card = 5
  decide +nativeAll goals completed! 🐙



@[category test, AMS 5]
theorem Star5_szeged : szegedIndex Star5 = 25 := by⊢ Star5.szegedIndex = 25
  rw [szeged_eq_computable⊢ Star5.computable_szeged_index = 25⊢ Star5.computable_szeged_index = 25]⊢ Star5.computable_szeged_index = 25; decide +nativeAll goals completed! 🐙



@[category test, AMS 5]
theorem Star5_wiener : wienerIndex Star5 = 25 := by⊢ Star5.wienerIndex = 25
  rw [wiener_eq_computable⊢ Star5.computable_wiener = 25⊢ Star5.computable_wiener = 25]⊢ Star5.computable_wiener = 25; decide +nativeAll goals completed! 🐙

@[category test, AMS 5]
theorem Star5_min_deg : Star5.minDegree = 1 := by⊢ Star5.minDegree = 1
  decide +nativeAll goals completed! 🐙

@[category test, AMS 5]
theorem Star5_max_deg : Star5.maxDegree = 5 := by⊢ Star5.maxDegree = 5
  decide +nativeAll goals completed! 🐙

@[category test, AMS 5]
theorem Star5_avg_deg : averageDegree Star5 = 5/3 := by⊢ Star5.averageDegree = 5 / 3
  unfold averageDegree⊢ (∑ v, ↑(Star5.degree v)) / ↑(Fintype.card (Fin 1 ⊕ Fin 5)) = 5 / 3; simp [Fintype.card_sum, Fintype.card_fin]⊢ (↑(Star5.degree (Sum.inl 0)) + ∑ a₂, ↑(Star5.degree (Sum.inr a₂))) / 6 = 5 / 3; decide +nativeAll goals completed! 🐙



@[category test, AMS 5]
theorem Star5_matching : matchingNumber Star5 = 1 := by⊢ Star5.matchingNumber = 1
  classical
  have hle : ∀ M : Subgraph Star5, M.IsMatching → M.edgeSet.toFinset.card ≤ 1 := by
    intro M hMM:Star5.SubgraphhM:M.IsMatching⊢ M.edgeSet.toFinset.card ≤ 1hle:∀ (M : Star5.Subgraph), M.IsMatching → M.edgeSet.toFinset.card ≤ 1⊢ Star5.matchingNumber = 1
    have hcenter : ∀ e ∈ M.edgeSet, (Sum.inl 0 : Fin 1 ⊕ Fin 5) ∈ e := by⊢ Star5.matchingNumber = 1M:Star5.SubgraphhM:M.IsMatchinghcenter:∀ e ∈ M.edgeSet, Sum.inl 0 ∈ e⊢ M.edgeSet.toFinset.card ≤ 1hle:∀ (M : Star5.Subgraph), M.IsMatching → M.edgeSet.toFinset.card ≤ 1⊢ Star5.matchingNumber = 1
      intro e heM:Star5.SubgraphhM:M.IsMatchinge:Sym2 (Fin 1 ⊕ Fin 5)he:e ∈ M.edgeSet⊢ Sum.inl 0 ∈ eM:Star5.SubgraphhM:M.IsMatchinghcenter:∀ e ∈ M.edgeSet, Sum.inl 0 ∈ e⊢ M.edgeSet.toFinset.card ≤ 1hle:∀ (M : Star5.Subgraph), M.IsMatching → M.edgeSet.toFinset.card ≤ 1⊢ Star5.matchingNumber = 1
      induction e using Sym2.inductionOn with | _ a b =>hfM:Star5.SubgraphhM:M.IsMatchinga:Fin 1 ⊕ Fin 5b:Fin 1 ⊕ Fin 5he:s(a, b) ∈ M.edgeSet⊢ Sum.inl 0 ∈ s(a, b)M:Star5.SubgraphhM:M.IsMatchinghcenter:∀ e ∈ M.edgeSet, Sum.inl 0 ∈ e⊢ M.edgeSet.toFinset.card ≤ 1hle:∀ (M : Star5.Subgraph), M.IsMatching → M.edgeSet.toFinset.card ≤ 1⊢ Star5.matchingNumber = 1
      rw [Subgraph.mem_edgeSethfM:Star5.SubgraphhM:M.IsMatchinga:Fin 1 ⊕ Fin 5b:Fin 1 ⊕ Fin 5he:M.Adj a b⊢ Sum.inl 0 ∈ s(a, b)hfM:Star5.SubgraphhM:M.IsMatchinga:Fin 1 ⊕ Fin 5b:Fin 1 ⊕ Fin 5he:M.Adj a b⊢ Sum.inl 0 ∈ s(a, b)M:Star5.SubgraphhM:M.IsMatchinghcenter:∀ e ∈ M.edgeSet, Sum.inl 0 ∈ e⊢ M.edgeSet.toFinset.card ≤ 1hle:∀ (M : Star5.Subgraph), M.IsMatching → M.edgeSet.toFinset.card ≤ 1⊢ Star5.matchingNumber = 1] at hehfM:Star5.SubgraphhM:M.IsMatchinga:Fin 1 ⊕ Fin 5b:Fin 1 ⊕ Fin 5he:M.Adj a b⊢ Sum.inl 0 ∈ s(a, b)M:Star5.SubgraphhM:M.IsMatchinghcenter:∀ e ∈ M.edgeSet, Sum.inl 0 ∈ e⊢ M.edgeSet.toFinset.card ≤ 1hle:∀ (M : Star5.Subgraph), M.IsMatching → M.edgeSet.toFinset.card ≤ 1⊢ Star5.matchingNumber = 1
      have hadj := he.adj_subhfM:Star5.SubgraphhM:M.IsMatchinga:Fin 1 ⊕ Fin 5b:Fin 1 ⊕ Fin 5he:M.Adj a bhadj:Star5.Adj a b⊢ Sum.inl 0 ∈ s(a, b)M:Star5.SubgraphhM:M.IsMatchinghcenter:∀ e ∈ M.edgeSet, Sum.inl 0 ∈ e⊢ M.edgeSet.toFinset.card ≤ 1hle:∀ (M : Star5.Subgraph), M.IsMatching → M.edgeSet.toFinset.card ≤ 1⊢ Star5.matchingNumber = 1
      simp only [Star5, completeBipartiteGraph] at hadjhfM:Star5.SubgraphhM:M.IsMatchinga:Fin 1 ⊕ Fin 5b:Fin 1 ⊕ Fin 5he:M.Adj a bhadj:a.isLeft = true ∧ b.isRight = true ∨ a.isRight = true ∧ b.isLeft = true⊢ Sum.inl 0 ∈ s(a, b)M:Star5.SubgraphhM:M.IsMatchinghcenter:∀ e ∈ M.edgeSet, Sum.inl 0 ∈ e⊢ M.edgeSet.toFinset.card ≤ 1hle:∀ (M : Star5.Subgraph), M.IsMatching → M.edgeSet.toFinset.card ≤ 1⊢ Star5.matchingNumber = 1
      rw [Sym2.mem_iffhfM:Star5.SubgraphhM:M.IsMatchinga:Fin 1 ⊕ Fin 5b:Fin 1 ⊕ Fin 5he:M.Adj a bhadj:a.isLeft = true ∧ b.isRight = true ∨ a.isRight = true ∧ b.isLeft = true⊢ Sum.inl 0 = a ∨ Sum.inl 0 = bhfM:Star5.SubgraphhM:M.IsMatchinga:Fin 1 ⊕ Fin 5b:Fin 1 ⊕ Fin 5he:M.Adj a bhadj:a.isLeft = true ∧ b.isRight = true ∨ a.isRight = true ∧ b.isLeft = true⊢ Sum.inl 0 = a ∨ Sum.inl 0 = bM:Star5.SubgraphhM:M.IsMatchinghcenter:∀ e ∈ M.edgeSet, Sum.inl 0 ∈ e⊢ M.edgeSet.toFinset.card ≤ 1hle:∀ (M : Star5.Subgraph), M.IsMatching → M.edgeSet.toFinset.card ≤ 1⊢ Star5.matchingNumber = 1]hfM:Star5.SubgraphhM:M.IsMatchinga:Fin 1 ⊕ Fin 5b:Fin 1 ⊕ Fin 5he:M.Adj a bhadj:a.isLeft = true ∧ b.isRight = true ∨ a.isRight = true ∧ b.isLeft = true⊢ Sum.inl 0 = a ∨ Sum.inl 0 = bM:Star5.SubgraphhM:M.IsMatchinghcenter:∀ e ∈ M.edgeSet, Sum.inl 0 ∈ e⊢ M.edgeSet.toFinset.card ≤ 1hle:∀ (M : Star5.Subgraph), M.IsMatching → M.edgeSet.toFinset.card ≤ 1⊢ Star5.matchingNumber = 1
      rcases hadj with ⟨ha, _⟩ | ⟨_, hb⟩hf.inlM:Star5.SubgraphhM:M.IsMatchinga:Fin 1 ⊕ Fin 5b:Fin 1 ⊕ Fin 5he:M.Adj a bha:a.isLeft = trueright✝:b.isRight = true⊢ Sum.inl 0 = a ∨ Sum.inl 0 = bhf.inrM:Star5.SubgraphhM:M.IsMatchinga:Fin 1 ⊕ Fin 5b:Fin 1 ⊕ Fin 5he:M.Adj a bleft✝:a.isRight = truehb:b.isLeft = true⊢ Sum.inl 0 = a ∨ Sum.inl 0 = bM:Star5.SubgraphhM:M.IsMatchinghcenter:∀ e ∈ M.edgeSet, Sum.inl 0 ∈ e⊢ M.edgeSet.toFinset.card ≤ 1hle:∀ (M : Star5.Subgraph), M.IsMatching → M.edgeSet.toFinset.card ≤ 1⊢ Star5.matchingNumber = 1
      ·hf.inlM:Star5.SubgraphhM:M.IsMatchinga:Fin 1 ⊕ Fin 5b:Fin 1 ⊕ Fin 5he:M.Adj a bha:a.isLeft = trueright✝:b.isRight = true⊢ Sum.inl 0 = a ∨ Sum.inl 0 = bM:Star5.SubgraphhM:M.IsMatchinghcenter:∀ e ∈ M.edgeSet, Sum.inl 0 ∈ e⊢ M.edgeSet.toFinset.card ≤ 1hle:∀ (M : Star5.Subgraph), M.IsMatching → M.edgeSet.toFinset.card ≤ 1⊢ Star5.matchingNumber = 1 lefthf.inlM:Star5.SubgraphhM:M.IsMatchinga:Fin 1 ⊕ Fin 5b:Fin 1 ⊕ Fin 5he:M.Adj a bha:a.isLeft = trueright✝:b.isRight = true⊢ Sum.inl 0 = aM:Star5.SubgraphhM:M.IsMatchinghcenter:∀ e ∈ M.edgeSet, Sum.inl 0 ∈ e⊢ M.edgeSet.toFinset.card ≤ 1hle:∀ (M : Star5.Subgraph), M.IsMatching → M.edgeSet.toFinset.card ≤ 1⊢ Star5.matchingNumber = 1; obtain ⟨a', rfl⟩ := Sum.isLeft_iff.mp hahf.inlM:Star5.SubgraphhM:M.IsMatchingb:Fin 1 ⊕ Fin 5right✝:b.isRight = truea':Fin 1he:M.Adj (Sum.inl a') bha:(Sum.inl a').isLeft = true⊢ Sum.inl 0 = Sum.inl a'M:Star5.SubgraphhM:M.IsMatchinghcenter:∀ e ∈ M.edgeSet, Sum.inl 0 ∈ e⊢ M.edgeSet.toFinset.card ≤ 1hle:∀ (M : Star5.Subgraph), M.IsMatching → M.edgeSet.toFinset.card ≤ 1⊢ Star5.matchingNumber = 1; exact congrArg Sum.inl (Subsingleton.elim 0 a')All goals completed! 🐙M:Star5.SubgraphhM:M.IsMatchinghcenter:∀ e ∈ M.edgeSet, Sum.inl 0 ∈ e⊢ M.edgeSet.toFinset.card ≤ 1hle:∀ (M : Star5.Subgraph), M.IsMatching → M.edgeSet.toFinset.card ≤ 1⊢ Star5.matchingNumber = 1
      ·hf.inrM:Star5.SubgraphhM:M.IsMatchinga:Fin 1 ⊕ Fin 5b:Fin 1 ⊕ Fin 5he:M.Adj a bleft✝:a.isRight = truehb:b.isLeft = true⊢ Sum.inl 0 = a ∨ Sum.inl 0 = bM:Star5.SubgraphhM:M.IsMatchinghcenter:∀ e ∈ M.edgeSet, Sum.inl 0 ∈ e⊢ M.edgeSet.toFinset.card ≤ 1hle:∀ (M : Star5.Subgraph), M.IsMatching → M.edgeSet.toFinset.card ≤ 1⊢ Star5.matchingNumber = 1 righthf.inrM:Star5.SubgraphhM:M.IsMatchinga:Fin 1 ⊕ Fin 5b:Fin 1 ⊕ Fin 5he:M.Adj a bleft✝:a.isRight = truehb:b.isLeft = true⊢ Sum.inl 0 = bM:Star5.SubgraphhM:M.IsMatchinghcenter:∀ e ∈ M.edgeSet, Sum.inl 0 ∈ e⊢ M.edgeSet.toFinset.card ≤ 1hle:∀ (M : Star5.Subgraph), M.IsMatching → M.edgeSet.toFinset.card ≤ 1⊢ Star5.matchingNumber = 1; obtain ⟨b', rfl⟩ := Sum.isLeft_iff.mp hbhf.inrM:Star5.SubgraphhM:M.IsMatchinga:Fin 1 ⊕ Fin 5left✝:a.isRight = trueb':Fin 1he:M.Adj a (Sum.inl b')hb:(Sum.inl b').isLeft = true⊢ Sum.inl 0 = Sum.inl b'M:Star5.SubgraphhM:M.IsMatchinghcenter:∀ e ∈ M.edgeSet, Sum.inl 0 ∈ e⊢ M.edgeSet.toFinset.card ≤ 1hle:∀ (M : Star5.Subgraph), M.IsMatching → M.edgeSet.toFinset.card ≤ 1⊢ Star5.matchingNumber = 1; exact congrArg Sum.inl (Subsingleton.elim 0 b')M:Star5.SubgraphhM:M.IsMatchinghcenter:∀ e ∈ M.edgeSet, Sum.inl 0 ∈ e⊢ M.edgeSet.toFinset.card ≤ 1hle:∀ (M : Star5.Subgraph), M.IsMatching → M.edgeSet.toFinset.card ≤ 1⊢ Star5.matchingNumber = 1M:Star5.SubgraphhM:M.IsMatchinghcenter:∀ e ∈ M.edgeSet, Sum.inl 0 ∈ e⊢ M.edgeSet.toFinset.card ≤ 1hle:∀ (M : Star5.Subgraph), M.IsMatching → M.edgeSet.toFinset.card ≤ 1⊢ Star5.matchingNumber = 1
    rw [Finset.card_le_oneM:Star5.SubgraphhM:M.IsMatchinghcenter:∀ e ∈ M.edgeSet, Sum.inl 0 ∈ e⊢ ∀ a ∈ M.edgeSet.toFinset, ∀ b ∈ M.edgeSet.toFinset, a = bM:Star5.SubgraphhM:M.IsMatchinghcenter:∀ e ∈ M.edgeSet, Sum.inl 0 ∈ e⊢ ∀ a ∈ M.edgeSet.toFinset, ∀ b ∈ M.edgeSet.toFinset, a = bhle:∀ (M : Star5.Subgraph), M.IsMatching → M.edgeSet.toFinset.card ≤ 1⊢ Star5.matchingNumber = 1]M:Star5.SubgraphhM:M.IsMatchinghcenter:∀ e ∈ M.edgeSet, Sum.inl 0 ∈ e⊢ ∀ a ∈ M.edgeSet.toFinset, ∀ b ∈ M.edgeSet.toFinset, a = bhle:∀ (M : Star5.Subgraph), M.IsMatching → M.edgeSet.toFinset.card ≤ 1⊢ Star5.matchingNumber = 1
    intro e he f hfM:Star5.SubgraphhM:M.IsMatchinghcenter:∀ e ∈ M.edgeSet, Sum.inl 0 ∈ ee:Sym2 (Fin 1 ⊕ Fin 5)he:e ∈ M.edgeSet.toFinsetf:Sym2 (Fin 1 ⊕ Fin 5)hf:f ∈ M.edgeSet.toFinset⊢ e = fhle:∀ (M : Star5.Subgraph), M.IsMatching → M.edgeSet.toFinset.card ≤ 1⊢ Star5.matchingNumber = 1
    rw [Set.mem_toFinsetM:Star5.SubgraphhM:M.IsMatchinghcenter:∀ e ∈ M.edgeSet, Sum.inl 0 ∈ ee:Sym2 (Fin 1 ⊕ Fin 5)he:e ∈ M.edgeSetf:Sym2 (Fin 1 ⊕ Fin 5)hf:f ∈ M.edgeSet⊢ e = fM:Star5.SubgraphhM:M.IsMatchinghcenter:∀ e ∈ M.edgeSet, Sum.inl 0 ∈ ee:Sym2 (Fin 1 ⊕ Fin 5)he:e ∈ M.edgeSetf:Sym2 (Fin 1 ⊕ Fin 5)hf:f ∈ M.edgeSet⊢ e = fhle:∀ (M : Star5.Subgraph), M.IsMatching → M.edgeSet.toFinset.card ≤ 1⊢ Star5.matchingNumber = 1] at he hfM:Star5.SubgraphhM:M.IsMatchinghcenter:∀ e ∈ M.edgeSet, Sum.inl 0 ∈ ee:Sym2 (Fin 1 ⊕ Fin 5)he:e ∈ M.edgeSetf:Sym2 (Fin 1 ⊕ Fin 5)hf:f ∈ M.edgeSet⊢ e = fhle:∀ (M : Star5.Subgraph), M.IsMatching → M.edgeSet.toFinset.card ≤ 1⊢ Star5.matchingNumber = 1
    obtain ⟨y, rfl⟩ := Sym2.mem_iff_exists.mp (hcenter e he)M:Star5.SubgraphhM:M.IsMatchinghcenter:∀ e ∈ M.edgeSet, Sum.inl 0 ∈ ef:Sym2 (Fin 1 ⊕ Fin 5)hf:f ∈ M.edgeSety:Fin 1 ⊕ Fin 5he:s(Sum.inl 0, y) ∈ M.edgeSet⊢ s(Sum.inl 0, y) = fhle:∀ (M : Star5.Subgraph), M.IsMatching → M.edgeSet.toFinset.card ≤ 1⊢ Star5.matchingNumber = 1
    obtain ⟨z, rfl⟩ := Sym2.mem_iff_exists.mp (hcenter f hf)M:Star5.SubgraphhM:M.IsMatchinghcenter:∀ e ∈ M.edgeSet, Sum.inl 0 ∈ ey:Fin 1 ⊕ Fin 5he:s(Sum.inl 0, y) ∈ M.edgeSetz:Fin 1 ⊕ Fin 5hf:s(Sum.inl 0, z) ∈ M.edgeSet⊢ s(Sum.inl 0, y) = s(Sum.inl 0, z)hle:∀ (M : Star5.Subgraph), M.IsMatching → M.edgeSet.toFinset.card ≤ 1⊢ Star5.matchingNumber = 1
    rw [Subgraph.mem_edgeSetM:Star5.SubgraphhM:M.IsMatchinghcenter:∀ e ∈ M.edgeSet, Sum.inl 0 ∈ ey:Fin 1 ⊕ Fin 5he:M.Adj (Sum.inl 0) yz:Fin 1 ⊕ Fin 5hf:M.Adj (Sum.inl 0) z⊢ s(Sum.inl 0, y) = s(Sum.inl 0, z)M:Star5.SubgraphhM:M.IsMatchinghcenter:∀ e ∈ M.edgeSet, Sum.inl 0 ∈ ey:Fin 1 ⊕ Fin 5he:M.Adj (Sum.inl 0) yz:Fin 1 ⊕ Fin 5hf:M.Adj (Sum.inl 0) z⊢ s(Sum.inl 0, y) = s(Sum.inl 0, z)hle:∀ (M : Star5.Subgraph), M.IsMatching → M.edgeSet.toFinset.card ≤ 1⊢ Star5.matchingNumber = 1] at he hfM:Star5.SubgraphhM:M.IsMatchinghcenter:∀ e ∈ M.edgeSet, Sum.inl 0 ∈ ey:Fin 1 ⊕ Fin 5he:M.Adj (Sum.inl 0) yz:Fin 1 ⊕ Fin 5hf:M.Adj (Sum.inl 0) z⊢ s(Sum.inl 0, y) = s(Sum.inl 0, z)hle:∀ (M : Star5.Subgraph), M.IsMatching → M.edgeSet.toFinset.card ≤ 1⊢ Star5.matchingNumber = 1
    rw [hM.eq_of_adj_left he hfM:Star5.SubgraphhM:M.IsMatchinghcenter:∀ e ∈ M.edgeSet, Sum.inl 0 ∈ ey:Fin 1 ⊕ Fin 5he:M.Adj (Sum.inl 0) yz:Fin 1 ⊕ Fin 5hf:M.Adj (Sum.inl 0) z⊢ s(Sum.inl 0, z) = s(Sum.inl 0, z)hle:∀ (M : Star5.Subgraph), M.IsMatching → M.edgeSet.toFinset.card ≤ 1⊢ Star5.matchingNumber = 1]hle:∀ (M : Star5.Subgraph), M.IsMatching → M.edgeSet.toFinset.card ≤ 1⊢ Star5.matchingNumber = 1hle:∀ (M : Star5.Subgraph), M.IsMatching → M.edgeSet.toFinset.card ≤ 1⊢ Star5.matchingNumber = 1
  have hbdd : BddAbove (Set.image (fun M : Subgraph Star5 => (M.edgeSet.toFinset.card : ℝ)) {M | M.IsMatching}) := by
    refine ⟨1, ?_⟩hle:∀ (M : Star5.Subgraph), M.IsMatching → M.edgeSet.toFinset.card ≤ 1⊢ 1 ∈ upperBounds ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})hle:∀ (M : Star5.Subgraph), M.IsMatching → M.edgeSet.toFinset.card ≤ 1hbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ Star5.matchingNumber = 1
    rintro x ⟨M, hM, rfl⟩hle:∀ (M : Star5.Subgraph), M.IsMatching → M.edgeSet.toFinset.card ≤ 1M:Star5.SubgraphhM:M ∈ {M | M.IsMatching}⊢ (fun M ↦ ↑M.edgeSet.toFinset.card) M ≤ 1hle:∀ (M : Star5.Subgraph), M.IsMatching → M.edgeSet.toFinset.card ≤ 1hbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ Star5.matchingNumber = 1
    show (M.edgeSet.toFinset.card : ℝ) ≤ 1hle:∀ (M : Star5.Subgraph), M.IsMatching → M.edgeSet.toFinset.card ≤ 1M:Star5.SubgraphhM:M ∈ {M | M.IsMatching}⊢ ↑M.edgeSet.toFinset.card ≤ 1hle:∀ (M : Star5.Subgraph), M.IsMatching → M.edgeSet.toFinset.card ≤ 1hbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ Star5.matchingNumber = 1
    exact_mod_cast hle M hMhle:∀ (M : Star5.Subgraph), M.IsMatching → M.edgeSet.toFinset.card ≤ 1hbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ Star5.matchingNumber = 1hle:∀ (M : Star5.Subgraph), M.IsMatching → M.edgeSet.toFinset.card ≤ 1hbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ Star5.matchingNumber = 1
  unfold matchingNumberhle:∀ (M : Star5.Subgraph), M.IsMatching → M.edgeSet.toFinset.card ≤ 1hbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ (have matchings := {M | M.IsMatching};
  sSup ((fun M ↦ ↑M.edgeSet.toFinset.card) '' matchings)) =
  1
  apply le_antisymmahle:∀ (M : Star5.Subgraph), M.IsMatching → M.edgeSet.toFinset.card ≤ 1hbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ (have matchings := {M | M.IsMatching};
  sSup ((fun M ↦ ↑M.edgeSet.toFinset.card) '' matchings)) ≤
  1ahle:∀ (M : Star5.Subgraph), M.IsMatching → M.edgeSet.toFinset.card ≤ 1hbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ 1 ≤
  have matchings := {M | M.IsMatching};
  sSup ((fun M ↦ ↑M.edgeSet.toFinset.card) '' matchings)
  ·ahle:∀ (M : Star5.Subgraph), M.IsMatching → M.edgeSet.toFinset.card ≤ 1hbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ (have matchings := {M | M.IsMatching};
  sSup ((fun M ↦ ↑M.edgeSet.toFinset.card) '' matchings)) ≤
  1 apply csSup_le (Set.Nonempty.image _ ⟨⊥, byhle:∀ (M : Star5.Subgraph), M.IsMatching → M.edgeSet.toFinset.card ≤ 1hbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ ⊥ ∈ {M | M.IsMatching} simp [Subgraph.IsMatching]All goals completed! 🐙⟩)
    rintro x ⟨M, hM, rfl⟩ahle:∀ (M : Star5.Subgraph), M.IsMatching → M.edgeSet.toFinset.card ≤ 1hbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})M:Star5.SubgraphhM:M ∈ {M | M.IsMatching}⊢ (fun M ↦ ↑M.edgeSet.toFinset.card) M ≤ 1
    show (M.edgeSet.toFinset.card : ℝ) ≤ 1ahle:∀ (M : Star5.Subgraph), M.IsMatching → M.edgeSet.toFinset.card ≤ 1hbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})M:Star5.SubgraphhM:M ∈ {M | M.IsMatching}⊢ ↑M.edgeSet.toFinset.card ≤ 1
    exact_mod_cast hle M hMAll goals completed! 🐙
  ·ahle:∀ (M : Star5.Subgraph), M.IsMatching → M.edgeSet.toFinset.card ≤ 1hbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ 1 ≤
  have matchings := {M | M.IsMatching};
  sSup ((fun M ↦ ↑M.edgeSet.toFinset.card) '' matchings) apply le_csSup hbddahle:∀ (M : Star5.Subgraph), M.IsMatching → M.edgeSet.toFinset.card ≤ 1hbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ 1 ∈ (fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching}
    refine ⟨Star5.subgraphOfAdj (show Star5.Adj (Sum.inl 0) (Sum.inr 0) by⊢ Star5.matchingNumber = 1 simp [Star5, completeBipartiteGraph]All goals completed! 🐙), ?_, ?_⟩
    ·a.refine_1hle:∀ (M : Star5.Subgraph), M.IsMatching → M.edgeSet.toFinset.card ≤ 1hbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ Star5.subgraphOfAdj ⋯ ∈ {M | M.IsMatching} exact Subgraph.IsMatching.subgraphOfAdj _All goals completed! 🐙
    ·a.refine_2hle:∀ (M : Star5.Subgraph), M.IsMatching → M.edgeSet.toFinset.card ≤ 1hbdd:BddAbove ((fun M ↦ ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})⊢ (fun M ↦ ↑M.edgeSet.toFinset.card) (Star5.subgraphOfAdj ⋯) = 1 simpAll goals completed! 🐙

@[category test, AMS 5]
theorem Star5_residue : residue Star5 = 5 := by⊢ Star5.residue = 5
  unfold residue⊢ residueAux ((Multiset.map (fun v ↦ Star5.degree v) Finset.univ.val).sort fun x1 x2 ↦ x1 ≥ x2) = 5; decide +nativeAll goals completed! 🐙

@[category test, AMS 5]
theorem Star5_annihilation : annihilationNumber Star5 = 5 := by⊢ Star5.annihilationNumber = 5
  decide +nativeAll goals completed! 🐙

@[category test, AMS 5]
theorem Star5_cvetkovic : cvetkovic Star5 = 5 := by⊢ Star5.cvetkovic = 5
  sorryAll goals completed! 🐙

end WrittenOnTheWallII.Test