Test.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 10 curated AI-written annotations and 7190 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

91 declarations, 7 contain sorry, 0 declared as axioms

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.

Imports (5)

Imported by 1 file

FormalConjectures/Subsets/FC100SolvedSet1.lean

abbrev WrittenOnTheWallII.Test.HouseGraph House Graph: Square 0-1-2-3-0 with roof 4 connected to 2,3 line 54 source
Source documentation
House Graph: Square 0-1-2-3-0 with roof 4 connected to 2,3.

standard axioms: Quot.sound, propext what this means
Statement uses: SimpleGraph, Fin, OfNat.ofNat, Nat
Proof uses: SimpleGraph.fromEdgeSet, Insert.insert, Sym2, Set, Sym2.mk, Singleton.singleton
6 instances, coercions and auxiliary constants left out.
```
abbrev HouseGraph : SimpleGraph (Fin 5) :=
…
```
abbrev WrittenOnTheWallII.Test.K4 K4: Complete graph on 4 vertices line 61 source
Source documentation
K4: Complete graph on 4 vertices.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SimpleGraph, Fin, OfNat.ofNat, Nat
Proof uses: SimpleGraph.completeGraph
2 instances, coercions and auxiliary constants left out.
```
abbrev K4 : SimpleGraph (Fin 4) := completeGraph (Fin 4)
```
abbrev WrittenOnTheWallII.Test.PetersenGraph Petersen Graph on 10 vertices line 64 source
Source documentation
Petersen Graph on 10 vertices.

standard axioms: Quot.sound, propext what this means
Statement uses: SimpleGraph, Fin, OfNat.ofNat, Nat
Proof uses: SimpleGraph.fromEdgeSet, Insert.insert, Sym2, Set, Sym2.mk, Singleton.singleton
6 instances, coercions and auxiliary constants left out.
```
abbrev PetersenGraph : SimpleGraph (Fin 10) :=
…
```
abbrev WrittenOnTheWallII.Test.C6 C6: Cycle graph on 6 vertices line 75 source
Source documentation
C6: Cycle graph on 6 vertices.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SimpleGraph, Fin, OfNat.ofNat, Nat
Proof uses: SimpleGraph.cycleGraph
2 instances, coercions and auxiliary constants left out.
```
abbrev C6 : SimpleGraph (Fin 6) := cycleGraph 6
```
abbrev WrittenOnTheWallII.Test.Star5 Star5: Star graph with center 0 and 5 leaves line 78 source
Source documentation
Star5: Star graph with center 0 and 5 leaves.

