LargestInducedTree.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

12 declarations, 0 contain sorry, 0 declared as axioms

Largest induced tree

This file defines largestInducedTreeSize, the number of vertices in a largest induced subtree of a graph.

Imports (5)

Imported by 2 files

def SimpleGraph.largestInducedTreeSize largestInducedTreeSize G is the number of vertices in a largest induced subtree of G line 39 source
Source documentation
largestInducedTreeSize G is the number of vertices in a largest induced subtree of G. A tree is a connected acyclic graph; an induced tree is an induced subgraph that is a tree.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SimpleGraph, Nat
Proof uses: SupSet.sSup, Set.ofPred, Exists, Finset, And, Eq, Finset.card, SimpleGraph.IsTree, SimpleGraph.induce
4 instances, coercions and auxiliary constants left out.
```
noncomputable def largestInducedTreeSize (G : SimpleGraph α) : ℕ :=
…
```
lemma SimpleGraph.card_le_largestInducedTreeSize The order of any induced tree is bounded by largestInducedTreeSize line 44 source
Source documentation
The order of any induced tree is bounded by largestInducedTreeSize.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, SimpleGraph, Finset, SimpleGraph.IsTree, SimpleGraph.induce, LE.le, Nat, Finset.card, SimpleGraph.largestInducedTreeSize
Proof uses: id, le_csSup, Set.ofPred, Exists, And, Eq, Exists.intro, Membership.mem, Set, upperBounds, Fintype.card, Finset.card_le_univ, And.intro, rfl
20 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
lemma card_le_largestInducedTreeSize {G : SimpleGraph α} {s : Finset α}
    (hs : (G.induce (s : Set α)).IsTree) :
    s.card ≤ largestInducedTreeSize G := by
…
```
Mentions: SimpleGraph.largestInducedTreeSize
lemma SimpleGraph.one_le_largestInducedTreeSize Every finite graph with a vertex has a nonempty induced tree line 57 source
Source documentation
Every finite graph with a vertex has a nonempty induced tree.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, SimpleGraph, Nonempty, LE.le, Nat, OfNat.ofNat, SimpleGraph.largestInducedTreeSize
Proof uses: Classical.choice, inferInstance, Finset, Singleton.singleton, Eq, Set, of_eq_true, Eq.trans, True, congrFun', congrArg, Finset.coe_singleton, eq_self, SimpleGraph.IsTree, SimpleGraph.induce, Eq.mpr, id, Nonempty.intro, Subtype.mk, Membership.mem and 12 more
13 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
```
lemma one_le_largestInducedTreeSize (G : SimpleGraph α) [Nonempty α] :
    1 ≤ largestInducedTreeSize G := by
…
```
Mentions: SimpleGraph.largestInducedTreeSize
lemma SimpleGraph.IsTree.induce_insert_of_unique_adj Attaching a new vertex along its unique neighbor in an induced tree gives a larger induced tree line 78 source
Source documentation
Attaching a new vertex along its unique neighbor in an induced tree gives a larger induced tree.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, SimpleGraph, Finset, SimpleGraph.IsTree, SimpleGraph.induce, Not, Membership.mem, SimpleGraph.Adj, Eq, Insert.insert
Proof uses: SimpleGraph.IsTree.mk, SimpleGraph.Preconnected, SimpleGraph.Connected.preconnected, SimpleGraph.IsTree.connected, Singleton.singleton, Set, SimpleGraph.Preconnected.of_subsingleton, SimpleGraph.Connected, Union.union, SimpleGraph.connected_induce_union, of_eq_true, Eq.trans, True, eq_self, Eq.mpr, id, congrArg, Finset.coe_insert, SimpleGraph.Walk, SimpleGraph.Walk.IsCycle and 47 more
32 instances, coercions and auxiliary constants left out.

Tactic trace: 67 steps
Open to load the checked before-and-after goal states.
```
lemma IsTree.induce_insert_of_unique_adj {G : SimpleGraph α} {s : Finset α} {z a : α}
    (hT : (G.induce (s : Set α)).IsTree)
    (_hz : z ∉ s) (ha : a ∈ s) (hza : G.Adj z a)
    (huniq : ∀ ⦃b : α⦄, b ∈ s → G.Adj z b → b = a) :
    (G.induce ((insert z s : Finset α) : Set α)).IsTree := by
