Theorem: add_ne_zero_of_abs_lt (Ray/Misc/Bounds.lean)

State before:
a b : ℂ
h : Complex.abs b < Complex.abs a
⊢ a + b ≠ 0
Tactic:
have e : a + b = a - -b := by abel
State after:
a b : ℂ
h : Complex.abs b < Complex.abs a
e : a + b = a - -b
⊢ a + b ≠ 0

State before:
a b : ℂ
h : Complex.abs b < Complex.abs a
e : a + b = a - -b
⊢ a + b ≠ 0
Tactic:
rw [e, sub_ne_zero]
State after:
a b : ℂ
h : Complex.abs b < Complex.abs a
e : a + b = a - -b
⊢ a ≠ -b

State before:
a b : ℂ
h : Complex.abs b < Complex.abs a
e : a + b = a - -b
⊢ a ≠ -b
Tactic:
contrapose h
State after:
a b : ℂ
e : a + b = a - -b
h : ¬a ≠ -b
⊢ ¬Complex.abs b < Complex.abs a

State before:
a b : ℂ
e : a + b = a - -b
h : ¬a ≠ -b
⊢ ¬Complex.abs b < Complex.abs a
Tactic:
simp only [not_not] at h
State after:
a b : ℂ
e : a + b = a - -b
h : a = -b
⊢ ¬Complex.abs b < Complex.abs a

State before:
a b : ℂ
e : a + b = a - -b
h : a = -b
⊢ ¬Complex.abs b < Complex.abs a
Tactic:
simp only [h, not_lt, AbsoluteValue.map_neg, le_refl]
State after:
no goals

State before:
a b : ℂ
h : Complex.abs b < Complex.abs a
⊢ a + b = a - -b
Tactic:
abel
State after:
no goals