-- Mathlib/Analysis/Complex/RemovableSingularity.lean
theorem two_pi_I_inv_smul_circleIntegral_sub_sq_inv_smul_of_differentiable {U : Set ℂ}
    (hU : IsOpen U) {c w₀ : ℂ} {R : ℝ} {f : ℂ → E} (hc : closedBall c R ⊆ U)
    (hf : DifferentiableOn ℂ f U) (hw₀ : w₀ ∈ ball c R) :
    ((2 * π * I : ℂ)⁻¹ • ∮ z in C(c, R), ((z - w₀) ^ 2)⁻¹ • f z) = deriv f w₀

Proof state:
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U : Set ℂ
hU : IsOpen U
c w₀ : ℂ
R : ℝ
f : ℂ → E
hc : closedBall c R ⊆ U
hf : DifferentiableOn ℂ f U
hw₀ : w₀ ∈ ball c R
hf' : DifferentiableOn ℂ (dslope f w₀) U
h0 : ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, R), (z - w₀)⁻¹ • dslope f w₀ z) = dslope f w₀ w₀
⊢ ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, R), ((z - w₀) ^ 2)⁻¹ • f z) = deriv f w₀

Tactic:
rw [← dslope_same, ← h0]

Result:
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U : Set ℂ
hU : IsOpen U
c w₀ : ℂ
R : ℝ
f : ℂ → E
hc : closedBall c R ⊆ U
hf : DifferentiableOn ℂ f U
hw₀ : w₀ ∈ ball c R
hf' : DifferentiableOn ℂ (dslope f w₀) U
h0 : ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, R), (z - w₀)⁻¹ • dslope f w₀ z) = dslope f w₀ w₀
⊢ ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, R), ((z - w₀) ^ 2)⁻¹ • f z) =
    (2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, R), (z - w₀)⁻¹ • dslope f w₀ z

Proof state:
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U : Set ℂ
hU : IsOpen U
c w₀ : ℂ
R : ℝ
f : ℂ → E
hc : closedBall c R ⊆ U
hf : DifferentiableOn ℂ f U
hw₀ : w₀ ∈ ball c R
hf' : DifferentiableOn ℂ (dslope f w₀) U
h0 : ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, R), (z - w₀)⁻¹ • dslope f w₀ z) = dslope f w₀ w₀
h1 : ContinuousOn (fun z => ((z - w₀) ^ 2)⁻¹) (sphere c R)
h2 : CircleIntegrable (fun z => ((z - w₀) ^ 2)⁻¹ • f z) c R
⊢ (∮ (z : ℂ) in C(c, R), ((z - w₀) ^ 2)⁻¹ • f z) = ∮ (z : ℂ) in C(c, R), ((z - w₀) ^ 2)⁻¹ • (f z - f w₀)

Tactic:
have h3 : CircleIntegrable (fun z : ℂ => ((z - w₀) ^ 2)⁻¹ • f w₀) c R :=
  ContinuousOn.circleIntegrable (pos_of_mem_ball hw₀).le (h1.smul continuousOn_const)

Result:
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U : Set ℂ
hU : IsOpen U
c w₀ : ℂ
R : ℝ
f : ℂ → E
hc : closedBall c R ⊆ U
hf : DifferentiableOn ℂ f U
hw₀ : w₀ ∈ ball c R
hf' : DifferentiableOn ℂ (dslope f w₀) U
h0 : ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, R), (z - w₀)⁻¹ • dslope f w₀ z) = dslope f w₀ w₀
h1 : ContinuousOn (fun z => ((z - w₀) ^ 2)⁻¹) (sphere c R)
h2 : CircleIntegrable (fun z => ((z - w₀) ^ 2)⁻¹ • f z) c R
h3 : CircleIntegrable (fun z => ((z - w₀) ^ 2)⁻¹ • f w₀) c R
⊢ (∮ (z : ℂ) in C(c, R), ((z - w₀) ^ 2)⁻¹ • f z) = ∮ (z : ℂ) in C(c, R), ((z - w₀) ^ 2)⁻¹ • (f z - f w₀)

