MIL/C05_Elementary_Number_Theory/S02_Induction_and_Recursion.lean

GitHub source file

35 declarations, 7 contain sorry, 0 declared as axioms

Imports (2)
Imported by 1 file
  1. example (example at line 4) line 4 source
  2. example (example at line 7) line 7 source
  3. def fac line 10 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_S02_Induction_and_Recursion.lean:4 (same declaration text).

    Tactic trace: 4 steps

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

  4. example (example at line 14) line 14 source
  5. example (example at line 17) line 17 source
  6. example (example at line 20) line 20 source
  7. example (example at line 23) line 23 source
  8. example (example at line 26) line 26 source
  9. example (example at line 29) line 29 source
  10. theorem fac_pos line 32 source

    standard axioms: propext what this means

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

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

    17 instances, coercions and auxiliary constants left out.

    Tactic trace: 6 steps

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

  11. theorem dvd_fac line 39 source

    standard axioms: propext what this means

    Statement uses: Nat, LT.lt, OfNat.ofNat, LE.le, Dvd.dvd, fac

    Proof uses: Nat.recAux, absurd, not_lt_of_ge, HAdd.hAdd, Eq.mpr, HMul.hMul, id, Eq, congrArg, Nat.succ, fac.eq_2, Or, Nat.of_le_succ, dvd_mul_of_dvd_right, dvd_mul_right

    16 instances, coercions and auxiliary constants left out.

    Tactic trace: 9 steps

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

  12. theorem pow_two_le_fac sorry line 48 source

    depends on sorry 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, sorryAx, Lean.Name, HAdd.hAdd, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

    32 instances, coercions and auxiliary constants left out.

    Distinct definitions of this name: MIL/C05_Elementary_Number_Theory/solutions/Solutions_S02_Induction_and_Recursion.lean:8 (same statement text; different proof or body). Qualify references as pow_two_le_fac@path.

    Tactic trace: 9 steps

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

  13. example (example at line 62) line 62 source
  14. example (example at line 65) line 65 source
  15. example (example at line 68) line 68 source
  16. example (example at line 71) line 71 source
  17. example (example at line 74) line 74 source
  18. example (example at line 77) line 77 source
  19. example (example at line 80) line 80 source
  20. example (example at line 83) line 83 source
  21. example (example at line 86) line 86 source
  22. example (example at line 91) line 91 source
  23. theorem sum_id line 94 source

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

    Statement uses: Nat, Eq, Finset.sum, Finset.range, HAdd.hAdd, OfNat.ofNat, 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, Singleton.singleton, Finset, Finset.sum_congr, Membership.mem, Finset.sum_singleton and 31 more

    48 instances, coercions and auxiliary constants left out.

    Tactic trace: 8 steps

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

  24. theorem sum_sqr sorry line 101 source

    depends on sorry what this means

    Statement uses: Nat, Eq, Finset.sum, Finset.range, HAdd.hAdd, OfNat.ofNat, HPow.hPow, HDiv.hDiv, HMul.hMul

    Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

    22 instances, coercions and auxiliary constants left out.

    Distinct definitions of this name: MIL/C05_Elementary_Number_Theory/solutions/Solutions_S02_Induction_and_Recursion.lean:26 (same statement text; different proof or body). Qualify references as sum_sqr@path.

    Tactic trace: 1 steps

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

  25. inductive MyNat line 105 source

    no axioms what this means

    Also declared: MIL/C05_Elementary_Number_Theory/solutions/Solutions_S02_Induction_and_Recursion.lean:36 (same declaration text).

  26. def MyNat.add line 111 source

    no axioms what this means

    Statement uses: MyNat

    2 instances, coercions and auxiliary constants left out.

    Also declared: MIL/C05_Elementary_Number_Theory/solutions/Solutions_S02_Induction_and_Recursion.lean:42 (same declaration text).

  27. def MyNat.mul line 115 source

    no axioms what this means

    Statement uses: MyNat

    2 instances, coercions and auxiliary constants left out.

    Also declared: MIL/C05_Elementary_Number_Theory/solutions/Solutions_S02_Induction_and_Recursion.lean:46 (same declaration text).

  28. theorem MyNat.zero_add line 119 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/solutions/Solutions_S02_Induction_and_Recursion.lean:50 (same declaration text).

    Tactic trace: 4 steps

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

  29. theorem MyNat.succ_add line 124 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/solutions/Solutions_S02_Induction_and_Recursion.lean:55 (same declaration text).

    Tactic trace: 5 steps

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

  30. theorem MyNat.add_comm line 130 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/solutions/Solutions_S02_Induction_and_Recursion.lean:61 (same declaration text).

    Tactic trace: 5 steps

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

  31. theorem MyNat.add_assoc sorry line 136 source

    depends on sorry what this means

    Statement uses: MyNat, Eq, MyNat.add

    Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Nat

    1 instances, coercions and auxiliary constants left out.

    Distinct definitions of this name: MIL/C05_Elementary_Number_Theory/solutions/Solutions_S02_Induction_and_Recursion.lean:67 (same statement text; different proof or body). Qualify references as MyNat.add_assoc@path.

    Tactic trace: 1 steps

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

  32. theorem MyNat.mul_add sorry line 138 source

    depends on sorry what this means

    Statement uses: MyNat, Eq, MyNat.mul, MyNat.add

    Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Nat

    1 instances, coercions and auxiliary constants left out.

    Distinct definitions of this name: MIL/C05_Elementary_Number_Theory/solutions/Solutions_S02_Induction_and_Recursion.lean:73 (same statement text; different proof or body). Qualify references as MyNat.mul_add@path.

    Tactic trace: 1 steps

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

  33. theorem MyNat.zero_mul sorry line 140 source

    depends on sorry what this means

    Statement uses: MyNat, Eq, MyNat.mul, MyNat.zero

    Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Nat

    1 instances, coercions and auxiliary constants left out.

    Distinct definitions of this name: MIL/C05_Elementary_Number_Theory/solutions/Solutions_S02_Induction_and_Recursion.lean:78 (same statement text; different proof or body). Qualify references as MyNat.zero_mul@path.

    Tactic trace: 1 steps

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

  34. theorem MyNat.succ_mul sorry line 142 source

    depends on sorry what this means

    Statement uses: MyNat, Eq, MyNat.mul, MyNat.succ, MyNat.add

    Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Nat

    1 instances, coercions and auxiliary constants left out.

    Distinct definitions of this name: MIL/C05_Elementary_Number_Theory/solutions/Solutions_S02_Induction_and_Recursion.lean:84 (same statement text; different proof or body). Qualify references as MyNat.succ_mul@path.

    Tactic trace: 1 steps

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

  35. theorem MyNat.mul_comm sorry line 144 source

    depends on sorry what this means

    Statement uses: MyNat, Eq, MyNat.mul

    Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Nat

    1 instances, coercions and auxiliary constants left out.

    Distinct definitions of this name: MIL/C05_Elementary_Number_Theory/solutions/Solutions_S02_Induction_and_Recursion.lean:90 (same statement text; different proof or body). Qualify references as MyNat.mul_comm@path.

    Tactic trace: 1 steps

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