Solutions_S03_Inductive_Structures.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 9 curated AI-written annotations and 7 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 Mathematics in Lean documentation, Pinned Mathematics in Lean textbook

18 declarations, 0 contain sorry, 0 declared as axioms

Imports (1)

Mathlib.Tactic

def MyListSpace3.reverse line 11 source
no axioms what this means
Statement uses: List
2 instances, coercions and auxiliary constants left out.

Distinct definitions of this name: MIL/C06_Discrete_Mathematics/S03_Inductive_Structures.lean:64 (different declaration text). Qualify references as MyListSpace3.reverse@path.
theorem MyListSpace3.reverse_append line 15 source
standard axioms: propext what this means
Statement uses: List, Eq, MyListSpace3.reverse, HAppend.hAppend
Proof uses: List.rec, Eq.mpr, List.nil, id, congrArg, List.nil_append, MyListSpace3.reverse.eq_1, List.append_nil, Eq.refl, List.cons, List.cons_append, MyListSpace3.reverse.eq_2, List.append_assoc
4 instances, coercions and auxiliary constants left out.

Distinct definitions of this name: MIL/C06_Discrete_Mathematics/S03_Inductive_Structures.lean:66 (same statement text; different proof or body). Qualify references as MyListSpace3.reverse_append@path.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
theorem MyListSpace3.reverse_reverse line 20 source
standard axioms: propext what this means
Statement uses: List, Eq, MyListSpace3.reverse
Proof uses: List.rec, Eq.refl, List.nil, Eq.mpr, List.cons, HAppend.hAppend, id, congrArg, MyListSpace3.reverse.eq_2, MyListSpace3.reverse_append, MyListSpace3.reverse.eq_1, List.nil_append, List.cons_append
2 instances, coercions and auxiliary constants left out.

Distinct definitions of this name: MIL/C06_Discrete_Mathematics/S03_Inductive_Structures.lean:69 (same statement text; different proof or body). Qualify references as MyListSpace3.reverse_reverse@path.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
inductive BinTree line 27 source
no axioms what this means

Also declared: MIL/C06_Discrete_Mathematics/S03_Inductive_Structures.lean:73 (same declaration text).
def BinTree.size line 33 source
no axioms what this means
Statement uses: BinTree, Nat
2 instances, coercions and auxiliary constants left out.

Also declared: MIL/C06_Discrete_Mathematics/S03_Inductive_Structures.lean:79 (same declaration text).
def BinTree.depth line 37 source
no axioms what this means
Statement uses: BinTree, Nat
2 instances, coercions and auxiliary constants left out.

Also declared: MIL/C06_Discrete_Mathematics/S03_Inductive_Structures.lean:83 (same declaration text).
theorem BinTree.depth_le_size line 41 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: BinTree, LE.le, Nat, BinTree.depth, BinTree.size
4 instances, coercions and auxiliary constants left out.

Distinct definitions of this name: MIL/C06_Discrete_Mathematics/S03_Inductive_Structures.lean:100 (different declaration text). Qualify references as BinTree.depth_le_size@path.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
def BinTree.flip line 51 source
no axioms what this means
Statement uses: BinTree
2 instances, coercions and auxiliary constants left out.

Distinct definitions of this name: MIL/C06_Discrete_Mathematics/S03_Inductive_Structures.lean:102 (different declaration text). Qualify references as BinTree.flip@path.
example BinTree.(example at line 55) line 55 source
theorem BinTree.size_flip line 58 source
standard axioms: Quot.sound, propext what this means
Statement uses: BinTree, Eq, Nat, BinTree.size, BinTree.flip
2 instances, coercions and auxiliary constants left out.

Distinct definitions of this name: MIL/C06_Discrete_Mathematics/S03_Inductive_Structures.lean:107 (different declaration text). Qualify references as BinTree.size_flip@path.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
inductive PropForm line 66 source
no axioms what this means

Also declared: MIL/C06_Discrete_Mathematics/S03_Inductive_Structures.lean:110 (same declaration text).
def PropForm.eval line 74 source
no axioms what this means
Statement uses: PropForm, Nat, Bool
2 instances, coercions and auxiliary constants left out.

Also declared: MIL/C06_Discrete_Mathematics/S03_Inductive_Structures.lean:118 (same declaration text).
def PropForm.vars line 81 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PropForm, Finset, Nat
2 instances, coercions and auxiliary constants left out.

Also declared: MIL/C06_Discrete_Mathematics/S03_Inductive_Structures.lean:125 (same declaration text).
def PropForm.subst line 88 source
no axioms what this means
Statement uses: PropForm, Nat
2 instances, coercions and auxiliary constants left out.

Also declared: MIL/C06_Discrete_Mathematics/S03_Inductive_Structures.lean:147 (same declaration text).
theorem PropForm.subst_eq_of_not_mem_vars line 95 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PropForm, Nat, Not, Membership.mem, Finset, PropForm.vars, Eq, PropForm.subst
6 instances, coercions and auxiliary constants left out.

Distinct definitions of this name: MIL/C06_Discrete_Mathematics/S03_Inductive_Structures.lean:154 (different declaration text). Qualify references as PropForm.subst_eq_of_not_mem_vars@path.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
theorem PropForm.subst_eq_of_not_mem_vars' alternative proof: line 107 source
Source comment
alternative proof:

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PropForm, Nat, Not, Membership.mem, Finset, PropForm.vars, Eq, PropForm.subst
6 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
theorem subst_eq_of_not_mem_vars' (A : PropForm) (n : ℕ) (C : PropForm):
    n ∉ A.vars → A.subst n C = A := by
…
```
Mentions: PropForm
theorem PropForm.subst_eval_eq line 111 source
standard axioms: propext what this means
Statement uses: PropForm, Nat, Bool, Eq, PropForm.eval, PropForm.subst, ite
4 instances, coercions and auxiliary constants left out.

Distinct definitions of this name: MIL/C06_Discrete_Mathematics/S03_Inductive_Structures.lean:157 (different declaration text). Qualify references as PropForm.subst_eval_eq@path.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
theorem PropForm.subst_eval_eq' alternative proof: line 126 source
Source comment
alternative proof:

standard axioms: propext what this means
Statement uses: PropForm, Nat, Bool, Eq, PropForm.eval, PropForm.subst, ite
4 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
theorem subst_eval_eq' (A : PropForm) (n : ℕ) (C : PropForm) (v : ℕ → Bool) :
    (A.subst n C).eval v = A.eval (fun m => if m = n then C.eval v else v m) := by
…
```
Mentions: PropForm, PropForm.eval