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

State before:
a z : ℂ
⊢ |Complex.abs (a - z) - Complex.abs a| ≤ Complex.abs z
Tactic:
rw [abs_le]
State after:
a z : ℂ
⊢ -Complex.abs z ≤ Complex.abs (a - z) - Complex.abs a ∧ Complex.abs (a - z) - Complex.abs a ≤ Complex.abs z

State before:
a z : ℂ
⊢ -Complex.abs z ≤ Complex.abs (a - z) - Complex.abs a ∧ Complex.abs (a - z) - Complex.abs a ≤ Complex.abs z
Tactic:
constructor
State after:
case left
a z : ℂ
⊢ -Complex.abs z ≤ Complex.abs (a - z) - Complex.abs a

case right
a z : ℂ
⊢ Complex.abs (a - z) - Complex.abs a ≤ Complex.abs z

State before:
case left
a z : ℂ
⊢ -Complex.abs z ≤ Complex.abs (a - z) - Complex.abs a
Tactic:
simp only [neg_le_sub_iff_le_add]
State after:
case left
a z : ℂ
⊢ Complex.abs a ≤ Complex.abs (a - z) + Complex.abs z

State before:
case left
a z : ℂ
⊢ Complex.abs a ≤ Complex.abs (a - z) + Complex.abs z
Tactic:
calc abs (a - z) + abs z
  _ ≥ |abs a - abs z| + abs z := by bound
  _ ≥ abs a - abs z + abs z := by bound
  _ = abs a := by simp only [sub_add_cancel]
State after:
no goals

State before:
a z : ℂ
⊢ Complex.abs (a - z) + Complex.abs z ≥ |Complex.abs a - Complex.abs z| + Complex.abs z
Tactic:
bound
State after:
no goals

State before:
a z : ℂ
⊢ |Complex.abs a - Complex.abs z| + Complex.abs z ≥ Complex.abs a - Complex.abs z + Complex.abs z
Tactic:
bound
State after:
no goals

State before:
a z : ℂ
⊢ Complex.abs a - Complex.abs z + Complex.abs z = Complex.abs a
Tactic:
simp only [sub_add_cancel]
State after:
no goals

State before:
case right
a z : ℂ
⊢ Complex.abs (a - z) - Complex.abs a ≤ Complex.abs z
Tactic:
calc
  abs (a - z) - abs a ≤ abs a + abs z - abs a := by bound
  _ = abs z := by simp only [add_sub_cancel_left]
State after:
no goals

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

State before:
a z : ℂ
⊢ Complex.abs a + Complex.abs z - Complex.abs a = Complex.abs z
Tactic:
simp only [add_sub_cancel_left]
State after:
no goals