Theorem: ContinuousOn.circleIntegral
Proof state before:
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
comp : (fun t => f x (circleMap c1 r t)) = uncurry f ∘ fun t => (x, circleMap c1 r t)
⊢ ContinuousOn (uncurry f ∘ fun t => (x, circleMap c1 r t)) (Ι 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:
apply ContinuousOn.comp fc
Proof state after:
case intro.refine_1.h.hf.hg.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
comp : (fun t => f x (circleMap c1 r t)) = uncurry f ∘ fun t => (x, circleMap c1 r t)
⊢ ContinuousOn (fun t => (x, circleMap c1 r t)) (Ι 0 (2 * π))

case intro.refine_1.h.hf.hg.h
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
comp : (fun t => f x (circleMap c1 r t)) = uncurry f ∘ fun t => (x, circleMap c1 r t)
⊢ Set.MapsTo (fun t => (x, circleMap c1 r t)) (Ι 0 (2 * π)) (s ×ˢ sphere c1 r)

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 * π))