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

State before:
z : ℂ
nz : z ≠ 0
r : ℝ
rp : 0 < r
⊢ ∃ w, Complex.abs (w - z) < r ∧ Complex.abs w < Complex.abs z
Tactic:
by_cases rz : abs z < r
State after:
case pos
z : ℂ
nz : z ≠ 0
r : ℝ
rp : 0 < r
rz : Complex.abs z < r
⊢ ∃ w, Complex.abs (w - z) < r ∧ Complex.abs w < Complex.abs z

case neg
z : ℂ
nz : z ≠ 0
r : ℝ
rp : 0 < r
rz : ¬Complex.abs z < r
⊢ ∃ w, Complex.abs (w - z) < r ∧ Complex.abs w < Complex.abs z

State before:
case neg
z : ℂ
nz : z ≠ 0
r : ℝ
rp : 0 < r
rz : ¬Complex.abs z < r
⊢ ∃ w, Complex.abs (w - z) < r ∧ Complex.abs w < Complex.abs z
Tactic:
simp only [not_lt] at rz
State after:
case neg
z : ℂ
nz : z ≠ 0
r : ℝ
rp : 0 < r
rz : r ≤ Complex.abs z
⊢ ∃ w, Complex.abs (w - z) < r ∧ Complex.abs w < Complex.abs z

State before:
case neg
z : ℂ
nz : z ≠ 0
r : ℝ
rp : 0 < r
rz : r ≤ Complex.abs z
⊢ ∃ w, Complex.abs (w - z) < r ∧ Complex.abs w < Complex.abs z
Tactic:
have azp : 0 < abs z := Complex.abs.pos nz
State after:
case neg
z : ℂ
nz : z ≠ 0
r : ℝ
rp : 0 < r
rz : r ≤ Complex.abs z
azp : 0 < Complex.abs z
⊢ ∃ w, Complex.abs (w - z) < r ∧ Complex.abs w < Complex.abs z

State before:
case neg
z : ℂ
nz : z ≠ 0
r : ℝ
rp : 0 < r
rz : r ≤ Complex.abs z
azp : 0 < Complex.abs z
⊢ ∃ w, Complex.abs (w - z) < r ∧ Complex.abs w < Complex.abs z
Tactic:
generalize ha : 1 - r/2/abs z = a
State after:
case neg
z : ℂ
nz : z ≠ 0
r : ℝ
rp : 0 < r
rz : r ≤ Complex.abs z
azp : 0 < Complex.abs z
a : ℝ
ha : 1 - r / 2 / Complex.abs z = a
⊢ ∃ w, Complex.abs (w - z) < r ∧ Complex.abs w < Complex.abs z

State before:
case neg
z : ℂ
nz : z ≠ 0
r : ℝ
rp : 0 < r
rz : r ≤ Complex.abs z
azp : 0 < Complex.abs z
a : ℝ
ha : 1 - r / 2 / Complex.abs z = a
⊢ ∃ w, Complex.abs (w - z) < r ∧ Complex.abs w < Complex.abs z
Tactic:
have a0 : 0 ≤ a := by rw [←ha, sub_nonneg, div_le_one azp]; exact _root_.trans (by bound) rz
State after:
case neg
z : ℂ
nz : z ≠ 0
r : ℝ
rp : 0 < r
rz : r ≤ Complex.abs z
azp : 0 < Complex.abs z
a : ℝ
ha : 1 - r / 2 / Complex.abs z = a
a0 : 0 ≤ a
⊢ ∃ w, Complex.abs (w - z) < r ∧ Complex.abs w < Complex.abs z

State before:
case neg
z : ℂ
nz : z ≠ 0
r : ℝ
rp : 0 < r
rz : r ≤ Complex.abs z
azp : 0 < Complex.abs z
a : ℝ
ha : 1 - r / 2 / Complex.abs z = a
a0 : 0 ≤ a
⊢ ∃ w, Complex.abs (w - z) < r ∧ Complex.abs w < Complex.abs z
Tactic:
have a1 : a < 1 := by rw [←ha, sub_lt_self_iff]; positivity
State after:
case neg
z : ℂ
nz : z ≠ 0
r : ℝ
rp : 0 < r
rz : r ≤ Complex.abs z
azp : 0 < Complex.abs z
a : ℝ
ha : 1 - r / 2 / Complex.abs z = a
a0 : 0 ≤ a
a1 : a < 1
⊢ ∃ w, Complex.abs (w - z) < r ∧ Complex.abs w < Complex.abs z

