Solutions_S02_Induction_and_Recursion.lean`

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Imports (2)

def fac line 4 source
no axioms what this means
Statement uses: Nat
2 instances, coercions and auxiliary constants left out.
Also declared: MIL/C05_Elementary_Number_Theory/S02_Induction_and_Recursion.lean:10 (same declaration text).
theorem pow_two_le_fac line 8 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, HPow.hPow, OfNat.ofNat, HSub.hSub, fac
Proof uses: Nat.casesAuxOn, of_eq_true, Eq.trans, True, congrFun', congrArg, zero_tsub, pow_zero, Nat.recAux, HAdd.hAdd, congr, zero_add, tsub_self, HMul.hMul, mul_one, Eq.mpr, id, Eq, add_tsub_cancel_right, pow_succ' and 6 more
53 instances, coercions and auxiliary constants left out.
Distinct definitions of this name: MIL/C05_Elementary_Number_Theory/S02_Induction_and_Recursion.lean:48 (same statement text; different proof or body). Qualify references as pow_two_le_fac@path.
Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
theorem sum_sqr line 26 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Finset.sum, Finset.range, HAdd.hAdd, OfNat.ofNat, HPow.hPow, HDiv.hDiv, HMul.hMul
Proof uses: Eq.symm, Nat.div_eq_of_eq_mul_right, Mathlib.Meta.NormNum.isNat_lt_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.false, Nat.recAux, of_eq_true, Eq.trans, True, congr, congrArg, zero_add, mul_one, congrFun', MulZeroClass.mul_zero, Singleton.singleton, Finset, Finset.sum_congr and 44 more
58 instances, coercions and auxiliary constants left out.
Distinct definitions of this name: MIL/C05_Elementary_Number_Theory/S02_Induction_and_Recursion.lean:101 (same statement text; different proof or body). Qualify references as sum_sqr@path.
Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
inductive MyNat line 36 source
no axioms what this means
Also declared: MIL/C05_Elementary_Number_Theory/S02_Induction_and_Recursion.lean:105 (same declaration text).
def MyNat.add line 42 source
no axioms what this means
Statement uses: MyNat
2 instances, coercions and auxiliary constants left out.
Also declared: MIL/C05_Elementary_Number_Theory/S02_Induction_and_Recursion.lean:111 (same declaration text).
def MyNat.mul line 46 source
no axioms what this means
Statement uses: MyNat
2 instances, coercions and auxiliary constants left out.
Also declared: MIL/C05_Elementary_Number_Theory/S02_Induction_and_Recursion.lean:115 (same declaration text).
theorem MyNat.zero_add line 50 source
no axioms what this means
Statement uses: MyNat, Eq, MyNat.add, MyNat.zero
Proof uses: MyNat.rec, Eq.refl, Eq.mpr, MyNat.succ, id, congrArg, MyNat.add.eq_2
Also declared: MIL/C05_Elementary_Number_Theory/S02_Induction_and_Recursion.lean:119 (same declaration text).
Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
theorem MyNat.succ_add line 55 source
no axioms what this means
Statement uses: MyNat, Eq, MyNat.add, MyNat.succ
Proof uses: MyNat.rec, Eq.refl, MyNat.zero, Eq.mpr, id, congrArg, MyNat.add.eq_2
Also declared: MIL/C05_Elementary_Number_Theory/S02_Induction_and_Recursion.lean:124 (same declaration text).
Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
theorem MyNat.add_comm line 61 source
no axioms what this means
Statement uses: MyNat, Eq, MyNat.add
Proof uses: MyNat.rec, Eq.mpr, MyNat.zero, id, congrArg, MyNat.zero_add, Eq.refl, MyNat.succ, MyNat.add.eq_2, MyNat.succ_add
Also declared: MIL/C05_Elementary_Number_Theory/S02_Induction_and_Recursion.lean:130 (same declaration text).
Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
theorem MyNat.add_assoc line 67 source
no axioms what this means
Statement uses: MyNat, Eq, MyNat.add
Proof uses: MyNat.rec, Eq.refl, MyNat.zero, Eq.mpr, MyNat.succ, id, congrArg, MyNat.add.eq_2
Distinct definitions of this name: MIL/C05_Elementary_Number_Theory/S02_Induction_and_Recursion.lean:136 (same statement text; different proof or body). Qualify references as MyNat.add_assoc@path.
Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
theorem MyNat.mul_add line 73 source
no axioms what this means
Statement uses: MyNat, Eq, MyNat.mul, MyNat.add
Proof uses: MyNat.rec, Eq.refl, MyNat.zero, Eq.mpr, MyNat.succ, id, congrArg, MyNat.add.eq_2, MyNat.mul.eq_2, MyNat.add_assoc
Distinct definitions of this name: MIL/C05_Elementary_Number_Theory/S02_Induction_and_Recursion.lean:138 (same statement text; different proof or body). Qualify references as MyNat.mul_add@path.
Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
theorem MyNat.zero_mul line 78 source
no axioms what this means
Statement uses: MyNat, Eq, MyNat.mul, MyNat.zero
Proof uses: MyNat.rec, Eq.refl, Eq.mpr, MyNat.succ, MyNat.add, id, congrArg, MyNat.mul.eq_2
Distinct definitions of this name: MIL/C05_Elementary_Number_Theory/S02_Induction_and_Recursion.lean:140 (same statement text; different proof or body). Qualify references as MyNat.zero_mul@path.
Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
theorem MyNat.succ_mul line 84 source
no axioms what this means
Statement uses: MyNat, Eq, MyNat.mul, MyNat.succ, MyNat.add
Proof uses: MyNat.rec, Eq.refl, MyNat.zero, Eq.mpr, id, congrArg, MyNat.mul.eq_2, MyNat.add_assoc, MyNat.add_comm, MyNat.succ_add
Distinct definitions of this name: MIL/C05_Elementary_Number_Theory/S02_Induction_and_Recursion.lean:142 (same statement text; different proof or body). Qualify references as MyNat.succ_mul@path.
Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
theorem MyNat.mul_comm line 90 source
no axioms what this means
Statement uses: MyNat, Eq, MyNat.mul
Proof uses: MyNat.rec, Eq.mpr, MyNat.zero, id, congrArg, MyNat.zero_mul, Eq.refl, MyNat.succ, MyNat.add, MyNat.mul.eq_2, MyNat.succ_mul
Distinct definitions of this name: MIL/C05_Elementary_Number_Theory/S02_Induction_and_Recursion.lean:144 (same statement text; different proof or body). Qualify references as MyNat.mul_comm@path.
Tactic trace: 5 steps
Open to load the checked before-and-after goal states.