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

State before:
a z : ℂ
⊢ |Complex.abs (a + z) - Complex.abs a| ≤ Complex.abs z
Tactic:
have h := sub_near a (-z)
State after:
a z : ℂ
h : |Complex.abs (a - -z) - Complex.abs a| ≤ Complex.abs (-z)
⊢ |Complex.abs (a + z) - Complex.abs a| ≤ Complex.abs z

State before:
a z : ℂ
h : |Complex.abs (a - -z) - Complex.abs a| ≤ Complex.abs (-z)
⊢ |Complex.abs (a + z) - Complex.abs a| ≤ Complex.abs z
Tactic:
simp only [sub_neg_eq_add, map_neg_eq_map] at h
State after:
a z : ℂ
h : |Complex.abs (a + z) - Complex.abs a| ≤ Complex.abs z
⊢ |Complex.abs (a + z) - Complex.abs a| ≤ Complex.abs z

State before:
a z : ℂ
h : |Complex.abs (a + z) - Complex.abs a| ≤ Complex.abs z
⊢ |Complex.abs (a + z) - Complex.abs a| ≤ Complex.abs z
Tactic:
assumption
State after:
no goals