…
```
Mentions: SimpleGraph.b
lemma SimpleGraph.Walk.induce_support_isTree_of_length_eq_dist A shortest walk induces a tree on its support line 148 source
Source documentation
A shortest walk induces a tree on its support.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, SimpleGraph, SimpleGraph.Walk, Eq, Nat, SimpleGraph.Walk.length, SimpleGraph.dist, SimpleGraph.IsTree, Finset, List.toFinset, SimpleGraph.Walk.support, SimpleGraph.induce
Proof uses: SimpleGraph.Walk.rec, SimpleGraph.Walk.nil, Set, Singleton.singleton, Set.ext, of_eq_true, Iff, Membership.mem, Eq.trans, True, congr, congrArg, congrFun', List.cons, List.nil, Insert.insert, List.toFinset_cons, LawfulSingleton.insert_empty_eq, Finset.coe_singleton, iff_self and 46 more
33 instances, coercions and auxiliary constants left out.

Tactic trace: 48 steps
Open to load the checked before-and-after goal states.
```
lemma Walk.induce_support_isTree_of_length_eq_dist {G : SimpleGraph α} {u v : α}
    (p : G.Walk u v) (hp : p.length = G.dist u v) :
    (G.induce (p.support.toFinset : Set α)).IsTree := by
…
```
theorem SimpleGraph.girth_sub_one_le_largestInducedTreeSize Removing one vertex from a shortest cycle gives an induced tree line 200 source
Source documentation
Removing one vertex from a shortest cycle gives an induced tree.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, SimpleGraph, Not, SimpleGraph.IsAcyclic, LE.le, Nat, HSub.hSub, SimpleGraph.girth, OfNat.ofNat, SimpleGraph.largestInducedTreeSize
Proof uses: Exists, SimpleGraph.Walk, And, SimpleGraph.Walk.IsCycle, Eq, SimpleGraph.Walk.length, Iff.mpr, SimpleGraph.exists_girth_eq_length, SimpleGraph.Walk.snd, SimpleGraph.Walk.penultimate, SimpleGraph.Walk.tail, SimpleGraph.Walk.dropLast, Finset, List.toFinset, SimpleGraph.Walk.support, LE.le.trans_eq, SimpleGraph.Walk.IsCircuit.three_le_length, SimpleGraph.Walk.IsCycle.isCircuit, Eq.symm, SimpleGraph.Walk.IsPath and 61 more
31 instances, coercions and auxiliary constants left out.

Tactic trace: 52 steps
Open to load the checked before-and-after goal states.
```
theorem girth_sub_one_le_largestInducedTreeSize (G : SimpleGraph α)
    (hcyc : ¬ G.IsAcyclic) :
    G.girth - 1 ≤ largestInducedTreeSize G := by
