Theorem: le_of_le_add_all (LeanTeaching/TutoLib.lean)

State before:
x y : ℝ
⊢ (∀ ε > 0, y ≤ x + ε) → y ≤ x
Tactic:
contrapose!
State after:
x y : ℝ
⊢ x < y → ∃ ε > 0, x + ε < y

State before:
x y : ℝ
⊢ x < y → ∃ ε > 0, x + ε < y
Tactic:
intro h
State after:
x y : ℝ
h : x < y
⊢ ∃ ε > 0, x + ε < y

State before:
x y : ℝ
h : x < y
⊢ ∃ ε > 0, x + ε < y
Tactic:
use (y-x)/2
State after:
case h
x y : ℝ
h : x < y
⊢ (y - x) / 2 > 0 ∧ x + (y - x) / 2 < y

State before:
case h
x y : ℝ
h : x < y
⊢ (y - x) / 2 > 0 ∧ x + (y - x) / 2 < y
Tactic:
constructor <;> linarith
State after:
no goals