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

State before:
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
⊢ Complex.abs (1 + z).log ≤ 1 / (1 - r) * Complex.abs z
Tactic:
by_cases rp : r ≤ 0
State after:
case pos
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : r ≤ 0
⊢ Complex.abs (1 + z).log ≤ 1 / (1 - r) * Complex.abs z

case neg
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : ¬r ≤ 0
⊢ Complex.abs (1 + z).log ≤ 1 / (1 - r) * Complex.abs z

State before:
case pos
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : r ≤ 0
⊢ Complex.abs (1 + z).log ≤ 1 / (1 - r) * Complex.abs z
Tactic:
have a0 : abs z < 0 := lt_of_lt_of_le h rp
State after:
case pos
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : r ≤ 0
a0 : Complex.abs z < 0
⊢ Complex.abs (1 + z).log ≤ 1 / (1 - r) * Complex.abs z

State before:
case pos
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : r ≤ 0
a0 : Complex.abs z < 0
⊢ Complex.abs (1 + z).log ≤ 1 / (1 - r) * Complex.abs z
Tactic:
have a0' : abs z ≥ 0 := by bound
State after:
case pos
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : r ≤ 0
a0 : Complex.abs z < 0
a0' : Complex.abs z ≥ 0
⊢ Complex.abs (1 + z).log ≤ 1 / (1 - r) * Complex.abs z

State before:
case pos
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : r ≤ 0
a0 : Complex.abs z < 0
a0' : Complex.abs z ≥ 0
⊢ Complex.abs (1 + z).log ≤ 1 / (1 - r) * Complex.abs z
Tactic:
exfalso
State after:
case pos
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : r ≤ 0
a0 : Complex.abs z < 0
a0' : Complex.abs z ≥ 0
⊢ False

