MIL/C03_Logic/solutions/Solutions_S04_Conjunction_and_Iff.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Imports (3)
  1. example C03S04.(example at line 7) line 7 source
  2. example C03S04.(example at line 15) line 15 source
  3. theorem C03S04.aux line 30 source

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

    Statement uses: Real, Eq, HAdd.hAdd, HPow.hPow, Nat, OfNat.ofNat

    Proof uses: Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt, Not.intro, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HSub.hSub, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, HMul.hMul, Nat.rawCast, Int.rawCast, inferInstance, Ring, Int.negOfNat, Mathlib.Tactic.Ring.Common.sub_congr, Mathlib.Tactic.Ring.Common.pow_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.mpr and 46 more

    76 instances, coercions and auxiliary constants left out.

    Distinct definitions of this name: MIL/C03_Logic/S04_Conjunction_and_Iff.lean:107 (same statement text; different proof or body). Qualify references as C03S04.aux@path.

    Tactic trace: 11 steps

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

  4. example C03S04.(example at line 34) line 34 source
  5. theorem C03S04.not_monotone_iff line 44 source

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

    Statement uses: Real, Iff, Not, Monotone, Exists, And, LE.le, GT.gt

    Proof uses: Eq.mpr, id, Eq, congrArg, Monotone.eq_1, LT.lt, congrFun', Eq.trans, Mathlib.Tactic.Push.not_forall_eq, funext, Iff.rfl

    13 instances, coercions and auxiliary constants left out.

    Also declared: MIL/C03_Logic/S04_Conjunction_and_Iff.lean:127 (same declaration text).

    Tactic trace: 34 steps

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

  6. example C03S04.(example at line 49) line 49 source
  7. example C03S04.(example at line 58) line 58 source
  8. example C03S04.(example at line 80) line 80 source
  9. example C03S04.(example at line 85) line 85 source