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 SimpleGraph


namespace WrittenOnTheWallII.Test


open Classical

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; 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; 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, show computable_avg_dist HouseGraph = (7 / 5 : ℚ) from by decide +native]⊢ ↑(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 decide)]⊢ ↑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 decide)]⊢ ↑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⊢ HouseGraph.girth = 3 decideAll goals completed! 🐙)
      (Walk.cons (show HouseGraph.Adj 3 4 by⊢ HouseGraph.girth = 3 decideAll goals completed! 🐙)
      (Walk.cons (show HouseGraph.Adj 4 2 by⊢ HouseGraph.girth = 3 decideAll goals completed! 🐙) Walk.nil))).IsCycle := by⊢ HouseGraph.girth = 3
    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
    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.Nodup
    ·refine_1⊢ (Walk.cons ⋯ (Walk.cons ⋯ (Walk.cons ⋯ Walk.nil))).IsTrail rw [Walk.isTrail_def]refine_1⊢ (Walk.cons ⋯ (Walk.cons ⋯ (Walk.cons ⋯ Walk.nil))).edges.Nodup; decideAll goals completed! 🐙
    ·refine_2⊢ Walk.cons ⋯ (Walk.cons ⋯ (Walk.cons ⋯ Walk.nil)) ≠ Walk.nil simpAll goals completed! 🐙
    ·refine_3⊢ (Walk.cons ⋯ (Walk.cons ⋯ (Walk.cons ⋯ Walk.nil))).support.tail.Nodup decideAll goals completed! 🐙
  refine le_antisymm ?_ (three_le_girth (fun hac => hac _ hcyc))hcyc:(Walk.cons ⋯ (Walk.cons ⋯ (Walk.cons ⋯ Walk.nil))).IsCycle := 
  Eq.mpr
    (id
      (congrArg (fun _a => _a)
        (propext
          (Walk.isCycle_def
            (Walk.cons
              (have this := of_decide_eq_true (id (Eq.refl true));
              this)
              (Walk.cons
                (have this := of_decide_eq_true (id (Eq.refl true));
                this)
                (Walk.cons
                  (have this := of_decide_eq_true (id (Eq.refl true));
                  this)
                  Walk.nil)))))))
    ⟨Eq.mpr
        (id
          (congrArg (fun _a => _a)
            (propext
              (Walk.isTrail_def
                (Walk.cons
                  (have this := of_decide_eq_true (id (Eq.refl true));
                  this)
                  (Walk.cons
                    (have this := of_decide_eq_true (id (Eq.refl true));
                    this)
                    (Walk.cons
                      (have this := of_decide_eq_true (id (Eq.refl true));
                      this)
                      Walk.nil)))))))
        (of_decide_eq_true (id (Eq.refl true))),
      ⟨of_eq_true
          (Eq.trans (congrArg Not (eq_false' fun h => False.elim (noConfusion_of_Nat Walk.ctorIdx h))) not_false_eq_true),
        of_decide_eq_true (id (Eq.refl true))⟩⟩⊢ HouseGraph.girth ≤ 3
  simpa using girth_le_length hcycAll goals completed! 🐙


@[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
  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; 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; 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
  have hbdd : BddAbove (Set.image (fun M : Subgraph HouseGraph => (M.edgeSet.toFinset.card : ℝ)) {M | M.IsMatching}) := by⊢ HouseGraph.matchingNumber = 2
    refine ⟨(Fintype.card (Fin 5) : ℝ), ?_⟩⊢ ↑(Fintype.card (Fin 5)) ∈ upperBounds ((fun M => ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})
    rintro x ⟨M, hM, rfl⟩M:HouseGraph.SubgraphhM:M ∈ {M | M.IsMatching}⊢ (fun M => ↑M.edgeSet.toFinset.card) M ≤ ↑(Fintype.card (Fin 5))
    show (M.edgeSet.toFinset.card : ℝ) ≤ Fintype.card (Fin 5)M:HouseGraph.SubgraphhM:M ∈ {M | M.IsMatching}⊢ ↑M.edgeSet.toFinset.card ≤ ↑(Fintype.card (Fin 5))
    have hb := matching_card_bound HouseGraph M hMM:HouseGraph.SubgraphhM:M ∈ {M | M.IsMatching}hb:2 * M.edgeSet.toFinset.card ≤ Fintype.card (Fin 5) := matching_card_bound HouseGraph M hM⊢ ↑M.edgeSet.toFinset.card ≤ ↑(Fintype.card (Fin 5))
    exact_mod_cast (byM:HouseGraph.SubgraphhM:M ∈ {M | M.IsMatching}hb:2 * M.edgeSet.toFinset.card ≤ Fintype.card (Fin 5) := matching_card_bound HouseGraph M hM⊢ M.edgeSet.toFinset.card ≤ Fintype.card (Fin 5) omegaAll goals completed! 🐙 : M.edgeSet.toFinset.card ≤ Fintype.card (Fin 5))
  unfold matchingNumberhbdd:BddAbove ((fun M => ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching}) := 
  Exists.intro ↑(Fintype.card (Fin 5)) fun ⦃x⦄ a =>
    Exists.casesOn a fun M h =>
      And.casesOn h fun hM right =>
        right ▸
          id
            (have hb := matching_card_bound HouseGraph M hM;
            cast (Eq.symm Nat.cast_le._simp_1) (Decidable.byContradiction fun a => house_matching._proof_1 M hb a))⊢ (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}) := 
  Exists.intro ↑(Fintype.card (Fin 5)) fun ⦃x⦄ a =>
    Exists.casesOn a fun M h =>
      And.casesOn h fun hM right =>
        right ▸
          id
            (have hb := matching_card_bound HouseGraph M hM;
            cast (Eq.symm Nat.cast_le._simp_1) (Decidable.byContradiction fun a => house_matching._proof_1 M hb a))⊢ (have matchings := {M | M.IsMatching};
  sSup ((fun M => ↑M.edgeSet.toFinset.card) '' matchings)) ≤
  2ahbdd:BddAbove ((fun M => ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching}) := 
  Exists.intro ↑(Fintype.card (Fin 5)) fun ⦃x⦄ a =>
    Exists.casesOn a fun M h =>
      And.casesOn h fun hM right =>
        right ▸
          id
            (have hb := matching_card_bound HouseGraph M hM;
            cast (Eq.symm Nat.cast_le._simp_1) (Decidable.byContradiction fun a => house_matching._proof_1 M hb a))⊢ 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}) := 
  Exists.intro ↑(Fintype.card (Fin 5)) fun ⦃x⦄ a =>
    Exists.casesOn a fun M h =>
      And.casesOn h fun hM right =>
        right ▸
          id
            (have hb := matching_card_bound HouseGraph M hM;
            cast (Eq.symm Nat.cast_le._simp_1) (Decidable.byContradiction fun a => house_matching._proof_1 M hb a))⊢ (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}) := 
  Exists.intro ↑(Fintype.card (Fin 5)) fun ⦃x⦄ a =>
    Exists.casesOn a fun M h =>
      And.casesOn h fun hM right =>
        right ▸
          id
            (have hb := matching_card_bound HouseGraph M hM;
            cast (Eq.symm Nat.cast_le._simp_1) (Decidable.byContradiction fun a => house_matching._proof_1 M hb a))⊢ ⊥ ∈ {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}) := 
  Exists.intro ↑(Fintype.card (Fin 5)) fun ⦃x⦄ a =>
    Exists.casesOn a fun M h =>
      And.casesOn h fun hM right =>
        right ▸
          id
            (have hb := matching_card_bound HouseGraph M hM;
            cast (Eq.symm Nat.cast_le._simp_1) (Decidable.byContradiction fun a => house_matching._proof_1 M hb a))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}) := 
  Exists.intro ↑(Fintype.card (Fin 5)) fun ⦃x⦄ a =>
    Exists.casesOn a fun M h =>
      And.casesOn h fun hM right =>
        right ▸
          id
            (have hb := matching_card_bound HouseGraph M hM;
            cast (Eq.symm Nat.cast_le._simp_1) (Decidable.byContradiction fun a => house_matching._proof_1 M hb a))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}) := 
  Exists.intro ↑(Fintype.card (Fin 5)) fun ⦃x⦄ a =>
    Exists.casesOn a fun M h =>
      And.casesOn h fun hM right =>
        right ▸
          id
            (have hb := matching_card_bound HouseGraph M hM;
            cast (Eq.symm Nat.cast_le._simp_1) (Decidable.byContradiction fun a => house_matching._proof_1 M hb a))M:HouseGraph.SubgraphhM:M ∈ {M | M.IsMatching}hb:2 * M.edgeSet.toFinset.card ≤ Fintype.card (Fin 5) := matching_card_bound HouseGraph M hM⊢ ↑M.edgeSet.toFinset.card ≤ 2
    simp only [Fintype.card_fin] at hbahbdd:BddAbove ((fun M => ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching}) := 
  Exists.intro ↑(Fintype.card (Fin 5)) fun ⦃x⦄ a =>
    Exists.casesOn a fun M h =>
      And.casesOn h fun hM right =>
        right ▸
          id
            (have hb := matching_card_bound HouseGraph M hM;
            cast (Eq.symm Nat.cast_le._simp_1) (Decidable.byContradiction fun a => house_matching._proof_1 M hb a))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}) := 
  Exists.intro ↑(Fintype.card (Fin 5)) fun ⦃x⦄ a =>
    Exists.casesOn a fun M h =>
      And.casesOn h fun hM right =>
        right ▸
          id
            (have hb := matching_card_bound HouseGraph M hM;
            cast (Eq.symm Nat.cast_le._simp_1) (Decidable.byContradiction fun a => house_matching._proof_1 M hb a))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}) := 
  Exists.intro ↑(Fintype.card (Fin 5)) fun ⦃x⦄ a =>
    Exists.casesOn a fun M h =>
      And.casesOn h fun hM right =>
        right ▸
          id
            (have hb := matching_card_bound HouseGraph M hM;
            cast (Eq.symm Nat.cast_le._simp_1) (Decidable.byContradiction fun a => house_matching._proof_1 M hb a))⊢ 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}) := 
  Exists.intro ↑(Fintype.card (Fin 5)) fun ⦃x⦄ a =>
    Exists.casesOn a fun M h =>
      And.casesOn h fun hM right =>
        right ▸
          id
            (have hb := matching_card_bound HouseGraph M hM;
            cast (Eq.symm Nat.cast_le._simp_1) (Decidable.byContradiction fun a => house_matching._proof_1 M hb a))⊢ 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}) := 
  Exists.intro ↑(Fintype.card (Fin 5)) fun ⦃x⦄ a =>
    Exists.casesOn a fun M h =>
      And.casesOn h fun hM right =>
        right ▸
          id
            (have hb := matching_card_bound HouseGraph M hM;
            cast (Eq.symm Nat.cast_le._simp_1) (Decidable.byContradiction fun a => house_matching._proof_1 M hb a))⊢ 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}) := 
  Exists.intro ↑(Fintype.card (Fin 5)) fun ⦃x⦄ a =>
    Exists.casesOn a fun M h =>
      And.casesOn h fun hM right =>
        right ▸
          id
            (have hb := matching_card_bound HouseGraph M hM;
            cast (Eq.symm Nat.cast_le._simp_1) (Decidable.byContradiction fun a => house_matching._proof_1 M hb a))⊢ Disjoint (HouseGraph.subgraphOfAdj ⋯).support (HouseGraph.subgraphOfAdj ⋯).support rw [support_subgraphOfAdj, support_subgraphOfAdj]hbdd:BddAbove ((fun M => ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching}) := 
  Exists.intro ↑(Fintype.card (Fin 5)) fun ⦃x⦄ a =>
    Exists.casesOn a fun M h =>
      And.casesOn h fun hM right =>
        right ▸
          id
            (have hb := matching_card_bound HouseGraph M hM;
            cast (Eq.symm Nat.cast_le._simp_1) (Decidable.byContradiction fun a => house_matching._proof_1 M hb a))⊢ 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}) := 
  Exists.intro ↑(Fintype.card (Fin 5)) fun ⦃x⦄ a =>
    Exists.casesOn a fun M h =>
      And.casesOn h fun hM right =>
        right ▸
          id
            (have hb := matching_card_bound HouseGraph M hM;
            cast (Eq.symm Nat.cast_le._simp_1) (Decidable.byContradiction fun a => house_matching._proof_1 M hb a))⊢ (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 declaration uses 'sorry'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; 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; decide +nativeAll goals completed! 🐙


@[category test, AMS 5]
theorem K4_avg_dist : averageDistance K4 = 1 := by⊢ K4.averageDistance = 1
  rw [avg_dist_eq_computable, show computable_avg_dist K4 = (1 : ℚ) from by decide +native]⊢ ↑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 decide)]⊢ ↑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 decide)]⊢ ↑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⊢ K4.girth = 3 decideAll goals completed! 🐙)
      (Walk.cons (show K4.Adj 1 2 by⊢ K4.girth = 3 decideAll goals completed! 🐙)
      (Walk.cons (show K4.Adj 2 0 by⊢ K4.girth = 3 decideAll goals completed! 🐙) Walk.nil))).IsCycle := by⊢ K4.girth = 3
    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
    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.Nodup
    ·refine_1⊢ (Walk.cons ⋯ (Walk.cons ⋯ (Walk.cons ⋯ Walk.nil))).IsTrail rw [Walk.isTrail_def]refine_1⊢ (Walk.cons ⋯ (Walk.cons ⋯ (Walk.cons ⋯ Walk.nil))).edges.Nodup; decideAll goals completed! 🐙
    ·refine_2⊢ Walk.cons ⋯ (Walk.cons ⋯ (Walk.cons ⋯ Walk.nil)) ≠ Walk.nil simpAll goals completed! 🐙
    ·refine_3⊢ (Walk.cons ⋯ (Walk.cons ⋯ (Walk.cons ⋯ Walk.nil))).support.tail.Nodup decideAll goals completed! 🐙
  refine le_antisymm ?_ (three_le_girth (fun hac => hac _ hcyc))hcyc:(Walk.cons ⋯ (Walk.cons ⋯ (Walk.cons ⋯ Walk.nil))).IsCycle := 
  Eq.mpr
    (id
      (congrArg (fun _a => _a)
        (propext
          (Walk.isCycle_def
            (Walk.cons
              (have this := of_decide_eq_true (id (Eq.refl true));
              this)
              (Walk.cons
                (have this := of_decide_eq_true (id (Eq.refl true));
                this)
                (Walk.cons
                  (have this := of_decide_eq_true (id (Eq.refl true));
                  this)
                  Walk.nil)))))))
    ⟨Eq.mpr
        (id
          (congrArg (fun _a => _a)
            (propext
              (Walk.isTrail_def
                (Walk.cons
                  (have this := of_decide_eq_true (id (Eq.refl true));
                  this)
                  (Walk.cons
                    (have this := of_decide_eq_true (id (Eq.refl true));
                    this)
                    (Walk.cons
                      (have this := of_decide_eq_true (id (Eq.refl true));
                      this)
                      Walk.nil)))))))
        (of_decide_eq_true (id (Eq.refl true))),
      ⟨of_eq_true
          (Eq.trans (congrArg Not (eq_false' fun h => False.elim (noConfusion_of_Nat Walk.ctorIdx h))) not_false_eq_true),
        of_decide_eq_true (id (Eq.refl true))⟩⟩⊢ K4.girth ≤ 3
  simpa using girth_le_length hcycAll goals completed! 🐙


@[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
  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; 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; 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
  have hbdd : BddAbove (Set.image (fun M : Subgraph K4 => (M.edgeSet.toFinset.card : ℝ)) {M | M.IsMatching}) := by⊢ K4.matchingNumber = 2
    refine ⟨(Fintype.card (Fin 4) : ℝ), ?_⟩⊢ ↑(Fintype.card (Fin 4)) ∈ upperBounds ((fun M => ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})
    rintro x ⟨M, hM, rfl⟩M:K4.SubgraphhM:M ∈ {M | M.IsMatching}⊢ (fun M => ↑M.edgeSet.toFinset.card) M ≤ ↑(Fintype.card (Fin 4))
    show (M.edgeSet.toFinset.card : ℝ) ≤ Fintype.card (Fin 4)M:K4.SubgraphhM:M ∈ {M | M.IsMatching}⊢ ↑M.edgeSet.toFinset.card ≤ ↑(Fintype.card (Fin 4))
    have hb := matching_card_bound K4 M hMM:K4.SubgraphhM:M ∈ {M | M.IsMatching}hb:2 * M.edgeSet.toFinset.card ≤ Fintype.card (Fin 4) := matching_card_bound K4 M hM⊢ ↑M.edgeSet.toFinset.card ≤ ↑(Fintype.card (Fin 4))
    exact_mod_cast (byM:K4.SubgraphhM:M ∈ {M | M.IsMatching}hb:2 * M.edgeSet.toFinset.card ≤ Fintype.card (Fin 4) := matching_card_bound K4 M hM⊢ M.edgeSet.toFinset.card ≤ Fintype.card (Fin 4) omegaAll goals completed! 🐙 : M.edgeSet.toFinset.card ≤ Fintype.card (Fin 4))
  unfold matchingNumberhbdd:BddAbove ((fun M => ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching}) := 
  Exists.intro ↑(Fintype.card (Fin 4)) fun ⦃x⦄ a =>
    Exists.casesOn a fun M h =>
      And.casesOn h fun hM right =>
        right ▸
          id
            (have hb := matching_card_bound K4 M hM;
            cast (Eq.symm Nat.cast_le._simp_1) (Decidable.byContradiction fun a => K4_matching._proof_1 M hb a))⊢ (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}) := 
  Exists.intro ↑(Fintype.card (Fin 4)) fun ⦃x⦄ a =>
    Exists.casesOn a fun M h =>
      And.casesOn h fun hM right =>
        right ▸
          id
            (have hb := matching_card_bound K4 M hM;
            cast (Eq.symm Nat.cast_le._simp_1) (Decidable.byContradiction fun a => K4_matching._proof_1 M hb a))⊢ (have matchings := {M | M.IsMatching};
  sSup ((fun M => ↑M.edgeSet.toFinset.card) '' matchings)) ≤
  2ahbdd:BddAbove ((fun M => ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching}) := 
  Exists.intro ↑(Fintype.card (Fin 4)) fun ⦃x⦄ a =>
    Exists.casesOn a fun M h =>
      And.casesOn h fun hM right =>
        right ▸
          id
            (have hb := matching_card_bound K4 M hM;
            cast (Eq.symm Nat.cast_le._simp_1) (Decidable.byContradiction fun a => K4_matching._proof_1 M hb a))⊢ 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}) := 
  Exists.intro ↑(Fintype.card (Fin 4)) fun ⦃x⦄ a =>
    Exists.casesOn a fun M h =>
      And.casesOn h fun hM right =>
        right ▸
          id
            (have hb := matching_card_bound K4 M hM;
            cast (Eq.symm Nat.cast_le._simp_1) (Decidable.byContradiction fun a => K4_matching._proof_1 M hb a))⊢ (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}) := 
  Exists.intro ↑(Fintype.card (Fin 4)) fun ⦃x⦄ a =>
    Exists.casesOn a fun M h =>
      And.casesOn h fun hM right =>
        right ▸
          id
            (have hb := matching_card_bound K4 M hM;
            cast (Eq.symm Nat.cast_le._simp_1) (Decidable.byContradiction fun a => K4_matching._proof_1 M hb a))⊢ ⊥ ∈ {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}) := 
  Exists.intro ↑(Fintype.card (Fin 4)) fun ⦃x⦄ a =>
    Exists.casesOn a fun M h =>
      And.casesOn h fun hM right =>
        right ▸
          id
            (have hb := matching_card_bound K4 M hM;
            cast (Eq.symm Nat.cast_le._simp_1) (Decidable.byContradiction fun a => K4_matching._proof_1 M hb a))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}) := 
  Exists.intro ↑(Fintype.card (Fin 4)) fun ⦃x⦄ a =>
    Exists.casesOn a fun M h =>
      And.casesOn h fun hM right =>
        right ▸
          id
            (have hb := matching_card_bound K4 M hM;
            cast (Eq.symm Nat.cast_le._simp_1) (Decidable.byContradiction fun a => K4_matching._proof_1 M hb a))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}) := 
  Exists.intro ↑(Fintype.card (Fin 4)) fun ⦃x⦄ a =>
    Exists.casesOn a fun M h =>
      And.casesOn h fun hM right =>
        right ▸
          id
            (have hb := matching_card_bound K4 M hM;
            cast (Eq.symm Nat.cast_le._simp_1) (Decidable.byContradiction fun a => K4_matching._proof_1 M hb a))M:K4.SubgraphhM:M ∈ {M | M.IsMatching}hb:2 * M.edgeSet.toFinset.card ≤ Fintype.card (Fin 4) := matching_card_bound K4 M hM⊢ ↑M.edgeSet.toFinset.card ≤ 2
    simp only [Fintype.card_fin] at hbahbdd:BddAbove ((fun M => ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching}) := 
  Exists.intro ↑(Fintype.card (Fin 4)) fun ⦃x⦄ a =>
    Exists.casesOn a fun M h =>
      And.casesOn h fun hM right =>
        right ▸
          id
            (have hb := matching_card_bound K4 M hM;
            cast (Eq.symm Nat.cast_le._simp_1) (Decidable.byContradiction fun a => K4_matching._proof_1 M hb a))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}) := 
  Exists.intro ↑(Fintype.card (Fin 4)) fun ⦃x⦄ a =>
    Exists.casesOn a fun M h =>
      And.casesOn h fun hM right =>
        right ▸
          id
            (have hb := matching_card_bound K4 M hM;
            cast (Eq.symm Nat.cast_le._simp_1) (Decidable.byContradiction fun a => K4_matching._proof_1 M hb a))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}) := 
  Exists.intro ↑(Fintype.card (Fin 4)) fun ⦃x⦄ a =>
    Exists.casesOn a fun M h =>
      And.casesOn h fun hM right =>
        right ▸
          id
            (have hb := matching_card_bound K4 M hM;
            cast (Eq.symm Nat.cast_le._simp_1) (Decidable.byContradiction fun a => K4_matching._proof_1 M hb a))⊢ 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}) := 
  Exists.intro ↑(Fintype.card (Fin 4)) fun ⦃x⦄ a =>
    Exists.casesOn a fun M h =>
      And.casesOn h fun hM right =>
        right ▸
          id
            (have hb := matching_card_bound K4 M hM;
            cast (Eq.symm Nat.cast_le._simp_1) (Decidable.byContradiction fun a => K4_matching._proof_1 M hb a))⊢ 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}) := 
  Exists.intro ↑(Fintype.card (Fin 4)) fun ⦃x⦄ a =>
    Exists.casesOn a fun M h =>
      And.casesOn h fun hM right =>
        right ▸
          id
            (have hb := matching_card_bound K4 M hM;
            cast (Eq.symm Nat.cast_le._simp_1) (Decidable.byContradiction fun a => K4_matching._proof_1 M hb a))⊢ 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}) := 
  Exists.intro ↑(Fintype.card (Fin 4)) fun ⦃x⦄ a =>
    Exists.casesOn a fun M h =>
      And.casesOn h fun hM right =>
        right ▸
          id
            (have hb := matching_card_bound K4 M hM;
            cast (Eq.symm Nat.cast_le._simp_1) (Decidable.byContradiction fun a => K4_matching._proof_1 M hb a))⊢ Disjoint (K4.subgraphOfAdj ⋯).support (K4.subgraphOfAdj ⋯).support rw [support_subgraphOfAdj, support_subgraphOfAdj]hbdd:BddAbove ((fun M => ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching}) := 
  Exists.intro ↑(Fintype.card (Fin 4)) fun ⦃x⦄ a =>
    Exists.casesOn a fun M h =>
      And.casesOn h fun hM right =>
        right ▸
          id
            (have hb := matching_card_bound K4 M hM;
            cast (Eq.symm Nat.cast_le._simp_1) (Decidable.byContradiction fun a => K4_matching._proof_1 M hb a))⊢ 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}) := 
  Exists.intro ↑(Fintype.card (Fin 4)) fun ⦃x⦄ a =>
    Exists.casesOn a fun M h =>
      And.casesOn h fun hM right =>
        right ▸
          id
            (have hb := matching_card_bound K4 M hM;
            cast (Eq.symm Nat.cast_le._simp_1) (Decidable.byContradiction fun a => K4_matching._proof_1 M hb a))⊢ (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 declaration uses 'sorry'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; 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; 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, show computable_avg_dist PetersenGraph = (5 / 3 : ℚ) from by decide +native]⊢ ↑(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 decide)]⊢ ↑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 decide)]⊢ ↑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 declaration uses 'sorry'petersen_girth : PetersenGraph.girth = 5 := by⊢ PetersenGraph.girth = 5
  sorryAll goals completed! 🐙


