E : Type u_1
ι : Type ?u.20084
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
hr : 0 < r
hf : ContinuousOn f (sphere z r)
hg : ContinuousOn g (sphere z r)
h1 : ContinuousOn (fun w => ((w - z) ^ 2)⁻¹) (sphere z r)
⊢ cderiv r (f - g) z = cderiv r f z - cderiv r g z
E : Type u_1
ι : Type ?u.20084
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
hr : 0 < r
hf : ContinuousOn f (sphere z r)
hg : ContinuousOn g (sphere z r)
⊢ cderiv r (f - g) z = cderiv r f z - cderiv r g z
have h1 : ContinuousOn (fun w : ℂ => ((w - z) ^ 2)⁻¹) (sphere z r) := by
  refine' ((continuous_id'.sub continuous_const).pow 2).continuousOn.inv₀ fun w hw h => hr.ne _
  rwa [mem_sphere_iff_norm, sq_eq_zero_iff.mp h, norm_zero] at hw
E : Type u_1
ι : Type ?u.20084
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
hr : 0 < r
hf : ContinuousOn f (sphere z r)
hg : ContinuousOn g (sphere z r)
h1 : ContinuousOn (fun w => ((w - z) ^ 2)⁻¹) (sphere z r)
⊢ ((2 * ↑π * I)⁻¹ • ∮ (w : ℂ) in C(z, r), ((w - z) ^ 2)⁻¹ • (f - g) w) =
    (2 * ↑π * I)⁻¹ • ((∮ (w : ℂ) in C(z, r), ((w - z) ^ 2)⁻¹ • f w) - ∮ (w : ℂ) in C(z, r), ((w - z) ^ 2)⁻¹ • g w)
E : Type u_1
ι : Type ?u.20084
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
hr : 0 < r
hf : ContinuousOn f (sphere z r)
hg : ContinuousOn g (sphere z r)
h1 : ContinuousOn (fun w => ((w - z) ^ 2)⁻¹) (sphere z r)
⊢ cderiv r (f - g) z = cderiv r f z - cderiv r g z
simp_rw [cderiv, ← smul_sub]
case e_a
E : Type u_1
ι : Type ?u.20084
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
hr : 0 < r
hf : ContinuousOn f (sphere z r)
hg : ContinuousOn g (sphere z r)
h1 : ContinuousOn (fun w => ((w - z) ^ 2)⁻¹) (sphere z r)
⊢ (∮ (w : ℂ) in C(z, r), ((w - z) ^ 2)⁻¹ • (f - g) w) =
    (∮ (w : ℂ) in C(z, r), ((w - z) ^ 2)⁻¹ • f w) - ∮ (w : ℂ) in C(z, r), ((w - z) ^ 2)⁻¹ • g w
E : Type u_1
ι : Type ?u.20084
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
hr : 0 < r
hf : ContinuousOn f (sphere z r)
hg : ContinuousOn g (sphere z r)
h1 : ContinuousOn (fun w => ((w - z) ^ 2)⁻¹) (sphere z r)
⊢ ((2 * ↑π * I)⁻¹ • ∮ (w : ℂ) in C(z, r), ((w - z) ^ 2)⁻¹ • (f - g) w) =
    (2 * ↑π * I)⁻¹ • ((∮ (w : ℂ) in C(z, r), ((w - z) ^ 2)⁻¹ • f w) - ∮ (w : ℂ) in C(z, r), ((w - z) ^ 2)⁻¹ • g w)
congr 1
no goals
case e_a
E : Type u_1
ι : Type ?u.20084
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
hr : 0 < r
hf : ContinuousOn f (sphere z r)
hg : ContinuousOn g (sphere z r)
h1 : ContinuousOn (fun w => ((w - z) ^ 2)⁻¹) (sphere z r)
⊢ (∮ (w : ℂ) in C(z, r), ((w - z) ^ 2)⁻¹ • (f - g) w) =
    (∮ (w : ℂ) in C(z, r), ((w - z) ^ 2)⁻¹ • f w) - ∮ (w : ℂ) in C(z, r), ((w - z) ^ 2)⁻¹ • g w
simpa only [Pi.sub_apply, smul_sub] using
  circleIntegral.integral_sub ((h1.smul hf).circleIntegrable hr.le)
    ((h1.smul hg).circleIntegrable hr.le)
E : Type u_1
ι : Type ?u.20084
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
hr : 0 < r
hf : ContinuousOn f (sphere z r)
hg : ContinuousOn g (sphere z r)
w : ℂ
hw : w ∈ sphere z r
h : (w - z) ^ 2 = 0
⊢ 0 = r
E : Type u_1
ι : Type ?u.20084
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
hr : 0 < r
hf : ContinuousOn f (sphere z r)
hg : ContinuousOn g (sphere z r)
⊢ ContinuousOn (fun w => ((w - z) ^ 2)⁻¹) (sphere z r)
refine' ((continuous_id'.sub continuous_const).pow 2).continuousOn.inv₀ fun w hw h => hr.ne _
no goals
E : Type u_1
ι : Type ?u.20084
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
hr : 0 < r
hf : ContinuousOn f (sphere z r)
hg : ContinuousOn g (sphere z r)
w : ℂ
hw : w ∈ sphere z r
h : (w - z) ^ 2 = 0
⊢ 0 = r
rwa [mem_sphere_iff_norm, sq_eq_zero_iff.mp h, norm_zero] at hw