E : Type ?u.57155
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R✝ : ℝ
z✝ w : ℂ
R r : ℝ
hr : r < R
z : ℂ
⊢ ContinuousOn (fun w => (1 / (circleMap z R w.snd - w.fst)) ^ 2) (closedBall z r ×ˢ univ)
E : Type ?u.57155
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R✝ : ℝ
z✝ w : ℂ
R r : ℝ
hr : r < R
z : ℂ
⊢ ContinuousOn (fun w => (circleMap z R w.snd - w.fst)⁻¹ ^ 2) (closedBall z r ×ˢ univ)
simp_rw [← one_div]
case hf.hg
E : Type ?u.57155
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R✝ : ℝ
z✝ w : ℂ
R r : ℝ
hr : r < R
z : ℂ
⊢ ContinuousOn (fun x => circleMap z R x.snd - x.fst) (closedBall z r ×ˢ univ)

case hf.h₀
E : Type ?u.57155
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R✝ : ℝ
z✝ w : ℂ
R r : ℝ
hr : r < R
z : ℂ
⊢ ∀ (x : ℂ × ℝ), x ∈ closedBall z r ×ˢ univ → circleMap z R x.snd - x.fst ≠ 0
E : Type ?u.57155
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R✝ : ℝ
z✝ w : ℂ
R r : ℝ
hr : r < R
z : ℂ
⊢ ContinuousOn (fun w => (1 / (circleMap z R w.snd - w.fst)) ^ 2) (closedBall z r ×ˢ univ)
apply_rules [ContinuousOn.pow, ContinuousOn.div, continuousOn_const]
case hf.h₀
E : Type ?u.57155
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R✝ : ℝ
z✝ w : ℂ
R r : ℝ
hr : r < R
z : ℂ
⊢ ∀ (x : ℂ × ℝ), x ∈ closedBall z r ×ˢ univ → circleMap z R x.snd - x.fst ≠ 0
case hf.hg
E : Type ?u.57155
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R✝ : ℝ
z✝ w : ℂ
R r : ℝ
hr : r < R
z : ℂ
⊢ ContinuousOn (fun x => circleMap z R x.snd - x.fst) (closedBall z r ×ˢ univ)

case hf.h₀
E : Type ?u.57155
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R✝ : ℝ
z✝ w : ℂ
R r : ℝ
hr : r < R
z : ℂ
⊢ ∀ (x : ℂ × ℝ), x ∈ closedBall z r ×ˢ univ → circleMap z R x.snd - x.fst ≠ 0
refine' ((continuous_circleMap z R).continuousOn.comp continuousOn_snd fun _ => And.right).sub
  (continuousOn_id.comp continuousOn_fst fun _ => And.left)
case hf.h₀
E : Type ?u.57155
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R✝ : ℝ
z✝ w : ℂ
R r : ℝ
hr : r < R
z : ℂ
⊢ ∀ (a : ℂ) (b : ℝ), a ∈ closedBall z r → b ∈ univ → ¬circleMap z R b - a = 0
case hf.h₀
E : Type ?u.57155
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R✝ : ℝ
z✝ w : ℂ
R r : ℝ
hr : r < R
z : ℂ
⊢ ∀ (x : ℂ × ℝ), x ∈ closedBall z r ×ˢ univ → circleMap z R x.snd - x.fst ≠ 0
simp only [mem_prod, Ne.def, and_imp, Prod.forall]
case hf.h₀
E : Type ?u.57155
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R✝ : ℝ
z✝ w : ℂ
R r : ℝ
hr : r < R
z a : ℂ
b : ℝ
ha : a ∈ closedBall z r
a✝ : b ∈ univ
⊢ ¬circleMap z R b - a = 0
case hf.h₀
E : Type ?u.57155
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R✝ : ℝ
z✝ w : ℂ
R r : ℝ
hr : r < R
z : ℂ
⊢ ∀ (a : ℂ) (b : ℝ), a ∈ closedBall z r → b ∈ univ → ¬circleMap z R b - a = 0
intro a b ha _
case hf.h₀
E : Type ?u.57155
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R✝ : ℝ
z✝ w : ℂ
R r : ℝ
hr : r < R
z a : ℂ
b : ℝ
ha : a ∈ closedBall z r
a✝ : b ∈ univ
ha2 : a ∈ ball z R
⊢ ¬circleMap z R b - a = 0
case hf.h₀
E : Type ?u.57155
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R✝ : ℝ
z✝ w : ℂ
R r : ℝ
hr : r < R
z a : ℂ
b : ℝ
ha : a ∈ closedBall z r
a✝ : b ∈ univ
⊢ ¬circleMap z R b - a = 0
have ha2 : a ∈ ball z R := by simp at *; linarith
no goals
case hf.h₀
E : Type ?u.57155
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R✝ : ℝ
z✝ w : ℂ
R r : ℝ
hr : r < R
z a : ℂ
b : ℝ
ha : a ∈ closedBall z r
a✝ : b ∈ univ
ha2 : a ∈ ball z R
⊢ ¬circleMap z R b - a = 0
exact sub_ne_zero.2 (circleMap_ne_mem_ball ha2 b)
E : Type ?u.57155
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R✝ : ℝ
z✝ w : ℂ
R r : ℝ
hr : r < R
z a : ℂ
b : ℝ
ha : dist a z ≤ r
a✝ : True
⊢ dist a z < R
E : Type ?u.57155
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R✝ : ℝ
z✝ w : ℂ
R r : ℝ
hr : r < R
z a : ℂ
b : ℝ
ha : a ∈ closedBall z r
a✝ : b ∈ univ
⊢ a ∈ ball z R
simp at *
no goals
E : Type ?u.57155
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R✝ : ℝ
z✝ w : ℂ
R r : ℝ
hr : r < R
z a : ℂ
b : ℝ
ha : dist a z ≤ r
a✝ : True
⊢ dist a z < R
linarith