@[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
  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; 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; 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
  have hbdd : BddAbove (Set.image (fun M : Subgraph PetersenGraph => (M.edgeSet.toFinset.card : ℝ)) {M | M.IsMatching}) := by⊢ PetersenGraph.matchingNumber = 5
    refine ⟨(Fintype.card (Fin 10) : ℝ), ?_⟩⊢ ↑(Fintype.card (Fin 10)) ∈ upperBounds ((fun M => ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})
    rintro x ⟨M, hM, rfl⟩M:PetersenGraph.SubgraphhM:M ∈ {M | M.IsMatching}⊢ (fun M => ↑M.edgeSet.toFinset.card) M ≤ ↑(Fintype.card (Fin 10))
    show (M.edgeSet.toFinset.card : ℝ) ≤ Fintype.card (Fin 10)M:PetersenGraph.SubgraphhM:M ∈ {M | M.IsMatching}⊢ ↑M.edgeSet.toFinset.card ≤ ↑(Fintype.card (Fin 10))
    have hb := matching_card_bound PetersenGraph M hMM:PetersenGraph.SubgraphhM:M ∈ {M | M.IsMatching}hb:2 * M.edgeSet.toFinset.card ≤ Fintype.card (Fin 10) := matching_card_bound PetersenGraph M hM⊢ ↑M.edgeSet.toFinset.card ≤ ↑(Fintype.card (Fin 10))
    exact_mod_cast (byM:PetersenGraph.SubgraphhM:M ∈ {M | M.IsMatching}hb:2 * M.edgeSet.toFinset.card ≤ Fintype.card (Fin 10) := matching_card_bound PetersenGraph M hM⊢ M.edgeSet.toFinset.card ≤ Fintype.card (Fin 10) omegaAll goals completed! 🐙 : M.edgeSet.toFinset.card ≤ Fintype.card (Fin 10))
  unfold matchingNumberhbdd:BddAbove ((fun M => ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching}) := 
  Exists.intro ↑(Fintype.card (Fin 10)) fun ⦃x⦄ a =>
    Exists.casesOn a fun M h =>
      And.casesOn h fun hM right =>
        right ▸
          id
            (have hb := matching_card_bound PetersenGraph M hM;
            cast (Eq.symm Nat.cast_le._simp_1) (Decidable.byContradiction fun a => petersen_matching._proof_1 M hb a))⊢ (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}) := 
  Exists.intro ↑(Fintype.card (Fin 10)) fun ⦃x⦄ a =>
    Exists.casesOn a fun M h =>
      And.casesOn h fun hM right =>
        right ▸
          id
            (have hb := matching_card_bound PetersenGraph M hM;
            cast (Eq.symm Nat.cast_le._simp_1) (Decidable.byContradiction fun a => petersen_matching._proof_1 M hb a))⊢ (have matchings := {M | M.IsMatching};
  sSup ((fun M => ↑M.edgeSet.toFinset.card) '' matchings)) ≤
  5ahbdd:BddAbove ((fun M => ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching}) := 
  Exists.intro ↑(Fintype.card (Fin 10)) fun ⦃x⦄ a =>
    Exists.casesOn a fun M h =>
      And.casesOn h fun hM right =>
        right ▸
          id
            (have hb := matching_card_bound PetersenGraph M hM;
            cast (Eq.symm Nat.cast_le._simp_1) (Decidable.byContradiction fun a => petersen_matching._proof_1 M hb a))⊢ 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}) := 
  Exists.intro ↑(Fintype.card (Fin 10)) fun ⦃x⦄ a =>
    Exists.casesOn a fun M h =>
      And.casesOn h fun hM right =>
        right ▸
          id
            (have hb := matching_card_bound PetersenGraph M hM;
            cast (Eq.symm Nat.cast_le._simp_1) (Decidable.byContradiction fun a => petersen_matching._proof_1 M hb a))⊢ (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}) := 
  Exists.intro ↑(Fintype.card (Fin 10)) fun ⦃x⦄ a =>
    Exists.casesOn a fun M h =>
      And.casesOn h fun hM right =>
        right ▸
          id
            (have hb := matching_card_bound PetersenGraph M hM;
            cast (Eq.symm Nat.cast_le._simp_1) (Decidable.byContradiction fun a => petersen_matching._proof_1 M hb a))⊢ ⊥ ∈ {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}) := 
  Exists.intro ↑(Fintype.card (Fin 10)) fun ⦃x⦄ a =>
    Exists.casesOn a fun M h =>
      And.casesOn h fun hM right =>
        right ▸
          id
            (have hb := matching_card_bound PetersenGraph M hM;
            cast (Eq.symm Nat.cast_le._simp_1) (Decidable.byContradiction fun a => petersen_matching._proof_1 M hb a))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}) := 
  Exists.intro ↑(Fintype.card (Fin 10)) fun ⦃x⦄ a =>
    Exists.casesOn a fun M h =>
      And.casesOn h fun hM right =>
        right ▸
          id
            (have hb := matching_card_bound PetersenGraph M hM;
            cast (Eq.symm Nat.cast_le._simp_1) (Decidable.byContradiction fun a => petersen_matching._proof_1 M hb a))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}) := 
  Exists.intro ↑(Fintype.card (Fin 10)) fun ⦃x⦄ a =>
    Exists.casesOn a fun M h =>
      And.casesOn h fun hM right =>
        right ▸
          id
            (have hb := matching_card_bound PetersenGraph M hM;
            cast (Eq.symm Nat.cast_le._simp_1) (Decidable.byContradiction fun a => petersen_matching._proof_1 M hb a))M:PetersenGraph.SubgraphhM:M ∈ {M | M.IsMatching}hb:2 * M.edgeSet.toFinset.card ≤ Fintype.card (Fin 10) := matching_card_bound PetersenGraph M hM⊢ ↑M.edgeSet.toFinset.card ≤ 5
    simp only [Fintype.card_fin] at hbahbdd:BddAbove ((fun M => ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching}) := 
  Exists.intro ↑(Fintype.card (Fin 10)) fun ⦃x⦄ a =>
    Exists.casesOn a fun M h =>
      And.casesOn h fun hM right =>
        right ▸
          id
            (have hb := matching_card_bound PetersenGraph M hM;
            cast (Eq.symm Nat.cast_le._simp_1) (Decidable.byContradiction fun a => petersen_matching._proof_1 M hb a))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}) := 
  Exists.intro ↑(Fintype.card (Fin 10)) fun ⦃x⦄ a =>
    Exists.casesOn a fun M h =>
      And.casesOn h fun hM right =>
        right ▸
          id
            (have hb := matching_card_bound PetersenGraph M hM;
            cast (Eq.symm Nat.cast_le._simp_1) (Decidable.byContradiction fun a => petersen_matching._proof_1 M hb a))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}) := 
  Exists.intro ↑(Fintype.card (Fin 10)) fun ⦃x⦄ a =>
    Exists.casesOn a fun M h =>
      And.casesOn h fun hM right =>
        right ▸
          id
            (have hb := matching_card_bound PetersenGraph M hM;
            cast (Eq.symm Nat.cast_le._simp_1) (Decidable.byContradiction fun a => petersen_matching._proof_1 M hb a))⊢ 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}) := 
  Exists.intro ↑(Fintype.card (Fin 10)) fun ⦃x⦄ a =>
    Exists.casesOn a fun M h =>
      And.casesOn h fun hM right =>
        right ▸
          id
            (have hb := matching_card_bound PetersenGraph M hM;
            cast (Eq.symm Nat.cast_le._simp_1) (Decidable.byContradiction fun a => petersen_matching._proof_1 M hb a))⊢ 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}) := 
  Exists.intro ↑(Fintype.card (Fin 10)) fun ⦃x⦄ a =>
    Exists.casesOn a fun M h =>
      And.casesOn h fun hM right =>
        right ▸
          id
            (have hb := matching_card_bound PetersenGraph M hM;
            cast (Eq.symm Nat.cast_le._simp_1) (Decidable.byContradiction fun a => petersen_matching._proof_1 M hb a))⊢ 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}) := 
  Exists.intro ↑(Fintype.card (Fin 10)) fun ⦃x⦄ a =>
    Exists.casesOn a fun M h =>
      And.casesOn h fun hM right =>
        right ▸
          id
            (have hb := matching_card_bound PetersenGraph M hM;
            cast (Eq.symm Nat.cast_le._simp_1) (Decidable.byContradiction fun a => petersen_matching._proof_1 M hb a))⊢ (PetersenGraph.subgraphOfAdj ⋯ ⊔ PetersenGraph.subgraphOfAdj ⋯ ⊔ PetersenGraph.subgraphOfAdj ⋯ ⊔
    PetersenGraph.subgraphOfAdj ⋯).IsMatchinga.refine_1.hM'hbdd:BddAbove ((fun M => ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching}) := 
  Exists.intro ↑(Fintype.card (Fin 10)) fun ⦃x⦄ a =>
    Exists.casesOn a fun M h =>
      And.casesOn h fun hM right =>
        right ▸
          id
            (have hb := matching_card_bound PetersenGraph M hM;
            cast (Eq.symm Nat.cast_le._simp_1) (Decidable.byContradiction fun a => petersen_matching._proof_1 M hb a))⊢ (PetersenGraph.subgraphOfAdj ⋯).IsMatchinga.refine_1.hdhbdd:BddAbove ((fun M => ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching}) := 
  Exists.intro ↑(Fintype.card (Fin 10)) fun ⦃x⦄ a =>
    Exists.casesOn a fun M h =>
      And.casesOn h fun hM right =>
        right ▸
          id
            (have hb := matching_card_bound PetersenGraph M hM;
            cast (Eq.symm Nat.cast_le._simp_1) (Decidable.byContradiction fun a => petersen_matching._proof_1 M hb a))⊢ 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}) := 
  Exists.intro ↑(Fintype.card (Fin 10)) fun ⦃x⦄ a =>
    Exists.casesOn a fun M h =>
      And.casesOn h fun hM right =>
        right ▸
          id
            (have hb := matching_card_bound PetersenGraph M hM;
            cast (Eq.symm Nat.cast_le._simp_1) (Decidable.byContradiction fun a => petersen_matching._proof_1 M hb a))⊢ (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}) := 
  Exists.intro ↑(Fintype.card (Fin 10)) fun ⦃x⦄ a =>
    Exists.casesOn a fun M h =>
      And.casesOn h fun hM right =>
        right ▸
          id
            (have hb := matching_card_bound PetersenGraph M hM;
            cast (Eq.symm Nat.cast_le._simp_1) (Decidable.byContradiction fun a => petersen_matching._proof_1 M hb a))⊢ (PetersenGraph.subgraphOfAdj ⋯ ⊔ PetersenGraph.subgraphOfAdj ⋯ ⊔ PetersenGraph.subgraphOfAdj ⋯).IsMatchinga.refine_1.hM.hM'hbdd:BddAbove ((fun M => ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching}) := 
  Exists.intro ↑(Fintype.card (Fin 10)) fun ⦃x⦄ a =>
    Exists.casesOn a fun M h =>
      And.casesOn h fun hM right =>
        right ▸
          id
            (have hb := matching_card_bound PetersenGraph M hM;
            cast (Eq.symm Nat.cast_le._simp_1) (Decidable.byContradiction fun a => petersen_matching._proof_1 M hb a))⊢ (PetersenGraph.subgraphOfAdj ⋯).IsMatchinga.refine_1.hM.hdhbdd:BddAbove ((fun M => ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching}) := 
  Exists.intro ↑(Fintype.card (Fin 10)) fun ⦃x⦄ a =>
    Exists.casesOn a fun M h =>
      And.casesOn h fun hM right =>
        right ▸
          id
            (have hb := matching_card_bound PetersenGraph M hM;
            cast (Eq.symm Nat.cast_le._simp_1) (Decidable.byContradiction fun a => petersen_matching._proof_1 M hb a))⊢ 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}) := 
  Exists.intro ↑(Fintype.card (Fin 10)) fun ⦃x⦄ a =>
    Exists.casesOn a fun M h =>
      And.casesOn h fun hM right =>
        right ▸
          id
            (have hb := matching_card_bound PetersenGraph M hM;
            cast (Eq.symm Nat.cast_le._simp_1) (Decidable.byContradiction fun a => petersen_matching._proof_1 M hb a))⊢ (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}) := 
  Exists.intro ↑(Fintype.card (Fin 10)) fun ⦃x⦄ a =>
    Exists.casesOn a fun M h =>
      And.casesOn h fun hM right =>
        right ▸
          id
            (have hb := matching_card_bound PetersenGraph M hM;
            cast (Eq.symm Nat.cast_le._simp_1) (Decidable.byContradiction fun a => petersen_matching._proof_1 M hb a))⊢ (PetersenGraph.subgraphOfAdj ⋯ ⊔ PetersenGraph.subgraphOfAdj ⋯).IsMatchinga.refine_1.hM.hM.hM'hbdd:BddAbove ((fun M => ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching}) := 
  Exists.intro ↑(Fintype.card (Fin 10)) fun ⦃x⦄ a =>
    Exists.casesOn a fun M h =>
      And.casesOn h fun hM right =>
        right ▸
          id
            (have hb := matching_card_bound PetersenGraph M hM;
            cast (Eq.symm Nat.cast_le._simp_1) (Decidable.byContradiction fun a => petersen_matching._proof_1 M hb a))⊢ (PetersenGraph.subgraphOfAdj ⋯).IsMatchinga.refine_1.hM.hM.hdhbdd:BddAbove ((fun M => ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching}) := 
  Exists.intro ↑(Fintype.card (Fin 10)) fun ⦃x⦄ a =>
    Exists.casesOn a fun M h =>
      And.casesOn h fun hM right =>
        right ▸
          id
            (have hb := matching_card_bound PetersenGraph M hM;
            cast (Eq.symm Nat.cast_le._simp_1) (Decidable.byContradiction fun a => petersen_matching._proof_1 M hb a))⊢ 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}) := 
  Exists.intro ↑(Fintype.card (Fin 10)) fun ⦃x⦄ a =>
    Exists.casesOn a fun M h =>
      And.casesOn h fun hM right =>
        right ▸
          id
            (have hb := matching_card_bound PetersenGraph M hM;
            cast (Eq.symm Nat.cast_le._simp_1) (Decidable.byContradiction fun a => petersen_matching._proof_1 M hb a))⊢ (PetersenGraph.subgraphOfAdj ⋯ ⊔ PetersenGraph.subgraphOfAdj ⋯).IsMatching exact (Subgraph.IsMatching.subgraphOfAdj _).sup (Subgraph.IsMatching.subgraphOfAdj _)
              (byhbdd:BddAbove ((fun M => ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching}) := 
  Exists.intro ↑(Fintype.card (Fin 10)) fun ⦃x⦄ a =>
    Exists.casesOn a fun M h =>
      And.casesOn h fun hM right =>
        right ▸
          id
            (have hb := matching_card_bound PetersenGraph M hM;
            cast (Eq.symm Nat.cast_le._simp_1) (Decidable.byContradiction fun a => petersen_matching._proof_1 M hb a))⊢ Disjoint (PetersenGraph.subgraphOfAdj ⋯).support (PetersenGraph.subgraphOfAdj ⋯).support rw [support_subgraphOfAdj, support_subgraphOfAdj]hbdd:BddAbove ((fun M => ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching}) := 
  Exists.intro ↑(Fintype.card (Fin 10)) fun ⦃x⦄ a =>
    Exists.casesOn a fun M h =>
      And.casesOn h fun hM right =>
        right ▸
          id
            (have hb := matching_card_bound PetersenGraph M hM;
            cast (Eq.symm Nat.cast_le._simp_1) (Decidable.byContradiction fun a => petersen_matching._proof_1 M hb a))⊢ 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}) := 
  Exists.intro ↑(Fintype.card (Fin 10)) fun ⦃x⦄ a =>
    Exists.casesOn a fun M h =>
      And.casesOn h fun hM right =>
        right ▸
          id
            (have hb := matching_card_bound PetersenGraph M hM;
            cast (Eq.symm Nat.cast_le._simp_1) (Decidable.byContradiction fun a => petersen_matching._proof_1 M hb a))⊢ (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}) := 
  Exists.intro ↑(Fintype.card (Fin 10)) fun ⦃x⦄ a =>
    Exists.casesOn a fun M h =>
      And.casesOn h fun hM right =>
        right ▸
          id
            (have hb := matching_card_bound PetersenGraph M hM;
            cast (Eq.symm Nat.cast_le._simp_1) (Decidable.byContradiction fun a => petersen_matching._proof_1 M hb a))⊢ 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}) := 
  Exists.intro ↑(Fintype.card (Fin 10)) fun ⦃x⦄ a =>
    Exists.casesOn a fun M h =>
      And.casesOn h fun hM right =>
        right ▸
          id
            (have hb := matching_card_bound PetersenGraph M hM;
            cast (Eq.symm Nat.cast_le._simp_1) (Decidable.byContradiction fun a => petersen_matching._proof_1 M hb a))⊢ 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}) := 
  Exists.intro ↑(Fintype.card (Fin 10)) fun ⦃x⦄ a =>
    Exists.casesOn a fun M h =>
      And.casesOn h fun hM right =>
        right ▸
          id
            (have hb := matching_card_bound PetersenGraph M hM;
            cast (Eq.symm Nat.cast_le._simp_1) (Decidable.byContradiction fun a => petersen_matching._proof_1 M hb a))⊢ (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}) := 
  Exists.intro ↑(Fintype.card (Fin 10)) fun ⦃x⦄ a =>
    Exists.casesOn a fun M h =>
      And.casesOn h fun hM right =>
        right ▸
          id
            (have hb := matching_card_bound PetersenGraph M hM;
            cast (Eq.symm Nat.cast_le._simp_1) (Decidable.byContradiction fun a => petersen_matching._proof_1 M hb a))⊢ 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}) := 
  Exists.intro ↑(Fintype.card (Fin 10)) fun ⦃x⦄ a =>
    Exists.casesOn a fun M h =>
      And.casesOn h fun hM right =>
        right ▸
          id
            (have hb := matching_card_bound PetersenGraph M hM;
            cast (Eq.symm Nat.cast_le._simp_1) (Decidable.byContradiction fun a => petersen_matching._proof_1 M hb a))⊢ 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}) := 
  Exists.intro ↑(Fintype.card (Fin 10)) fun ⦃x⦄ a =>
    Exists.casesOn a fun M h =>
      And.casesOn h fun hM right =>
        right ▸
          id
            (have hb := matching_card_bound PetersenGraph M hM;
            cast (Eq.symm Nat.cast_le._simp_1) (Decidable.byContradiction fun a => petersen_matching._proof_1 M hb a))⊢ (PetersenGraph.subgraphOfAdj ⋯).IsMatching exact Subgraph.IsMatching.subgraphOfAdj _All goals completed! 🐙
      ·a.refine_1.hdhbdd:BddAbove ((fun M => ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching}) := 
  Exists.intro ↑(Fintype.card (Fin 10)) fun ⦃x⦄ a =>
    Exists.casesOn a fun M h =>
      And.casesOn h fun hM right =>
        right ▸
          id
            (have hb := matching_card_bound PetersenGraph M hM;
            cast (Eq.symm Nat.cast_le._simp_1) (Decidable.byContradiction fun a => petersen_matching._proof_1 M hb a))⊢ 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}) := 
  Exists.intro ↑(Fintype.card (Fin 10)) fun ⦃x⦄ a =>
    Exists.casesOn a fun M h =>
      And.casesOn h fun hM right =>
        right ▸
          id
            (have hb := matching_card_bound PetersenGraph M hM;
            cast (Eq.symm Nat.cast_le._simp_1) (Decidable.byContradiction fun a => petersen_matching._proof_1 M hb a))⊢ 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}) := 
  Exists.intro ↑(Fintype.card (Fin 10)) fun ⦃x⦄ a =>
    Exists.casesOn a fun M h =>
      And.casesOn h fun hM right =>
        right ▸
          id
            (have hb := matching_card_bound PetersenGraph M hM;
            cast (Eq.symm Nat.cast_le._simp_1) (Decidable.byContradiction fun a => petersen_matching._proof_1 M hb a))⊢ (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 declaration uses 'sorry'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; 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; 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, show computable_avg_dist C6 = (9 / 5 : ℚ) from by decide +native]⊢ ↑(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 decide)]⊢ ↑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 decide)]⊢ ↑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 declaration uses 'sorry'C6_girth : C6.girth = 6 := by⊢ C6.girth = 6
  sorryAll goals completed! 🐙


