MIL/C08_Hierarchies/S01_Basics.lean

GitHub source file

59 declarations, 8 contain sorry, 0 declared as axioms

Imports (3)
Imported by 1 file
  1. class One₁ line 8 source

    no axioms what this means

    Also declared: MIL/C08_Hierarchies/solutions/Solutions_S01_Basics.lean:8 (same declaration text).

  2. structure One₂ line 15 source

    no axioms what this means

    Also declared: MIL/C08_Hierarchies/solutions/Solutions_S01_Basics.lean:15 (same declaration text).

  3. example (example at line 22) line 22 source
  4. example (example at line 24) line 24 source
  5. example (example at line 29) line 29 source
  6. example (example at line 31) line 31 source
  7. class Dia₁ line 34 source

    no axioms what this means

    Also declared: MIL/C08_Hierarchies/solutions/Solutions_S01_Basics.lean:34 (same declaration text).

  8. class Semigroup₀ line 40 source

    no axioms what this means

    Also declared: MIL/C08_Hierarchies/solutions/Solutions_S01_Basics.lean:40 (same declaration text).

  9. example (example at line 48) line 48 source
  10. class Semigroup₁ line 51 source

    no axioms what this means

    Also declared: MIL/C08_Hierarchies/solutions/Solutions_S01_Basics.lean:51 (same declaration text).

  11. example (example at line 55) line 55 source
  12. class Semigroup₂ line 58 source

    no axioms what this means

    Also declared: MIL/C08_Hierarchies/solutions/Solutions_S01_Basics.lean:58 (same declaration text).

  13. class DiaOneClass₁ line 62 source

    no axioms what this means

    Also declared: MIL/C08_Hierarchies/solutions/Solutions_S01_Basics.lean:62 (same declaration text).

  14. example (example at line 71) line 71 source
  15. class Monoid₁ line 74 source

    no axioms what this means

    Also declared: MIL/C08_Hierarchies/solutions/Solutions_S01_Basics.lean:74 (same declaration text).

  16. class Monoid₂ line 77 source

    no axioms what this means

    Also declared: MIL/C08_Hierarchies/solutions/Solutions_S01_Basics.lean:77 (same declaration text).

  17. example (example at line 82) line 82 source
  18. class Inv₁ line 97 source

    no axioms what this means

    Also declared: MIL/C08_Hierarchies/solutions/Solutions_S01_Basics.lean:97 (same declaration text).

  19. class Group₁ line 104 source

    no axioms what this means

    Also declared: MIL/C08_Hierarchies/solutions/Solutions_S01_Basics.lean:104 (same declaration text).

  20. lemma left_inv_eq_right_inv₁ line 108 source

    no axioms what this means

    Statement uses: Monoid₁, Eq, Dia₁.dia, One₁.one

    Proof uses: Eq.mpr, id, congrArg, Eq.symm, DiaOneClass₁.one_dia, Semigroup₁.dia_assoc, DiaOneClass₁.dia_one, Eq.refl

    8 instances, coercions and auxiliary constants left out.

    Also declared: MIL/C08_Hierarchies/solutions/Solutions_S01_Basics.lean:108 (same declaration text).

    Tactic trace: 2 steps

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

  21. example (example at line 117) line 117 source
  22. lemma inv_eq_of_dia sorry line 121 source

    depends on sorry what this means

    Statement uses: Group₁, Eq, Dia₁.dia, One₁.one, Inv₁.inv

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

    11 instances, coercions and auxiliary constants left out.

    Distinct definitions of this name: MIL/C08_Hierarchies/solutions/Solutions_S01_Basics.lean:121 (same statement text; different proof or body). Qualify references as inv_eq_of_dia@path.

  23. lemma dia_inv sorry line 124 source

    depends on sorry what this means

    Statement uses: Group₁, Eq, Dia₁.dia, Inv₁.inv, One₁.one

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

    11 instances, coercions and auxiliary constants left out.

    Distinct definitions of this name: MIL/C08_Hierarchies/solutions/Solutions_S01_Basics.lean:124 (same statement text; different proof or body). Qualify references as dia_inv@path.

  24. class AddSemigroup₃ line 130 source

    no axioms what this means

    Also declared: MIL/C08_Hierarchies/solutions/Solutions_S01_Basics.lean:131 (same declaration text).

  25. class Semigroup₃ line 135 source

    no axioms what this means

    Also declared: MIL/C08_Hierarchies/solutions/Solutions_S01_Basics.lean:136 (same declaration text).

  26. class AddMonoid₃ line 139 source

    no axioms what this means

    Also declared: MIL/C08_Hierarchies/solutions/Solutions_S01_Basics.lean:140 (same declaration text).

  27. class Monoid₃ line 142 source

    no axioms what this means

    Also declared: MIL/C08_Hierarchies/solutions/Solutions_S01_Basics.lean:143 (same declaration text).

  28. lemma left_inv_eq_right_inv' line 149 source

    no axioms what this means

    Statement uses: Monoid₃, Eq, HMul.hMul, OfNat.ofNat

    Proof uses: Eq.mpr, id, congrArg, Eq.symm, one_mul, Semigroup₃.mul_assoc₃, mul_one, Eq.refl

    15 instances, coercions and auxiliary constants left out.

    Also declared: MIL/C08_Hierarchies/solutions/Solutions_S01_Basics.lean:150 (same declaration text).

    Tactic trace: 1 steps

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

  29. class AddCommSemigroup₃ line 154 source

    no axioms what this means

    Also declared: MIL/C08_Hierarchies/solutions/Solutions_S01_Basics.lean:155 (same declaration text).

  30. class CommSemigroup₃ line 158 source

    no axioms what this means

    Also declared: MIL/C08_Hierarchies/solutions/Solutions_S01_Basics.lean:159 (same declaration text).

  31. class AddCommMonoid₃ line 161 source

    no axioms what this means

    Also declared: MIL/C08_Hierarchies/solutions/Solutions_S01_Basics.lean:162 (same declaration text).

  32. class CommMonoid₃ line 164 source

    no axioms what this means

    Also declared: MIL/C08_Hierarchies/solutions/Solutions_S01_Basics.lean:165 (same declaration text).

  33. class AddGroup₃ line 166 source

    no axioms what this means

    Also declared: MIL/C08_Hierarchies/solutions/Solutions_S01_Basics.lean:167 (same declaration text).

  34. class Group₃ line 170 source

    no axioms what this means

    Also declared: MIL/C08_Hierarchies/solutions/Solutions_S01_Basics.lean:171 (same declaration text).

  35. lemma inv_eq_of_mul sorry line 179 source

    depends on sorry what this means

    Statement uses: Group₃, Eq, HMul.hMul, OfNat.ofNat, Inv.inv

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

    19 instances, coercions and auxiliary constants left out.

    Distinct definitions of this name: MIL/C08_Hierarchies/solutions/Solutions_S01_Basics.lean:180 (same statement text; different proof or body). Qualify references as inv_eq_of_mul@path.

  36. lemma Group₃.mul_inv sorry line 184 source

    depends on sorry what this means

    Statement uses: Group₃, Eq, HMul.hMul, Inv.inv, OfNat.ofNat

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

    19 instances, coercions and auxiliary constants left out.

    Distinct definitions of this name: MIL/C08_Hierarchies/solutions/Solutions_S01_Basics.lean:185 (same statement text; different proof or body). Qualify references as Group₃.mul_inv@path.

    Tactic trace: 1 steps

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

  37. lemma mul_left_cancel₃ sorry line 188 source

    depends on sorry what this means

    Statement uses: Group₃, Eq, HMul.hMul

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

    9 instances, coercions and auxiliary constants left out.

    Distinct definitions of this name: MIL/C08_Hierarchies/solutions/Solutions_S01_Basics.lean:189 (same statement text; different proof or body). Qualify references as mul_left_cancel₃@path.

    Tactic trace: 1 steps

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

  38. lemma mul_right_cancel₃ sorry line 192 source

    depends on sorry what this means

    Statement uses: Group₃, Eq, HMul.hMul

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

    9 instances, coercions and auxiliary constants left out.

    Distinct definitions of this name: MIL/C08_Hierarchies/solutions/Solutions_S01_Basics.lean:193 (same statement text; different proof or body). Qualify references as mul_right_cancel₃@path.

    Tactic trace: 1 steps

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

  39. class AddCommGroup₃ line 195 source

    no axioms what this means

    Also declared: MIL/C08_Hierarchies/solutions/Solutions_S01_Basics.lean:196 (same declaration text).

  40. class CommGroup₃ line 198 source

    no axioms what this means

    Also declared: MIL/C08_Hierarchies/solutions/Solutions_S01_Basics.lean:199 (same declaration text).

  41. class Ring₃ line 202 source

    no axioms what this means

    Also declared: MIL/C08_Hierarchies/solutions/Solutions_S01_Basics.lean:203 (same declaration text).

    Tactic trace: 8 steps

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

  42. instance (instance at line 208) sorry line 208 source
  43. instance (instance at line 212) line 212 source
  44. class LE₁ line 230 source

    no axioms what this means

    Also declared: MIL/C08_Hierarchies/solutions/Solutions_S01_Basics.lean:240 (same declaration text).

  45. class Preorder₁ line 236 source

    no axioms what this means

    Distinct definitions of this name: MIL/C08_Hierarchies/solutions/Solutions_S01_Basics.lean:246 (different declaration text). Qualify references as Preorder₁@path.

  46. class PartialOrder₁ line 238 source

    no axioms what this means

    Distinct definitions of this name: MIL/C08_Hierarchies/solutions/Solutions_S01_Basics.lean:251 (different declaration text). Qualify references as PartialOrder₁@path.

  47. class OrderedCommMonoid₁ line 240 source

    no axioms what this means

    Distinct definitions of this name: MIL/C08_Hierarchies/solutions/Solutions_S01_Basics.lean:255 (different declaration text). Qualify references as OrderedCommMonoid₁@path.

  48. instance (instance at line 242) line 242 source
  49. class SMul₃ line 244 source

    no axioms what this means

    Also declared: MIL/C08_Hierarchies/solutions/Solutions_S01_Basics.lean:272 (same declaration text).

  50. class Module₁ line 251 source

    depends on sorry what this means

    Statement uses: Ring₃, AddCommGroup₃

    Also declared: MIL/C08_Hierarchies/solutions/Solutions_S01_Basics.lean:279 (same declaration text).

  51. instance selfModule line 258 source

    depends on sorry what this means

    Statement uses: Ring₃, Module₁

    Proof uses: Module₁.mk, SMul₃.mk, HMul.hMul, Ring₃.right_distrib, Ring₃.left_distrib

    9 instances, coercions and auxiliary constants left out.

    Also declared: MIL/C08_Hierarchies/solutions/Solutions_S01_Basics.lean:286 (same declaration text).

  52. def nsmul₁ line 266 source

    no axioms what this means

    Statement uses: Zero, Add, Nat

    2 instances, coercions and auxiliary constants left out.

    Also declared: MIL/C08_Hierarchies/solutions/Solutions_S01_Basics.lean:294 (same declaration text).

  53. def zsmul₁ line 270 source

    no axioms what this means

    Statement uses: Zero, Add, Neg, Int

    Proof uses: zsmul₁.match_1, Nat, nsmul₁, Neg.neg, Nat.succ

    Also declared: MIL/C08_Hierarchies/solutions/Solutions_S01_Basics.lean:298 (same declaration text).

  54. instance abGrpModule sorry line 274 source

    depends on sorry what this means

    Statement uses: AddCommGroup₃, Module₁, Int

    Proof uses: Module₁.mk, SMul₃.mk, zsmul₁, sorryAx, Lean.Name, Eq, OfNat.ofNat, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, Nat, HMul.hMul, HAdd.hAdd

    26 instances, coercions and auxiliary constants left out.

    Also declared: MIL/C08_Hierarchies/solutions/Solutions_S01_Basics.lean:302 (same declaration text).

  55. class AddMonoid₄ line 285 source

    no axioms what this means

    Also declared: MIL/C08_Hierarchies/solutions/Solutions_S01_Basics.lean:313 (same declaration text).

  56. instance mySMul line 293 source

    no axioms what this means

    Statement uses: AddMonoid₄, SMul, Nat

    Proof uses: SMul.mk, AddMonoid₄.nsmul

    Also declared: MIL/C08_Hierarchies/solutions/Solutions_S01_Basics.lean:321 (same declaration text).

    Tactic trace: 7 steps

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

  57. instance (instance at line 295) line 295 source
  58. instance (instance at line 302) line 302 source
  59. example (example at line 313) line 313 source