Theorem: le_sqr_add (Ray/Tactic/BoundTests.lean)

State before:
c z : ℂ
cz : Complex.abs c ≤ Complex.abs z
z3 : 3 ≤ Complex.abs z
⊢ 2 * Complex.abs z ≤ Complex.abs (z ^ 2 + c)
Tactic:
calc Complex.abs (z^2 + c)
  _ ≥ Complex.abs (z^2) - abs c := by bound
  _ ≥ Complex.abs (z^2) - abs z := by bound
  _ ≥ (abs z - 1) * abs z := by rw [mul_comm, mul_sub_one, ←pow_two, ←Complex.abs.map_pow]
  _ ≥ 2 * abs z := by bound
State after:
no goals

State before:
c z : ℂ
cz : Complex.abs c ≤ Complex.abs z
z3 : 3 ≤ Complex.abs z
⊢ Complex.abs (z ^ 2 + c) ≥ Complex.abs (z ^ 2) - Complex.abs c
Tactic:
bound
State after:
no goals

State before:
c z : ℂ
cz : Complex.abs c ≤ Complex.abs z
z3 : 3 ≤ Complex.abs z
⊢ Complex.abs (z ^ 2) - Complex.abs c ≥ Complex.abs (z ^ 2) - Complex.abs z
Tactic:
bound
State after:
no goals

State before:
c z : ℂ
cz : Complex.abs c ≤ Complex.abs z
z3 : 3 ≤ Complex.abs z
⊢ Complex.abs (z ^ 2) - Complex.abs z ≥ (Complex.abs z - 1) * Complex.abs z
Tactic:
rw [mul_comm, mul_sub_one, ←pow_two, ←Complex.abs.map_pow]
State after:
no goals

State before:
c z : ℂ
cz : Complex.abs c ≤ Complex.abs z
z3 : 3 ≤ Complex.abs z
⊢ (Complex.abs z - 1) * Complex.abs z ≥ 2 * Complex.abs z
Tactic:
bound
State after:
no goals