Theorem: ContinuousOn.circleIntegral
Proof state before:
case intro.refine_1.h.hf.hf
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b✝ : ℝ
f : ℂ → ℂ → E
s : Set ℂ
rp : r > 0
cs : IsCompact s
fc : ContinuousOn (uncurry f) (s ×ˢ sphere c1 r)
b : ℝ
bh : ∀ ⦃x : ℂ × ℂ⦄, x ∈ s ×ˢ sphere c1 r → ‖uncurry f x‖ ≤ b
z1 : ℂ
z1s : z1 ∈ s
fb :
  ∀ᶠ (x : ℂ) in 𝓝[s] z1,
    ∀ᵐ (t : ℝ), t ∈ Ι 0 (2 * π) → ‖deriv (circleMap c1 r) t • (fun z1 => f x z1) (circleMap c1 r t)‖ ≤ r * b
x : ℂ
xs : x ∈ s
⊢ ContinuousOn (fun x => deriv (circleMap c1 r) x) (Ι 0 (2 * π))

case intro.refine_1.h.hf.hg
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b✝ : ℝ
f : ℂ → ℂ → E
s : Set ℂ
rp : r > 0
cs : IsCompact s
fc : ContinuousOn (uncurry f) (s ×ˢ sphere c1 r)
b : ℝ
bh : ∀ ⦃x : ℂ × ℂ⦄, x ∈ s ×ˢ sphere c1 r → ‖uncurry f x‖ ≤ b
z1 : ℂ
z1s : z1 ∈ s
fb :
  ∀ᶠ (x : ℂ) in 𝓝[s] z1,
    ∀ᵐ (t : ℝ), t ∈ Ι 0 (2 * π) → ‖deriv (circleMap c1 r) t • (fun z1 => f x z1) (circleMap c1 r t)‖ ≤ r * b
x : ℂ
xs : x ∈ s
⊢ ContinuousOn (fun x_1 => (fun z1 => f x z1) (circleMap c1 r x_1)) (Ι 0 (2 * π))

case intro.refine_1.h.hs
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b✝ : ℝ
f : ℂ → ℂ → E
s : Set ℂ
rp : r > 0
cs : IsCompact s
fc : ContinuousOn (uncurry f) (s ×ˢ sphere c1 r)
b : ℝ
bh : ∀ ⦃x : ℂ × ℂ⦄, x ∈ s ×ˢ sphere c1 r → ‖uncurry f x‖ ≤ b
z1 : ℂ
z1s : z1 ∈ s
fb :
  ∀ᶠ (x : ℂ) in 𝓝[s] z1,
    ∀ᵐ (t : ℝ), t ∈ Ι 0 (2 * π) → ‖deriv (circleMap c1 r) t • (fun z1 => f x z1) (circleMap c1 r t)‖ ≤ r * b
x : ℂ
xs : x ∈ s
⊢ MeasurableSet (Ι 0 (2 * π))
Tactic:
simp
Proof state after:
case intro.refine_1.h.hf.hf
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b✝ : ℝ
f : ℂ → ℂ → E
s : Set ℂ
rp : r > 0
cs : IsCompact s
fc : ContinuousOn (uncurry f) (s ×ˢ sphere c1 r)
b : ℝ
bh : ∀ ⦃x : ℂ × ℂ⦄, x ∈ s ×ˢ sphere c1 r → ‖uncurry f x‖ ≤ b
z1 : ℂ
z1s : z1 ∈ s
fb :
  ∀ᶠ (x : ℂ) in 𝓝[s] z1,
    ∀ᵐ (t : ℝ), t ∈ Ι 0 (2 * π) → ‖deriv (circleMap c1 r) t • (fun z1 => f x z1) (circleMap c1 r t)‖ ≤ r * b
x : ℂ
xs : x ∈ s
⊢ ContinuousOn (fun x => circleMap 0 r x * I) (Ι 0 (2 * π))

case intro.refine_1.h.hf.hg
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b✝ : ℝ
f : ℂ → ℂ → E
s : Set ℂ
rp : r > 0
cs : IsCompact s
fc : ContinuousOn (uncurry f) (s ×ˢ sphere c1 r)
b : ℝ
bh : ∀ ⦃x : ℂ × ℂ⦄, x ∈ s ×ˢ sphere c1 r → ‖uncurry f x‖ ≤ b
z1 : ℂ
z1s : z1 ∈ s
fb :
  ∀ᶠ (x : ℂ) in 𝓝[s] z1,
    ∀ᵐ (t : ℝ), t ∈ Ι 0 (2 * π) → ‖deriv (circleMap c1 r) t • (fun z1 => f x z1) (circleMap c1 r t)‖ ≤ r * b
x : ℂ
xs : x ∈ s
⊢ ContinuousOn (fun x_1 => (fun z1 => f x z1) (circleMap c1 r x_1)) (Ι 0 (2 * π))

case intro.refine_1.h.hs
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f✝ : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b✝ : ℝ
f : ℂ → ℂ → E
s : Set ℂ
rp : r > 0
cs : IsCompact s
fc : ContinuousOn (uncurry f) (s ×ˢ sphere c1 r)
b : ℝ
bh : ∀ ⦃x : ℂ × ℂ⦄, x ∈ s ×ˢ sphere c1 r → ‖uncurry f x‖ ≤ b
z1 : ℂ
z1s : z1 ∈ s
fb :
  ∀ᶠ (x : ℂ) in 𝓝[s] z1,
    ∀ᵐ (t : ℝ), t ∈ Ι 0 (2 * π) → ‖deriv (circleMap c1 r) t • (fun z1 => f x z1) (circleMap c1 r t)‖ ≤ r * b
x : ℂ
xs : x ∈ s
⊢ MeasurableSet (Ι 0 (2 * π))