State before:
case neg
z : ℂ
nz : z ≠ 0
r : ℝ
rp : 0 < r
rz : r ≤ Complex.abs z
azp : 0 < Complex.abs z
a : ℝ
ha : 1 - r / 2 / Complex.abs z = a
a0 : 0 ≤ a
a1 : a < 1
⊢ ∃ w, Complex.abs (w - z) < r ∧ Complex.abs w < Complex.abs z
Tactic:
generalize hw : ↑a * z = w
State after:
case neg
z : ℂ
nz : z ≠ 0
r : ℝ
rp : 0 < r
rz : r ≤ Complex.abs z
azp : 0 < Complex.abs z
a : ℝ
ha : 1 - r / 2 / Complex.abs z = a
a0 : 0 ≤ a
a1 : a < 1
w : ℂ
hw : ↑a * z = w
⊢ ∃ w, Complex.abs (w - z) < r ∧ Complex.abs w < Complex.abs z

State before:
case neg
z : ℂ
nz : z ≠ 0
r : ℝ
rp : 0 < r
rz : r ≤ Complex.abs z
azp : 0 < Complex.abs z
a : ℝ
ha : 1 - r / 2 / Complex.abs z = a
a0 : 0 ≤ a
a1 : a < 1
w : ℂ
hw : ↑a * z = w
⊢ ∃ w, Complex.abs (w - z) < r ∧ Complex.abs w < Complex.abs z
Tactic:
use w
State after:
case h
z : ℂ
nz : z ≠ 0
r : ℝ
rp : 0 < r
rz : r ≤ Complex.abs z
azp : 0 < Complex.abs z
a : ℝ
ha : 1 - r / 2 / Complex.abs z = a
a0 : 0 ≤ a
a1 : a < 1
w : ℂ
hw : ↑a * z = w
⊢ Complex.abs (w - z) < r ∧ Complex.abs w < Complex.abs z

State before:
case h
z : ℂ
nz : z ≠ 0
r : ℝ
rp : 0 < r
rz : r ≤ Complex.abs z
azp : 0 < Complex.abs z
a : ℝ
ha : 1 - r / 2 / Complex.abs z = a
a0 : 0 ≤ a
a1 : a < 1
w : ℂ
hw : ↑a * z = w
⊢ Complex.abs (w - z) < r ∧ Complex.abs w < Complex.abs z
Tactic:
constructor
State after:
case h.left
z : ℂ
nz : z ≠ 0
r : ℝ
rp : 0 < r
rz : r ≤ Complex.abs z
azp : 0 < Complex.abs z
a : ℝ
ha : 1 - r / 2 / Complex.abs z = a
a0 : 0 ≤ a
a1 : a < 1
w : ℂ
hw : ↑a * z = w
⊢ Complex.abs (w - z) < r

case h.right
z : ℂ
nz : z ≠ 0
r : ℝ
rp : 0 < r
rz : r ≤ Complex.abs z
azp : 0 < Complex.abs z
a : ℝ
ha : 1 - r / 2 / Complex.abs z = a
a0 : 0 ≤ a
a1 : a < 1
w : ℂ
hw : ↑a * z = w
⊢ Complex.abs w < Complex.abs z

State before:
case pos
z : ℂ
nz : z ≠ 0
r : ℝ
rp : 0 < r
rz : Complex.abs z < r
⊢ ∃ w, Complex.abs (w - z) < r ∧ Complex.abs w < Complex.abs z
Tactic:
use 0
State after:
case h
z : ℂ
nz : z ≠ 0
r : ℝ
rp : 0 < r
rz : Complex.abs z < r
⊢ Complex.abs (0 - z) < r ∧ Complex.abs 0 < Complex.abs z

State before:
case h
z : ℂ
nz : z ≠ 0
r : ℝ
rp : 0 < r
rz : Complex.abs z < r
⊢ Complex.abs (0 - z) < r ∧ Complex.abs 0 < Complex.abs z
Tactic:
simp only [zero_sub, map_neg_eq_map, rz, map_zero, AbsoluteValue.pos_iff, ne_eq, nz,
  not_false_eq_true, and_self]
State after:
no goals

