MIL/C05_Elementary_Number_Theory/S04_More_Induction.lean

GitHub source file

21 declarations, 1 contain sorry, 0 declared as axioms

1. def more_induction.fac line 7 source

   no axioms what this means

   Statement uses: Nat

   2 instances, coercions and auxiliary constants left out.

2. theorem more_induction.fac_pos line 11 source

   standard axioms: propext what this means

   Statement uses: Nat, LT.lt, OfNat.ofNat, more_induction.fac

   Proof uses: Nat.recAux, Eq.mpr, id, Eq, congrArg, more_induction.fac.eq_1, zero_lt_one, HAdd.hAdd, HMul.hMul, Nat.succ, more_induction.fac.eq_2, mul_pos, Nat.succ_pos

   17 instances, coercions and auxiliary constants left out.

   Tactic trace: 18 steps

   Open to load the checked before-and-after goal states.

3. example more_induction.(example at line 18) line 18 source
4. example more_induction.(example at line 27) line 27 source
5. theorem more_induction.fac_pos' line 36 source

   standard axioms: propext what this means

   Statement uses: Nat, LT.lt, OfNat.ofNat, more_induction.fac

   6 instances, coercions and auxiliary constants left out.

   Tactic trace: 4 steps

   Open to load the checked before-and-after goal states.

6. def more_induction.fib line 44 source

   no axioms what this means

   Statement uses: Nat

   2 instances, coercions and auxiliary constants left out.

   Also declared: MIL/C05_Elementary_Number_Theory/solutions/Solutions_S04_More_Induction.lean:7 (same declaration text).

7. theorem more_induction.fib_add_two line 49 source

   no axioms what this means

   Statement uses: Nat, Eq, more_induction.fib, HAdd.hAdd, OfNat.ofNat

   Proof uses: rfl

   6 instances, coercions and auxiliary constants left out.

   Also declared: MIL/C05_Elementary_Number_Theory/solutions/Solutions_S04_More_Induction.lean:12 (same declaration text).

   Tactic trace: 1 steps

   Open to load the checked before-and-after goal states.

8. example more_induction.(example at line 51) line 51 source
9. def more_induction.phi line 55 source

   standard axioms: Classical.choice, Quot.sound, propext what this means

   Statement uses: Real

   Proof uses: HDiv.hDiv, HAdd.hAdd, OfNat.ofNat, Real.sqrt

   11 instances, coercions and auxiliary constants left out.

10. def more_induction.phi' line 56 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Real

    Proof uses: HDiv.hDiv, HSub.hSub, OfNat.ofNat, Real.sqrt

    11 instances, coercions and auxiliary constants left out.

11. theorem more_induction.fib_eq line 58 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, Eq, Real, more_induction.fib, HDiv.hDiv, HSub.hSub, HPow.hPow, more_induction.phi, more_induction.phi', Real.sqrt, OfNat.ofNat

    30 instances, coercions and auxiliary constants left out.

    Tactic trace: 6 steps

    Open to load the checked before-and-after goal states.

12. theorem more_induction.fib_coprime_fib_succ line 65 source

    standard axioms: Quot.sound, propext what this means

    Statement uses: Nat, Nat.Coprime, more_induction.fib, HAdd.hAdd, OfNat.ofNat

    Proof uses: Nat.recAux, of_eq_true, Nat.coprime_one_right_eq_true, Eq.mpr, id, Eq, Nat.Coprime.symm

    7 instances, coercions and auxiliary constants left out.

    Tactic trace: 4 steps

    Open to load the checked before-and-after goal states.

13. def more_induction.fib' line 75 source

    no axioms what this means

    Statement uses: Nat

    Proof uses: more_induction.fib'.aux, OfNat.ofNat

    1 instances, coercions and auxiliary constants left out.

14. theorem more_induction.fib'.aux_eq line 81 source

    standard axioms: propext what this means

    Statement uses: Nat, Eq, more_induction.fib'.aux, more_induction.fib, HAdd.hAdd, OfNat.ofNat

    Proof uses: Nat.recAux, of_eq_true, Eq.trans, True, congrArg, zero_add, eq_self, Eq.mpr, id, Nat.succ, more_induction.fib'.aux.eq_2, Eq.symm, more_induction.fib_add_two, add_assoc, add_comm, Eq.refl

    13 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

    Open to load the checked before-and-after goal states.

15. theorem more_induction.fib'_eq_fib line 86 source

    standard axioms: Quot.sound, propext what this means

    Statement uses: Eq, Nat, more_induction.fib', more_induction.fib

    Proof uses: funext, Eq.mpr, more_induction.fib'.aux, OfNat.ofNat, id, congrArg, more_induction.fib'.eq_1, HAdd.hAdd, more_induction.fib'.aux_eq, Eq.refl

    3 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

    Open to load the checked before-and-after goal states.

16. theorem more_induction.fib_add line 92 source

    standard axioms: propext what this means

    Statement uses: Nat, Eq, more_induction.fib, HAdd.hAdd, OfNat.ofNat, HMul.hMul

    Proof uses: Nat.recAux, of_eq_true, Eq.trans, True, congr, congrArg, congrFun', add_zero, MulZeroClass.mul_zero, mul_one, zero_add, eq_self, Eq.mpr, id, Eq.mp, add_comm, add_assoc, Mathlib.Tactic.Ring.of_eq, HPow.hPow, Nat.rawCast and 19 more

    33 instances, coercions and auxiliary constants left out.

    Also declared: MIL/C05_Elementary_Number_Theory/solutions/Solutions_S04_More_Induction.lean:14 (same declaration text).

    Tactic trace: 6 steps

    Open to load the checked before-and-after goal states.

17. theorem more_induction.fib_add' line 101 source

    standard axioms: propext what this means

    Statement uses: Nat, Eq, more_induction.fib, HAdd.hAdd, OfNat.ofNat, HMul.hMul

    12 instances, coercions and auxiliary constants left out.

    Tactic trace: 6 steps

    Open to load the checked before-and-after goal states.

18. example more_induction.(example at line 109) sorry line 109 source
19. theorem more_induction.ne_one_iff_exists_prime_dvd line 114 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, Iff, Ne, OfNat.ofNat, Exists, And, Nat.Prime, Dvd.dvd

    Proof uses: WellFounded.Nat.fix, InvImage, LT.lt, more_induction.fib_eq.match_1, Unit, Eq.mpr, id, Eq, Eq.trans, True, congr, congrArg, Not, False, not_false_eq_true, funext, and_true, true_iff, Exists.intro, Nat.prime_two and 55 more

    51 instances, coercions and auxiliary constants left out.

    Tactic trace: 19 steps

    Open to load the checked before-and-after goal states.

20. theorem more_induction.zero_lt_of_mul_eq_one line 131 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, Eq, HMul.hMul, OfNat.ofNat, And, LT.lt

    Proof uses: Nat.casesAuxOn, of_eq_true, Eq.trans, False, True, implies_congr, congrFun', congrArg, MulZeroClass.mul_zero, congr, and_self, Eq.symm, HAdd.hAdd, MulZeroClass.zero_mul, LE.le, and_true, Eq.refl, and_false, Units, implies_true

    69 instances, coercions and auxiliary constants left out.

    Tactic trace: 7 steps

    Open to load the checked before-and-after goal states.

21. example more_induction.(example at line 134) line 134 source