MIL/C03_Logic/solutions/Solutions_S05_Disjunction.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Imports (2)
  1. theorem C03S05.MyAbs.le_abs_self line 12 source

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

    Statement uses: Real, LE.le, abs

    Proof uses: OfNat.ofNat, LT.lt, Or, le_or_gt, Eq.mpr, id, Eq, congrArg, abs_of_nonneg, le_refl, Neg.neg, abs_of_neg, le_of_not_gt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HAdd.hAdd, HMul.hMul, Nat, HSub.hSub, Mathlib.Tactic.Ring.of_eq and 51 more

    68 instances, coercions and auxiliary constants left out.

    Distinct definitions of this name: MIL/C03_Logic/S05_Disjunction.lean:60 (same statement text; different proof or body). Qualify references as C03S05.MyAbs.le_abs_self@path.

    Tactic trace: 6 steps

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

  2. theorem C03S05.MyAbs.neg_le_abs line 18 source

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

    Statement uses: Real, LE.le, Neg.neg, abs

    Proof uses: OfNat.ofNat, LT.lt, Or, le_or_gt, Eq.mpr, id, Eq, congrArg, abs_of_nonneg, le_of_not_gt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HAdd.hAdd, HMul.hMul, Nat, HSub.hSub, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, HPow.hPow, Nat.rawCast and 53 more

    70 instances, coercions and auxiliary constants left out.

    Distinct definitions of this name: MIL/C03_Logic/S05_Disjunction.lean:63 (same statement text; different proof or body). Qualify references as C03S05.MyAbs.neg_le_abs@path.

    Tactic trace: 6 steps

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

  3. theorem C03S05.MyAbs.abs_add_le line 24 source

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

    Statement uses: Real, LE.le, abs, HAdd.hAdd

    Proof uses: OfNat.ofNat, LT.lt, Or, le_or_gt, Eq.mpr, id, Eq, congrArg, abs_of_nonneg, le_of_not_gt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HSub.hSub, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, HMul.hMul, HPow.hPow, Nat, Nat.rawCast, Int.rawCast and 40 more

    62 instances, coercions and auxiliary constants left out.

    Distinct definitions of this name: MIL/C03_Logic/S05_Disjunction.lean:66 (same statement text; different proof or body). Qualify references as C03S05.MyAbs.abs_add_le@path.

    Tactic trace: 7 steps

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

  4. theorem C03S05.MyAbs.lt_abs line 31 source

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

    Statement uses: Real, Iff, LT.lt, abs, Or, Neg.neg

    Proof uses: LE.le, OfNat.ofNat, le_or_gt, Eq.mpr, id, Eq, congrArg, abs_of_nonneg, Iff.intro, Or.inl, lt_of_not_ge, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HAdd.hAdd, HMul.hMul, Nat, HSub.hSub, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, HPow.hPow and 59 more

    70 instances, coercions and auxiliary constants left out.

    Distinct definitions of this name: MIL/C03_Logic/S05_Disjunction.lean:69 (same statement text; different proof or body). Qualify references as C03S05.MyAbs.lt_abs@path.

    Tactic trace: 28 steps

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

  5. theorem C03S05.MyAbs.abs_lt line 52 source

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

    Statement uses: Real, Iff, LT.lt, abs, And, Neg.neg

    Proof uses: LE.le, OfNat.ofNat, Or, le_or_gt, Eq.mpr, id, Eq, congrArg, abs_of_nonneg, Iff.intro, And.intro, lt_of_not_ge, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HAdd.hAdd, HMul.hMul, Nat, HSub.hSub, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr and 60 more

    71 instances, coercions and auxiliary constants left out.

    Distinct definitions of this name: MIL/C03_Logic/S05_Disjunction.lean:72 (same statement text; different proof or body). Qualify references as C03S05.MyAbs.abs_lt@path.

    Tactic trace: 94 steps

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

  6. example C03S05.(example at line 76) line 76 source
  7. example C03S05.(example at line 79) line 79 source
  8. example C03S05.(example at line 90) line 90 source
  9. example C03S05.(example at line 105) line 105 source
  10. example C03S05.(example at line 116) line 116 source
  11. example C03S05.(example at line 129) line 129 source