MIL/C02_Basics/solutions/Solutions_S05_Proving_Facts_about_Algebraic_Structures.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Imports (2)
  1. example (example at line 8) line 8 source
  2. example (example at line 15) line 15 source
  3. example (example at line 36) line 36 source
  4. example (example at line 43) line 43 source
  5. theorem absorb1 line 64 source

    no axioms what this means

    Statement uses: Lattice, Eq, Min.min, Max.max

    Proof uses: le_antisymm, inf_le_left, le_inf, le_refl, le_sup_left

    10 instances, coercions and auxiliary constants left out.

    Distinct definitions of this name: MIL/C02_Basics/S05_Proving_Facts_about_Algebraic_Structures.lean:50 (same statement text; different proof or body). Qualify references as absorb1@path.

    Tactic trace: 7 steps

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

  6. theorem absorb2 line 71 source

    no axioms what this means

    Statement uses: Lattice, Eq, Max.max, Min.min

    Proof uses: le_antisymm, sup_le, le_refl, inf_le_left, le_sup_left

    10 instances, coercions and auxiliary constants left out.

    Distinct definitions of this name: MIL/C02_Basics/S05_Proving_Facts_about_Algebraic_Structures.lean:53 (same statement text; different proof or body). Qualify references as absorb2@path.

    Tactic trace: 9 steps

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

  7. example (example at line 94) line 94 source
  8. example (example at line 98) line 98 source
  9. theorem aux1 line 108 source

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

    Statement uses: Ring, PartialOrder, IsStrictOrderedRing, LE.le, OfNat.ofNat, HSub.hSub

    Proof uses: Eq.mpr, id, Eq, congrArg, Eq.symm, sub_self, HAdd.hAdd, Neg.neg, sub_eq_add_neg, add_comm, add_le_add_right

    41 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  10. theorem aux2 line 112 source

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

    Statement uses: Ring, PartialOrder, IsStrictOrderedRing, LE.le, OfNat.ofNat, HSub.hSub

    Proof uses: Eq.mpr, HAdd.hAdd, id, Eq, congrArg, Eq.symm, add_zero, sub_add_cancel, add_comm, add_le_add_right

    42 instances, coercions and auxiliary constants left out.

    Tactic trace: 9 steps

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

  11. example (example at line 116) line 116 source
  12. example (example at line 127) line 127 source