@[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
  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; 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; 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
  have hbdd : BddAbove (Set.image (fun M : Subgraph C6 => (M.edgeSet.toFinset.card : ℝ)) {M | M.IsMatching}) := by⊢ C6.matchingNumber = 3
    refine ⟨(Fintype.card (Fin 6) : ℝ), ?_⟩⊢ ↑(Fintype.card (Fin 6)) ∈ upperBounds ((fun M => ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})
    rintro x ⟨M, hM, rfl⟩M:C6.SubgraphhM:M ∈ {M | M.IsMatching}⊢ (fun M => ↑M.edgeSet.toFinset.card) M ≤ ↑(Fintype.card (Fin 6))
    show (M.edgeSet.toFinset.card : ℝ) ≤ Fintype.card (Fin 6)M:C6.SubgraphhM:M ∈ {M | M.IsMatching}⊢ ↑M.edgeSet.toFinset.card ≤ ↑(Fintype.card (Fin 6))
    have hb := matching_card_bound C6 M hMM:C6.SubgraphhM:M ∈ {M | M.IsMatching}hb:2 * M.edgeSet.toFinset.card ≤ Fintype.card (Fin 6) := matching_card_bound C6 M hM⊢ ↑M.edgeSet.toFinset.card ≤ ↑(Fintype.card (Fin 6))
    exact_mod_cast (byM:C6.SubgraphhM:M ∈ {M | M.IsMatching}hb:2 * M.edgeSet.toFinset.card ≤ Fintype.card (Fin 6) := matching_card_bound C6 M hM⊢ M.edgeSet.toFinset.card ≤ Fintype.card (Fin 6) omegaAll goals completed! 🐙 : M.edgeSet.toFinset.card ≤ Fintype.card (Fin 6))
  unfold matchingNumberhbdd:BddAbove ((fun M => ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching}) := 
  Exists.intro ↑(Fintype.card (Fin 6)) fun ⦃x⦄ a =>
    Exists.casesOn a fun M h =>
      And.casesOn h fun hM right =>
        right ▸
          id
            (have hb := matching_card_bound C6 M hM;
            cast (Eq.symm Nat.cast_le._simp_1) (Decidable.byContradiction fun a => C6_matching._proof_1 M hb a))⊢ (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}) := 
  Exists.intro ↑(Fintype.card (Fin 6)) fun ⦃x⦄ a =>
    Exists.casesOn a fun M h =>
      And.casesOn h fun hM right =>
        right ▸
          id
            (have hb := matching_card_bound C6 M hM;
            cast (Eq.symm Nat.cast_le._simp_1) (Decidable.byContradiction fun a => C6_matching._proof_1 M hb a))⊢ (have matchings := {M | M.IsMatching};
  sSup ((fun M => ↑M.edgeSet.toFinset.card) '' matchings)) ≤
  3ahbdd:BddAbove ((fun M => ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching}) := 
  Exists.intro ↑(Fintype.card (Fin 6)) fun ⦃x⦄ a =>
    Exists.casesOn a fun M h =>
      And.casesOn h fun hM right =>
        right ▸
          id
            (have hb := matching_card_bound C6 M hM;
            cast (Eq.symm Nat.cast_le._simp_1) (Decidable.byContradiction fun a => C6_matching._proof_1 M hb a))⊢ 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}) := 
  Exists.intro ↑(Fintype.card (Fin 6)) fun ⦃x⦄ a =>
    Exists.casesOn a fun M h =>
      And.casesOn h fun hM right =>
        right ▸
          id
            (have hb := matching_card_bound C6 M hM;
            cast (Eq.symm Nat.cast_le._simp_1) (Decidable.byContradiction fun a => C6_matching._proof_1 M hb a))⊢ (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}) := 
  Exists.intro ↑(Fintype.card (Fin 6)) fun ⦃x⦄ a =>
    Exists.casesOn a fun M h =>
      And.casesOn h fun hM right =>
        right ▸
          id
            (have hb := matching_card_bound C6 M hM;
            cast (Eq.symm Nat.cast_le._simp_1) (Decidable.byContradiction fun a => C6_matching._proof_1 M hb a))⊢ ⊥ ∈ {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}) := 
  Exists.intro ↑(Fintype.card (Fin 6)) fun ⦃x⦄ a =>
    Exists.casesOn a fun M h =>
      And.casesOn h fun hM right =>
        right ▸
          id
            (have hb := matching_card_bound C6 M hM;
            cast (Eq.symm Nat.cast_le._simp_1) (Decidable.byContradiction fun a => C6_matching._proof_1 M hb a))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}) := 
  Exists.intro ↑(Fintype.card (Fin 6)) fun ⦃x⦄ a =>
    Exists.casesOn a fun M h =>
      And.casesOn h fun hM right =>
        right ▸
          id
            (have hb := matching_card_bound C6 M hM;
            cast (Eq.symm Nat.cast_le._simp_1) (Decidable.byContradiction fun a => C6_matching._proof_1 M hb a))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}) := 
  Exists.intro ↑(Fintype.card (Fin 6)) fun ⦃x⦄ a =>
    Exists.casesOn a fun M h =>
      And.casesOn h fun hM right =>
        right ▸
          id
            (have hb := matching_card_bound C6 M hM;
            cast (Eq.symm Nat.cast_le._simp_1) (Decidable.byContradiction fun a => C6_matching._proof_1 M hb a))M:C6.SubgraphhM:M ∈ {M | M.IsMatching}hb:2 * M.edgeSet.toFinset.card ≤ Fintype.card (Fin 6) := matching_card_bound C6 M hM⊢ ↑M.edgeSet.toFinset.card ≤ 3
    simp only [Fintype.card_fin] at hbahbdd:BddAbove ((fun M => ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching}) := 
  Exists.intro ↑(Fintype.card (Fin 6)) fun ⦃x⦄ a =>
    Exists.casesOn a fun M h =>
      And.casesOn h fun hM right =>
        right ▸
          id
            (have hb := matching_card_bound C6 M hM;
            cast (Eq.symm Nat.cast_le._simp_1) (Decidable.byContradiction fun a => C6_matching._proof_1 M hb a))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}) := 
  Exists.intro ↑(Fintype.card (Fin 6)) fun ⦃x⦄ a =>
    Exists.casesOn a fun M h =>
      And.casesOn h fun hM right =>
        right ▸
          id
            (have hb := matching_card_bound C6 M hM;
            cast (Eq.symm Nat.cast_le._simp_1) (Decidable.byContradiction fun a => C6_matching._proof_1 M hb a))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}) := 
  Exists.intro ↑(Fintype.card (Fin 6)) fun ⦃x⦄ a =>
    Exists.casesOn a fun M h =>
      And.casesOn h fun hM right =>
        right ▸
          id
            (have hb := matching_card_bound C6 M hM;
            cast (Eq.symm Nat.cast_le._simp_1) (Decidable.byContradiction fun a => C6_matching._proof_1 M hb a))⊢ 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}) := 
  Exists.intro ↑(Fintype.card (Fin 6)) fun ⦃x⦄ a =>
    Exists.casesOn a fun M h =>
      And.casesOn h fun hM right =>
        right ▸
          id
            (have hb := matching_card_bound C6 M hM;
            cast (Eq.symm Nat.cast_le._simp_1) (Decidable.byContradiction fun a => C6_matching._proof_1 M hb a))⊢ 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}) := 
  Exists.intro ↑(Fintype.card (Fin 6)) fun ⦃x⦄ a =>
    Exists.casesOn a fun M h =>
      And.casesOn h fun hM right =>
        right ▸
          id
            (have hb := matching_card_bound C6 M hM;
            cast (Eq.symm Nat.cast_le._simp_1) (Decidable.byContradiction fun a => C6_matching._proof_1 M hb a))⊢ 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}) := 
  Exists.intro ↑(Fintype.card (Fin 6)) fun ⦃x⦄ a =>
    Exists.casesOn a fun M h =>
      And.casesOn h fun hM right =>
        right ▸
          id
            (have hb := matching_card_bound C6 M hM;
            cast (Eq.symm Nat.cast_le._simp_1) (Decidable.byContradiction fun a => C6_matching._proof_1 M hb a))⊢ (C6.subgraphOfAdj ⋯ ⊔ C6.subgraphOfAdj ⋯).IsMatchinga.refine_1.hM'hbdd:BddAbove ((fun M => ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching}) := 
  Exists.intro ↑(Fintype.card (Fin 6)) fun ⦃x⦄ a =>
    Exists.casesOn a fun M h =>
      And.casesOn h fun hM right =>
        right ▸
          id
            (have hb := matching_card_bound C6 M hM;
            cast (Eq.symm Nat.cast_le._simp_1) (Decidable.byContradiction fun a => C6_matching._proof_1 M hb a))⊢ (C6.subgraphOfAdj ⋯).IsMatchinga.refine_1.hdhbdd:BddAbove ((fun M => ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching}) := 
  Exists.intro ↑(Fintype.card (Fin 6)) fun ⦃x⦄ a =>
    Exists.casesOn a fun M h =>
      And.casesOn h fun hM right =>
        right ▸
          id
            (have hb := matching_card_bound C6 M hM;
            cast (Eq.symm Nat.cast_le._simp_1) (Decidable.byContradiction fun a => C6_matching._proof_1 M hb a))⊢ Disjoint (C6.subgraphOfAdj ⋯ ⊔ C6.subgraphOfAdj ⋯).support (C6.subgraphOfAdj ⋯).support
      ·a.refine_1.hMhbdd:BddAbove ((fun M => ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching}) := 
  Exists.intro ↑(Fintype.card (Fin 6)) fun ⦃x⦄ a =>
    Exists.casesOn a fun M h =>
      And.casesOn h fun hM right =>
        right ▸
          id
            (have hb := matching_card_bound C6 M hM;
            cast (Eq.symm Nat.cast_le._simp_1) (Decidable.byContradiction fun a => C6_matching._proof_1 M hb a))⊢ (C6.subgraphOfAdj ⋯ ⊔ C6.subgraphOfAdj ⋯).IsMatching exact (Subgraph.IsMatching.subgraphOfAdj _).sup (Subgraph.IsMatching.subgraphOfAdj _)
          (byhbdd:BddAbove ((fun M => ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching}) := 
  Exists.intro ↑(Fintype.card (Fin 6)) fun ⦃x⦄ a =>
    Exists.casesOn a fun M h =>
      And.casesOn h fun hM right =>
        right ▸
          id
            (have hb := matching_card_bound C6 M hM;
            cast (Eq.symm Nat.cast_le._simp_1) (Decidable.byContradiction fun a => C6_matching._proof_1 M hb a))⊢ Disjoint (C6.subgraphOfAdj ⋯).support (C6.subgraphOfAdj ⋯).support rw [support_subgraphOfAdj, support_subgraphOfAdj]hbdd:BddAbove ((fun M => ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching}) := 
  Exists.intro ↑(Fintype.card (Fin 6)) fun ⦃x⦄ a =>
    Exists.casesOn a fun M h =>
      And.casesOn h fun hM right =>
        right ▸
          id
            (have hb := matching_card_bound C6 M hM;
            cast (Eq.symm Nat.cast_le._simp_1) (Decidable.byContradiction fun a => C6_matching._proof_1 M hb a))⊢ 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}) := 
  Exists.intro ↑(Fintype.card (Fin 6)) fun ⦃x⦄ a =>
    Exists.casesOn a fun M h =>
      And.casesOn h fun hM right =>
        right ▸
          id
            (have hb := matching_card_bound C6 M hM;
            cast (Eq.symm Nat.cast_le._simp_1) (Decidable.byContradiction fun a => C6_matching._proof_1 M hb a))⊢ (C6.subgraphOfAdj ⋯).IsMatching exact Subgraph.IsMatching.subgraphOfAdj _All goals completed! 🐙
      ·a.refine_1.hdhbdd:BddAbove ((fun M => ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching}) := 
  Exists.intro ↑(Fintype.card (Fin 6)) fun ⦃x⦄ a =>
    Exists.casesOn a fun M h =>
      And.casesOn h fun hM right =>
        right ▸
          id
            (have hb := matching_card_bound C6 M hM;
            cast (Eq.symm Nat.cast_le._simp_1) (Decidable.byContradiction fun a => C6_matching._proof_1 M hb a))⊢ 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}) := 
  Exists.intro ↑(Fintype.card (Fin 6)) fun ⦃x⦄ a =>
    Exists.casesOn a fun M h =>
      And.casesOn h fun hM right =>
        right ▸
          id
            (have hb := matching_card_bound C6 M hM;
            cast (Eq.symm Nat.cast_le._simp_1) (Decidable.byContradiction fun a => C6_matching._proof_1 M hb a))⊢ 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}) := 
  Exists.intro ↑(Fintype.card (Fin 6)) fun ⦃x⦄ a =>
    Exists.casesOn a fun M h =>
      And.casesOn h fun hM right =>
        right ▸
          id
            (have hb := matching_card_bound C6 M hM;
            cast (Eq.symm Nat.cast_le._simp_1) (Decidable.byContradiction fun a => C6_matching._proof_1 M hb a))⊢ (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 declaration uses 'sorry'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; 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; 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, show computable_avg_dist Star5 = (5 / 3 : ℚ) from by decide +native]⊢ ↑(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 decide)]⊢ ↑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 decide)]⊢ ↑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
  have key : ∀ (b : Fin 5) (c : Star5.Walk (Sum.inr b) (Sum.inr b)), ¬ c.IsCycle := by⊢ Star5.egirth = ⊤
    intro b cb:Fin 5c:Star5.Walk (Sum.inr b) (Sum.inr b)⊢ ¬c.IsCycle hcb:Fin 5c:Star5.Walk (Sum.inr b) (Sum.inr b)hc:c.IsCycle⊢ False
    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 := Walk.adj_snd (Walk.IsCycle.not_nil hc)⊢ False
    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.snd := Walk.adj_snd (Walk.IsCycle.not_nil hc)h2:Star5.Adj c.penultimate (Sum.inr b) := Walk.adj_penultimate (Walk.IsCycle.not_nil hc)⊢ False
    have hs : c.snd.isLeft := by⊢ Star5.egirth = ⊤
      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) := Walk.adj_penultimate (Walk.IsCycle.not_nil hc)h1:false = true ∧ c.snd.isRight = true ∨ True ∧ c.snd.isLeft = true⊢ c.snd.isLeft = true
      tautoAll goals completed! 🐙
    have hp : c.penultimate.isLeft := by⊢ Star5.egirth = ⊤
      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.snd := Walk.adj_snd (Walk.IsCycle.not_nil hc)hs:c.snd.isLeft = true := 
  Or.casesOn (Eq.mp (congrArg (fun x => false = true ∧ c.snd.isRight = true ∨ x ∧ c.snd.isLeft = true) (eq_self true)) h1)
    (fun h => And.casesOn h fun left right => False.elim (noConfusion_of_Nat Bool.ctorIdx left)) fun h =>
    And.casesOn h fun left right => righth2:c.penultimate.isLeft = true ∧ True ∨ c.penultimate.isRight = true ∧ false = true⊢ c.penultimate.isLeft = true
      tautoAll goals completed! 🐙
    apply hc.snd_ne_penultimateb:Fin 5c:Star5.Walk (Sum.inr b) (Sum.inr b)hc:c.IsCycleh1:Star5.Adj (Sum.inr b) c.snd := Walk.adj_snd (Walk.IsCycle.not_nil hc)h2:Star5.Adj c.penultimate (Sum.inr b) := Walk.adj_penultimate (Walk.IsCycle.not_nil hc)hs:c.snd.isLeft = true := 
  Or.casesOn (Eq.mp (congrArg (fun x => false = true ∧ c.snd.isRight = true ∨ x ∧ c.snd.isLeft = true) (eq_self true)) h1)
    (fun h => And.casesOn h fun left right => False.elim (noConfusion_of_Nat Bool.ctorIdx left)) fun h =>
    And.casesOn h fun left right => righthp:c.penultimate.isLeft = true := 
  Or.casesOn
    (Eq.mp
      (congrArg (fun x => c.penultimate.isLeft = true ∧ x ∨ c.penultimate.isRight = true ∧ false = true) (eq_self true))
      h2)
    (fun h => And.casesOn h fun left right => left) fun h =>
    And.casesOn h fun left right => False.elim (noConfusion_of_Nat Bool.ctorIdx right)⊢ c.snd = c.penultimate
    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.snd := Walk.adj_snd (Walk.IsCycle.not_nil hc)h2:Star5.Adj c.penultimate (Sum.inr b) := Walk.adj_penultimate (Walk.IsCycle.not_nil hc)hs:c.snd.isLeft = true := 
  Or.casesOn (Eq.mp (congrArg (fun x => false = true ∧ c.snd.isRight = true ∨ x ∧ c.snd.isLeft = true) (eq_self true)) h1)
    (fun h => And.casesOn h fun left right => False.elim (noConfusion_of_Nat Bool.ctorIdx left)) fun h =>
    And.casesOn h fun left right => righthp:c.penultimate.isLeft = true := 
  Or.casesOn
    (Eq.mp
      (congrArg (fun x => c.penultimate.isLeft = true ∧ x ∨ c.penultimate.isRight = true ∧ false = true) (eq_self true))
      h2)
    (fun h => And.casesOn h fun left right => left) fun h =>
    And.casesOn h fun left right => False.elim (noConfusion_of_Nat Bool.ctorIdx right)x:Fin 1hx:c.snd = Sum.inl x⊢ c.snd = c.penultimate
    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.snd := Walk.adj_snd (Walk.IsCycle.not_nil hc)h2:Star5.Adj c.penultimate (Sum.inr b) := Walk.adj_penultimate (Walk.IsCycle.not_nil hc)hs:c.snd.isLeft = true := 
  Or.casesOn (Eq.mp (congrArg (fun x => false = true ∧ c.snd.isRight = true ∨ x ∧ c.snd.isLeft = true) (eq_self true)) h1)
    (fun h => And.casesOn h fun left right => False.elim (noConfusion_of_Nat Bool.ctorIdx left)) fun h =>
    And.casesOn h fun left right => righthp:c.penultimate.isLeft = true := 
  Or.casesOn
    (Eq.mp
      (congrArg (fun x => c.penultimate.isLeft = true ∧ x ∨ c.penultimate.isRight = true ∧ false = true) (eq_self true))
      h2)
    (fun h => And.casesOn h fun left right => left) fun h =>
    And.casesOn h fun left right => False.elim (noConfusion_of_Nat Bool.ctorIdx right)x:Fin 1hx:c.snd = Sum.inl xy:Fin 1hy:c.penultimate = Sum.inl y⊢ c.snd = c.penultimate
    rw [hx, hy, Subsingleton.elim x y]All goals completed! 🐙
  intro v ckey:∀ (b : Fin 5) (c : Star5.Walk (Sum.inr b) (Sum.inr b)), ¬c.IsCycle := 
  fun b c hc =>
    have h1 := Walk.adj_snd (Walk.IsCycle.not_nil hc);
    have h2 := Walk.adj_penultimate (Walk.IsCycle.not_nil hc);
    have hs :=
      Or.casesOn
        (Eq.mp (congrArg (fun x => false = true ∧ c.snd.isRight = true ∨ x ∧ c.snd.isLeft = true) (eq_self true)) h1)
        (fun h => And.casesOn h fun left right => False.elim (noConfusion_of_Nat Bool.ctorIdx left)) fun h =>
        And.casesOn h fun left right => right;
    have hp :=
      Or.casesOn
        (Eq.mp
          (congrArg (fun x => c.penultimate.isLeft = true ∧ x ∨ c.penultimate.isRight = true ∧ false = true)
            (eq_self true))
          h2)
        (fun h => And.casesOn h fun left right => left) fun h =>
        And.casesOn h fun left right => False.elim (noConfusion_of_Nat Bool.ctorIdx right);
    Walk.IsCycle.snd_ne_penultimate hc
      (Exists.casesOn (Sum.isLeft_iff.mp hs) fun x hx =>
        Exists.casesOn (Sum.isLeft_iff.mp hp) fun y hy =>
          Eq.mpr (id (congrArg (fun _a => _a = c.penultimate) hx))
            (Eq.mpr (id (congrArg (fun _a => Sum.inl x = _a) hy))
              (Eq.mpr (id (congrArg (fun _a => Sum.inl _a = Sum.inl y) (Subsingleton.elim x y))) (Eq.refl (Sum.inl y)))))v:Fin 1 ⊕ Fin 5c:Star5.Walk v v⊢ ¬c.IsCycle hckey:∀ (b : Fin 5) (c : Star5.Walk (Sum.inr b) (Sum.inr b)), ¬c.IsCycle := 
  fun b c hc =>
    have h1 := Walk.adj_snd (Walk.IsCycle.not_nil hc);
    have h2 := Walk.adj_penultimate (Walk.IsCycle.not_nil hc);
    have hs :=
      Or.casesOn
        (Eq.mp (congrArg (fun x => false = true ∧ c.snd.isRight = true ∨ x ∧ c.snd.isLeft = true) (eq_self true)) h1)
        (fun h => And.casesOn h fun left right => False.elim (noConfusion_of_Nat Bool.ctorIdx left)) fun h =>
        And.casesOn h fun left right => right;
    have hp :=
      Or.casesOn
        (Eq.mp
          (congrArg (fun x => c.penultimate.isLeft = true ∧ x ∨ c.penultimate.isRight = true ∧ false = true)
            (eq_self true))
          h2)
        (fun h => And.casesOn h fun left right => left) fun h =>
        And.casesOn h fun left right => False.elim (noConfusion_of_Nat Bool.ctorIdx right);
    Walk.IsCycle.snd_ne_penultimate hc
      (Exists.casesOn (Sum.isLeft_iff.mp hs) fun x hx =>
        Exists.casesOn (Sum.isLeft_iff.mp hp) fun y hy =>
          Eq.mpr (id (congrArg (fun _a => _a = c.penultimate) hx))
            (Eq.mpr (id (congrArg (fun _a => Sum.inl x = _a) hy))
              (Eq.mpr (id (congrArg (fun _a => Sum.inl _a = Sum.inl y) (Subsingleton.elim x y))) (Eq.refl (Sum.inl y)))))v: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.IsCycle := 
  fun b c hc =>
    have h1 := Walk.adj_snd (Walk.IsCycle.not_nil hc);
    have h2 := Walk.adj_penultimate (Walk.IsCycle.not_nil hc);
    have hs :=
      Or.casesOn
        (Eq.mp (congrArg (fun x => false = true ∧ c.snd.isRight = true ∨ x ∧ c.snd.isLeft = true) (eq_self true)) h1)
        (fun h => And.casesOn h fun left right => False.elim (noConfusion_of_Nat Bool.ctorIdx left)) fun h =>
        And.casesOn h fun left right => right;
    have hp :=
      Or.casesOn
        (Eq.mp
          (congrArg (fun x => c.penultimate.isLeft = true ∧ x ∨ c.penultimate.isRight = true ∧ false = true)
            (eq_self true))
          h2)
        (fun h => And.casesOn h fun left right => left) fun h =>
        And.casesOn h fun left right => False.elim (noConfusion_of_Nat Bool.ctorIdx right);
    Walk.IsCycle.snd_ne_penultimate hc
      (Exists.casesOn (Sum.isLeft_iff.mp hs) fun x hx =>
        Exists.casesOn (Sum.isLeft_iff.mp hp) fun y hy =>
          Eq.mpr (id (congrArg (fun _a => _a = c.penultimate) hx))
            (Eq.mpr (id (congrArg (fun _a => Sum.inl x = _a) hy))
              (Eq.mpr (id (congrArg (fun _a => Sum.inl _a = Sum.inl y) (Subsingleton.elim x y))) (Eq.refl (Sum.inl y)))))b: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.IsCycle := 
  fun b c hc =>
    have h1 := Walk.adj_snd (Walk.IsCycle.not_nil hc);
    have h2 := Walk.adj_penultimate (Walk.IsCycle.not_nil hc);
    have hs :=
      Or.casesOn
        (Eq.mp (congrArg (fun x => false = true ∧ c.snd.isRight = true ∨ x ∧ c.snd.isLeft = true) (eq_self true)) h1)
        (fun h => And.casesOn h fun left right => False.elim (noConfusion_of_Nat Bool.ctorIdx left)) fun h =>
        And.casesOn h fun left right => right;
    have hp :=
      Or.casesOn
        (Eq.mp
          (congrArg (fun x => c.penultimate.isLeft = true ∧ x ∨ c.penultimate.isRight = true ∧ false = true)
            (eq_self true))
          h2)
        (fun h => And.casesOn h fun left right => left) fun h =>
        And.casesOn h fun left right => False.elim (noConfusion_of_Nat Bool.ctorIdx right);
    Walk.IsCycle.snd_ne_penultimate hc
      (Exists.casesOn (Sum.isLeft_iff.mp hs) fun x hx =>
        Exists.casesOn (Sum.isLeft_iff.mp hp) fun y hy =>
          Eq.mpr (id (congrArg (fun _a => _a = c.penultimate) hx))
            (Eq.mpr (id (congrArg (fun _a => Sum.inl x = _a) hy))
              (Eq.mpr (id (congrArg (fun _a => Sum.inl _a = Sum.inl y) (Subsingleton.elim x y))) (Eq.refl (Sum.inl y)))))a: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.IsCycle := 
  fun b c hc =>
    have h1 := Walk.adj_snd (Walk.IsCycle.not_nil hc);
    have h2 := Walk.adj_penultimate (Walk.IsCycle.not_nil hc);
    have hs :=
      Or.casesOn
        (Eq.mp (congrArg (fun x => false = true ∧ c.snd.isRight = true ∨ x ∧ c.snd.isLeft = true) (eq_self true)) h1)
        (fun h => And.casesOn h fun left right => False.elim (noConfusion_of_Nat Bool.ctorIdx left)) fun h =>
        And.casesOn h fun left right => right;
    have hp :=
      Or.casesOn
        (Eq.mp
          (congrArg (fun x => c.penultimate.isLeft = true ∧ x ∨ c.penultimate.isRight = true ∧ false = true)
            (eq_self true))
          h2)
        (fun h => And.casesOn h fun left right => left) fun h =>
        And.casesOn h fun left right => False.elim (noConfusion_of_Nat Bool.ctorIdx right);
    Walk.IsCycle.snd_ne_penultimate hc
      (Exists.casesOn (Sum.isLeft_iff.mp hs) fun x hx =>
        Exists.casesOn (Sum.isLeft_iff.mp hp) fun y hy =>
          Eq.mpr (id (congrArg (fun _a => _a = c.penultimate) hx))
            (Eq.mpr (id (congrArg (fun _a => Sum.inl x = _a) hy))
              (Eq.mpr (id (congrArg (fun _a => Sum.inl _a = Sum.inl y) (Subsingleton.elim x y))) (Eq.refl (Sum.inl y)))))a:Fin 1c:Star5.Walk (Sum.inl a) (Sum.inl a)hc:c.IsCycleh1:Star5.Adj (Sum.inl a) c.snd := Walk.adj_snd (Walk.IsCycle.not_nil hc)⊢ False
    obtain ⟨b, hb⟩ : ∃ b, c.snd = Sum.inr b := bykey:∀ (b : Fin 5) (c : Star5.Walk (Sum.inr b) (Sum.inr b)), ¬c.IsCycle := 
  fun b c hc =>
    have h1 := Walk.adj_snd (Walk.IsCycle.not_nil hc);
    have h2 := Walk.adj_penultimate (Walk.IsCycle.not_nil hc);
    have hs :=
      Or.casesOn
        (Eq.mp (congrArg (fun x => false = true ∧ c.snd.isRight = true ∨ x ∧ c.snd.isLeft = true) (eq_self true)) h1)
        (fun h => And.casesOn h fun left right => False.elim (noConfusion_of_Nat Bool.ctorIdx left)) fun h =>
        And.casesOn h fun left right => right;
    have hp :=
      Or.casesOn
        (Eq.mp
          (congrArg (fun x => c.penultimate.isLeft = true ∧ x ∨ c.penultimate.isRight = true ∧ false = true)
            (eq_self true))
          h2)
        (fun h => And.casesOn h fun left right => left) fun h =>
        And.casesOn h fun left right => False.elim (noConfusion_of_Nat Bool.ctorIdx right);
    Walk.IsCycle.snd_ne_penultimate hc
      (Exists.casesOn (Sum.isLeft_iff.mp hs) fun x hx =>
        Exists.casesOn (Sum.isLeft_iff.mp hp) fun y hy =>
          Eq.mpr (id (congrArg (fun _a => _a = c.penultimate) hx))
            (Eq.mpr (id (congrArg (fun _a => Sum.inl x = _a) hy))
              (Eq.mpr (id (congrArg (fun _a => Sum.inl _a = Sum.inl y) (Subsingleton.elim x y))) (Eq.refl (Sum.inl y)))))a:Fin 1c:Star5.Walk (Sum.inl a) (Sum.inl a)hc:c.IsCycleh1:Star5.Adj (Sum.inl a) c.snd := Walk.adj_snd (Walk.IsCycle.not_nil hc)⊢ ∃ b, c.snd = Sum.inr b
      rcases hsnd : c.snd with x | yinlkey:∀ (b : Fin 5) (c : Star5.Walk (Sum.inr b) (Sum.inr b)), ¬c.IsCycle := 
  fun b c hc =>
    have h1 := Walk.adj_snd (Walk.IsCycle.not_nil hc);
    have h2 := Walk.adj_penultimate (Walk.IsCycle.not_nil hc);
    have hs :=
      Or.casesOn
        (Eq.mp (congrArg (fun x => false = true ∧ c.snd.isRight = true ∨ x ∧ c.snd.isLeft = true) (eq_self true)) h1)
        (fun h => And.casesOn h fun left right => False.elim (noConfusion_of_Nat Bool.ctorIdx left)) fun h =>
        And.casesOn h fun left right => right;
    have hp :=
      Or.casesOn
        (Eq.mp
          (congrArg (fun x => c.penultimate.isLeft = true ∧ x ∨ c.penultimate.isRight = true ∧ false = true)
            (eq_self true))
          h2)
        (fun h => And.casesOn h fun left right => left) fun h =>
        And.casesOn h fun left right => False.elim (noConfusion_of_Nat Bool.ctorIdx right);
    Walk.IsCycle.snd_ne_penultimate hc
      (Exists.casesOn (Sum.isLeft_iff.mp hs) fun x hx =>
        Exists.casesOn (Sum.isLeft_iff.mp hp) fun y hy =>
          Eq.mpr (id (congrArg (fun _a => _a = c.penultimate) hx))
            (Eq.mpr (id (congrArg (fun _a => Sum.inl x = _a) hy))
              (Eq.mpr (id (congrArg (fun _a => Sum.inl _a = Sum.inl y) (Subsingleton.elim x y))) (Eq.refl (Sum.inl y)))))a:Fin 1c:Star5.Walk (Sum.inl a) (Sum.inl a)hc:c.IsCycleh1:Star5.Adj (Sum.inl a) c.snd := Walk.adj_snd (Walk.IsCycle.not_nil hc)x: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.IsCycle := 
  fun b c hc =>
    have h1 := Walk.adj_snd (Walk.IsCycle.not_nil hc);
    have h2 := Walk.adj_penultimate (Walk.IsCycle.not_nil hc);
    have hs :=
      Or.casesOn
        (Eq.mp (congrArg (fun x => false = true ∧ c.snd.isRight = true ∨ x ∧ c.snd.isLeft = true) (eq_self true)) h1)
        (fun h => And.casesOn h fun left right => False.elim (noConfusion_of_Nat Bool.ctorIdx left)) fun h =>
        And.casesOn h fun left right => right;
    have hp :=
      Or.casesOn
        (Eq.mp
          (congrArg (fun x => c.penultimate.isLeft = true ∧ x ∨ c.penultimate.isRight = true ∧ false = true)
            (eq_self true))
          h2)
        (fun h => And.casesOn h fun left right => left) fun h =>
        And.casesOn h fun left right => False.elim (noConfusion_of_Nat Bool.ctorIdx right);
    Walk.IsCycle.snd_ne_penultimate hc
      (Exists.casesOn (Sum.isLeft_iff.mp hs) fun x hx =>
        Exists.casesOn (Sum.isLeft_iff.mp hp) fun y hy =>
          Eq.mpr (id (congrArg (fun _a => _a = c.penultimate) hx))
            (Eq.mpr (id (congrArg (fun _a => Sum.inl x = _a) hy))
              (Eq.mpr (id (congrArg (fun _a => Sum.inl _a = Sum.inl y) (Subsingleton.elim x y))) (Eq.refl (Sum.inl y)))))a:Fin 1c:Star5.Walk (Sum.inl a) (Sum.inl a)hc:c.IsCycleh1:Star5.Adj (Sum.inl a) c.snd := Walk.adj_snd (Walk.IsCycle.not_nil hc)y:Fin 5hsnd:c.snd = Sum.inr y⊢ ∃ b, Sum.inr y = Sum.inr b
      ·inlkey:∀ (b : Fin 5) (c : Star5.Walk (Sum.inr b) (Sum.inr b)), ¬c.IsCycle := 
  fun b c hc =>
    have h1 := Walk.adj_snd (Walk.IsCycle.not_nil hc);
    have h2 := Walk.adj_penultimate (Walk.IsCycle.not_nil hc);
    have hs :=
      Or.casesOn
        (Eq.mp (congrArg (fun x => false = true ∧ c.snd.isRight = true ∨ x ∧ c.snd.isLeft = true) (eq_self true)) h1)
        (fun h => And.casesOn h fun left right => False.elim (noConfusion_of_Nat Bool.ctorIdx left)) fun h =>
        And.casesOn h fun left right => right;
    have hp :=
      Or.casesOn
        (Eq.mp
          (congrArg (fun x => c.penultimate.isLeft = true ∧ x ∨ c.penultimate.isRight = true ∧ false = true)
            (eq_self true))
          h2)
        (fun h => And.casesOn h fun left right => left) fun h =>
        And.casesOn h fun left right => False.elim (noConfusion_of_Nat Bool.ctorIdx right);
    Walk.IsCycle.snd_ne_penultimate hc
      (Exists.casesOn (Sum.isLeft_iff.mp hs) fun x hx =>
        Exists.casesOn (Sum.isLeft_iff.mp hp) fun y hy =>
          Eq.mpr (id (congrArg (fun _a => _a = c.penultimate) hx))
            (Eq.mpr (id (congrArg (fun _a => Sum.inl x = _a) hy))
              (Eq.mpr (id (congrArg (fun _a => Sum.inl _a = Sum.inl y) (Subsingleton.elim x y))) (Eq.refl (Sum.inl y)))))a:Fin 1c:Star5.Walk (Sum.inl a) (Sum.inl a)hc:c.IsCycleh1:Star5.Adj (Sum.inl a) c.snd := Walk.adj_snd (Walk.IsCycle.not_nil hc)x:Fin 1hsnd:c.snd = Sum.inl x⊢ ∃ b, Sum.inl x = Sum.inr b rw [hsnd] at h1inlkey:∀ (b : Fin 5) (c : Star5.Walk (Sum.inr b) (Sum.inr b)), ¬c.IsCycle := 
  fun b c hc =>
    have h1 := Walk.adj_snd (Walk.IsCycle.not_nil hc);
    have h2 := Walk.adj_penultimate (Walk.IsCycle.not_nil hc);
    have hs :=
      Or.casesOn
        (Eq.mp (congrArg (fun x => false = true ∧ c.snd.isRight = true ∨ x ∧ c.snd.isLeft = true) (eq_self true)) h1)
        (fun h => And.casesOn h fun left right => False.elim (noConfusion_of_Nat Bool.ctorIdx left)) fun h =>
        And.casesOn h fun left right => right;
    have hp :=
      Or.casesOn
        (Eq.mp
          (congrArg (fun x => c.penultimate.isLeft = true ∧ x ∨ c.penultimate.isRight = true ∧ false = true)
            (eq_self true))
          h2)
        (fun h => And.casesOn h fun left right => left) fun h =>
        And.casesOn h fun left right => False.elim (noConfusion_of_Nat Bool.ctorIdx right);
    Walk.IsCycle.snd_ne_penultimate hc
      (Exists.casesOn (Sum.isLeft_iff.mp hs) fun x hx =>
        Exists.casesOn (Sum.isLeft_iff.mp hp) fun y hy =>
          Eq.mpr (id (congrArg (fun _a => _a = c.penultimate) hx))
            (Eq.mpr (id (congrArg (fun _a => Sum.inl x = _a) hy))
              (Eq.mpr (id (congrArg (fun _a => Sum.inl _a = Sum.inl y) (Subsingleton.elim x y))) (Eq.refl (Sum.inl y)))))a: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 b; simp [Star5, completeBipartiteGraph] at h1All goals completed! 🐙
      ·inrkey:∀ (b : Fin 5) (c : Star5.Walk (Sum.inr b) (Sum.inr b)), ¬c.IsCycle := 
  fun b c hc =>
    have h1 := Walk.adj_snd (Walk.IsCycle.not_nil hc);
    have h2 := Walk.adj_penultimate (Walk.IsCycle.not_nil hc);
    have hs :=
      Or.casesOn
        (Eq.mp (congrArg (fun x => false = true ∧ c.snd.isRight = true ∨ x ∧ c.snd.isLeft = true) (eq_self true)) h1)
        (fun h => And.casesOn h fun left right => False.elim (noConfusion_of_Nat Bool.ctorIdx left)) fun h =>
        And.casesOn h fun left right => right;
    have hp :=
      Or.casesOn
        (Eq.mp
          (congrArg (fun x => c.penultimate.isLeft = true ∧ x ∨ c.penultimate.isRight = true ∧ false = true)
            (eq_self true))
          h2)
        (fun h => And.casesOn h fun left right => left) fun h =>
        And.casesOn h fun left right => False.elim (noConfusion_of_Nat Bool.ctorIdx right);
    Walk.IsCycle.snd_ne_penultimate hc
      (Exists.casesOn (Sum.isLeft_iff.mp hs) fun x hx =>
        Exists.casesOn (Sum.isLeft_iff.mp hp) fun y hy =>
          Eq.mpr (id (congrArg (fun _a => _a = c.penultimate) hx))
            (Eq.mpr (id (congrArg (fun _a => Sum.inl x = _a) hy))
              (Eq.mpr (id (congrArg (fun _a => Sum.inl _a = Sum.inl y) (Subsingleton.elim x y))) (Eq.refl (Sum.inl y)))))a:Fin 1c:Star5.Walk (Sum.inl a) (Sum.inl a)hc:c.IsCycleh1:Star5.Adj (Sum.inl a) c.snd := Walk.adj_snd (Walk.IsCycle.not_nil hc)y:Fin 5hsnd:c.snd = Sum.inr y⊢ ∃ b, Sum.inr y = Sum.inr b exact ⟨y, rfl⟩All goals completed! 🐙
    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.IsCycle := 
  fun b c hc =>
    have h1 := Walk.adj_snd (Walk.IsCycle.not_nil hc);
    have h2 := Walk.adj_penultimate (Walk.IsCycle.not_nil hc);
    have hs :=
      Or.casesOn
        (Eq.mp (congrArg (fun x => false = true ∧ c.snd.isRight = true ∨ x ∧ c.snd.isLeft = true) (eq_self true)) h1)
        (fun h => And.casesOn h fun left right => False.elim (noConfusion_of_Nat Bool.ctorIdx left)) fun h =>
        And.casesOn h fun left right => right;
    have hp :=
      Or.casesOn
        (Eq.mp
          (congrArg (fun x => c.penultimate.isLeft = true ∧ x ∨ c.penultimate.isRight = true ∧ false = true)
            (eq_self true))
          h2)
        (fun h => And.casesOn h fun left right => left) fun h =>
        And.casesOn h fun left right => False.elim (noConfusion_of_Nat Bool.ctorIdx right);
    Walk.IsCycle.snd_ne_penultimate hc
      (Exists.casesOn (Sum.isLeft_iff.mp hs) fun x hx =>
        Exists.casesOn (Sum.isLeft_iff.mp hp) fun y hy =>
          Eq.mpr (id (congrArg (fun _a => _a = c.penultimate) hx))
            (Eq.mpr (id (congrArg (fun _a => Sum.inl x = _a) hy))
              (Eq.mpr (id (congrArg (fun _a => Sum.inl _a = Sum.inl y) (Subsingleton.elim x y))) (Eq.refl (Sum.inl y)))))a:Fin 1c:Star5.Walk (Sum.inl a) (Sum.inl a)hc:c.IsCycleh1:Star5.Adj (Sum.inl a) c.snd := Walk.adj_snd (Walk.IsCycle.not_nil hc)b:Fin 5hb:c.snd = Sum.inr bhmem:Sum.inr b ∈ c.support := hb ▸ List.mem_of_mem_tail (Walk.snd_mem_tail_support (Walk.IsCycle.not_nil hc))⊢ False
    exact key b (c.rotate hmem) (hc.rotate hmem)All goals completed! 🐙