…
```
Mentions: SimpleGraph.largestInducedTreeSize
lemma SimpleGraph.Connected.exists_induced_tree_containing_pair Every pair of vertices in a connected graph lies in an induced tree line 257 source
Source documentation
Every pair of vertices in a connected graph lies in an induced tree.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, SimpleGraph, SimpleGraph.Connected, Exists, Finset, And, Membership.mem, SimpleGraph.IsTree, SimpleGraph.induce
Proof uses: SimpleGraph.Walk, SimpleGraph.Walk.IsPath, Eq, Nat, SimpleGraph.Walk.length, SimpleGraph.dist, SimpleGraph.Connected.exists_path_of_dist, Exists.intro, List.toFinset, SimpleGraph.Walk.support, And.intro, of_eq_true, Eq.trans, List, True, SimpleGraph.Walk.induce_support_isTree_of_length_eq_dist
14 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
lemma Connected.exists_induced_tree_containing_pair {G : SimpleGraph α}
    (hG : G.Connected) (x y : α) :
    ∃ s : Finset α, x ∈ s ∧ y ∈ s ∧ (G.induce (s : Set α)).IsTree := by
…
```
lemma SimpleGraph.exists_maximum_induced_tree_containing A nonempty family of induced trees with prescribed vertices has a largest member line 268 source
Source documentation
A nonempty family of induced trees with prescribed vertices has a largest member.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, SimpleGraph, Finset, Exists, And, LE.le, SimpleGraph.IsTree, SimpleGraph.induce, Nat, Finset.card
Proof uses: Set, Set.ofPred, Set.Finite, Set.toFinite, Membership.mem, Set.Nonempty, Exists.intro, And.intro, Set.exists_max_image, And.left, Subtype, And.right
26 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
```
lemma exists_maximum_induced_tree_containing (G : SimpleGraph α) (r : Finset α)
    (hr : ∃ s : Finset α, r ⊆ s ∧ (G.induce (s : Set α)).IsTree) :
    ∃ s : Finset α,
      r ⊆ s ∧
      (G.induce (s : Set α)).IsTree ∧
      ∀ t : Finset α, r ⊆ t →
        (G.induce (t : Set α)).IsTree → t.card ≤ s.card := by
…
```
lemma SimpleGraph.Connected.exists_adj_finset_compl A nonempty proper vertex set in a connected graph has an edge across its boundary line 288 source
Source documentation
A nonempty proper vertex set in a connected graph has an edge across its boundary.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, SimpleGraph, SimpleGraph.Connected, Finset, Finset.Nonempty, Ne, Finset.univ, Exists, And, Not, Membership.mem, SimpleGraph.Adj
Proof uses: Decidable.byContradiction, Finset.eq_univ_of_forall, Eq.mp, Eq.trans, binderNameHint, forall_congr, SimpleGraph.Walk, SimpleGraph.Reachable, SimpleGraph.Connected.preconnected, SimpleGraph.Dart, List, SimpleGraph.Walk.darts, Set, Prod.fst, SimpleGraph.Dart.toProd, Prod.snd, SimpleGraph.Walk.exists_boundary_dart, Eq.mpr, id, Eq and 5 more
16 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
```
lemma Connected.exists_adj_finset_compl {G : SimpleGraph α}
    (hG : G.Connected) {s : Finset α} (hs : s.Nonempty) (hsu : s ≠ Finset.univ) :
    ∃ z ∉ s, ∃ a ∈ s, G.Adj z a := by
…
```
lemma SimpleGraph.exists_two_adj_of_maximum_induced_tree_containing A boundary vertex of a largest prescribed induced tree has two neighbors in the tree line 304 source
Source documentation
A boundary vertex of a largest prescribed induced tree has two neighbors in the tree.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, SimpleGraph, Finset, SimpleGraph.Connected, LE.le, Finset.Nonempty, SimpleGraph.IsTree, SimpleGraph.induce, Nat, Finset.card, Ne, Finset.univ, Exists, And, Not, Membership.mem, SimpleGraph.Adj
Proof uses: SimpleGraph.Connected.exists_adj_finset_compl, dite, Eq, Classical.propDecidable, Exists.intro, And.intro, Ne.symm, Decidable.byContradiction, Insert.insert, SimpleGraph.IsTree.induce_insert_of_unique_adj, Finset.mem_insert_of_mem, HAdd.hAdd, OfNat.ofNat, Finset.card_insert_of_notMem, Classical.byContradiction
26 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
```
lemma exists_two_adj_of_maximum_induced_tree_containing
    {G : SimpleGraph α} {r s : Finset α}
    (hG : G.Connected) (hrs : r ⊆ s) (hs : s.Nonempty)
    (hT : (G.induce (s : Set α)).IsTree)
    (hmax : ∀ t : Finset α, r ⊆ t →
      (G.induce (t : Set α)).IsTree → t.card ≤ s.card)
    (hsu : s ≠ Finset.univ) :
    ∃ z ∉ s, ∃ a ∈ s, ∃ b ∈ s,
      a ≠ b ∧ G.Adj z a ∧ G.Adj z b := by
…
```
Mentions: SimpleGraph.b
lemma SimpleGraph.IsTree.girth_add_one_le_card_of_two_leaves_of_two_adj Two leaves outside the boundary cycle force an extra two vertices in the induced tree line 330 source
Source documentation
Two leaves outside the boundary cycle force an extra two vertices in the induced tree.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, SimpleGraph, DecidableRel, SimpleGraph.Adj, Finset, SimpleGraph.IsTree, SimpleGraph.induce, Membership.mem, Ne, Eq, Nat, SimpleGraph.degree, Set, SimpleGraph.neighborSet, OfNat.ofNat, Not, LE.le, HAdd.hAdd, SimpleGraph.girth and 1 more
Proof uses: SimpleGraph.Embedding, SimpleGraph.Embedding.induce, SimpleGraph.Walk, Subtype.mk, Eq.mpr, id, And, SimpleGraph.Walk.IsPath, ExistsUnique, SimpleGraph.IsTree.existsUnique_path, SimpleGraph.Walk.map, SimpleGraph.Embedding.toHom, Iff.mpr, SimpleGraph.Hom, Subtype, SimpleGraph.Walk.isPath_map_iff_of_injective, RelEmbedding.injective, List, SimpleGraph.Walk.support, Exists and 66 more
47 instances, coercions and auxiliary constants left out.