State before:
case pos
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : r ≤ 0
a0 : Complex.abs z < 0
a0' : Complex.abs z ≥ 0
⊢ False
Tactic:
linarith [a0, a0']
State after:
no goals

State before:
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : r ≤ 0
a0 : Complex.abs z < 0
⊢ Complex.abs z ≥ 0
Tactic:
bound
State after:
no goals

State before:
case neg
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : ¬r ≤ 0
⊢ Complex.abs (1 + z).log ≤ 1 / (1 - r) * Complex.abs z
Tactic:
simp only [not_le] at rp
State after:
case neg
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
⊢ Complex.abs (1 + z).log ≤ 1 / (1 - r) * Complex.abs z

State before:
case neg
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
L : ‖(1 + z).log - log 1‖ ≤ 1 / (1 - r) * ‖1 + z - 1‖
⊢ Complex.abs (1 + z).log ≤ 1 / (1 - r) * Complex.abs z
Tactic:
simp only [Complex.log_one, sub_zero, Complex.norm_eq_abs, one_div, add_sub_cancel_left] at L
State after:
case neg
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
L : Complex.abs (1 + z).log ≤ (1 - r)⁻¹ * Complex.abs z
⊢ Complex.abs (1 + z).log ≤ 1 / (1 - r) * Complex.abs z

State before:
case neg
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
L : Complex.abs (1 + z).log ≤ (1 - r)⁻¹ * Complex.abs z
⊢ Complex.abs (1 + z).log ≤ 1 / (1 - r) * Complex.abs z
Tactic:
simpa only [one_div, ge_iff_le]
State after:
no goals

State before:
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
⊢ ‖(1 + z).log - log 1‖ ≤ 1 / (1 - r) * ‖1 + z - 1‖
Tactic:
generalize hs : Metric.ball (1:ℂ) r = s
State after:
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
⊢ ‖(1 + z).log - log 1‖ ≤ 1 / (1 - r) * ‖1 + z - 1‖

State before:
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
⊢ ‖(1 + z).log - log 1‖ ≤ 1 / (1 - r) * ‖1 + z - 1‖
Tactic:
have o : IsOpen s := by rw [← hs]; exact Metric.isOpen_ball
State after:
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
⊢ ‖(1 + z).log - log 1‖ ≤ 1 / (1 - r) * ‖1 + z - 1‖

State before:
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
⊢ ‖(1 + z).log - log 1‖ ≤ 1 / (1 - r) * ‖1 + z - 1‖
Tactic:
have s1z : 1 + z ∈ s := by simp [← hs]; assumption
State after:
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
⊢ ‖(1 + z).log - log 1‖ ≤ 1 / (1 - r) * ‖1 + z - 1‖

State before:
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
⊢ ‖(1 + z).log - log 1‖ ≤ 1 / (1 - r) * ‖1 + z - 1‖
Tactic:
have s1 : (1:ℂ) ∈ s := by simp [← hs]; assumption
State after:
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
⊢ ‖(1 + z).log - log 1‖ ≤ 1 / (1 - r) * ‖1 + z - 1‖

State before:
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
⊢ ‖(1 + z).log - log 1‖ ≤ 1 / (1 - r) * ‖1 + z - 1‖
Tactic:
have sp : ∀ w : ℂ, w ∈ s → w.re > 0 ∨ w.im ≠ 0 := by
  intro w ws
  apply mem_slitPlane_of_near_one
  simp only [Metric.mem_ball, Complex.dist_eq, ← hs] at ws
  calc abs (w - 1) < r := by assumption
    _ < 1 := r1
State after:
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
⊢ ‖(1 + z).log - log 1‖ ≤ 1 / (1 - r) * ‖1 + z - 1‖

State before:
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
⊢ ‖(1 + z).log - log 1‖ ≤ 1 / (1 - r) * ‖1 + z - 1‖
Tactic:
have sa : ∀ w : ℂ, w ∈ s → abs w ≥ 1 - r := by
  intro w ws
  simp only [Metric.mem_ball, Complex.dist_eq, ← hs] at ws
  calc abs w = abs (1 + (w - 1)) := by ring_nf
    _ ≥ abs (1 : ℂ) - abs (w - 1) := by bound
    _ ≥ abs (1 : ℂ) - r := by bound
    _ = 1 - r := by rw [Complex.abs.map_one]
State after:
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
⊢ ‖(1 + z).log - log 1‖ ≤ 1 / (1 - r) * ‖1 + z - 1‖

State before:
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
⊢ ‖(1 + z).log - log 1‖ ≤ 1 / (1 - r) * ‖1 + z - 1‖
Tactic:
refine Convex.norm_image_sub_le_of_norm_derivWithin_le ?_ ?_ ?_ s1 s1z
State after:
case refine_1
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
⊢ DifferentiableOn ℂ log s

case refine_2
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
⊢ ∀ x ∈ s, ‖derivWithin log s x‖ ≤ 1 / (1 - r)

case refine_3
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
⊢ Convex ℝ s

State before:
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
⊢ IsOpen s
Tactic:
rw [← hs]
State after:
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
⊢ IsOpen (Metric.ball 1 r)

State before:
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
⊢ IsOpen (Metric.ball 1 r)
Tactic:
exact Metric.isOpen_ball
State after:
no goals

State before:
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
⊢ 1 + z ∈ s
Tactic:
simp [← hs]
State after:
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
⊢ Complex.abs z < r

State before:
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
⊢ Complex.abs z < r
Tactic:
assumption
State after:
no goals

State before:
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
⊢ 1 ∈ s
Tactic:
simp [← hs]
State after:
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
⊢ 0 < r

State before:
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
⊢ 0 < r
Tactic:
assumption
State after:
no goals

State before:
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
⊢ ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
Tactic:
intro w ws
State after:
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
w : ℂ
ws : w ∈ s
⊢ w.re > 0 ∨ w.im ≠ 0

State before:
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
w : ℂ
ws : w ∈ s
⊢ w.re > 0 ∨ w.im ≠ 0
Tactic:
apply mem_slitPlane_of_near_one
State after:
case a
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
w : ℂ
ws : w ∈ s
⊢ Complex.abs (w - 1) < 1

State before:
case a
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
w : ℂ
ws : w ∈ s
⊢ Complex.abs (w - 1) < 1
Tactic:
simp only [Metric.mem_ball, Complex.dist_eq, ← hs] at ws
State after:
case a
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
w : ℂ
ws : Complex.abs (w - 1) < r
⊢ Complex.abs (w - 1) < 1

State before:
case a
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
w : ℂ
ws : Complex.abs (w - 1) < r
⊢ Complex.abs (w - 1) < 1
Tactic:
calc abs (w - 1) < r := by assumption
  _ < 1 := r1
State after:
no goals

State before:
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
w : ℂ
ws : Complex.abs (w - 1) < r
⊢ Complex.abs (w - 1) < r
Tactic:
assumption
State after:
no goals

State before:
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
⊢ ∀ w ∈ s, Complex.abs w ≥ 1 - r
Tactic:
intro w ws
State after:
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
w : ℂ
ws : w ∈ s
⊢ Complex.abs w ≥ 1 - r

State before:
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
w : ℂ
ws : w ∈ s
⊢ Complex.abs w ≥ 1 - r
Tactic:
simp only [Metric.mem_ball, Complex.dist_eq, ← hs] at ws
State after:
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
w : ℂ
ws : Complex.abs (w - 1) < r
⊢ Complex.abs w ≥ 1 - r

State before:
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
w : ℂ
ws : Complex.abs (w - 1) < r
⊢ Complex.abs w ≥ 1 - r
Tactic:
calc abs w = abs (1 + (w - 1)) := by ring_nf
  _ ≥ abs (1 : ℂ) - abs (w - 1) := by bound
  _ ≥ abs (1 : ℂ) - r := by bound
  _ = 1 - r := by rw [Complex.abs.map_one]
State after:
no goals

State before:
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
w : ℂ
ws : Complex.abs (w - 1) < r
⊢ Complex.abs w = Complex.abs (1 + (w - 1))
Tactic:
ring_nf
State after:
no goals

State before:
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
w : ℂ
ws : Complex.abs (w - 1) < r
⊢ Complex.abs (1 + (w - 1)) ≥ Complex.abs 1 - Complex.abs (w - 1)
Tactic:
bound
State after:
no goals

State before:
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
w : ℂ
ws : Complex.abs (w - 1) < r
⊢ Complex.abs 1 - Complex.abs (w - 1) ≥ Complex.abs 1 - r
Tactic:
bound
State after:
no goals

State before:
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
w : ℂ
ws : Complex.abs (w - 1) < r
⊢ Complex.abs 1 - r = 1 - r
Tactic:
rw [Complex.abs.map_one]
State after:
no goals

State before:
case refine_1
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
⊢ DifferentiableOn ℂ log s
Tactic:
exact DifferentiableOn.clog differentiableOn_id sp
State after:
no goals

State before:
case refine_2
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
⊢ ∀ x ∈ s, ‖derivWithin log s x‖ ≤ 1 / (1 - r)
Tactic:
intro w ws
State after:
case refine_2
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ ‖derivWithin log s w‖ ≤ 1 / (1 - r)

State before:
case refine_2
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ ‖derivWithin log s w‖ ≤ 1 / (1 - r)
Tactic:
rw [derivWithin.clog o ws, derivWithin.cid o ws]
State after:
case refine_2
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ ‖1 / w‖ ≤ 1 / (1 - r)

case refine_2.hf
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ DifferentiableWithinAt ℂ (fun z => z) s w

case refine_2.hx
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ w.re > 0 ∨ w.im ≠ 0

State before:
case refine_2
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ ‖1 / w‖ ≤ 1 / (1 - r)

case refine_2.hf
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ DifferentiableWithinAt ℂ (fun z => z) s w

case refine_2.hx
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ w.re > 0 ∨ w.im ≠ 0
Tactic:
simp only [one_div, norm_inv, Complex.norm_eq_abs]
State after:
case refine_2
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ (Complex.abs w)⁻¹ ≤ (1 - r)⁻¹

case refine_2.hf
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ DifferentiableWithinAt ℂ (fun z => z) s w

case refine_2.hx
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ w.re > 0 ∨ w.im ≠ 0

State before:
case refine_2
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ (Complex.abs w)⁻¹ ≤ (1 - r)⁻¹

case refine_2.hf
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ DifferentiableWithinAt ℂ (fun z => z) s w

case refine_2.hx
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ w.re > 0 ∨ w.im ≠ 0
Tactic:
rw [inv_le]
State after:
case refine_2
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ (1 - r)⁻¹⁻¹ ≤ Complex.abs w

case refine_2.ha
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ 0 < Complex.abs w

case refine_2.hb
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ 0 < (1 - r)⁻¹

case refine_2.hf
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ DifferentiableWithinAt ℂ (fun z => z) s w

case refine_2.hx
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ w.re > 0 ∨ w.im ≠ 0

State before:
case refine_2
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ (1 - r)⁻¹⁻¹ ≤ Complex.abs w

case refine_2.ha
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ 0 < Complex.abs w

case refine_2.hb
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ 0 < (1 - r)⁻¹

case refine_2.hf
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ DifferentiableWithinAt ℂ (fun z => z) s w

case refine_2.hx
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ w.re > 0 ∨ w.im ≠ 0
Tactic:
have aw := sa w ws
State after:
case refine_2
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
aw : Complex.abs w ≥ 1 - r
⊢ (1 - r)⁻¹⁻¹ ≤ Complex.abs w

case refine_2.ha
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ 0 < Complex.abs w

case refine_2.hb
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ 0 < (1 - r)⁻¹

case refine_2.hf
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ DifferentiableWithinAt ℂ (fun z => z) s w

case refine_2.hx
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ w.re > 0 ∨ w.im ≠ 0

State before:
case refine_2
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
aw : Complex.abs w ≥ 1 - r
⊢ (1 - r)⁻¹⁻¹ ≤ Complex.abs w

case refine_2.ha
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ 0 < Complex.abs w

case refine_2.hb
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ 0 < (1 - r)⁻¹

case refine_2.hf
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ DifferentiableWithinAt ℂ (fun z => z) s w

case refine_2.hx
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ w.re > 0 ∨ w.im ≠ 0
Tactic:
simp at aw
State after:
case refine_2
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
aw : 1 ≤ Complex.abs w + r
⊢ (1 - r)⁻¹⁻¹ ≤ Complex.abs w

case refine_2.ha
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ 0 < Complex.abs w

case refine_2.hb
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ 0 < (1 - r)⁻¹

case refine_2.hf
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ DifferentiableWithinAt ℂ (fun z => z) s w

case refine_2.hx
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ w.re > 0 ∨ w.im ≠ 0

State before:
case refine_2
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
aw : 1 ≤ Complex.abs w + r
⊢ (1 - r)⁻¹⁻¹ ≤ Complex.abs w

case refine_2.ha
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ 0 < Complex.abs w

case refine_2.hb
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ 0 < (1 - r)⁻¹

case refine_2.hf
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ DifferentiableWithinAt ℂ (fun z => z) s w

case refine_2.hx
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ w.re > 0 ∨ w.im ≠ 0
Tactic:
field_simp
State after:
case refine_2
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
aw : 1 ≤ Complex.abs w + r
⊢ 1 ≤ Complex.abs w + r

case refine_2.ha
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ 0 < Complex.abs w

case refine_2.hb
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ 0 < (1 - r)⁻¹

case refine_2.hf
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ DifferentiableWithinAt ℂ (fun z => z) s w

case refine_2.hx
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ w.re > 0 ∨ w.im ≠ 0

State before:
case refine_2
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
aw : 1 ≤ Complex.abs w + r
⊢ 1 ≤ Complex.abs w + r

case refine_2.ha
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ 0 < Complex.abs w

case refine_2.hb
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ 0 < (1 - r)⁻¹

case refine_2.hf
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ DifferentiableWithinAt ℂ (fun z => z) s w

case refine_2.hx
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ w.re > 0 ∨ w.im ≠ 0
Tactic:
assumption
State after:
case refine_2.ha
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ 0 < Complex.abs w

case refine_2.hb
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ 0 < (1 - r)⁻¹

case refine_2.hf
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ DifferentiableWithinAt ℂ (fun z => z) s w

case refine_2.hx
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ w.re > 0 ∨ w.im ≠ 0

State before:
case refine_2.ha
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ 0 < Complex.abs w

case refine_2.hb
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ 0 < (1 - r)⁻¹

case refine_2.hf
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ DifferentiableWithinAt ℂ (fun z => z) s w

case refine_2.hx
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ w.re > 0 ∨ w.im ≠ 0
Tactic:
have aw := sa w ws
State after:
case refine_2.ha
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
aw : Complex.abs w ≥ 1 - r
⊢ 0 < Complex.abs w

case refine_2.hb
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ 0 < (1 - r)⁻¹

case refine_2.hf
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ DifferentiableWithinAt ℂ (fun z => z) s w

case refine_2.hx
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ w.re > 0 ∨ w.im ≠ 0

State before:
case refine_2.ha
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
aw : Complex.abs w ≥ 1 - r
⊢ 0 < Complex.abs w

case refine_2.hb
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ 0 < (1 - r)⁻¹

case refine_2.hf
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ DifferentiableWithinAt ℂ (fun z => z) s w

case refine_2.hx
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ w.re > 0 ∨ w.im ≠ 0
Tactic:
linarith
State after:
case refine_2.hb
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ 0 < (1 - r)⁻¹

case refine_2.hf
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ DifferentiableWithinAt ℂ (fun z => z) s w

case refine_2.hx
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ w.re > 0 ∨ w.im ≠ 0

State before:
case refine_2.hb
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ 0 < (1 - r)⁻¹

case refine_2.hf
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ DifferentiableWithinAt ℂ (fun z => z) s w

case refine_2.hx
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ w.re > 0 ∨ w.im ≠ 0
Tactic:
norm_num
State after:
case refine_2.hb
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ r < 1

case refine_2.hf
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ DifferentiableWithinAt ℂ (fun z => z) s w

case refine_2.hx
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ w.re > 0 ∨ w.im ≠ 0

State before:
case refine_2.hb
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ r < 1

case refine_2.hf
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ DifferentiableWithinAt ℂ (fun z => z) s w

case refine_2.hx
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ w.re > 0 ∨ w.im ≠ 0
Tactic:
assumption
State after:
case refine_2.hf
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ DifferentiableWithinAt ℂ (fun z => z) s w

case refine_2.hx
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ w.re > 0 ∨ w.im ≠ 0

State before:
case refine_2.hf
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ DifferentiableWithinAt ℂ (fun z => z) s w

case refine_2.hx
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ w.re > 0 ∨ w.im ≠ 0
Tactic:
exact differentiableWithinAt_id
State after:
case refine_2.hx
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ w.re > 0 ∨ w.im ≠ 0

State before:
case refine_2.hx
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
w : ℂ
ws : w ∈ s
⊢ w.re > 0 ∨ w.im ≠ 0
Tactic:
exact sp w ws
State after:
no goals

State before:
case refine_3
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
⊢ Convex ℝ s
Tactic:
rw [← hs]
State after:
case refine_3
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
⊢ Convex ℝ (Metric.ball 1 r)

State before:
case refine_3
z : ℂ
r : ℝ
r1 : r < 1
h : Complex.abs z < r
rp : 0 < r
s : Set ℂ
hs : Metric.ball 1 r = s
o : IsOpen s
s1z : 1 + z ∈ s
s1 : 1 ∈ s
sp : ∀ w ∈ s, w.re > 0 ∨ w.im ≠ 0
sa : ∀ w ∈ s, Complex.abs w ≥ 1 - r
⊢ Convex ℝ (Metric.ball 1 r)
Tactic:
exact convex_ball _ _
State after:
no goals