standard axioms: Quot.sound, propext what this means
Statement uses: SimpleGraph, Sum, Fin, OfNat.ofNat, Nat
Proof uses: completeBipartiteGraph
2 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
abbrev Star5 : SimpleGraph (Fin 1 ⊕ Fin 5) := completeBipartiteGraph (Fin 1) (Fin 5)
```
instance WrittenOnTheWallII.Test.(instance at line 80) line 80 source
theorem WrittenOnTheWallII.Test.house_indep line 86 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, SimpleGraph.indepNum, Fin, OfNat.ofNat, WrittenOnTheWallII.Test.HouseGraph
Proof uses: Eq.mpr, SimpleGraph.computable_indep_num, Insert.insert, Sym2, Set, Sym2.mk, Singleton.singleton, id, congrArg, SimpleGraph.indep_num_eq_computable, of_decide_eq_true, Bool, Decidable.decide, Bool.true, Eq.refl
13 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem WrittenOnTheWallII.Test.house_dom line 91 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, SimpleGraph.dominationNumber, Fin, OfNat.ofNat, WrittenOnTheWallII.Test.HouseGraph
Proof uses: Eq.mpr, SimpleGraph.computable_dom_num, Insert.insert, Sym2, Set, Sym2.mk, Singleton.singleton, id, congrArg, SimpleGraph.dom_num_eq_computable
13 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem WrittenOnTheWallII.Test.house_avg_dist line 95 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Real, SimpleGraph.averageDistance, Fin, OfNat.ofNat, Nat, WrittenOnTheWallII.Test.HouseGraph, HDiv.hDiv
Proof uses: Eq.mpr, SimpleGraph.computable_avg_dist, Insert.insert, Sym2, Set, Sym2.mk, Singleton.singleton, id, congrArg, SimpleGraph.avg_dist_eq_computable, Rat, Mathlib.Meta.NormNum.isNNRat_eq_true, inferInstance, DivisionSemiring, Mathlib.Meta.NormNum.isNNRat_ratCast, Mathlib.Meta.NormNum.isNNRat_div, Mathlib.Meta.NormNum.isNNRat_mul, HMul.hMul, Inv.inv, Eq.refl and 5 more
62 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
theorem WrittenOnTheWallII.Test.house_diameter line 101 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, ENat, SimpleGraph.ediam, Fin, OfNat.ofNat, Nat, WrittenOnTheWallII.Test.HouseGraph
Proof uses: Eq.mpr, SimpleGraph.computable_ediam, Insert.insert, Sym2, Set, Sym2.mk, Singleton.singleton, id, congrArg, SimpleGraph.ediam_eq_computable, of_decide_eq_true, SimpleGraph.Connected, Bool, Decidable.decide, Bool.true, Eq.refl, cast, Eq.symm
29 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
theorem WrittenOnTheWallII.Test.house_radius line 106 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, ENat, SimpleGraph.radius, Fin, OfNat.ofNat, Nat, WrittenOnTheWallII.Test.HouseGraph
Proof uses: Eq.mpr, SimpleGraph.computable_radius, Insert.insert, Sym2, Set, Sym2.mk, Singleton.singleton, id, congrArg, SimpleGraph.radius_eq_computable, of_decide_eq_true, SimpleGraph.Connected, Bool, Decidable.decide, Bool.true, Eq.refl, cast, Eq.symm
29 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
theorem WrittenOnTheWallII.Test.house_girth line 111 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, SimpleGraph.girth, Fin, OfNat.ofNat, WrittenOnTheWallII.Test.HouseGraph
Proof uses: SimpleGraph.Walk.IsCycle, SimpleGraph.Walk.cons, SimpleGraph.Adj, of_decide_eq_true, Insert.insert, Sym2, Set, Sym2.mk, Singleton.singleton, id, Bool, Decidable.decide, Bool.true, Eq.refl, SimpleGraph.Walk.nil, Eq.mpr, And, SimpleGraph.Walk.IsTrail, Ne, SimpleGraph.Walk and 26 more
21 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
theorem WrittenOnTheWallII.Test.house_order line 125 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, Fintype.card, Fin, OfNat.ofNat, SimpleGraph.Subgraph.verts, WrittenOnTheWallII.Test.HouseGraph, Top.top, SimpleGraph.Subgraph, Membership.mem, Set, Classical.propDecidable
Proof uses: Eq.mpr, id, congrArg, Fintype.card_congr, RelIso.toEquiv, SimpleGraph.Adj, SimpleGraph.Subgraph.coe, SimpleGraph.Subgraph.topIso, Eq.refl
12 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem WrittenOnTheWallII.Test.house_size line 130 source
extra axioms: _private.0.WrittenOnTheWallII.Test.house_size._native.decide.ax_1 what this means
Statement uses: Eq, Nat, Finset.card, Sym2, Fin, OfNat.ofNat, SimpleGraph.edgeFinset, WrittenOnTheWallII.Test.HouseGraph, Insert.insert, Set, Sym2.mk, Singleton.singleton
Proof uses: of_decide_eq_true
22 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem WrittenOnTheWallII.Test.house_szeged line 134 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, SimpleGraph.szegedIndex, Fin, OfNat.ofNat, WrittenOnTheWallII.Test.HouseGraph, Insert.insert, Sym2, Set, Sym2.mk, Singleton.singleton
Proof uses: Eq.mpr, SimpleGraph.computable_szeged_index, id, congrArg, SimpleGraph.szeged_eq_computable
23 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem WrittenOnTheWallII.Test.house_wiener line 138 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, SimpleGraph.wienerIndex, Fin, OfNat.ofNat, WrittenOnTheWallII.Test.HouseGraph
Proof uses: Eq.mpr, SimpleGraph.computable_wiener, Insert.insert, Sym2, Set, Sym2.mk, Singleton.singleton, id, congrArg, SimpleGraph.wiener_eq_computable
14 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem WrittenOnTheWallII.Test.house_min_deg line 142 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, SimpleGraph.minDegree, Fin, OfNat.ofNat, WrittenOnTheWallII.Test.HouseGraph, Insert.insert, Sym2, Set, Sym2.mk, Singleton.singleton
12 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem WrittenOnTheWallII.Test.house_max_deg line 146 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, SimpleGraph.maxDegree, Fin, OfNat.ofNat, WrittenOnTheWallII.Test.HouseGraph, Insert.insert, Sym2, Set, Sym2.mk, Singleton.singleton
12 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem WrittenOnTheWallII.Test.house_avg_deg line 150 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Rat, SimpleGraph.averageDegree, Fin, OfNat.ofNat, Nat, WrittenOnTheWallII.Test.HouseGraph, Insert.insert, Sym2, Set, Sym2.mk, Singleton.singleton, HDiv.hDiv
Proof uses: id, Eq.mpr, Finset.sum, Finset.univ, SimpleGraph.degree, Membership.mem, SimpleGraph.neighborSet, Fintype.card, Eq.trans, congrFun', congrArg, Fintype.card_fin, of_eq_true, Not, False, True, not_false_eq_true
54 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
theorem WrittenOnTheWallII.Test.house_matching line 154 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Real, SimpleGraph.matchingNumber, Fin, OfNat.ofNat, Nat, WrittenOnTheWallII.Test.HouseGraph, Insert.insert, Sym2, Set, Sym2.mk, Singleton.singleton
Proof uses: BddAbove, Set.image, SimpleGraph.Subgraph, Finset.card, Set.toFinset, SimpleGraph.Subgraph.edgeSet, Membership.mem, Classical.propDecidable, Set.ofPred, SimpleGraph.Subgraph.IsMatching, Exists.intro, upperBounds, Fintype.card, And, LE.le, id, HMul.hMul, SimpleGraph.matching_card_bound, cast, Eq.symm and 62 more
106 instances, coercions and auxiliary constants left out.

Tactic trace: 30 steps
Open to load the checked before-and-after goal states.
theorem WrittenOnTheWallII.Test.house_residue line 177 source
extra axioms: _private.0.WrittenOnTheWallII.Test.house_residue._native.decide.ax_1 what this means
Statement uses: Eq, Nat, SimpleGraph.residue, Fin, OfNat.ofNat, WrittenOnTheWallII.Test.HouseGraph, Insert.insert, Sym2, Set, Sym2.mk, Singleton.singleton
Proof uses: id, of_decide_eq_true, SimpleGraph.residueAux, Multiset.sort, Multiset.map, SimpleGraph.degree, Membership.mem, SimpleGraph.neighborSet, Finset.val, Finset.univ, GE.ge
35 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem WrittenOnTheWallII.Test.house_annihilation line 181 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, SimpleGraph.annihilationNumber, Fin, OfNat.ofNat, WrittenOnTheWallII.Test.HouseGraph, Insert.insert, Sym2, Set, Sym2.mk, Singleton.singleton
12 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem WrittenOnTheWallII.Test.house_cvetkovic sorry line 185 source
depends on sorry what this means
Statement uses: Eq, Nat, SimpleGraph.cvetkovic, Fin, OfNat.ofNat, WrittenOnTheWallII.Test.HouseGraph, Insert.insert, Sym2, Set, Sym2.mk, Singleton.singleton
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
22 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem WrittenOnTheWallII.Test.K4_indep line 192 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, SimpleGraph.indepNum, Fin, OfNat.ofNat, WrittenOnTheWallII.Test.K4
Proof uses: Eq.mpr, SimpleGraph.computable_indep_num, id, congrArg, SimpleGraph.indep_num_eq_computable
6 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem WrittenOnTheWallII.Test.K4_dom line 196 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, SimpleGraph.dominationNumber, Fin, OfNat.ofNat, WrittenOnTheWallII.Test.K4
Proof uses: Eq.mpr, SimpleGraph.computable_dom_num, id, congrArg, SimpleGraph.dom_num_eq_computable
6 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem WrittenOnTheWallII.Test.K4_avg_dist line 200 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Real, SimpleGraph.averageDistance, Fin, OfNat.ofNat, Nat, WrittenOnTheWallII.Test.K4
Proof uses: Eq.mpr, SimpleGraph.computable_avg_dist, id, congrArg, SimpleGraph.avg_dist_eq_computable, Rat, Mathlib.Meta.NormNum.isNat_eq_true, Mathlib.Meta.NormNum.isNat_ratCast, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Nat.cast_one
20 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
theorem WrittenOnTheWallII.Test.K4_diameter line 205 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, ENat, SimpleGraph.ediam, Fin, OfNat.ofNat, Nat, WrittenOnTheWallII.Test.K4
Proof uses: Eq.mpr, SimpleGraph.computable_ediam, id, congrArg, SimpleGraph.ediam_eq_computable, of_decide_eq_true, SimpleGraph.Connected, Bool, Decidable.decide, Bool.true, Eq.refl, cast, Eq.symm, Eq.trans, Nat.cast_one
21 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
theorem WrittenOnTheWallII.Test.K4_radius line 210 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, ENat, SimpleGraph.radius, Fin, OfNat.ofNat, Nat, WrittenOnTheWallII.Test.K4
Proof uses: Eq.mpr, SimpleGraph.computable_radius, id, congrArg, SimpleGraph.radius_eq_computable, of_decide_eq_true, SimpleGraph.Connected, Bool, Decidable.decide, Bool.true, Eq.refl, cast, Eq.symm, Eq.trans, Nat.cast_one
21 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
theorem WrittenOnTheWallII.Test.K4_girth line 215 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, SimpleGraph.girth, Fin, OfNat.ofNat, WrittenOnTheWallII.Test.K4
Proof uses: SimpleGraph.Walk.IsCycle, SimpleGraph.Walk.cons, SimpleGraph.Adj, of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl, SimpleGraph.Walk.nil, Eq.mpr, And, SimpleGraph.Walk.IsTrail, Ne, SimpleGraph.Walk, List.Nodup, List.tail, SimpleGraph.Walk.support, congrArg, propext and 24 more
22 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
theorem WrittenOnTheWallII.Test.K4_order line 229 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, Fintype.card, Fin, OfNat.ofNat, SimpleGraph.Subgraph.verts, WrittenOnTheWallII.Test.K4, Top.top, SimpleGraph.Subgraph, Membership.mem, Set, Classical.propDecidable
Proof uses: Eq.mpr, id, congrArg, Fintype.card_congr, RelIso.toEquiv, SimpleGraph.Adj, SimpleGraph.Subgraph.coe, SimpleGraph.Subgraph.topIso, Eq.refl
12 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem WrittenOnTheWallII.Test.K4_size line 234 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, Finset.card, Sym2, Fin, OfNat.ofNat, SimpleGraph.edgeFinset, WrittenOnTheWallII.Test.K4
7 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem WrittenOnTheWallII.Test.K4_szeged line 238 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, SimpleGraph.szegedIndex, Fin, OfNat.ofNat, WrittenOnTheWallII.Test.K4
Proof uses: Eq.mpr, SimpleGraph.computable_szeged_index, id, congrArg, SimpleGraph.szeged_eq_computable
9 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem WrittenOnTheWallII.Test.K4_wiener line 242 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, SimpleGraph.wienerIndex, Fin, OfNat.ofNat, WrittenOnTheWallII.Test.K4
Proof uses: Eq.mpr, SimpleGraph.computable_wiener, id, congrArg, SimpleGraph.wiener_eq_computable
7 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem WrittenOnTheWallII.Test.K4_min_deg line 246 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, SimpleGraph.minDegree, Fin, OfNat.ofNat, WrittenOnTheWallII.Test.K4
5 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem WrittenOnTheWallII.Test.K4_max_deg line 250 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, SimpleGraph.maxDegree, Fin, OfNat.ofNat, WrittenOnTheWallII.Test.K4
5 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem WrittenOnTheWallII.Test.K4_avg_deg line 254 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Rat, SimpleGraph.averageDegree, Fin, OfNat.ofNat, Nat, WrittenOnTheWallII.Test.K4
Proof uses: id, of_eq_true, HDiv.hDiv, Finset.sum, Finset.univ, SimpleGraph.degree, Membership.mem, Set, SimpleGraph.neighborSet, Fintype.card, Eq.trans, True, congrFun', congrArg, HMul.hMul, congr, HSMul.hSMul, Finset.card, Finset.sum_congr, Eq.refl and 12 more
54 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem WrittenOnTheWallII.Test.K4_matching line 259 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Real, SimpleGraph.matchingNumber, Fin, OfNat.ofNat, Nat, WrittenOnTheWallII.Test.K4
Proof uses: BddAbove, Set.image, SimpleGraph.Subgraph, Finset.card, Sym2, Set.toFinset, SimpleGraph.Subgraph.edgeSet, Membership.mem, Set, Classical.propDecidable, Set.ofPred, SimpleGraph.Subgraph.IsMatching, Exists.intro, upperBounds, Fintype.card, And, LE.le, id, HMul.hMul, SimpleGraph.matching_card_bound and 69 more
99 instances, coercions and auxiliary constants left out.

Tactic trace: 30 steps
Open to load the checked before-and-after goal states.
theorem WrittenOnTheWallII.Test.K4_residue line 282 source
extra axioms: _private.0.WrittenOnTheWallII.Test.K4_residue._native.decide.ax_1 what this means
Statement uses: Eq, Nat, SimpleGraph.residue, Fin, OfNat.ofNat, WrittenOnTheWallII.Test.K4
Proof uses: id, of_decide_eq_true, SimpleGraph.residueAux, Multiset.sort, Multiset.map, SimpleGraph.degree, Membership.mem, Set, SimpleGraph.neighborSet, Finset.val, Finset.univ, GE.ge
21 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem WrittenOnTheWallII.Test.K4_annihilation line 286 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, SimpleGraph.annihilationNumber, Fin, OfNat.ofNat, WrittenOnTheWallII.Test.K4
5 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem WrittenOnTheWallII.Test.K4_cvetkovic sorry line 290 source
depends on sorry what this means
Statement uses: Eq, Nat, SimpleGraph.cvetkovic, Fin, OfNat.ofNat, WrittenOnTheWallII.Test.K4
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
8 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem WrittenOnTheWallII.Test.petersen_indep line 297 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, SimpleGraph.indepNum, Fin, OfNat.ofNat, WrittenOnTheWallII.Test.PetersenGraph
Proof uses: Eq.mpr, SimpleGraph.computable_indep_num, Insert.insert, Sym2, Set, Sym2.mk, Singleton.singleton, id, congrArg, SimpleGraph.indep_num_eq_computable
13 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem WrittenOnTheWallII.Test.petersen_dom line 301 source
extra axioms: _private.0.WrittenOnTheWallII.Test.petersen_dom._native.decide.ax_1 what this means
Statement uses: Eq, Nat, SimpleGraph.dominationNumber, Fin, OfNat.ofNat, WrittenOnTheWallII.Test.PetersenGraph
Proof uses: Eq.mpr, SimpleGraph.computable_dom_num, Insert.insert, Sym2, Set, Sym2.mk, Singleton.singleton, id, congrArg, SimpleGraph.dom_num_eq_computable, of_decide_eq_true
14 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem WrittenOnTheWallII.Test.petersen_avg_dist line 305 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Real, SimpleGraph.averageDistance, Fin, OfNat.ofNat, Nat, WrittenOnTheWallII.Test.PetersenGraph, HDiv.hDiv
Proof uses: Eq.mpr, SimpleGraph.computable_avg_dist, Insert.insert, Sym2, Set, Sym2.mk, Singleton.singleton, id, congrArg, SimpleGraph.avg_dist_eq_computable, Rat, Mathlib.Meta.NormNum.isNNRat_eq_true, inferInstance, DivisionSemiring, Mathlib.Meta.NormNum.isNNRat_ratCast, Mathlib.Meta.NormNum.isNNRat_div, Mathlib.Meta.NormNum.isNNRat_mul, HMul.hMul, Inv.inv, Eq.refl and 5 more
62 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
theorem WrittenOnTheWallII.Test.petersen_diameter line 311 source
extra axioms: _private.0.WrittenOnTheWallII.Test.petersen_diameter._native.decide.ax_1 what this means
Statement uses: Eq, ENat, SimpleGraph.ediam, Fin, OfNat.ofNat, Nat, WrittenOnTheWallII.Test.PetersenGraph
Proof uses: Eq.mpr, SimpleGraph.computable_ediam, Insert.insert, Sym2, Set, Sym2.mk, Singleton.singleton, id, congrArg, SimpleGraph.ediam_eq_computable, of_decide_eq_true, SimpleGraph.Connected, Bool, Decidable.decide, Bool.true, Eq.refl, cast, Eq.symm
30 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
theorem WrittenOnTheWallII.Test.petersen_radius line 316 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, ENat, SimpleGraph.radius, Fin, OfNat.ofNat, Nat, WrittenOnTheWallII.Test.PetersenGraph
Proof uses: Eq.mpr, SimpleGraph.computable_radius, Insert.insert, Sym2, Set, Sym2.mk, Singleton.singleton, id, congrArg, SimpleGraph.radius_eq_computable, of_decide_eq_true, SimpleGraph.Connected, Bool, Decidable.decide, Bool.true, Eq.refl, cast, Eq.symm
29 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
theorem WrittenOnTheWallII.Test.petersen_girth sorry line 321 source
depends on sorry what this means
Statement uses: Eq, Nat, SimpleGraph.girth, Fin, OfNat.ofNat, WrittenOnTheWallII.Test.PetersenGraph
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
2 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem WrittenOnTheWallII.Test.petersen_order line 326 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, Fintype.card, Fin, OfNat.ofNat, SimpleGraph.Subgraph.verts, WrittenOnTheWallII.Test.PetersenGraph, Top.top, SimpleGraph.Subgraph, Membership.mem, Set, Classical.propDecidable
Proof uses: Eq.mpr, id, congrArg, Fintype.card_congr, RelIso.toEquiv, SimpleGraph.Adj, SimpleGraph.Subgraph.coe, SimpleGraph.Subgraph.topIso, Eq.refl
12 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem WrittenOnTheWallII.Test.petersen_size line 331 source
extra axioms: _private.0.WrittenOnTheWallII.Test.petersen_size._native.decide.ax_1 what this means
Statement uses: Eq, Nat, Finset.card, Sym2, Fin, OfNat.ofNat, SimpleGraph.edgeFinset, WrittenOnTheWallII.Test.PetersenGraph, Insert.insert, Set, Sym2.mk, Singleton.singleton
Proof uses: of_decide_eq_true
22 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem WrittenOnTheWallII.Test.petersen_szeged line 335 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, SimpleGraph.szegedIndex, Fin, OfNat.ofNat, WrittenOnTheWallII.Test.PetersenGraph, Insert.insert, Sym2, Set, Sym2.mk, Singleton.singleton
Proof uses: Eq.mpr, SimpleGraph.computable_szeged_index, id, congrArg, SimpleGraph.szeged_eq_computable
23 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem WrittenOnTheWallII.Test.petersen_wiener line 339 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, SimpleGraph.wienerIndex, Fin, OfNat.ofNat, WrittenOnTheWallII.Test.PetersenGraph
Proof uses: Eq.mpr, SimpleGraph.computable_wiener, Insert.insert, Sym2, Set, Sym2.mk, Singleton.singleton, id, congrArg, SimpleGraph.wiener_eq_computable
14 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem WrittenOnTheWallII.Test.petersen_min_deg line 343 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, SimpleGraph.minDegree, Fin, OfNat.ofNat, WrittenOnTheWallII.Test.PetersenGraph, Insert.insert, Sym2, Set, Sym2.mk, Singleton.singleton
12 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem WrittenOnTheWallII.Test.petersen_max_deg line 347 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, SimpleGraph.maxDegree, Fin, OfNat.ofNat, WrittenOnTheWallII.Test.PetersenGraph, Insert.insert, Sym2, Set, Sym2.mk, Singleton.singleton
12 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem WrittenOnTheWallII.Test.petersen_avg_deg line 351 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Rat, SimpleGraph.averageDegree, Fin, OfNat.ofNat, Nat, WrittenOnTheWallII.Test.PetersenGraph, Insert.insert, Sym2, Set, Sym2.mk, Singleton.singleton
Proof uses: id, Eq.mpr, HDiv.hDiv, Finset.sum, Finset.univ, SimpleGraph.degree, Membership.mem, SimpleGraph.neighborSet, Fintype.card, congrFun', congrArg, Fintype.card_fin
36 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
theorem WrittenOnTheWallII.Test.petersen_matching line 355 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Real, SimpleGraph.matchingNumber, Fin, OfNat.ofNat, Nat, WrittenOnTheWallII.Test.PetersenGraph, Insert.insert, Sym2, Set, Sym2.mk, Singleton.singleton
Proof uses: BddAbove, Set.image, SimpleGraph.Subgraph, Finset.card, Set.toFinset, SimpleGraph.Subgraph.edgeSet, Membership.mem, Classical.propDecidable, Set.ofPred, SimpleGraph.Subgraph.IsMatching, Exists.intro, upperBounds, Fintype.card, And, LE.le, id, HMul.hMul, SimpleGraph.matching_card_bound, cast, Eq.symm and 67 more
121 instances, coercions and auxiliary constants left out.

Tactic trace: 54 steps
Open to load the checked before-and-after goal states.
theorem WrittenOnTheWallII.Test.petersen_residue line 390 source
extra axioms: _private.0.WrittenOnTheWallII.Test.petersen_residue._native.decide.ax_1 what this means
Statement uses: Eq, Nat, SimpleGraph.residue, Fin, OfNat.ofNat, WrittenOnTheWallII.Test.PetersenGraph, Insert.insert, Sym2, Set, Sym2.mk, Singleton.singleton
Proof uses: id, of_decide_eq_true, SimpleGraph.residueAux, Multiset.sort, Multiset.map, SimpleGraph.degree, Membership.mem, SimpleGraph.neighborSet, Finset.val, Finset.univ, GE.ge
35 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem WrittenOnTheWallII.Test.petersen_annihilation line 394 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, SimpleGraph.annihilationNumber, Fin, OfNat.ofNat, WrittenOnTheWallII.Test.PetersenGraph, Insert.insert, Sym2, Set, Sym2.mk, Singleton.singleton
12 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem WrittenOnTheWallII.Test.petersen_cvetkovic sorry line 398 source
depends on sorry what this means
Statement uses: Eq, Nat, SimpleGraph.cvetkovic, Fin, OfNat.ofNat, WrittenOnTheWallII.Test.PetersenGraph, Insert.insert, Sym2, Set, Sym2.mk, Singleton.singleton
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
22 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem WrittenOnTheWallII.Test.C6_indep line 405 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, SimpleGraph.indepNum, Fin, OfNat.ofNat, WrittenOnTheWallII.Test.C6
Proof uses: Eq.mpr, SimpleGraph.computable_indep_num, id, congrArg, SimpleGraph.indep_num_eq_computable
6 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem WrittenOnTheWallII.Test.C6_dom line 409 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, SimpleGraph.dominationNumber, Fin, OfNat.ofNat, WrittenOnTheWallII.Test.C6
Proof uses: Eq.mpr, SimpleGraph.computable_dom_num, id, congrArg, SimpleGraph.dom_num_eq_computable
6 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem WrittenOnTheWallII.Test.C6_avg_dist line 413 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Real, SimpleGraph.averageDistance, Fin, OfNat.ofNat, Nat, WrittenOnTheWallII.Test.C6, HDiv.hDiv
Proof uses: Eq.mpr, SimpleGraph.computable_avg_dist, id, congrArg, SimpleGraph.avg_dist_eq_computable, Rat, Mathlib.Meta.NormNum.isNNRat_eq_true, inferInstance, DivisionSemiring, Mathlib.Meta.NormNum.isNNRat_ratCast, Mathlib.Meta.NormNum.isNNRat_div, Mathlib.Meta.NormNum.isNNRat_mul, HMul.hMul, Inv.inv, Eq.refl, Mathlib.Meta.NormNum.IsNat.to_isNNRat, Mathlib.Meta.NormNum.isNat_ofNat, Mathlib.Meta.NormNum.isNNRat_inv_pos, Nat.mul, Mathlib.Meta.NormNum.instAtLeastTwo
55 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
theorem WrittenOnTheWallII.Test.C6_diameter line 418 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, ENat, SimpleGraph.ediam, Fin, OfNat.ofNat, Nat, WrittenOnTheWallII.Test.C6
Proof uses: Eq.mpr, SimpleGraph.computable_ediam, id, congrArg, SimpleGraph.ediam_eq_computable, of_decide_eq_true, SimpleGraph.Connected, Bool, Decidable.decide, Bool.true, Eq.refl, cast, Eq.symm
22 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
theorem WrittenOnTheWallII.Test.C6_radius line 423 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, ENat, SimpleGraph.radius, Fin, OfNat.ofNat, Nat, WrittenOnTheWallII.Test.C6
Proof uses: Eq.mpr, SimpleGraph.computable_radius, id, congrArg, SimpleGraph.radius_eq_computable, of_decide_eq_true, SimpleGraph.Connected, Bool, Decidable.decide, Bool.true, Eq.refl, cast, Eq.symm
22 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
theorem WrittenOnTheWallII.Test.C6_girth sorry line 428 source
depends on sorry what this means
Statement uses: Eq, Nat, SimpleGraph.girth, Fin, OfNat.ofNat, WrittenOnTheWallII.Test.C6
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
2 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem WrittenOnTheWallII.Test.C6_order line 433 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, Fintype.card, Fin, OfNat.ofNat, SimpleGraph.Subgraph.verts, WrittenOnTheWallII.Test.C6, Top.top, SimpleGraph.Subgraph, Membership.mem, Set, Classical.propDecidable
Proof uses: Eq.mpr, id, congrArg, Fintype.card_congr, RelIso.toEquiv, SimpleGraph.Adj, SimpleGraph.Subgraph.coe, SimpleGraph.Subgraph.topIso, Eq.refl
12 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem WrittenOnTheWallII.Test.C6_size line 438 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, Finset.card, Sym2, Fin, OfNat.ofNat, SimpleGraph.edgeFinset, WrittenOnTheWallII.Test.C6
6 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem WrittenOnTheWallII.Test.C6_szeged line 442 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, SimpleGraph.szegedIndex, Fin, OfNat.ofNat, WrittenOnTheWallII.Test.C6
Proof uses: Eq.mpr, SimpleGraph.computable_szeged_index, id, congrArg, SimpleGraph.szeged_eq_computable
8 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem WrittenOnTheWallII.Test.C6_wiener line 446 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, SimpleGraph.wienerIndex, Fin, OfNat.ofNat, WrittenOnTheWallII.Test.C6
Proof uses: Eq.mpr, SimpleGraph.computable_wiener, id, congrArg, SimpleGraph.wiener_eq_computable
7 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem WrittenOnTheWallII.Test.C6_min_deg line 450 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, SimpleGraph.minDegree, Fin, OfNat.ofNat, WrittenOnTheWallII.Test.C6
4 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem WrittenOnTheWallII.Test.C6_max_deg line 454 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, SimpleGraph.maxDegree, Fin, OfNat.ofNat, WrittenOnTheWallII.Test.C6
4 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem WrittenOnTheWallII.Test.C6_avg_deg line 458 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Rat, SimpleGraph.averageDegree, Fin, OfNat.ofNat, Nat, WrittenOnTheWallII.Test.C6
Proof uses: id, Eq.mpr, HDiv.hDiv, Finset.sum, Finset.univ, SimpleGraph.degree, Membership.mem, Set, SimpleGraph.neighborSet, Fintype.card, congrFun', congrArg, Fintype.card_fin
20 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
theorem WrittenOnTheWallII.Test.C6_matching line 462 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Real, SimpleGraph.matchingNumber, Fin, OfNat.ofNat, Nat, WrittenOnTheWallII.Test.C6
Proof uses: BddAbove, Set.image, SimpleGraph.Subgraph, Finset.card, Sym2, Set.toFinset, SimpleGraph.Subgraph.edgeSet, Membership.mem, Set, Classical.propDecidable, Set.ofPred, SimpleGraph.Subgraph.IsMatching, Exists.intro, upperBounds, Fintype.card, And, LE.le, id, HMul.hMul, SimpleGraph.matching_card_bound and 72 more
96 instances, coercions and auxiliary constants left out.

Tactic trace: 38 steps
Open to load the checked before-and-after goal states.
theorem WrittenOnTheWallII.Test.C6_residue line 489 source
extra axioms: _private.0.WrittenOnTheWallII.Test.C6_residue._native.decide.ax_1 what this means
Statement uses: Eq, Nat, SimpleGraph.residue, Fin, OfNat.ofNat, WrittenOnTheWallII.Test.C6
Proof uses: id, of_decide_eq_true, SimpleGraph.residueAux, Multiset.sort, Multiset.map, SimpleGraph.degree, Membership.mem, Set, SimpleGraph.neighborSet, Finset.val, Finset.univ, GE.ge
19 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem WrittenOnTheWallII.Test.C6_annihilation line 493 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, SimpleGraph.annihilationNumber, Fin, OfNat.ofNat, WrittenOnTheWallII.Test.C6
4 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem WrittenOnTheWallII.Test.C6_cvetkovic sorry line 497 source
depends on sorry what this means
Statement uses: Eq, Nat, SimpleGraph.cvetkovic, Fin, OfNat.ofNat, WrittenOnTheWallII.Test.C6
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
8 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem WrittenOnTheWallII.Test.Star5_indep line 503 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, SimpleGraph.indepNum, Sum, Fin, OfNat.ofNat, WrittenOnTheWallII.Test.Star5
Proof uses: Eq.mpr, SimpleGraph.computable_indep_num, id, congrArg, SimpleGraph.indep_num_eq_computable
8 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem WrittenOnTheWallII.Test.Star5_dom line 507 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, SimpleGraph.dominationNumber, Sum, Fin, OfNat.ofNat, WrittenOnTheWallII.Test.Star5
Proof uses: Eq.mpr, SimpleGraph.computable_dom_num, id, congrArg, SimpleGraph.dom_num_eq_computable
8 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem WrittenOnTheWallII.Test.Star5_avg_dist line 511 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Real, SimpleGraph.averageDistance, Sum, Fin, OfNat.ofNat, Nat, WrittenOnTheWallII.Test.Star5, HDiv.hDiv
Proof uses: Eq.mpr, SimpleGraph.computable_avg_dist, id, congrArg, SimpleGraph.avg_dist_eq_computable, Rat, Mathlib.Meta.NormNum.isNNRat_eq_true, inferInstance, DivisionSemiring, Mathlib.Meta.NormNum.isNNRat_ratCast, Mathlib.Meta.NormNum.isNNRat_div, Mathlib.Meta.NormNum.isNNRat_mul, HMul.hMul, Inv.inv, Eq.refl, Mathlib.Meta.NormNum.IsNat.to_isNNRat, Mathlib.Meta.NormNum.isNat_ofNat, Mathlib.Meta.NormNum.isNNRat_inv_pos, Nat.mul, Mathlib.Meta.NormNum.instAtLeastTwo
58 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
theorem WrittenOnTheWallII.Test.Star5_diameter line 517 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, ENat, SimpleGraph.ediam, Sum, Fin, OfNat.ofNat, Nat, WrittenOnTheWallII.Test.Star5
Proof uses: Eq.mpr, SimpleGraph.computable_ediam, id, congrArg, SimpleGraph.ediam_eq_computable, of_decide_eq_true, SimpleGraph.Connected, Bool, Decidable.decide, Bool.true, Eq.refl, cast, Eq.symm
25 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
theorem WrittenOnTheWallII.Test.Star5_radius line 522 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, ENat, SimpleGraph.radius, Sum, Fin, OfNat.ofNat, Nat, WrittenOnTheWallII.Test.Star5
Proof uses: Eq.mpr, SimpleGraph.computable_radius, id, congrArg, SimpleGraph.radius_eq_computable, of_decide_eq_true, SimpleGraph.Connected, Bool, Decidable.decide, Bool.true, Eq.refl, cast, Eq.symm, Eq.trans, Nat.cast_one
24 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
theorem WrittenOnTheWallII.Test.Star5_girth line 527 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, ENat, SimpleGraph.egirth, Sum, Fin, OfNat.ofNat, Nat, WrittenOnTheWallII.Test.Star5, Top.top
Proof uses: Eq.mpr, SimpleGraph.IsAcyclic, id, congrArg, propext, SimpleGraph.egirth_eq_top, SimpleGraph.Walk, Sum.inr, Not, SimpleGraph.Walk.IsCycle, SimpleGraph.Adj, SimpleGraph.Walk.snd, SimpleGraph.Walk.adj_snd, SimpleGraph.Walk.IsCycle.not_nil, SimpleGraph.Walk.penultimate, SimpleGraph.Walk.adj_penultimate, Bool, Sum.isLeft, Bool.true, And and 36 more
15 instances, coercions and auxiliary constants left out.

Tactic trace: 28 steps
Open to load the checked before-and-after goal states.
theorem WrittenOnTheWallII.Test.Star5_order line 557 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, Fintype.card, Sum, Fin, OfNat.ofNat, SimpleGraph.Subgraph.verts, WrittenOnTheWallII.Test.Star5, Top.top, SimpleGraph.Subgraph, Membership.mem, Set, Classical.propDecidable
Proof uses: Eq.mpr, id, congrArg, Fintype.card_congr, RelIso.toEquiv, SimpleGraph.Adj, SimpleGraph.Subgraph.coe, SimpleGraph.Subgraph.topIso, Eq.refl
14 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem WrittenOnTheWallII.Test.Star5_size line 562 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, Finset.card, Sym2, Sum, Fin, OfNat.ofNat, SimpleGraph.edgeFinset, WrittenOnTheWallII.Test.Star5
7 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem WrittenOnTheWallII.Test.Star5_szeged line 566 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, SimpleGraph.szegedIndex, Sum, Fin, OfNat.ofNat, WrittenOnTheWallII.Test.Star5
Proof uses: Eq.mpr, SimpleGraph.computable_szeged_index, id, congrArg, SimpleGraph.szeged_eq_computable
11 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem WrittenOnTheWallII.Test.Star5_wiener line 570 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, SimpleGraph.wienerIndex, Sum, Fin, OfNat.ofNat, WrittenOnTheWallII.Test.Star5
Proof uses: Eq.mpr, SimpleGraph.computable_wiener, id, congrArg, SimpleGraph.wiener_eq_computable
10 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem WrittenOnTheWallII.Test.Star5_min_deg line 574 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, SimpleGraph.minDegree, Sum, Fin, OfNat.ofNat, WrittenOnTheWallII.Test.Star5
5 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem WrittenOnTheWallII.Test.Star5_max_deg line 578 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, SimpleGraph.maxDegree, Sum, Fin, OfNat.ofNat, WrittenOnTheWallII.Test.Star5
5 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem WrittenOnTheWallII.Test.Star5_avg_deg line 582 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Rat, SimpleGraph.averageDegree, Sum, Fin, OfNat.ofNat, Nat, WrittenOnTheWallII.Test.Star5, HDiv.hDiv
Proof uses: id, Eq.mpr, Finset.sum, Finset.univ, SimpleGraph.degree, Membership.mem, Set, SimpleGraph.neighborSet, Fintype.card, HAdd.hAdd, Sum.inl, Sum.inr, congrFun', congrArg, congr, Eq.trans, Fintype.sum_sum_type, Singleton.singleton, Finset, Finset.sum_congr and 6 more
36 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
theorem WrittenOnTheWallII.Test.Star5_matching line 586 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Real, SimpleGraph.matchingNumber, Sum, Fin, OfNat.ofNat, Nat, WrittenOnTheWallII.Test.Star5
Proof uses: SimpleGraph.Subgraph, SimpleGraph.Subgraph.IsMatching, LE.le, Finset.card, Sym2, Set.toFinset, SimpleGraph.Subgraph.edgeSet, Membership.mem, Set, Classical.propDecidable, Sum.inl, Sym2.inductionOn, Sym2.mk, SimpleGraph.Adj, SimpleGraph.Subgraph.Adj.adj_sub, Eq.mp, SimpleGraph.Subgraph.Adj, congrArg, propext, SimpleGraph.Subgraph.mem_edgeSet and 61 more
65 instances, coercions and auxiliary constants left out.

Tactic trace: 47 steps
Open to load the checked before-and-after goal states.
theorem WrittenOnTheWallII.Test.Star5_residue line 624 source
extra axioms: _private.0.WrittenOnTheWallII.Test.Star5_residue._native.decide.ax_1 what this means
Statement uses: Eq, Nat, SimpleGraph.residue, Sum, Fin, OfNat.ofNat, WrittenOnTheWallII.Test.Star5
Proof uses: id, of_decide_eq_true, SimpleGraph.residueAux, Multiset.sort, Multiset.map, SimpleGraph.degree, Membership.mem, Set, SimpleGraph.neighborSet, Finset.val, Finset.univ, GE.ge
21 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem WrittenOnTheWallII.Test.Star5_annihilation line 628 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, SimpleGraph.annihilationNumber, Sum, Fin, OfNat.ofNat, WrittenOnTheWallII.Test.Star5
5 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem WrittenOnTheWallII.Test.Star5_cvetkovic sorry line 632 source
depends on sorry what this means
Statement uses: Eq, Nat, SimpleGraph.cvetkovic, Sum, Fin, OfNat.ofNat, WrittenOnTheWallII.Test.Star5
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
12 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.