MIL/C08_Hierarchies/solutions/Solutions_S01_Basics.lean

GitHub source file

61 declarations, 1 contain sorry, 0 declared as axioms

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

    no axioms what this means

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

  2. structure One₂ line 15 source

    no axioms what this means

    Also declared: MIL/C08_Hierarchies/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/S01_Basics.lean:34 (same declaration text).

  8. class Semigroup₀ line 40 source

    no axioms what this means

    Also declared: MIL/C08_Hierarchies/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/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/S01_Basics.lean:58 (same declaration text).

  13. class DiaOneClass₁ line 62 source

    no axioms what this means

    Also declared: MIL/C08_Hierarchies/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/S01_Basics.lean:74 (same declaration text).

  16. class Monoid₂ line 77 source

    no axioms what this means

    Also declared: MIL/C08_Hierarchies/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/S01_Basics.lean:97 (same declaration text).

  19. class Group₁ line 104 source

    no axioms what this means

    Also declared: MIL/C08_Hierarchies/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/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 line 121 source

    no axioms what this means

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

    Proof uses: left_inv_eq_right_inv₁, Group₁.inv_dia

    10 instances, coercions and auxiliary constants left out.

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

  23. lemma dia_inv line 124 source

    no axioms what this means

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

    Proof uses: Eq.mpr, id, congrArg, Monoid₁.toOne₁, Eq.symm, Group₁.inv_dia, inv_eq_of_dia, Eq.refl

    12 instances, coercions and auxiliary constants left out.

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

    Tactic trace: 1 steps

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

  24. class AddSemigroup₃ line 131 source

    no axioms what this means

    Also declared: MIL/C08_Hierarchies/S01_Basics.lean:130 (same declaration text).

  25. class Semigroup₃ line 136 source

    no axioms what this means

    Also declared: MIL/C08_Hierarchies/S01_Basics.lean:135 (same declaration text).

  26. class AddMonoid₃ line 140 source

    no axioms what this means

    Also declared: MIL/C08_Hierarchies/S01_Basics.lean:139 (same declaration text).

  27. class Monoid₃ line 143 source

    no axioms what this means

    Also declared: MIL/C08_Hierarchies/S01_Basics.lean:142 (same declaration text).

  28. lemma left_inv_eq_right_inv' line 150 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/S01_Basics.lean:149 (same declaration text).

    Tactic trace: 1 steps

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

  29. class AddCommSemigroup₃ line 155 source

    no axioms what this means

    Also declared: MIL/C08_Hierarchies/S01_Basics.lean:154 (same declaration text).

  30. class CommSemigroup₃ line 159 source

    no axioms what this means

    Also declared: MIL/C08_Hierarchies/S01_Basics.lean:158 (same declaration text).

  31. class AddCommMonoid₃ line 162 source

    no axioms what this means

    Also declared: MIL/C08_Hierarchies/S01_Basics.lean:161 (same declaration text).

  32. class CommMonoid₃ line 165 source

    no axioms what this means

    Also declared: MIL/C08_Hierarchies/S01_Basics.lean:164 (same declaration text).

  33. class AddGroup₃ line 167 source

    no axioms what this means

    Also declared: MIL/C08_Hierarchies/S01_Basics.lean:166 (same declaration text).

  34. class Group₃ line 171 source

    no axioms what this means

    Also declared: MIL/C08_Hierarchies/S01_Basics.lean:170 (same declaration text).

  35. lemma inv_eq_of_mul line 180 source

    no axioms what this means

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

    Proof uses: left_inv_eq_right_inv', Group₃.inv_mul

    18 instances, coercions and auxiliary constants left out.

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

  36. lemma Group₃.mul_inv line 185 source

    no axioms what this means

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

    Proof uses: Eq.mpr, id, congrArg, Monoid₃.toOne, Eq.symm, Group₃.inv_mul, inv_eq_of_mul, Eq.refl

    18 instances, coercions and auxiliary constants left out.

    Distinct definitions of this name: MIL/C08_Hierarchies/S01_Basics.lean:184 (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₃ line 189 source

    no axioms what this means

    Statement uses: Group₃, Eq, HMul.hMul

    Proof uses: Eq.mp, Inv.inv, congr, congrArg, Eq.trans, OfNat.ofNat, Monoid₃.toOne, congrFun', Group₃.inv_mul, one_mul, congr_arg

    12 instances, coercions and auxiliary constants left out.

    Distinct definitions of this name: MIL/C08_Hierarchies/S01_Basics.lean:188 (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₃ line 193 source

    no axioms what this means

    Statement uses: Group₃, Eq, HMul.hMul

    Proof uses: Eq.mp, Inv.inv, congr, congrArg, Eq.trans, Semigroup₃.mul_assoc₃, OfNat.ofNat, Group₃.mul_inv, mul_one, congr_arg

    13 instances, coercions and auxiliary constants left out.

    Distinct definitions of this name: MIL/C08_Hierarchies/S01_Basics.lean:192 (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 196 source

    no axioms what this means

    Also declared: MIL/C08_Hierarchies/S01_Basics.lean:195 (same declaration text).

  40. class CommGroup₃ line 199 source

    no axioms what this means

    Also declared: MIL/C08_Hierarchies/S01_Basics.lean:198 (same declaration text).

  41. class Ring₃ line 203 source

    no axioms what this means

    Also declared: MIL/C08_Hierarchies/S01_Basics.lean:202 (same declaration text).

    Tactic trace: 17 steps

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

  42. instance (instance at line 209) line 209 source
  43. instance (instance at line 222) line 222 source
  44. class LE₁ line 240 source

    no axioms what this means

    Also declared: MIL/C08_Hierarchies/S01_Basics.lean:230 (same declaration text).

  45. class Preorder₁ line 246 source

    no axioms what this means

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

  46. class PartialOrder₁ line 251 source

    no axioms what this means

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

  47. class OrderedCommMonoid₁ line 255 source

    no axioms what this means

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

  48. instance (instance at line 259) line 259 source
  49. class SMul₃ line 272 source

    no axioms what this means

    Also declared: MIL/C08_Hierarchies/S01_Basics.lean:244 (same declaration text).

  50. class Module₁ line 279 source

    standard axioms: propext what this means

    Statement uses: Ring₃, AddCommGroup₃

    Also declared: MIL/C08_Hierarchies/S01_Basics.lean:251 (same declaration text).

  51. instance selfModule line 286 source

    standard axioms: propext 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/S01_Basics.lean:258 (same declaration text).

  52. def nsmul₁ line 294 source

    no axioms what this means

    Statement uses: Zero, Add, Nat

    2 instances, coercions and auxiliary constants left out.

    Also declared: MIL/C08_Hierarchies/S01_Basics.lean:266 (same declaration text).

  53. def zsmul₁ line 298 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/S01_Basics.lean:270 (same declaration text).

  54. instance abGrpModule sorry line 302 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/S01_Basics.lean:274 (same declaration text).

  55. class AddMonoid₄ line 313 source

    no axioms what this means

    Also declared: MIL/C08_Hierarchies/S01_Basics.lean:285 (same declaration text).

  56. instance mySMul line 321 source

    no axioms what this means

    Statement uses: AddMonoid₄, SMul, Nat

    Proof uses: SMul.mk, AddMonoid₄.nsmul

    Also declared: MIL/C08_Hierarchies/S01_Basics.lean:293 (same declaration text).

    Tactic trace: 7 steps

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

  57. instance (instance at line 323) line 323 source
  58. instance (instance at line 330) line 330 source
  59. example (example at line 341) line 341 source
  60. class LT₁ line 342 source

    no axioms what this means

  61. class PreOrder₂ line 348 source

    no axioms what this means