In the file exercises/02Iff.lean, the following examples are given for practicing equivalence splitting:
Using equivalences as pairs of implications
The second line in the above proof is a bit silly: we use statement rewriting to reduce
the goal to our assumption ha, but it would be more natural to see the equivalence as a
double implication. We can access the two implications of an equivalence h : P ↔ Q as
h.1 : P → Q and h.2 : Q → P. This allows us to rewrite the above proof as:
-/
example {a b : ℝ} (ha : 0 ≤ a) : b ≤ a + b := by
calc
b = 0 + b := by ring
_ ≤ a + b := by exact (add_le_add_iff_right b).2 ha
/- Let's do a variant using add_le_add_iff_left a : a + b ≤ a + c ↔ b ≤ c instead. -/
example (a b : ℝ) (hb : 0 ≤ b) : a ≤ a + b := by
sorry
/-
Important note: in the previous exercises, we used lemmas like add_le_add_iff_left as
elementary examples to manipulate equivalences. But invoking those lemmas by hand when
working on interesting mathematics would be awfully tedious. There are tactics
whose job is to do these things automatically, but this is not the topic of this file.
lines 138 - 161
however, the second one is a bit nasty, because the exact tactic with the same syntax as above
_ ≤ a + b := by exact (add_le_add_iff_left a).2 hb
does not work: Lean does not recognise 0, b from hb. The following code works:
_ ≤ a + b := by exact (add_le_add_iff_left a).2 (show (0 : ℝ) ≤ b from hb)
I would suggest replacing with another example (will pull request).
In the file exercises/02Iff.lean, the following examples are given for practicing equivalence splitting:
Using equivalences as pairs of implications
The second line in the above proof is a bit silly: we use statement rewriting to reduce
the goal to our assumption
ha, but it would be more natural to see the equivalence as adouble implication. We can access the two implications of an equivalence
h : P ↔ Qash.1 : P → Qandh.2 : Q → P. This allows us to rewrite the above proof as:-/
example {a b : ℝ} (ha : 0 ≤ a) : b ≤ a + b := by
calc
b = 0 + b := by ring
_ ≤ a + b := by exact (add_le_add_iff_right b).2 ha
/- Let's do a variant using
add_le_add_iff_left a : a + b ≤ a + c ↔ b ≤ cinstead. -/example (a b : ℝ) (hb : 0 ≤ b) : a ≤ a + b := by
sorry
/-
Important note: in the previous exercises, we used lemmas like
add_le_add_iff_leftaselementary examples to manipulate equivalences. But invoking those lemmas by hand when
working on interesting mathematics would be awfully tedious. There are tactics
whose job is to do these things automatically, but this is not the topic of this file.
lines 138 - 161
however, the second one is a bit nasty, because the exact tactic with the same syntax as above
_ ≤ a + b := by exact (add_le_add_iff_left a).2 hb
does not work: Lean does not recognise 0, b from hb. The following code works:
_ ≤ a + b := by exact (add_le_add_iff_left a).2 (show (0 : ℝ) ≤ b from hb)
I would suggest replacing with another example (will pull request).