Tactic trace: 78 steps
Open to load the checked before-and-after goal states.
```
lemma IsTree.girth_add_one_le_card_of_two_leaves_of_two_adj
    {G : SimpleGraph α} [DecidableRel G.Adj] {s : Finset α}
    (hT : (G.induce (s : Set α)).IsTree)
    {x y z a b : α}
    (hxs : x ∈ s) (hys : y ∈ s) (hxy : x ≠ y)
    (hx : G.degree x = 1) (hy : G.degree y = 1)
    (hz : z ∉ s) (ha : a ∈ s) (hb : b ∈ s)
    (hab : a ≠ b) (hza : G.Adj z a) (hzb : G.Adj z b) :
    G.girth + 1 ≤ s.card := by
…
```
Mentions: SimpleGraph.b
lemma SimpleGraph.girth_add_one_le_largestInducedTreeSize_of_two_leaves Two distinct leaves in a connected cyclic graph yield an induced tree of order at least girth plus one line 413 source
Source documentation
Two distinct leaves in a connected cyclic graph yield an induced tree of order at least girth plus one.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, SimpleGraph, DecidableRel, SimpleGraph.Adj, SimpleGraph.Connected, Not, SimpleGraph.IsAcyclic, Ne, Eq, Nat, SimpleGraph.degree, Membership.mem, Set, SimpleGraph.neighborSet, OfNat.ofNat, LE.le, HAdd.hAdd, SimpleGraph.girth, SimpleGraph.largestInducedTreeSize
Proof uses: Finset, And, SimpleGraph.IsTree, SimpleGraph.induce, Exists, SimpleGraph.Connected.exists_induced_tree_containing_pair, Insert.insert, Singleton.singleton, Exists.intro, And.intro, Or, Iff.mp, Finset.mem_insert, Finset.mem_singleton, Eq.symm, Finset.card, SimpleGraph.exists_maximum_induced_tree_containing, of_eq_true, Eq.trans, True and 22 more
31 instances, coercions and auxiliary constants left out.

Tactic trace: 30 steps
Open to load the checked before-and-after goal states.
```
lemma girth_add_one_le_largestInducedTreeSize_of_two_leaves
    (G : SimpleGraph α) [DecidableRel G.Adj]
    (hG : G.Connected) (hcyc : ¬ G.IsAcyclic)
    {x y : α} (hxy : x ≠ y)
    (hx : G.degree x = 1) (hy : G.degree y = 1) :
    G.girth + 1 ≤ largestInducedTreeSize G := by
…
```
Mentions: SimpleGraph.largestInducedTreeSize