Theorem: Section2sheet6Solutions.eq_zero_of_abs_lt_eps (FormalisingMathematics2024/Solutions/Section02reals/Sheet6.lean)

State before:
r : ℝ
h : ∀ ε > 0, |r| < ε
⊢ r = 0
Tactic:
by_contra h2
State after:
r : ℝ
h : ∀ ε > 0, |r| < ε
h2 : ¬r = 0
⊢ False

State before:
r : ℝ
h : ∀ ε > 0, |r| < ε
h2 : ¬r = 0
⊢ False
Tactic:
specialize h |r| (abs_pos.mpr h2)
State after:
r : ℝ
h2 : ¬r = 0
h : |r| < |r|
⊢ False

State before:
r : ℝ
h2 : ¬r = 0
h : |r| < |r|
⊢ False
Tactic:
linarith
State after:
no goals