Solutions_S03_Using_Theorems_and_Lemmas.lean`

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Imports (2)

example (example at line 7) line 7 source
example (example at line 12) line 12 source
example (example at line 18) line 18 source
Source comment
an alternative using `linarith`.
```
example (h₀ : d ≤ e) : c + exp (a + d) ≤ c + exp (a + e) := by
…
```
example (example at line 24) line 24 source
example (example at line 30) line 30 source
Source comment
SOLUTION.
```
example (h : a ≤ b) : c - exp b ≤ c - exp a := by
…
```
example (example at line 35) line 35 source
Source comment
alternatively:
```
example (h : a ≤ b) : c - exp b ≤ c - exp a := by
…
```
theorem fact1 line 38 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, LE.le, HMul.hMul, OfNat.ofNat, Nat, HAdd.hAdd, HPow.hPow
Proof uses: le_of_not_gt, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HSub.hSub, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Nat.rawCast, Mathlib.Meta.NormNum.instAddMonoidWithOne, inferInstance, Ring, Int.rawCast, Int.negOfNat, Mathlib.Tactic.Ring.Common.sub_congr, Mathlib.Tactic.Ring.cast_zero, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_zero, Mathlib.Tactic.Ring.Common.pow_congr, Mathlib.Tactic.Ring.Common.atom_pf and 59 more
83 instances, coercions and auxiliary constants left out.
Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
theorem fact2 line 45 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, LE.le, HMul.hMul, Neg.neg, OfNat.ofNat, Nat, HAdd.hAdd, HPow.hPow
Proof uses: le_of_not_gt, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HSub.hSub, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Nat.rawCast, Int.rawCast, inferInstance, Ring, Int.negOfNat, Mathlib.Meta.NormNum.instAddMonoidWithOne, Mathlib.Tactic.Ring.Common.sub_congr, Mathlib.Tactic.Ring.cast_zero, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_zero, Mathlib.Tactic.Ring.Common.pow_congr, Mathlib.Tactic.Ring.Common.atom_pf and 59 more
84 instances, coercions and auxiliary constants left out.
Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
example (example at line 52) line 52 source