Proof state:
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U : Set ℂ
hU : IsOpen U
c w₀ : ℂ
R : ℝ
f : ℂ → E
hc : closedBall c R ⊆ U
hf : DifferentiableOn ℂ f U
hw₀ : w₀ ∈ ball c R
hf' : DifferentiableOn ℂ (dslope f w₀) U
h0 : ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, R), (z - w₀)⁻¹ • dslope f w₀ z) = dslope f w₀ w₀
⊢ ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, R), ((z - w₀) ^ 2)⁻¹ • f z) =
    (2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, R), (z - w₀)⁻¹ • dslope f w₀ z

Tactic:
congr 1

Result:
case e_a
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U : Set ℂ
hU : IsOpen U
c w₀ : ℂ
R : ℝ
f : ℂ → E
hc : closedBall c R ⊆ U
hf : DifferentiableOn ℂ f U
hw₀ : w₀ ∈ ball c R
hf' : DifferentiableOn ℂ (dslope f w₀) U
h0 : ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, R), (z - w₀)⁻¹ • dslope f w₀ z) = dslope f w₀ w₀
⊢ (∮ (z : ℂ) in C(c, R), ((z - w₀) ^ 2)⁻¹ • f z) = ∮ (z : ℂ) in C(c, R), (z - w₀)⁻¹ • dslope f w₀ z

Proof state:
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U : Set ℂ
hU : IsOpen U
c w₀ : ℂ
R : ℝ
f : ℂ → E
hc : closedBall c R ⊆ U
hf : DifferentiableOn ℂ f U
hw₀ : w₀ ∈ ball c R
hf' : DifferentiableOn ℂ (dslope f w₀) U
h0 : ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, R), (z - w₀)⁻¹ • dslope f w₀ z) = dslope f w₀ w₀
h1 : ContinuousOn (fun z => ((z - w₀) ^ 2)⁻¹) (sphere c R)
h2 : CircleIntegrable (fun z => ((z - w₀) ^ 2)⁻¹ • f z) c R
h3 : CircleIntegrable (fun z => ((z - w₀) ^ 2)⁻¹ • f w₀) c R
⊢ -2 ≠ -1

Tactic:
decide

Result:
no goals

Proof state:
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U : Set ℂ
hU : IsOpen U
c w₀ : ℂ
R : ℝ
f : ℂ → E
hc : closedBall c R ⊆ U
hf : DifferentiableOn ℂ f U
hw₀ : w₀ ∈ ball c R
hf' : DifferentiableOn ℂ (dslope f w₀) U
h0 : ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, R), (z - w₀)⁻¹ • dslope f w₀ z) = dslope f w₀ w₀
h1 : ContinuousOn (fun z => ((z - w₀) ^ 2)⁻¹) (sphere c R)
⊢ ContinuousOn (fun z => ((z - w₀) ^ 2)⁻¹ • f z) (sphere c R)

Tactic:
exact h1.smul (hf.continuousOn.mono (sphere_subset_closedBall.trans hc))

Result:
no goals

Proof state:
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U : Set ℂ
hU : IsOpen U
c w₀ : ℂ
R : ℝ
f : ℂ → E
hc : closedBall c R ⊆ U
hf : DifferentiableOn ℂ f U
hw₀ : w₀ ∈ ball c R
hf' : DifferentiableOn ℂ (dslope f w₀) U
h0 : ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, R), (z - w₀)⁻¹ • dslope f w₀ z) = dslope f w₀ w₀
h1 : ContinuousOn (fun z => ((z - w₀) ^ 2)⁻¹) (sphere c R)
h2 : CircleIntegrable (fun z => ((z - w₀) ^ 2)⁻¹ • f z) c R
h3 : CircleIntegrable (fun z => ((z - w₀) ^ 2)⁻¹ • f w₀) c R
⊢ (∮ (z : ℂ) in C(c, R), ((z - w₀) ^ 2)⁻¹ • f z) = ∮ (z : ℂ) in C(c, R), ((z - w₀) ^ 2)⁻¹ • (f z - f w₀)

