MIL/C03_Logic/S02_The_Existential_Quantifier.lean

GitHub source file

30 declarations, 5 contain sorry, 0 declared as axioms

Imports (2)
Imported by 1 file
  1. example C03S02.(example at line 8) line 8 source
  2. example C03S02.(example at line 12) line 12 source
  3. example C03S02.(example at line 17) line 17 source
  4. example C03S02.(example at line 21) line 21 source
  5. example C03S02.(example at line 25) line 25 source
  6. def C03S02.FnUb line 28 source

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

    Statement uses: Real

    Proof uses: LE.le

    1 instances, coercions and auxiliary constants left out.

    Also declared: MIL/C03_Logic/solutions/Solutions_S02_The_Existential_Quantifier.lean:8 (same declaration text).

  7. def C03S02.FnLb line 31 source

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

    Statement uses: Real

    Proof uses: LE.le

    1 instances, coercions and auxiliary constants left out.

    Also declared: MIL/C03_Logic/solutions/Solutions_S02_The_Existential_Quantifier.lean:11 (same declaration text).

  8. def C03S02.FnHasUb line 34 source

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

    Statement uses: Real

    Proof uses: Exists, C03S02.FnUb

    Also declared: MIL/C03_Logic/solutions/Solutions_S02_The_Existential_Quantifier.lean:14 (same declaration text).

  9. def C03S02.FnHasLb line 37 source

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

    Statement uses: Real

    Proof uses: Exists, C03S02.FnLb

    Also declared: MIL/C03_Logic/solutions/Solutions_S02_The_Existential_Quantifier.lean:17 (same declaration text).

  10. theorem C03S02.fnUb_add line 40 source

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

    Statement uses: Real, C03S02.FnUb, HAdd.hAdd

    Proof uses: add_le_add, LE.le

    10 instances, coercions and auxiliary constants left out.

    Also declared: MIL/C03_Logic/solutions/Solutions_S02_The_Existential_Quantifier.lean:20 (same declaration text).

    Tactic trace: 23 steps

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

  11. example C03S02.(example at line 48) line 48 source
  12. example C03S02.(example at line 54) sorry line 54 source
  13. example C03S02.(example at line 57) sorry line 57 source
  14. example C03S02.(example at line 60) line 60 source
  15. example C03S02.(example at line 64) line 64 source
  16. example C03S02.(example at line 69) line 69 source
  17. example C03S02.(example at line 74) line 74 source
  18. example C03S02.(example at line 81) line 81 source
  19. example C03S02.(example at line 88) line 88 source
  20. example C03S02.(example at line 93) line 93 source
  21. def C03S02.SumOfSquares line 102 source

    no axioms what this means

    Statement uses: CommRing

    Proof uses: Exists, Eq, HAdd.hAdd, HPow.hPow, Nat, OfNat.ofNat

    9 instances, coercions and auxiliary constants left out.

  22. theorem C03S02.sumOfSquares_mul line 105 source

    standard axioms: Quot.sound, propext what this means

    Statement uses: CommRing, C03S02.SumOfSquares, HMul.hMul

    Proof uses: Exists, Eq, HAdd.hAdd, HPow.hPow, Nat, OfNat.ofNat, Eq.mpr, id, congrArg, Exists.intro, HSub.hSub, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.pow_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.symm, Eq.refl and 52 more

    38 instances, coercions and auxiliary constants left out.

    Tactic trace: 5 steps

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

  23. theorem C03S02.sumOfSquares_mul' line 113 source

    standard axioms: Quot.sound, propext what this means

    Statement uses: CommRing, C03S02.SumOfSquares, HMul.hMul

    Proof uses: Exists, Eq, HAdd.hAdd, HPow.hPow, Nat, OfNat.ofNat, Exists.intro, HSub.hSub, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.pow_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.mpr, id, congrArg, Eq.symm, Eq.refl and 52 more

    39 instances, coercions and auxiliary constants left out.

    Tactic trace: 22 steps

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

  24. example C03S02.(example at line 125) line 125 source
  25. example C03S02.(example at line 131) sorry line 131 source
  26. example C03S02.(example at line 140) line 140 source
  27. example C03S02.(example at line 145) sorry line 145 source
  28. example C03S02.(example at line 148) line 148 source
  29. example C03S02.(example at line 152) line 152 source
  30. example C03S02.(example at line 165) sorry line 165 source