Theorem: eq_of_abs_sub_le_all (GlimpseOfLean/Library/Basic.lean)

State before:
x y : ℝ
⊢ (∀ ε > 0, |x - y| ≤ ε) → x = y
Tactic:
intro h
State after:
x y : ℝ
h : ∀ ε > 0, |x - y| ≤ ε
⊢ x = y

State before:
x y : ℝ
h : ∀ ε > 0, |x - y| ≤ ε
⊢ x = y
Tactic:
apply eq_of_abs_sub_nonpos
State after:
case h
x y : ℝ
h : ∀ ε > 0, |x - y| ≤ ε
⊢ |x - y| ≤ 0

State before:
case h
x y : ℝ
h : ∀ ε > 0, |x - y| ≤ ε
⊢ |x - y| ≤ 0
Tactic:
by_contra H
State after:
case h
x y : ℝ
h : ∀ ε > 0, |x - y| ≤ ε
H : ¬|x - y| ≤ 0
⊢ False

State before:
case h
x y : ℝ
h : ∀ ε > 0, |x - y| ≤ ε
H : ¬|x - y| ≤ 0
⊢ False
Tactic:
push_neg at H
State after:
case h
x y : ℝ
h : ∀ ε > 0, |x - y| ≤ ε
H : 0 < |x - y|
⊢ False

State before:
case h
x y : ℝ
h : ∀ ε > 0, |x - y| ≤ ε
H : 0 < |x - y|
⊢ False
Tactic:
specialize h (|x-y|/2) (by linarith)
State after:
case h
x y : ℝ
H : 0 < |x - y|
h : |x - y| ≤ |x - y| / 2
⊢ False

State before:
case h
x y : ℝ
H : 0 < |x - y|
h : |x - y| ≤ |x - y| / 2
⊢ False
Tactic:
rw [← sub_nonpos, sub_half] at h
State after:
case h
x y : ℝ
H : 0 < |x - y|
h : |x - y| / 2 ≤ 0
⊢ False

State before:
case h
x y : ℝ
H : 0 < |x - y|
h : |x - y| / 2 ≤ 0
⊢ False
Tactic:
linarith
State after:
no goals

State before:
x y : ℝ
h : ∀ ε > 0, |x - y| ≤ ε
H : 0 < |x - y|
⊢ |x - y| / 2 > 0
Tactic:
linarith
State after:
no goals