@[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
  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; 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; 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
  have hle : ∀ M : Subgraph Star5, M.IsMatching → M.edgeSet.toFinset.card ≤ 1 := by⊢ Star5.matchingNumber = 1
    intro M hMM:Star5.SubgraphhM:M.IsMatching⊢ M.edgeSet.toFinset.card ≤ 1
    have hcenter : ∀ e ∈ M.edgeSet, (Sum.inl 0 : Fin 1 ⊕ Fin 5) ∈ e := by⊢ Star5.matchingNumber = 1
      intro e heM:Star5.SubgraphhM:M.IsMatchinge:Sym2 (Fin 1 ⊕ Fin 5)he:e ∈ M.edgeSet⊢ Sum.inl 0 ∈ e
      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)
      rw [Subgraph.mem_edgeSet] at hehfM:Star5.SubgraphhM:M.IsMatchinga:Fin 1 ⊕ Fin 5b:Fin 1 ⊕ Fin 5he:M.Adj a b⊢ Sum.inl 0 ∈ s(a, b)
      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 := Subgraph.Adj.adj_sub he⊢ Sum.inl 0 ∈ s(a, b)
      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 := Subgraph.Adj.adj_sub he⊢ Sum.inl 0 ∈ s(a, b)
      rw [Sym2.mem_iff]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 := Subgraph.Adj.adj_sub he⊢ Sum.inl 0 = a ∨ Sum.inl 0 = b
      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 = b
      ·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 = b lefthf.inl.hM: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; obtain ⟨a', rfl⟩ := Sum.isLeft_iff.mp hahf.inl.hM: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'; exact congrArg Sum.inl (Subsingleton.elim 0 a')All goals completed! 🐙
      ·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 = b righthf.inr.hM: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 = b; obtain ⟨b', rfl⟩ := Sum.isLeft_iff.mp hbhf.inr.hM: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'; exact congrArg Sum.inl (Subsingleton.elim 0 b')All goals completed! 🐙
    rw [Finset.card_le_one]M:Star5.SubgraphhM:M.IsMatchinghcenter:∀ e ∈ M.edgeSet, Sum.inl 0 ∈ e := 
  fun e he =>
    Sym2.inductionOn e
      (fun a b he =>
        have hadj := Subgraph.Adj.adj_sub (Eq.mp (congrArg (fun _a => _a) (propext Subgraph.mem_edgeSet)) he);
        Eq.mpr (id (congrArg (fun _a => _a) (propext Sym2.mem_iff)))
          (Or.casesOn hadj
            (fun h =>
              And.casesOn h fun ha right =>
                Or.inl
                  (Exists.casesOn (Sum.isLeft_iff.mp ha) fun a' h =>
                    Eq.ndrec (motive := fun a => M.Adj a b → a.isLeft = true → Sum.inl 0 = a)
                      (fun he ha => congrArg Sum.inl (Subsingleton.elim 0 a')) (Eq.symm h)
                      (Eq.mp (congrArg (fun _a => _a) (propext Subgraph.mem_edgeSet)) he) ha))
            fun h =>
            And.casesOn h fun left hb =>
              Or.inr
                (Exists.casesOn (Sum.isLeft_iff.mp hb) fun b' h =>
                  Eq.ndrec (motive := fun b => M.Adj a b → b.isLeft = true → Sum.inl 0 = b)
                    (fun he hb => congrArg Sum.inl (Subsingleton.elim 0 b')) (Eq.symm h)
                    (Eq.mp (congrArg (fun _a => _a) (propext Subgraph.mem_edgeSet)) he) hb)))
      he⊢ ∀ a ∈ M.edgeSet.toFinset, ∀ b ∈ M.edgeSet.toFinset, a = b
    intro e heM:Star5.SubgraphhM:M.IsMatchinghcenter:∀ e ∈ M.edgeSet, Sum.inl 0 ∈ e := 
  fun e he =>
    Sym2.inductionOn e
      (fun a b he =>
        have hadj := Subgraph.Adj.adj_sub (Eq.mp (congrArg (fun _a => _a) (propext Subgraph.mem_edgeSet)) he);
        Eq.mpr (id (congrArg (fun _a => _a) (propext Sym2.mem_iff)))
          (Or.casesOn hadj
            (fun h =>
              And.casesOn h fun ha right =>
                Or.inl
                  (Exists.casesOn (Sum.isLeft_iff.mp ha) fun a' h =>
                    Eq.ndrec (motive := fun a => M.Adj a b → a.isLeft = true → Sum.inl 0 = a)
                      (fun he ha => congrArg Sum.inl (Subsingleton.elim 0 a')) (Eq.symm h)
                      (Eq.mp (congrArg (fun _a => _a) (propext Subgraph.mem_edgeSet)) he) ha))
            fun h =>
            And.casesOn h fun left hb =>
              Or.inr
                (Exists.casesOn (Sum.isLeft_iff.mp hb) fun b' h =>
                  Eq.ndrec (motive := fun b => M.Adj a b → b.isLeft = true → Sum.inl 0 = b)
                    (fun he hb => congrArg Sum.inl (Subsingleton.elim 0 b')) (Eq.symm h)
                    (Eq.mp (congrArg (fun _a => _a) (propext Subgraph.mem_edgeSet)) he) hb)))
      hee:Sym2 (Fin 1 ⊕ Fin 5)he:e ∈ M.edgeSet.toFinset⊢ ∀ b ∈ M.edgeSet.toFinset, e = b fM:Star5.SubgraphhM:M.IsMatchinghcenter:∀ e ∈ M.edgeSet, Sum.inl 0 ∈ e := 
  fun e he =>
    Sym2.inductionOn e
      (fun a b he =>
        have hadj := Subgraph.Adj.adj_sub (Eq.mp (congrArg (fun _a => _a) (propext Subgraph.mem_edgeSet)) he);
        Eq.mpr (id (congrArg (fun _a => _a) (propext Sym2.mem_iff)))
          (Or.casesOn hadj
            (fun h =>
              And.casesOn h fun ha right =>
                Or.inl
                  (Exists.casesOn (Sum.isLeft_iff.mp ha) fun a' h =>
                    Eq.ndrec (motive := fun a => M.Adj a b → a.isLeft = true → Sum.inl 0 = a)
                      (fun he ha => congrArg Sum.inl (Subsingleton.elim 0 a')) (Eq.symm h)
                      (Eq.mp (congrArg (fun _a => _a) (propext Subgraph.mem_edgeSet)) he) ha))
            fun h =>
            And.casesOn h fun left hb =>
              Or.inr
                (Exists.casesOn (Sum.isLeft_iff.mp hb) fun b' h =>
                  Eq.ndrec (motive := fun b => M.Adj a b → b.isLeft = true → Sum.inl 0 = b)
                    (fun he hb => congrArg Sum.inl (Subsingleton.elim 0 b')) (Eq.symm h)
                    (Eq.mp (congrArg (fun _a => _a) (propext Subgraph.mem_edgeSet)) he) hb)))
      hee:Sym2 (Fin 1 ⊕ Fin 5)he:e ∈ M.edgeSet.toFinsetf:Sym2 (Fin 1 ⊕ Fin 5)⊢ f ∈ M.edgeSet.toFinset → e = f hfM:Star5.SubgraphhM:M.IsMatchinghcenter:∀ e ∈ M.edgeSet, Sum.inl 0 ∈ e := 
  fun e he =>
    Sym2.inductionOn e
      (fun a b he =>
        have hadj := Subgraph.Adj.adj_sub (Eq.mp (congrArg (fun _a => _a) (propext Subgraph.mem_edgeSet)) he);
        Eq.mpr (id (congrArg (fun _a => _a) (propext Sym2.mem_iff)))
          (Or.casesOn hadj
            (fun h =>
              And.casesOn h fun ha right =>
                Or.inl
                  (Exists.casesOn (Sum.isLeft_iff.mp ha) fun a' h =>
                    Eq.ndrec (motive := fun a => M.Adj a b → a.isLeft = true → Sum.inl 0 = a)
                      (fun he ha => congrArg Sum.inl (Subsingleton.elim 0 a')) (Eq.symm h)
                      (Eq.mp (congrArg (fun _a => _a) (propext Subgraph.mem_edgeSet)) he) ha))
            fun h =>
            And.casesOn h fun left hb =>
              Or.inr
                (Exists.casesOn (Sum.isLeft_iff.mp hb) fun b' h =>
                  Eq.ndrec (motive := fun b => M.Adj a b → b.isLeft = true → Sum.inl 0 = b)
                    (fun he hb => congrArg Sum.inl (Subsingleton.elim 0 b')) (Eq.symm h)
                    (Eq.mp (congrArg (fun _a => _a) (propext Subgraph.mem_edgeSet)) he) hb)))
      hee:Sym2 (Fin 1 ⊕ Fin 5)he:e ∈ M.edgeSet.toFinsetf:Sym2 (Fin 1 ⊕ Fin 5)hf:f ∈ M.edgeSet.toFinset⊢ e = f
    rw [Set.mem_toFinset] at he hfM:Star5.SubgraphhM:M.IsMatchinghcenter:∀ e ∈ M.edgeSet, Sum.inl 0 ∈ e := 
  fun e he =>
    Sym2.inductionOn e
      (fun a b he =>
        have hadj := Subgraph.Adj.adj_sub (Eq.mp (congrArg (fun _a => _a) (propext Subgraph.mem_edgeSet)) he);
        Eq.mpr (id (congrArg (fun _a => _a) (propext Sym2.mem_iff)))
          (Or.casesOn hadj
            (fun h =>
              And.casesOn h fun ha right =>
                Or.inl
                  (Exists.casesOn (Sum.isLeft_iff.mp ha) fun a' h =>
                    Eq.ndrec (motive := fun a => M.Adj a b → a.isLeft = true → Sum.inl 0 = a)
                      (fun he ha => congrArg Sum.inl (Subsingleton.elim 0 a')) (Eq.symm h)
                      (Eq.mp (congrArg (fun _a => _a) (propext Subgraph.mem_edgeSet)) he) ha))
            fun h =>
            And.casesOn h fun left hb =>
              Or.inr
                (Exists.casesOn (Sum.isLeft_iff.mp hb) fun b' h =>
                  Eq.ndrec (motive := fun b => M.Adj a b → b.isLeft = true → Sum.inl 0 = b)
                    (fun he hb => congrArg Sum.inl (Subsingleton.elim 0 b')) (Eq.symm h)
                    (Eq.mp (congrArg (fun _a => _a) (propext Subgraph.mem_edgeSet)) he) hb)))
      hee:Sym2 (Fin 1 ⊕ Fin 5)he:e ∈ M.edgeSetf:Sym2 (Fin 1 ⊕ Fin 5)hf:f ∈ M.edgeSet⊢ e = f
    obtain ⟨y, rfl⟩ := Sym2.mem_iff_exists.mp (hcenter e he)M:Star5.SubgraphhM:M.IsMatchinghcenter:∀ e ∈ M.edgeSet, Sum.inl 0 ∈ e := 
  fun e he =>
    Sym2.inductionOn e
      (fun a b he =>
        have hadj := Subgraph.Adj.adj_sub (Eq.mp (congrArg (fun _a => _a) (propext Subgraph.mem_edgeSet)) he);
        Eq.mpr (id (congrArg (fun _a => _a) (propext Sym2.mem_iff)))
          (Or.casesOn hadj
            (fun h =>
              And.casesOn h fun ha right =>
                Or.inl
                  (Exists.casesOn (Sum.isLeft_iff.mp ha) fun a' h =>
                    Eq.ndrec (motive := fun a => M.Adj a b → a.isLeft = true → Sum.inl 0 = a)
                      (fun he ha => congrArg Sum.inl (Subsingleton.elim 0 a')) (Eq.symm h)
                      (Eq.mp (congrArg (fun _a => _a) (propext Subgraph.mem_edgeSet)) he) ha))
            fun h =>
            And.casesOn h fun left hb =>
              Or.inr
                (Exists.casesOn (Sum.isLeft_iff.mp hb) fun b' h =>
                  Eq.ndrec (motive := fun b => M.Adj a b → b.isLeft = true → Sum.inl 0 = b)
                    (fun he hb => congrArg Sum.inl (Subsingleton.elim 0 b')) (Eq.symm h)
                    (Eq.mp (congrArg (fun _a => _a) (propext Subgraph.mem_edgeSet)) he) hb)))
      hef: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) = f
    obtain ⟨z, rfl⟩ := Sym2.mem_iff_exists.mp (hcenter f hf)M:Star5.SubgraphhM:M.IsMatchinghcenter:∀ e ∈ M.edgeSet, Sum.inl 0 ∈ e := 
  fun e he =>
    Sym2.inductionOn e
      (fun a b he =>
        have hadj := Subgraph.Adj.adj_sub (Eq.mp (congrArg (fun _a => _a) (propext Subgraph.mem_edgeSet)) he);
        Eq.mpr (id (congrArg (fun _a => _a) (propext Sym2.mem_iff)))
          (Or.casesOn hadj
            (fun h =>
              And.casesOn h fun ha right =>
                Or.inl
                  (Exists.casesOn (Sum.isLeft_iff.mp ha) fun a' h =>
                    Eq.ndrec (motive := fun a => M.Adj a b → a.isLeft = true → Sum.inl 0 = a)
                      (fun he ha => congrArg Sum.inl (Subsingleton.elim 0 a')) (Eq.symm h)
                      (Eq.mp (congrArg (fun _a => _a) (propext Subgraph.mem_edgeSet)) he) ha))
            fun h =>
            And.casesOn h fun left hb =>
              Or.inr
                (Exists.casesOn (Sum.isLeft_iff.mp hb) fun b' h =>
                  Eq.ndrec (motive := fun b => M.Adj a b → b.isLeft = true → Sum.inl 0 = b)
                    (fun he hb => congrArg Sum.inl (Subsingleton.elim 0 b')) (Eq.symm h)
                    (Eq.mp (congrArg (fun _a => _a) (propext Subgraph.mem_edgeSet)) he) hb)))
      hey: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)
    rw [Subgraph.mem_edgeSet] at he hfM:Star5.SubgraphhM:M.IsMatchinghcenter:∀ e ∈ M.edgeSet, Sum.inl 0 ∈ e := 
  fun e he =>
    Sym2.inductionOn e
      (fun a b he =>
        have hadj := Subgraph.Adj.adj_sub (Eq.mp (congrArg (fun _a => _a) (propext Subgraph.mem_edgeSet)) he);
        Eq.mpr (id (congrArg (fun _a => _a) (propext Sym2.mem_iff)))
          (Or.casesOn hadj
            (fun h =>
              And.casesOn h fun ha right =>
                Or.inl
                  (Exists.casesOn (Sum.isLeft_iff.mp ha) fun a' h =>
                    Eq.ndrec (motive := fun a => M.Adj a b → a.isLeft = true → Sum.inl 0 = a)
                      (fun he ha => congrArg Sum.inl (Subsingleton.elim 0 a')) (Eq.symm h)
                      (Eq.mp (congrArg (fun _a => _a) (propext Subgraph.mem_edgeSet)) he) ha))
            fun h =>
            And.casesOn h fun left hb =>
              Or.inr
                (Exists.casesOn (Sum.isLeft_iff.mp hb) fun b' h =>
                  Eq.ndrec (motive := fun b => M.Adj a b → b.isLeft = true → Sum.inl 0 = b)
                    (fun he hb => congrArg Sum.inl (Subsingleton.elim 0 b')) (Eq.symm h)
                    (Eq.mp (congrArg (fun _a => _a) (propext Subgraph.mem_edgeSet)) he) hb)))
      hey: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)
    rw [hM.eq_of_adj_left he hf]All goals completed! 🐙
  have hbdd : BddAbove (Set.image (fun M : Subgraph Star5 => (M.edgeSet.toFinset.card : ℝ)) {M | M.IsMatching}) := by⊢ Star5.matchingNumber = 1
    refine ⟨1, ?_⟩hle:∀ (M : Star5.Subgraph), M.IsMatching → M.edgeSet.toFinset.card ≤ 1 := 
  fun M hM =>
    have hcenter := fun e he =>
      Sym2.inductionOn e
        (fun a b he =>
          have hadj := Subgraph.Adj.adj_sub (Eq.mp (congrArg (fun _a => _a) (propext Subgraph.mem_edgeSet)) he);
          Eq.mpr (id (congrArg (fun _a => _a) (propext Sym2.mem_iff)))
            (Or.casesOn hadj
              (fun h =>
                And.casesOn h fun ha right =>
                  Or.inl
                    (Exists.casesOn (Sum.isLeft_iff.mp ha) fun a' h =>
                      Eq.ndrec (motive := fun a => M.Adj a b → a.isLeft = true → Sum.inl 0 = a)
                        (fun he ha => congrArg Sum.inl (Subsingleton.elim 0 a')) (Eq.symm h)
                        (Eq.mp (congrArg (fun _a => _a) (propext Subgraph.mem_edgeSet)) he) ha))
              fun h =>
              And.casesOn h fun left hb =>
                Or.inr
                  (Exists.casesOn (Sum.isLeft_iff.mp hb) fun b' h =>
                    Eq.ndrec (motive := fun b => M.Adj a b → b.isLeft = true → Sum.inl 0 = b)
                      (fun he hb => congrArg Sum.inl (Subsingleton.elim 0 b')) (Eq.symm h)
                      (Eq.mp (congrArg (fun _a => _a) (propext Subgraph.mem_edgeSet)) he) hb)))
        he;
    Eq.mpr (id (congrArg (fun _a => _a) (propext Finset.card_le_one))) fun e he f hf =>
      Exists.casesOn (Sym2.mem_iff_exists.mp (hcenter e (Eq.mp (congrArg (fun _a => _a) (propext Set.mem_toFinset)) he)))
        fun y h =>
        Eq.ndrec (motive := fun e => e ∈ M.edgeSet → e = f)
          (fun he =>
            Exists.casesOn
              (Sym2.mem_iff_exists.mp (hcenter f (Eq.mp (congrArg (fun _a => _a) (propext Set.mem_toFinset)) hf)))
              fun z h =>
              Eq.ndrec (motive := fun f => f ∈ M.edgeSet → s(Sum.inl 0, y) = f)
                (fun hf =>
                  Eq.mpr
                    (id
                      (congrArg (fun _a => s(Sum.inl 0, _a) = s(Sum.inl 0, z))
                        (Subgraph.IsMatching.eq_of_adj_left hM
                          (Eq.mp (congrArg (fun _a => _a) (propext Subgraph.mem_edgeSet)) he)
                          (Eq.mp (congrArg (fun _a => _a) (propext Subgraph.mem_edgeSet)) hf))))
                    (Eq.refl s(Sum.inl 0, z)))
                (Eq.symm h) (Eq.mp (congrArg (fun _a => _a) (propext Set.mem_toFinset)) hf))
          (Eq.symm h) (Eq.mp (congrArg (fun _a => _a) (propext Set.mem_toFinset)) he)⊢ 1 ∈ upperBounds ((fun M => ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching})
    rintro x ⟨M, hM, rfl⟩hle:∀ (M : Star5.Subgraph), M.IsMatching → M.edgeSet.toFinset.card ≤ 1 := 
  fun M hM =>
    have hcenter := fun e he =>
      Sym2.inductionOn e
        (fun a b he =>
          have hadj := Subgraph.Adj.adj_sub (Eq.mp (congrArg (fun _a => _a) (propext Subgraph.mem_edgeSet)) he);
          Eq.mpr (id (congrArg (fun _a => _a) (propext Sym2.mem_iff)))
            (Or.casesOn hadj
              (fun h =>
                And.casesOn h fun ha right =>
                  Or.inl
                    (Exists.casesOn (Sum.isLeft_iff.mp ha) fun a' h =>
                      Eq.ndrec (motive := fun a => M.Adj a b → a.isLeft = true → Sum.inl 0 = a)
                        (fun he ha => congrArg Sum.inl (Subsingleton.elim 0 a')) (Eq.symm h)
                        (Eq.mp (congrArg (fun _a => _a) (propext Subgraph.mem_edgeSet)) he) ha))
              fun h =>
              And.casesOn h fun left hb =>
                Or.inr
                  (Exists.casesOn (Sum.isLeft_iff.mp hb) fun b' h =>
                    Eq.ndrec (motive := fun b => M.Adj a b → b.isLeft = true → Sum.inl 0 = b)
                      (fun he hb => congrArg Sum.inl (Subsingleton.elim 0 b')) (Eq.symm h)
                      (Eq.mp (congrArg (fun _a => _a) (propext Subgraph.mem_edgeSet)) he) hb)))
        he;
    Eq.mpr (id (congrArg (fun _a => _a) (propext Finset.card_le_one))) fun e he f hf =>
      Exists.casesOn (Sym2.mem_iff_exists.mp (hcenter e (Eq.mp (congrArg (fun _a => _a) (propext Set.mem_toFinset)) he)))
        fun y h =>
        Eq.ndrec (motive := fun e => e ∈ M.edgeSet → e = f)
          (fun he =>
            Exists.casesOn
              (Sym2.mem_iff_exists.mp (hcenter f (Eq.mp (congrArg (fun _a => _a) (propext Set.mem_toFinset)) hf)))
              fun z h =>
              Eq.ndrec (motive := fun f => f ∈ M.edgeSet → s(Sum.inl 0, y) = f)
                (fun hf =>
                  Eq.mpr
                    (id
                      (congrArg (fun _a => s(Sum.inl 0, _a) = s(Sum.inl 0, z))
                        (Subgraph.IsMatching.eq_of_adj_left hM
                          (Eq.mp (congrArg (fun _a => _a) (propext Subgraph.mem_edgeSet)) he)
                          (Eq.mp (congrArg (fun _a => _a) (propext Subgraph.mem_edgeSet)) hf))))
                    (Eq.refl s(Sum.inl 0, z)))
                (Eq.symm h) (Eq.mp (congrArg (fun _a => _a) (propext Set.mem_toFinset)) hf))
          (Eq.symm h) (Eq.mp (congrArg (fun _a => _a) (propext Set.mem_toFinset)) he)M:Star5.SubgraphhM:M ∈ {M | M.IsMatching}⊢ (fun M => ↑M.edgeSet.toFinset.card) M ≤ 1
    show (M.edgeSet.toFinset.card : ℝ) ≤ 1hle:∀ (M : Star5.Subgraph), M.IsMatching → M.edgeSet.toFinset.card ≤ 1 := 
  fun M hM =>
    have hcenter := fun e he =>
      Sym2.inductionOn e
        (fun a b he =>
          have hadj := Subgraph.Adj.adj_sub (Eq.mp (congrArg (fun _a => _a) (propext Subgraph.mem_edgeSet)) he);
          Eq.mpr (id (congrArg (fun _a => _a) (propext Sym2.mem_iff)))
            (Or.casesOn hadj
              (fun h =>
                And.casesOn h fun ha right =>
                  Or.inl
                    (Exists.casesOn (Sum.isLeft_iff.mp ha) fun a' h =>
                      Eq.ndrec (motive := fun a => M.Adj a b → a.isLeft = true → Sum.inl 0 = a)
                        (fun he ha => congrArg Sum.inl (Subsingleton.elim 0 a')) (Eq.symm h)
                        (Eq.mp (congrArg (fun _a => _a) (propext Subgraph.mem_edgeSet)) he) ha))
              fun h =>
              And.casesOn h fun left hb =>
                Or.inr
                  (Exists.casesOn (Sum.isLeft_iff.mp hb) fun b' h =>
                    Eq.ndrec (motive := fun b => M.Adj a b → b.isLeft = true → Sum.inl 0 = b)
                      (fun he hb => congrArg Sum.inl (Subsingleton.elim 0 b')) (Eq.symm h)
                      (Eq.mp (congrArg (fun _a => _a) (propext Subgraph.mem_edgeSet)) he) hb)))
        he;
    Eq.mpr (id (congrArg (fun _a => _a) (propext Finset.card_le_one))) fun e he f hf =>
      Exists.casesOn (Sym2.mem_iff_exists.mp (hcenter e (Eq.mp (congrArg (fun _a => _a) (propext Set.mem_toFinset)) he)))
        fun y h =>
        Eq.ndrec (motive := fun e => e ∈ M.edgeSet → e = f)
          (fun he =>
            Exists.casesOn
              (Sym2.mem_iff_exists.mp (hcenter f (Eq.mp (congrArg (fun _a => _a) (propext Set.mem_toFinset)) hf)))
              fun z h =>
              Eq.ndrec (motive := fun f => f ∈ M.edgeSet → s(Sum.inl 0, y) = f)
                (fun hf =>
                  Eq.mpr
                    (id
                      (congrArg (fun _a => s(Sum.inl 0, _a) = s(Sum.inl 0, z))
                        (Subgraph.IsMatching.eq_of_adj_left hM
                          (Eq.mp (congrArg (fun _a => _a) (propext Subgraph.mem_edgeSet)) he)
                          (Eq.mp (congrArg (fun _a => _a) (propext Subgraph.mem_edgeSet)) hf))))
                    (Eq.refl s(Sum.inl 0, z)))
                (Eq.symm h) (Eq.mp (congrArg (fun _a => _a) (propext Set.mem_toFinset)) hf))
          (Eq.symm h) (Eq.mp (congrArg (fun _a => _a) (propext Set.mem_toFinset)) he)M:Star5.SubgraphhM:M ∈ {M | M.IsMatching}⊢ ↑M.edgeSet.toFinset.card ≤ 1
    exact_mod_cast hle M hMAll goals completed! 🐙
  unfold matchingNumberhle:∀ (M : Star5.Subgraph), M.IsMatching → M.edgeSet.toFinset.card ≤ 1 := 
  fun M hM =>
    have hcenter := fun e he =>
      Sym2.inductionOn e
        (fun a b he =>
          have hadj := Subgraph.Adj.adj_sub (Eq.mp (congrArg (fun _a => _a) (propext Subgraph.mem_edgeSet)) he);
          Eq.mpr (id (congrArg (fun _a => _a) (propext Sym2.mem_iff)))
            (Or.casesOn hadj
              (fun h =>
                And.casesOn h fun ha right =>
                  Or.inl
                    (Exists.casesOn (Sum.isLeft_iff.mp ha) fun a' h =>
                      Eq.ndrec (motive := fun a => M.Adj a b → a.isLeft = true → Sum.inl 0 = a)
                        (fun he ha => congrArg Sum.inl (Subsingleton.elim 0 a')) (Eq.symm h)
                        (Eq.mp (congrArg (fun _a => _a) (propext Subgraph.mem_edgeSet)) he) ha))
              fun h =>
              And.casesOn h fun left hb =>
                Or.inr
                  (Exists.casesOn (Sum.isLeft_iff.mp hb) fun b' h =>
                    Eq.ndrec (motive := fun b => M.Adj a b → b.isLeft = true → Sum.inl 0 = b)
                      (fun he hb => congrArg Sum.inl (Subsingleton.elim 0 b')) (Eq.symm h)
                      (Eq.mp (congrArg (fun _a => _a) (propext Subgraph.mem_edgeSet)) he) hb)))
        he;
    Eq.mpr (id (congrArg (fun _a => _a) (propext Finset.card_le_one))) fun e he f hf =>
      Exists.casesOn (Sym2.mem_iff_exists.mp (hcenter e (Eq.mp (congrArg (fun _a => _a) (propext Set.mem_toFinset)) he)))
        fun y h =>
        Eq.ndrec (motive := fun e => e ∈ M.edgeSet → e = f)
          (fun he =>
            Exists.casesOn
              (Sym2.mem_iff_exists.mp (hcenter f (Eq.mp (congrArg (fun _a => _a) (propext Set.mem_toFinset)) hf)))
              fun z h =>
              Eq.ndrec (motive := fun f => f ∈ M.edgeSet → s(Sum.inl 0, y) = f)
                (fun hf =>
                  Eq.mpr
                    (id
                      (congrArg (fun _a => s(Sum.inl 0, _a) = s(Sum.inl 0, z))
                        (Subgraph.IsMatching.eq_of_adj_left hM
                          (Eq.mp (congrArg (fun _a => _a) (propext Subgraph.mem_edgeSet)) he)
                          (Eq.mp (congrArg (fun _a => _a) (propext Subgraph.mem_edgeSet)) hf))))
                    (Eq.refl s(Sum.inl 0, z)))
                (Eq.symm h) (Eq.mp (congrArg (fun _a => _a) (propext Set.mem_toFinset)) hf))
          (Eq.symm h) (Eq.mp (congrArg (fun _a => _a) (propext Set.mem_toFinset)) he)hbdd:BddAbove ((fun M => ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching}) := 
  Exists.intro 1 fun ⦃x⦄ a =>
    Exists.casesOn a fun M h =>
      And.casesOn h fun hM right =>
        right ▸
          id
            (cast
              (Eq.symm (Eq.trans (congrArg (LE.le ↑M.edgeSet.toFinset.card) (Eq.symm Nat.cast_one)) Nat.cast_le._simp_1))
              (hle M hM))⊢ (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 ≤ 1 := 
  fun M hM =>
    have hcenter := fun e he =>
      Sym2.inductionOn e
        (fun a b he =>
          have hadj := Subgraph.Adj.adj_sub (Eq.mp (congrArg (fun _a => _a) (propext Subgraph.mem_edgeSet)) he);
          Eq.mpr (id (congrArg (fun _a => _a) (propext Sym2.mem_iff)))
            (Or.casesOn hadj
              (fun h =>
                And.casesOn h fun ha right =>
                  Or.inl
                    (Exists.casesOn (Sum.isLeft_iff.mp ha) fun a' h =>
                      Eq.ndrec (motive := fun a => M.Adj a b → a.isLeft = true → Sum.inl 0 = a)
                        (fun he ha => congrArg Sum.inl (Subsingleton.elim 0 a')) (Eq.symm h)
                        (Eq.mp (congrArg (fun _a => _a) (propext Subgraph.mem_edgeSet)) he) ha))
              fun h =>
              And.casesOn h fun left hb =>
                Or.inr
                  (Exists.casesOn (Sum.isLeft_iff.mp hb) fun b' h =>
                    Eq.ndrec (motive := fun b => M.Adj a b → b.isLeft = true → Sum.inl 0 = b)
                      (fun he hb => congrArg Sum.inl (Subsingleton.elim 0 b')) (Eq.symm h)
                      (Eq.mp (congrArg (fun _a => _a) (propext Subgraph.mem_edgeSet)) he) hb)))
        he;
    Eq.mpr (id (congrArg (fun _a => _a) (propext Finset.card_le_one))) fun e he f hf =>
      Exists.casesOn (Sym2.mem_iff_exists.mp (hcenter e (Eq.mp (congrArg (fun _a => _a) (propext Set.mem_toFinset)) he)))
        fun y h =>
        Eq.ndrec (motive := fun e => e ∈ M.edgeSet → e = f)
          (fun he =>
            Exists.casesOn
              (Sym2.mem_iff_exists.mp (hcenter f (Eq.mp (congrArg (fun _a => _a) (propext Set.mem_toFinset)) hf)))
              fun z h =>
              Eq.ndrec (motive := fun f => f ∈ M.edgeSet → s(Sum.inl 0, y) = f)
                (fun hf =>
                  Eq.mpr
                    (id
                      (congrArg (fun _a => s(Sum.inl 0, _a) = s(Sum.inl 0, z))
                        (Subgraph.IsMatching.eq_of_adj_left hM
                          (Eq.mp (congrArg (fun _a => _a) (propext Subgraph.mem_edgeSet)) he)
                          (Eq.mp (congrArg (fun _a => _a) (propext Subgraph.mem_edgeSet)) hf))))
                    (Eq.refl s(Sum.inl 0, z)))
                (Eq.symm h) (Eq.mp (congrArg (fun _a => _a) (propext Set.mem_toFinset)) hf))
          (Eq.symm h) (Eq.mp (congrArg (fun _a => _a) (propext Set.mem_toFinset)) he)hbdd:BddAbove ((fun M => ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching}) := 
  Exists.intro 1 fun ⦃x⦄ a =>
    Exists.casesOn a fun M h =>
      And.casesOn h fun hM right =>
        right ▸
          id
            (cast
              (Eq.symm (Eq.trans (congrArg (LE.le ↑M.edgeSet.toFinset.card) (Eq.symm Nat.cast_one)) Nat.cast_le._simp_1))
              (hle M hM))⊢ (have matchings := {M | M.IsMatching};
  sSup ((fun M => ↑M.edgeSet.toFinset.card) '' matchings)) ≤
  1ahle:∀ (M : Star5.Subgraph), M.IsMatching → M.edgeSet.toFinset.card ≤ 1 := 
  fun M hM =>
    have hcenter := fun e he =>
      Sym2.inductionOn e
        (fun a b he =>
          have hadj := Subgraph.Adj.adj_sub (Eq.mp (congrArg (fun _a => _a) (propext Subgraph.mem_edgeSet)) he);
          Eq.mpr (id (congrArg (fun _a => _a) (propext Sym2.mem_iff)))
            (Or.casesOn hadj
              (fun h =>
                And.casesOn h fun ha right =>
                  Or.inl
                    (Exists.casesOn (Sum.isLeft_iff.mp ha) fun a' h =>
                      Eq.ndrec (motive := fun a => M.Adj a b → a.isLeft = true → Sum.inl 0 = a)
                        (fun he ha => congrArg Sum.inl (Subsingleton.elim 0 a')) (Eq.symm h)
                        (Eq.mp (congrArg (fun _a => _a) (propext Subgraph.mem_edgeSet)) he) ha))
              fun h =>
              And.casesOn h fun left hb =>
                Or.inr
                  (Exists.casesOn (Sum.isLeft_iff.mp hb) fun b' h =>
                    Eq.ndrec (motive := fun b => M.Adj a b → b.isLeft = true → Sum.inl 0 = b)
                      (fun he hb => congrArg Sum.inl (Subsingleton.elim 0 b')) (Eq.symm h)
                      (Eq.mp (congrArg (fun _a => _a) (propext Subgraph.mem_edgeSet)) he) hb)))
        he;
    Eq.mpr (id (congrArg (fun _a => _a) (propext Finset.card_le_one))) fun e he f hf =>
      Exists.casesOn (Sym2.mem_iff_exists.mp (hcenter e (Eq.mp (congrArg (fun _a => _a) (propext Set.mem_toFinset)) he)))
        fun y h =>
        Eq.ndrec (motive := fun e => e ∈ M.edgeSet → e = f)
          (fun he =>
            Exists.casesOn
              (Sym2.mem_iff_exists.mp (hcenter f (Eq.mp (congrArg (fun _a => _a) (propext Set.mem_toFinset)) hf)))
              fun z h =>
              Eq.ndrec (motive := fun f => f ∈ M.edgeSet → s(Sum.inl 0, y) = f)
                (fun hf =>
                  Eq.mpr
                    (id
                      (congrArg (fun _a => s(Sum.inl 0, _a) = s(Sum.inl 0, z))
                        (Subgraph.IsMatching.eq_of_adj_left hM
                          (Eq.mp (congrArg (fun _a => _a) (propext Subgraph.mem_edgeSet)) he)
                          (Eq.mp (congrArg (fun _a => _a) (propext Subgraph.mem_edgeSet)) hf))))
                    (Eq.refl s(Sum.inl 0, z)))
                (Eq.symm h) (Eq.mp (congrArg (fun _a => _a) (propext Set.mem_toFinset)) hf))
          (Eq.symm h) (Eq.mp (congrArg (fun _a => _a) (propext Set.mem_toFinset)) he)hbdd:BddAbove ((fun M => ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching}) := 
  Exists.intro 1 fun ⦃x⦄ a =>
    Exists.casesOn a fun M h =>
      And.casesOn h fun hM right =>
        right ▸
          id
            (cast
              (Eq.symm (Eq.trans (congrArg (LE.le ↑M.edgeSet.toFinset.card) (Eq.symm Nat.cast_one)) Nat.cast_le._simp_1))
              (hle M hM))⊢ 1 ≤
  have matchings := {M | M.IsMatching};
  sSup ((fun M => ↑M.edgeSet.toFinset.card) '' matchings)
  ·ahle:∀ (M : Star5.Subgraph), M.IsMatching → M.edgeSet.toFinset.card ≤ 1 := 
  fun M hM =>
    have hcenter := fun e he =>
      Sym2.inductionOn e
        (fun a b he =>
          have hadj := Subgraph.Adj.adj_sub (Eq.mp (congrArg (fun _a => _a) (propext Subgraph.mem_edgeSet)) he);
          Eq.mpr (id (congrArg (fun _a => _a) (propext Sym2.mem_iff)))
            (Or.casesOn hadj
              (fun h =>
                And.casesOn h fun ha right =>
                  Or.inl
                    (Exists.casesOn (Sum.isLeft_iff.mp ha) fun a' h =>
                      Eq.ndrec (motive := fun a => M.Adj a b → a.isLeft = true → Sum.inl 0 = a)
                        (fun he ha => congrArg Sum.inl (Subsingleton.elim 0 a')) (Eq.symm h)
                        (Eq.mp (congrArg (fun _a => _a) (propext Subgraph.mem_edgeSet)) he) ha))
              fun h =>
              And.casesOn h fun left hb =>
                Or.inr
                  (Exists.casesOn (Sum.isLeft_iff.mp hb) fun b' h =>
                    Eq.ndrec (motive := fun b => M.Adj a b → b.isLeft = true → Sum.inl 0 = b)
                      (fun he hb => congrArg Sum.inl (Subsingleton.elim 0 b')) (Eq.symm h)
                      (Eq.mp (congrArg (fun _a => _a) (propext Subgraph.mem_edgeSet)) he) hb)))
        he;
    Eq.mpr (id (congrArg (fun _a => _a) (propext Finset.card_le_one))) fun e he f hf =>
      Exists.casesOn (Sym2.mem_iff_exists.mp (hcenter e (Eq.mp (congrArg (fun _a => _a) (propext Set.mem_toFinset)) he)))
        fun y h =>
        Eq.ndrec (motive := fun e => e ∈ M.edgeSet → e = f)
          (fun he =>
            Exists.casesOn
              (Sym2.mem_iff_exists.mp (hcenter f (Eq.mp (congrArg (fun _a => _a) (propext Set.mem_toFinset)) hf)))
              fun z h =>
              Eq.ndrec (motive := fun f => f ∈ M.edgeSet → s(Sum.inl 0, y) = f)
                (fun hf =>
                  Eq.mpr
                    (id
                      (congrArg (fun _a => s(Sum.inl 0, _a) = s(Sum.inl 0, z))
                        (Subgraph.IsMatching.eq_of_adj_left hM
                          (Eq.mp (congrArg (fun _a => _a) (propext Subgraph.mem_edgeSet)) he)
                          (Eq.mp (congrArg (fun _a => _a) (propext Subgraph.mem_edgeSet)) hf))))
                    (Eq.refl s(Sum.inl 0, z)))
                (Eq.symm h) (Eq.mp (congrArg (fun _a => _a) (propext Set.mem_toFinset)) hf))
          (Eq.symm h) (Eq.mp (congrArg (fun _a => _a) (propext Set.mem_toFinset)) he)hbdd:BddAbove ((fun M => ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching}) := 
  Exists.intro 1 fun ⦃x⦄ a =>
    Exists.casesOn a fun M h =>
      And.casesOn h fun hM right =>
        right ▸
          id
            (cast
              (Eq.symm (Eq.trans (congrArg (LE.le ↑M.edgeSet.toFinset.card) (Eq.symm Nat.cast_one)) Nat.cast_le._simp_1))
              (hle M hM))⊢ (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 ≤ 1 := 
  fun M hM =>
    have hcenter := fun e he =>
      Sym2.inductionOn e
        (fun a b he =>
          have hadj := Subgraph.Adj.adj_sub (Eq.mp (congrArg (fun _a => _a) (propext Subgraph.mem_edgeSet)) he);
          Eq.mpr (id (congrArg (fun _a => _a) (propext Sym2.mem_iff)))
            (Or.casesOn hadj
              (fun h =>
                And.casesOn h fun ha right =>
                  Or.inl
                    (Exists.casesOn (Sum.isLeft_iff.mp ha) fun a' h =>
                      Eq.ndrec (motive := fun a => M.Adj a b → a.isLeft = true → Sum.inl 0 = a)
                        (fun he ha => congrArg Sum.inl (Subsingleton.elim 0 a')) (Eq.symm h)
                        (Eq.mp (congrArg (fun _a => _a) (propext Subgraph.mem_edgeSet)) he) ha))
              fun h =>
              And.casesOn h fun left hb =>
                Or.inr
                  (Exists.casesOn (Sum.isLeft_iff.mp hb) fun b' h =>
                    Eq.ndrec (motive := fun b => M.Adj a b → b.isLeft = true → Sum.inl 0 = b)
                      (fun he hb => congrArg Sum.inl (Subsingleton.elim 0 b')) (Eq.symm h)
                      (Eq.mp (congrArg (fun _a => _a) (propext Subgraph.mem_edgeSet)) he) hb)))
        he;
    Eq.mpr (id (congrArg (fun _a => _a) (propext Finset.card_le_one))) fun e he f hf =>
      Exists.casesOn (Sym2.mem_iff_exists.mp (hcenter e (Eq.mp (congrArg (fun _a => _a) (propext Set.mem_toFinset)) he)))
        fun y h =>
        Eq.ndrec (motive := fun e => e ∈ M.edgeSet → e = f)
          (fun he =>
            Exists.casesOn
              (Sym2.mem_iff_exists.mp (hcenter f (Eq.mp (congrArg (fun _a => _a) (propext Set.mem_toFinset)) hf)))
              fun z h =>
              Eq.ndrec (motive := fun f => f ∈ M.edgeSet → s(Sum.inl 0, y) = f)
                (fun hf =>
                  Eq.mpr
                    (id
                      (congrArg (fun _a => s(Sum.inl 0, _a) = s(Sum.inl 0, z))
                        (Subgraph.IsMatching.eq_of_adj_left hM
                          (Eq.mp (congrArg (fun _a => _a) (propext Subgraph.mem_edgeSet)) he)
                          (Eq.mp (congrArg (fun _a => _a) (propext Subgraph.mem_edgeSet)) hf))))
                    (Eq.refl s(Sum.inl 0, z)))
                (Eq.symm h) (Eq.mp (congrArg (fun _a => _a) (propext Set.mem_toFinset)) hf))
          (Eq.symm h) (Eq.mp (congrArg (fun _a => _a) (propext Set.mem_toFinset)) he)hbdd:BddAbove ((fun M => ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching}) := 
  Exists.intro 1 fun ⦃x⦄ a =>
    Exists.casesOn a fun M h =>
      And.casesOn h fun hM right =>
        right ▸
          id
            (cast
              (Eq.symm (Eq.trans (congrArg (LE.le ↑M.edgeSet.toFinset.card) (Eq.symm Nat.cast_one)) Nat.cast_le._simp_1))
              (hle M hM))⊢ ⊥ ∈ {M | M.IsMatching} simp [Subgraph.IsMatching]All goals completed! 🐙⟩)
    rintro x ⟨M, hM, rfl⟩ahle:∀ (M : Star5.Subgraph), M.IsMatching → M.edgeSet.toFinset.card ≤ 1 := 
  fun M hM =>
    have hcenter := fun e he =>
      Sym2.inductionOn e
        (fun a b he =>
          have hadj := Subgraph.Adj.adj_sub (Eq.mp (congrArg (fun _a => _a) (propext Subgraph.mem_edgeSet)) he);
          Eq.mpr (id (congrArg (fun _a => _a) (propext Sym2.mem_iff)))
            (Or.casesOn hadj
              (fun h =>
                And.casesOn h fun ha right =>
                  Or.inl
                    (Exists.casesOn (Sum.isLeft_iff.mp ha) fun a' h =>
                      Eq.ndrec (motive := fun a => M.Adj a b → a.isLeft = true → Sum.inl 0 = a)
                        (fun he ha => congrArg Sum.inl (Subsingleton.elim 0 a')) (Eq.symm h)
                        (Eq.mp (congrArg (fun _a => _a) (propext Subgraph.mem_edgeSet)) he) ha))
              fun h =>
              And.casesOn h fun left hb =>
                Or.inr
                  (Exists.casesOn (Sum.isLeft_iff.mp hb) fun b' h =>
                    Eq.ndrec (motive := fun b => M.Adj a b → b.isLeft = true → Sum.inl 0 = b)
                      (fun he hb => congrArg Sum.inl (Subsingleton.elim 0 b')) (Eq.symm h)
                      (Eq.mp (congrArg (fun _a => _a) (propext Subgraph.mem_edgeSet)) he) hb)))
        he;
    Eq.mpr (id (congrArg (fun _a => _a) (propext Finset.card_le_one))) fun e he f hf =>
      Exists.casesOn (Sym2.mem_iff_exists.mp (hcenter e (Eq.mp (congrArg (fun _a => _a) (propext Set.mem_toFinset)) he)))
        fun y h =>
        Eq.ndrec (motive := fun e => e ∈ M.edgeSet → e = f)
          (fun he =>
            Exists.casesOn
              (Sym2.mem_iff_exists.mp (hcenter f (Eq.mp (congrArg (fun _a => _a) (propext Set.mem_toFinset)) hf)))
              fun z h =>
              Eq.ndrec (motive := fun f => f ∈ M.edgeSet → s(Sum.inl 0, y) = f)
                (fun hf =>
                  Eq.mpr
                    (id
                      (congrArg (fun _a => s(Sum.inl 0, _a) = s(Sum.inl 0, z))
                        (Subgraph.IsMatching.eq_of_adj_left hM
                          (Eq.mp (congrArg (fun _a => _a) (propext Subgraph.mem_edgeSet)) he)
                          (Eq.mp (congrArg (fun _a => _a) (propext Subgraph.mem_edgeSet)) hf))))
                    (Eq.refl s(Sum.inl 0, z)))
                (Eq.symm h) (Eq.mp (congrArg (fun _a => _a) (propext Set.mem_toFinset)) hf))
          (Eq.symm h) (Eq.mp (congrArg (fun _a => _a) (propext Set.mem_toFinset)) he)hbdd:BddAbove ((fun M => ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching}) := 
  Exists.intro 1 fun ⦃x⦄ a =>
    Exists.casesOn a fun M h =>
      And.casesOn h fun hM right =>
        right ▸
          id
            (cast
              (Eq.symm (Eq.trans (congrArg (LE.le ↑M.edgeSet.toFinset.card) (Eq.symm Nat.cast_one)) Nat.cast_le._simp_1))
              (hle M hM))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 ≤ 1 := 
  fun M hM =>
    have hcenter := fun e he =>
      Sym2.inductionOn e
        (fun a b he =>
          have hadj := Subgraph.Adj.adj_sub (Eq.mp (congrArg (fun _a => _a) (propext Subgraph.mem_edgeSet)) he);
          Eq.mpr (id (congrArg (fun _a => _a) (propext Sym2.mem_iff)))
            (Or.casesOn hadj
              (fun h =>
                And.casesOn h fun ha right =>
                  Or.inl
                    (Exists.casesOn (Sum.isLeft_iff.mp ha) fun a' h =>
                      Eq.ndrec (motive := fun a => M.Adj a b → a.isLeft = true → Sum.inl 0 = a)
                        (fun he ha => congrArg Sum.inl (Subsingleton.elim 0 a')) (Eq.symm h)
                        (Eq.mp (congrArg (fun _a => _a) (propext Subgraph.mem_edgeSet)) he) ha))
              fun h =>
              And.casesOn h fun left hb =>
                Or.inr
                  (Exists.casesOn (Sum.isLeft_iff.mp hb) fun b' h =>
                    Eq.ndrec (motive := fun b => M.Adj a b → b.isLeft = true → Sum.inl 0 = b)
                      (fun he hb => congrArg Sum.inl (Subsingleton.elim 0 b')) (Eq.symm h)
                      (Eq.mp (congrArg (fun _a => _a) (propext Subgraph.mem_edgeSet)) he) hb)))
        he;
    Eq.mpr (id (congrArg (fun _a => _a) (propext Finset.card_le_one))) fun e he f hf =>
      Exists.casesOn (Sym2.mem_iff_exists.mp (hcenter e (Eq.mp (congrArg (fun _a => _a) (propext Set.mem_toFinset)) he)))
        fun y h =>
        Eq.ndrec (motive := fun e => e ∈ M.edgeSet → e = f)
          (fun he =>
            Exists.casesOn
              (Sym2.mem_iff_exists.mp (hcenter f (Eq.mp (congrArg (fun _a => _a) (propext Set.mem_toFinset)) hf)))
              fun z h =>
              Eq.ndrec (motive := fun f => f ∈ M.edgeSet → s(Sum.inl 0, y) = f)
                (fun hf =>
                  Eq.mpr
                    (id
                      (congrArg (fun _a => s(Sum.inl 0, _a) = s(Sum.inl 0, z))
                        (Subgraph.IsMatching.eq_of_adj_left hM
                          (Eq.mp (congrArg (fun _a => _a) (propext Subgraph.mem_edgeSet)) he)
                          (Eq.mp (congrArg (fun _a => _a) (propext Subgraph.mem_edgeSet)) hf))))
                    (Eq.refl s(Sum.inl 0, z)))
                (Eq.symm h) (Eq.mp (congrArg (fun _a => _a) (propext Set.mem_toFinset)) hf))
          (Eq.symm h) (Eq.mp (congrArg (fun _a => _a) (propext Set.mem_toFinset)) he)hbdd:BddAbove ((fun M => ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching}) := 
  Exists.intro 1 fun ⦃x⦄ a =>
    Exists.casesOn a fun M h =>
      And.casesOn h fun hM right =>
        right ▸
          id
            (cast
              (Eq.symm (Eq.trans (congrArg (LE.le ↑M.edgeSet.toFinset.card) (Eq.symm Nat.cast_one)) Nat.cast_le._simp_1))
              (hle M hM))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 ≤ 1 := 
  fun M hM =>
    have hcenter := fun e he =>
      Sym2.inductionOn e
        (fun a b he =>
          have hadj := Subgraph.Adj.adj_sub (Eq.mp (congrArg (fun _a => _a) (propext Subgraph.mem_edgeSet)) he);
          Eq.mpr (id (congrArg (fun _a => _a) (propext Sym2.mem_iff)))
            (Or.casesOn hadj
              (fun h =>
                And.casesOn h fun ha right =>
                  Or.inl
                    (Exists.casesOn (Sum.isLeft_iff.mp ha) fun a' h =>
                      Eq.ndrec (motive := fun a => M.Adj a b → a.isLeft = true → Sum.inl 0 = a)
                        (fun he ha => congrArg Sum.inl (Subsingleton.elim 0 a')) (Eq.symm h)
                        (Eq.mp (congrArg (fun _a => _a) (propext Subgraph.mem_edgeSet)) he) ha))
              fun h =>
              And.casesOn h fun left hb =>
                Or.inr
                  (Exists.casesOn (Sum.isLeft_iff.mp hb) fun b' h =>
                    Eq.ndrec (motive := fun b => M.Adj a b → b.isLeft = true → Sum.inl 0 = b)
                      (fun he hb => congrArg Sum.inl (Subsingleton.elim 0 b')) (Eq.symm h)
                      (Eq.mp (congrArg (fun _a => _a) (propext Subgraph.mem_edgeSet)) he) hb)))
        he;
    Eq.mpr (id (congrArg (fun _a => _a) (propext Finset.card_le_one))) fun e he f hf =>
      Exists.casesOn (Sym2.mem_iff_exists.mp (hcenter e (Eq.mp (congrArg (fun _a => _a) (propext Set.mem_toFinset)) he)))
        fun y h =>
        Eq.ndrec (motive := fun e => e ∈ M.edgeSet → e = f)
          (fun he =>
            Exists.casesOn
              (Sym2.mem_iff_exists.mp (hcenter f (Eq.mp (congrArg (fun _a => _a) (propext Set.mem_toFinset)) hf)))
              fun z h =>
              Eq.ndrec (motive := fun f => f ∈ M.edgeSet → s(Sum.inl 0, y) = f)
                (fun hf =>
                  Eq.mpr
                    (id
                      (congrArg (fun _a => s(Sum.inl 0, _a) = s(Sum.inl 0, z))
                        (Subgraph.IsMatching.eq_of_adj_left hM
                          (Eq.mp (congrArg (fun _a => _a) (propext Subgraph.mem_edgeSet)) he)
                          (Eq.mp (congrArg (fun _a => _a) (propext Subgraph.mem_edgeSet)) hf))))
                    (Eq.refl s(Sum.inl 0, z)))
                (Eq.symm h) (Eq.mp (congrArg (fun _a => _a) (propext Set.mem_toFinset)) hf))
          (Eq.symm h) (Eq.mp (congrArg (fun _a => _a) (propext Set.mem_toFinset)) he)hbdd:BddAbove ((fun M => ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching}) := 
  Exists.intro 1 fun ⦃x⦄ a =>
    Exists.casesOn a fun M h =>
      And.casesOn h fun hM right =>
        right ▸
          id
            (cast
              (Eq.symm (Eq.trans (congrArg (LE.le ↑M.edgeSet.toFinset.card) (Eq.symm Nat.cast_one)) Nat.cast_le._simp_1))
              (hle M hM))⊢ 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 ≤ 1 := 
  fun M hM =>
    have hcenter := fun e he =>
      Sym2.inductionOn e
        (fun a b he =>
          have hadj := Subgraph.Adj.adj_sub (Eq.mp (congrArg (fun _a => _a) (propext Subgraph.mem_edgeSet)) he);
          Eq.mpr (id (congrArg (fun _a => _a) (propext Sym2.mem_iff)))
            (Or.casesOn hadj
              (fun h =>
                And.casesOn h fun ha right =>
                  Or.inl
                    (Exists.casesOn (Sum.isLeft_iff.mp ha) fun a' h =>
                      Eq.ndrec (motive := fun a => M.Adj a b → a.isLeft = true → Sum.inl 0 = a)
                        (fun he ha => congrArg Sum.inl (Subsingleton.elim 0 a')) (Eq.symm h)
                        (Eq.mp (congrArg (fun _a => _a) (propext Subgraph.mem_edgeSet)) he) ha))
              fun h =>
              And.casesOn h fun left hb =>
                Or.inr
                  (Exists.casesOn (Sum.isLeft_iff.mp hb) fun b' h =>
                    Eq.ndrec (motive := fun b => M.Adj a b → b.isLeft = true → Sum.inl 0 = b)
                      (fun he hb => congrArg Sum.inl (Subsingleton.elim 0 b')) (Eq.symm h)
                      (Eq.mp (congrArg (fun _a => _a) (propext Subgraph.mem_edgeSet)) he) hb)))
        he;
    Eq.mpr (id (congrArg (fun _a => _a) (propext Finset.card_le_one))) fun e he f hf =>
      Exists.casesOn (Sym2.mem_iff_exists.mp (hcenter e (Eq.mp (congrArg (fun _a => _a) (propext Set.mem_toFinset)) he)))
        fun y h =>
        Eq.ndrec (motive := fun e => e ∈ M.edgeSet → e = f)
          (fun he =>
            Exists.casesOn
              (Sym2.mem_iff_exists.mp (hcenter f (Eq.mp (congrArg (fun _a => _a) (propext Set.mem_toFinset)) hf)))
              fun z h =>
              Eq.ndrec (motive := fun f => f ∈ M.edgeSet → s(Sum.inl 0, y) = f)
                (fun hf =>
                  Eq.mpr
                    (id
                      (congrArg (fun _a => s(Sum.inl 0, _a) = s(Sum.inl 0, z))
                        (Subgraph.IsMatching.eq_of_adj_left hM
                          (Eq.mp (congrArg (fun _a => _a) (propext Subgraph.mem_edgeSet)) he)
                          (Eq.mp (congrArg (fun _a => _a) (propext Subgraph.mem_edgeSet)) hf))))
                    (Eq.refl s(Sum.inl 0, z)))
                (Eq.symm h) (Eq.mp (congrArg (fun _a => _a) (propext Set.mem_toFinset)) hf))
          (Eq.symm h) (Eq.mp (congrArg (fun _a => _a) (propext Set.mem_toFinset)) he)hbdd:BddAbove ((fun M => ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching}) := 
  Exists.intro 1 fun ⦃x⦄ a =>
    Exists.casesOn a fun M h =>
      And.casesOn h fun hM right =>
        right ▸
          id
            (cast
              (Eq.symm (Eq.trans (congrArg (LE.le ↑M.edgeSet.toFinset.card) (Eq.symm Nat.cast_one)) Nat.cast_le._simp_1))
              (hle M hM))⊢ 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 ≤ 1 := 
  fun M hM =>
    have hcenter := fun e he =>
      Sym2.inductionOn e
        (fun a b he =>
          have hadj := Subgraph.Adj.adj_sub (Eq.mp (congrArg (fun _a => _a) (propext Subgraph.mem_edgeSet)) he);
          Eq.mpr (id (congrArg (fun _a => _a) (propext Sym2.mem_iff)))
            (Or.casesOn hadj
              (fun h =>
                And.casesOn h fun ha right =>
                  Or.inl
                    (Exists.casesOn (Sum.isLeft_iff.mp ha) fun a' h =>
                      Eq.ndrec (motive := fun a => M.Adj a b → a.isLeft = true → Sum.inl 0 = a)
                        (fun he ha => congrArg Sum.inl (Subsingleton.elim 0 a')) (Eq.symm h)
                        (Eq.mp (congrArg (fun _a => _a) (propext Subgraph.mem_edgeSet)) he) ha))
              fun h =>
              And.casesOn h fun left hb =>
                Or.inr
                  (Exists.casesOn (Sum.isLeft_iff.mp hb) fun b' h =>
                    Eq.ndrec (motive := fun b => M.Adj a b → b.isLeft = true → Sum.inl 0 = b)
                      (fun he hb => congrArg Sum.inl (Subsingleton.elim 0 b')) (Eq.symm h)
                      (Eq.mp (congrArg (fun _a => _a) (propext Subgraph.mem_edgeSet)) he) hb)))
        he;
    Eq.mpr (id (congrArg (fun _a => _a) (propext Finset.card_le_one))) fun e he f hf =>
      Exists.casesOn (Sym2.mem_iff_exists.mp (hcenter e (Eq.mp (congrArg (fun _a => _a) (propext Set.mem_toFinset)) he)))
        fun y h =>
        Eq.ndrec (motive := fun e => e ∈ M.edgeSet → e = f)
          (fun he =>
            Exists.casesOn
              (Sym2.mem_iff_exists.mp (hcenter f (Eq.mp (congrArg (fun _a => _a) (propext Set.mem_toFinset)) hf)))
              fun z h =>
              Eq.ndrec (motive := fun f => f ∈ M.edgeSet → s(Sum.inl 0, y) = f)
                (fun hf =>
                  Eq.mpr
                    (id
                      (congrArg (fun _a => s(Sum.inl 0, _a) = s(Sum.inl 0, z))
                        (Subgraph.IsMatching.eq_of_adj_left hM
                          (Eq.mp (congrArg (fun _a => _a) (propext Subgraph.mem_edgeSet)) he)
                          (Eq.mp (congrArg (fun _a => _a) (propext Subgraph.mem_edgeSet)) hf))))
                    (Eq.refl s(Sum.inl 0, z)))
                (Eq.symm h) (Eq.mp (congrArg (fun _a => _a) (propext Set.mem_toFinset)) hf))
          (Eq.symm h) (Eq.mp (congrArg (fun _a => _a) (propext Set.mem_toFinset)) he)hbdd:BddAbove ((fun M => ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching}) := 
  Exists.intro 1 fun ⦃x⦄ a =>
    Exists.casesOn a fun M h =>
      And.casesOn h fun hM right =>
        right ▸
          id
            (cast
              (Eq.symm (Eq.trans (congrArg (LE.le ↑M.edgeSet.toFinset.card) (Eq.symm Nat.cast_one)) Nat.cast_le._simp_1))
              (hle M hM))⊢ Star5.subgraphOfAdj ⋯ ∈ {M | M.IsMatching} exact Subgraph.IsMatching.subgraphOfAdj _All goals completed! 🐙
    ·a.refine_2hle:∀ (M : Star5.Subgraph), M.IsMatching → M.edgeSet.toFinset.card ≤ 1 := 
  fun M hM =>
    have hcenter := fun e he =>
      Sym2.inductionOn e
        (fun a b he =>
          have hadj := Subgraph.Adj.adj_sub (Eq.mp (congrArg (fun _a => _a) (propext Subgraph.mem_edgeSet)) he);
          Eq.mpr (id (congrArg (fun _a => _a) (propext Sym2.mem_iff)))
            (Or.casesOn hadj
              (fun h =>
                And.casesOn h fun ha right =>
                  Or.inl
                    (Exists.casesOn (Sum.isLeft_iff.mp ha) fun a' h =>
                      Eq.ndrec (motive := fun a => M.Adj a b → a.isLeft = true → Sum.inl 0 = a)
                        (fun he ha => congrArg Sum.inl (Subsingleton.elim 0 a')) (Eq.symm h)
                        (Eq.mp (congrArg (fun _a => _a) (propext Subgraph.mem_edgeSet)) he) ha))
              fun h =>
              And.casesOn h fun left hb =>
                Or.inr
                  (Exists.casesOn (Sum.isLeft_iff.mp hb) fun b' h =>
                    Eq.ndrec (motive := fun b => M.Adj a b → b.isLeft = true → Sum.inl 0 = b)
                      (fun he hb => congrArg Sum.inl (Subsingleton.elim 0 b')) (Eq.symm h)
                      (Eq.mp (congrArg (fun _a => _a) (propext Subgraph.mem_edgeSet)) he) hb)))
        he;
    Eq.mpr (id (congrArg (fun _a => _a) (propext Finset.card_le_one))) fun e he f hf =>
      Exists.casesOn (Sym2.mem_iff_exists.mp (hcenter e (Eq.mp (congrArg (fun _a => _a) (propext Set.mem_toFinset)) he)))
        fun y h =>
        Eq.ndrec (motive := fun e => e ∈ M.edgeSet → e = f)
          (fun he =>
            Exists.casesOn
              (Sym2.mem_iff_exists.mp (hcenter f (Eq.mp (congrArg (fun _a => _a) (propext Set.mem_toFinset)) hf)))
              fun z h =>
              Eq.ndrec (motive := fun f => f ∈ M.edgeSet → s(Sum.inl 0, y) = f)
                (fun hf =>
                  Eq.mpr
                    (id
                      (congrArg (fun _a => s(Sum.inl 0, _a) = s(Sum.inl 0, z))
                        (Subgraph.IsMatching.eq_of_adj_left hM
                          (Eq.mp (congrArg (fun _a => _a) (propext Subgraph.mem_edgeSet)) he)
                          (Eq.mp (congrArg (fun _a => _a) (propext Subgraph.mem_edgeSet)) hf))))
                    (Eq.refl s(Sum.inl 0, z)))
                (Eq.symm h) (Eq.mp (congrArg (fun _a => _a) (propext Set.mem_toFinset)) hf))
          (Eq.symm h) (Eq.mp (congrArg (fun _a => _a) (propext Set.mem_toFinset)) he)hbdd:BddAbove ((fun M => ↑M.edgeSet.toFinset.card) '' {M | M.IsMatching}) := 
  Exists.intro 1 fun ⦃x⦄ a =>
    Exists.casesOn a fun M h =>
      And.casesOn h fun hM right =>
        right ▸
          id
            (cast
              (Eq.symm (Eq.trans (congrArg (LE.le ↑M.edgeSet.toFinset.card) (Eq.symm Nat.cast_one)) Nat.cast_le._simp_1))
              (hle M hM))⊢ (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 declaration uses 'sorry'Star5_cvetkovic : cvetkovic Star5 = 5 := by⊢ Star5.cvetkovic = 5
  sorryAll goals completed! 🐙


end WrittenOnTheWallII.Test