E : Type ?u.76109
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R✝ : ℝ
z✝ w : ℂ
R r : ℝ
hr : r < R
z : ℂ
this : ContinuousOn (circleTransformBoundingFunction R z) (closedBall z r ×ˢ ⊤)
⊢ ContinuousOn (↑abs ∘ fun t => circleTransformBoundingFunction R z t) (closedBall z r ×ˢ univ)
E : Type ?u.76109
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R✝ : ℝ
z✝ w : ℂ
R r : ℝ
hr : r < R
z : ℂ
⊢ ContinuousOn (↑abs ∘ fun t => circleTransformBoundingFunction R z t) (closedBall z r ×ˢ univ)
have : ContinuousOn (circleTransformBoundingFunction R z) (closedBall z r ×ˢ (⊤ : Set ℝ)) := by
  apply_rules [ContinuousOn.smul, continuousOn_const]
  simp only [deriv_circleMap]
  have c := (continuous_circleMap 0 R).continuousOn (s := ⊤)
  apply_rules [ContinuousOn.mul, c.comp continuousOn_snd fun _ => And.right, continuousOn_const]
  simp_rw [← inv_pow]
  apply continuousOn_prod_circle_transform_function hr
E : Type ?u.76109
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R✝ : ℝ
z✝ w : ℂ
R r : ℝ
hr : r < R
z : ℂ
this : ContinuousOn (circleTransformBoundingFunction R z) (closedBall z r ×ˢ ⊤)
⊢ MapsTo (fun t => circleTransformBoundingFunction R z t) (closedBall z r ×ˢ univ) ⊤
E : Type ?u.76109
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R✝ : ℝ
z✝ w : ℂ
R r : ℝ
hr : r < R
z : ℂ
this : ContinuousOn (circleTransformBoundingFunction R z) (closedBall z r ×ˢ ⊤)
⊢ ContinuousOn (↑abs ∘ fun t => circleTransformBoundingFunction R z t) (closedBall z r ×ˢ univ)
refine' continuous_abs.continuousOn (s := ⊤).comp this _
E : Type ?u.76109
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R✝ : ℝ
z✝ w : ℂ
R r : ℝ
hr : r < R
z : ℂ
this : ContinuousOn (circleTransformBoundingFunction R z) (closedBall z r ×ˢ ⊤)
⊢ MapsTo (fun t => circleTransformBoundingFunction R z t) (closedBall z r ×ˢ univ) ⊤
E : Type ?u.76109
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R✝ : ℝ
z✝ w : ℂ
R r : ℝ
hr : r < R
z : ℂ
this : ContinuousOn (circleTransformBoundingFunction R z) (closedBall z r ×ˢ ⊤)
⊢ MapsTo (fun t => circleTransformBoundingFunction R z t) (closedBall z r ×ˢ univ) ⊤
show MapsTo _ _ (⊤ : Set ℂ)
no goals
E : Type ?u.76109
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R✝ : ℝ
z✝ w : ℂ
R r : ℝ
hr : r < R
z : ℂ
this : ContinuousOn (circleTransformBoundingFunction R z) (closedBall z r ×ˢ ⊤)
⊢ MapsTo (fun t => circleTransformBoundingFunction R z t) (closedBall z r ×ˢ univ) ⊤
simp [MapsTo]
case hg.hf
E : Type ?u.76109
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R✝ : ℝ
z✝ w : ℂ
R r : ℝ
hr : r < R
z : ℂ
⊢ ContinuousOn (fun x => deriv (circleMap z R) x.snd) (closedBall z r ×ˢ ⊤)

case hg.hg.hf
E : Type ?u.76109
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) ^ 2)⁻¹) (closedBall z r ×ˢ ⊤)
E : Type ?u.76109
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R✝ : ℝ
z✝ w : ℂ
R r : ℝ
hr : r < R
z : ℂ
⊢ ContinuousOn (circleTransformBoundingFunction R z) (closedBall z r ×ˢ ⊤)
apply_rules [ContinuousOn.smul, continuousOn_const]
case hg.hf
E : Type ?u.76109
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R✝ : ℝ
z✝ w : ℂ
R r : ℝ
hr : r < R
z : ℂ
⊢ ContinuousOn (fun x => circleMap 0 R x.snd * I) (closedBall z r ×ˢ ⊤)

case hg.hg.hf
E : Type ?u.76109
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) ^ 2)⁻¹) (closedBall z r ×ˢ ⊤)
case hg.hf
E : Type ?u.76109
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R✝ : ℝ
z✝ w : ℂ
R r : ℝ
hr : r < R
z : ℂ
⊢ ContinuousOn (fun x => deriv (circleMap z R) x.snd) (closedBall z r ×ˢ ⊤)

case hg.hg.hf
E : Type ?u.76109
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) ^ 2)⁻¹) (closedBall z r ×ˢ ⊤)
simp only [deriv_circleMap]
case hg.hf
E : Type ?u.76109
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R✝ : ℝ
z✝ w : ℂ
R r : ℝ
hr : r < R
z : ℂ
c : ContinuousOn (circleMap 0 R) ⊤
⊢ ContinuousOn (fun x => circleMap 0 R x.snd * I) (closedBall z r ×ˢ ⊤)

case hg.hg.hf
E : Type ?u.76109
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) ^ 2)⁻¹) (closedBall z r ×ˢ ⊤)
case hg.hf
E : Type ?u.76109
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R✝ : ℝ
z✝ w : ℂ
R r : ℝ
hr : r < R
z : ℂ
⊢ ContinuousOn (fun x => circleMap 0 R x.snd * I) (closedBall z r ×ˢ ⊤)

case hg.hg.hf
E : Type ?u.76109
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) ^ 2)⁻¹) (closedBall z r ×ˢ ⊤)
have c := (continuous_circleMap 0 R).continuousOn (s := ⊤)
case hg.hg.hf
E : Type ?u.76109
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) ^ 2)⁻¹) (closedBall z r ×ˢ ⊤)
case hg.hf
E : Type ?u.76109
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R✝ : ℝ
z✝ w : ℂ
R r : ℝ
hr : r < R
z : ℂ
c : ContinuousOn (circleMap 0 R) ⊤
⊢ ContinuousOn (fun x => circleMap 0 R x.snd * I) (closedBall z r ×ˢ ⊤)

case hg.hg.hf
E : Type ?u.76109
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) ^ 2)⁻¹) (closedBall z r ×ˢ ⊤)
apply_rules [ContinuousOn.mul, c.comp continuousOn_snd fun _ => And.right, continuousOn_const]
case hg.hg.hf
E : Type ?u.76109
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)⁻¹ ^ 2) (closedBall z r ×ˢ ⊤)
case hg.hg.hf
E : Type ?u.76109
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) ^ 2)⁻¹) (closedBall z r ×ˢ ⊤)
simp_rw [← inv_pow]
no goals
case hg.hg.hf
E : Type ?u.76109
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)⁻¹ ^ 2) (closedBall z r ×ˢ ⊤)
apply continuousOn_prod_circle_transform_function hr