State before:
z : ℂ
nz : z ≠ 0
r : ℝ
rp : 0 < r
rz : r ≤ Complex.abs z
azp : 0 < Complex.abs z
a : ℝ
ha : 1 - r / 2 / Complex.abs z = a
⊢ 0 ≤ a
Tactic:
rw [←ha, sub_nonneg, div_le_one azp]
State after:
z : ℂ
nz : z ≠ 0
r : ℝ
rp : 0 < r
rz : r ≤ Complex.abs z
azp : 0 < Complex.abs z
a : ℝ
ha : 1 - r / 2 / Complex.abs z = a
⊢ r / 2 ≤ Complex.abs z

State before:
z : ℂ
nz : z ≠ 0
r : ℝ
rp : 0 < r
rz : r ≤ Complex.abs z
azp : 0 < Complex.abs z
a : ℝ
ha : 1 - r / 2 / Complex.abs z = a
⊢ r / 2 ≤ Complex.abs z
Tactic:
exact _root_.trans (by bound) rz
State after:
no goals

State before:
z : ℂ
nz : z ≠ 0
r : ℝ
rp : 0 < r
rz : r ≤ Complex.abs z
azp : 0 < Complex.abs z
a : ℝ
ha : 1 - r / 2 / Complex.abs z = a
⊢ r / 2 ≤ r
Tactic:
bound
State after:
no goals

State before:
z : ℂ
nz : z ≠ 0
r : ℝ
rp : 0 < r
rz : r ≤ Complex.abs z
azp : 0 < Complex.abs z
a : ℝ
ha : 1 - r / 2 / Complex.abs z = a
a0 : 0 ≤ a
⊢ a < 1
Tactic:
rw [←ha, sub_lt_self_iff]
State after:
z : ℂ
nz : z ≠ 0
r : ℝ
rp : 0 < r
rz : r ≤ Complex.abs z
azp : 0 < Complex.abs z
a : ℝ
ha : 1 - r / 2 / Complex.abs z = a
a0 : 0 ≤ a
⊢ 0 < r / 2 / Complex.abs z

State before:
z : ℂ
nz : z ≠ 0
r : ℝ
rp : 0 < r
rz : r ≤ Complex.abs z
azp : 0 < Complex.abs z
a : ℝ
ha : 1 - r / 2 / Complex.abs z = a
a0 : 0 ≤ a
⊢ 0 < r / 2 / Complex.abs z
Tactic:
positivity
State after:
no goals

State before:
case h.left
z : ℂ
nz : z ≠ 0
r : ℝ
rp : 0 < r
rz : r ≤ Complex.abs z
azp : 0 < Complex.abs z
a : ℝ
ha : 1 - r / 2 / Complex.abs z = a
a0 : 0 ≤ a
a1 : a < 1
w : ℂ
hw : ↑a * z = w
⊢ Complex.abs (w - z) < r
Tactic:
rw [←hw,←ha]
State after:
case h.left
z : ℂ
nz : z ≠ 0
r : ℝ
rp : 0 < r
rz : r ≤ Complex.abs z
azp : 0 < Complex.abs z
a : ℝ
ha : 1 - r / 2 / Complex.abs z = a
a0 : 0 ≤ a
a1 : a < 1
w : ℂ
hw : ↑a * z = w
⊢ Complex.abs (↑(1 - r / 2 / Complex.abs z) * z - z) < r

State before:
case h.left
z : ℂ
nz : z ≠ 0
r : ℝ
rp : 0 < r
rz : r ≤ Complex.abs z
azp : 0 < Complex.abs z
a : ℝ
ha : 1 - r / 2 / Complex.abs z = a
a0 : 0 ≤ a
a1 : a < 1
w : ℂ
hw : ↑a * z = w
⊢ Complex.abs (↑(1 - r / 2 / Complex.abs z) * z - z) < r
Tactic:
simp only [Complex.ofReal_sub, Complex.ofReal_one, Complex.ofReal_div]
State after:
case h.left
z : ℂ
nz : z ≠ 0
r : ℝ
rp : 0 < r
rz : r ≤ Complex.abs z
azp : 0 < Complex.abs z
a : ℝ
ha : 1 - r / 2 / Complex.abs z = a
a0 : 0 ≤ a
a1 : a < 1
w : ℂ
hw : ↑a * z = w
⊢ Complex.abs ((1 - ↑r / ↑2 / ↑(Complex.abs z)) * z - z) < r