Tactic:
have h4 : (∮ z : ℂ in C(c, R), ((z - w₀) ^ 2)⁻¹) = 0 := by
  simpa using circleIntegral.integral_sub_zpow_of_ne (by decide : (-2 : ℤ) ≠ -1) c w₀ R

Result:
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U : Set ℂ
hU : IsOpen U
c w₀ : ℂ
R : ℝ
f : ℂ → E
hc : closedBall c R ⊆ U
hf : DifferentiableOn ℂ f U
hw₀ : w₀ ∈ ball c R
hf' : DifferentiableOn ℂ (dslope f w₀) U
h0 : ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, R), (z - w₀)⁻¹ • dslope f w₀ z) = dslope f w₀ w₀
h1 : ContinuousOn (fun z => ((z - w₀) ^ 2)⁻¹) (sphere c R)
h2 : CircleIntegrable (fun z => ((z - w₀) ^ 2)⁻¹ • f z) c R
h3 : CircleIntegrable (fun z => ((z - w₀) ^ 2)⁻¹ • f w₀) c R
h4 : (∮ (z : ℂ) in C(c, R), ((z - w₀) ^ 2)⁻¹) = 0
⊢ (∮ (z : ℂ) in C(c, R), ((z - w₀) ^ 2)⁻¹ • f z) = ∮ (z : ℂ) in C(c, R), ((z - w₀) ^ 2)⁻¹ • (f z - f w₀)

Proof state:
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U : Set ℂ
hU : IsOpen U
c w₀ : ℂ
R : ℝ
f : ℂ → E
hc : closedBall c R ⊆ U
hf : DifferentiableOn ℂ f U
hw₀ : w₀ ∈ ball c R
hf' : DifferentiableOn ℂ (dslope f w₀) U
h0 : ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, R), (z - w₀)⁻¹ • dslope f w₀ z) = dslope f w₀ w₀
h1 : ContinuousOn (fun z => ((z - w₀) ^ 2)⁻¹) (sphere c R)
⊢ (∮ (z : ℂ) in C(c, R), ((z - w₀) ^ 2)⁻¹ • f z) = ∮ (z : ℂ) in C(c, R), ((z - w₀) ^ 2)⁻¹ • (f z - f w₀)

Tactic:
have h2 : CircleIntegrable (fun z : ℂ => ((z - w₀) ^ 2)⁻¹ • f z) c R := by
  refine ContinuousOn.circleIntegrable (pos_of_mem_ball hw₀).le ?_
  exact h1.smul (hf.continuousOn.mono (sphere_subset_closedBall.trans hc))

Result:
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U : Set ℂ
hU : IsOpen U
c w₀ : ℂ
R : ℝ
f : ℂ → E
hc : closedBall c R ⊆ U
hf : DifferentiableOn ℂ f U
hw₀ : w₀ ∈ ball c R
hf' : DifferentiableOn ℂ (dslope f w₀) U
h0 : ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, R), (z - w₀)⁻¹ • dslope f w₀ z) = dslope f w₀ w₀
h1 : ContinuousOn (fun z => ((z - w₀) ^ 2)⁻¹) (sphere c R)
h2 : CircleIntegrable (fun z => ((z - w₀) ^ 2)⁻¹ • f z) c R
⊢ (∮ (z : ℂ) in C(c, R), ((z - w₀) ^ 2)⁻¹ • f z) = ∮ (z : ℂ) in C(c, R), ((z - w₀) ^ 2)⁻¹ • (f z - f w₀)