State before:
case h.left
z : ℂ
nz : z ≠ 0
r : ℝ
rp : 0 < r
rz : r ≤ Complex.abs z
azp : 0 < Complex.abs z
a : ℝ
ha : 1 - r / 2 / Complex.abs z = a
a0 : 0 ≤ a
a1 : a < 1
w : ℂ
hw : ↑a * z = w
⊢ Complex.abs ((1 - ↑r / ↑2 / ↑(Complex.abs z)) * z - z) < r
Tactic:
rw [mul_sub_right_distrib]
State after:
case h.left
z : ℂ
nz : z ≠ 0
r : ℝ
rp : 0 < r
rz : r ≤ Complex.abs z
azp : 0 < Complex.abs z
a : ℝ
ha : 1 - r / 2 / Complex.abs z = a
a0 : 0 ≤ a
a1 : a < 1
w : ℂ
hw : ↑a * z = w
⊢ Complex.abs (1 * z - ↑r / ↑2 / ↑(Complex.abs z) * z - z) < r

State before:
case h.left
z : ℂ
nz : z ≠ 0
r : ℝ
rp : 0 < r
rz : r ≤ Complex.abs z
azp : 0 < Complex.abs z
a : ℝ
ha : 1 - r / 2 / Complex.abs z = a
a0 : 0 ≤ a
a1 : a < 1
w : ℂ
hw : ↑a * z = w
⊢ Complex.abs (1 * z - ↑r / ↑2 / ↑(Complex.abs z) * z - z) < r
Tactic:
simp only [one_mul, sub_sub_cancel_left, AbsoluteValue.map_neg, AbsoluteValue.map_mul, map_div₀,
  Complex.abs_ofReal, Complex.abs_two, Complex.abs_abs, abs_of_pos rp, div_mul (r/2),
  div_mul_cancel₀ _ azp.ne', div_one, abs_two, div_self azp.ne']
State after:
case h.left
z : ℂ
nz : z ≠ 0
r : ℝ
rp : 0 < r
rz : r ≤ Complex.abs z
azp : 0 < Complex.abs z
a : ℝ
ha : 1 - r / 2 / Complex.abs z = a
a0 : 0 ≤ a
a1 : a < 1
w : ℂ
hw : ↑a * z = w
⊢ r / 2 < r

State before:
case h.left
z : ℂ
nz : z ≠ 0
r : ℝ
rp : 0 < r
rz : r ≤ Complex.abs z
azp : 0 < Complex.abs z
a : ℝ
ha : 1 - r / 2 / Complex.abs z = a
a0 : 0 ≤ a
a1 : a < 1
w : ℂ
hw : ↑a * z = w
⊢ r / 2 < r
Tactic:
bound
State after:
no goals

State before:
case h.right
z : ℂ
nz : z ≠ 0
r : ℝ
rp : 0 < r
rz : r ≤ Complex.abs z
azp : 0 < Complex.abs z
a : ℝ
ha : 1 - r / 2 / Complex.abs z = a
a0 : 0 ≤ a
a1 : a < 1
w : ℂ
hw : ↑a * z = w
⊢ Complex.abs w < Complex.abs z
Tactic:
simp only [←hw, AbsoluteValue.map_mul, Complex.abs_ofReal, abs_of_nonneg a0]
State after:
case h.right
z : ℂ
nz : z ≠ 0
r : ℝ
rp : 0 < r
rz : r ≤ Complex.abs z
azp : 0 < Complex.abs z
a : ℝ
ha : 1 - r / 2 / Complex.abs z = a
a0 : 0 ≤ a
a1 : a < 1
w : ℂ
hw : ↑a * z = w
⊢ a * Complex.abs z < Complex.abs z

State before:
case h.right
z : ℂ
nz : z ≠ 0
r : ℝ
rp : 0 < r
rz : r ≤ Complex.abs z
azp : 0 < Complex.abs z
a : ℝ
ha : 1 - r / 2 / Complex.abs z = a
a0 : 0 ≤ a
a1 : a < 1
w : ℂ
hw : ↑a * z = w
⊢ a * Complex.abs z < Complex.abs z
Tactic:
calc a * abs z < 1 * abs z := mul_lt_mul_of_pos_right a1 azp
  _ = abs z := by ring
State after:
no goals

State before:
z : ℂ
nz : z ≠ 0
r : ℝ
rp : 0 < r
rz : r ≤ Complex.abs z
azp : 0 < Complex.abs z
a : ℝ
ha : 1 - r / 2 / Complex.abs z = a
a0 : 0 ≤ a
a1 : a < 1
w : ℂ
hw : ↑a * z = w
⊢ 1 * Complex.abs z = Complex.abs z
Tactic:
ring
State after:
no goals