-- Mathlib/MeasureTheory/Integral/CircleIntegral.lean
theorem integral_sub_inv_smul_sub_smul (f : ℂ → E) (c w : ℂ) (R : ℝ) :
    (∮ z in C(c, R), (z - w)⁻¹ • (z - w) • f z) = ∮ z in C(c, R), f z

Proof state:
case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c w : ℂ
R : ℝ
hR : R ≠ 0
this : (circleMap c R ⁻¹' {w}).Countable
θ : ℝ
hθ : θ ∉ circleMap c R ⁻¹' {w}
_' : θ ∈ Ι 0 (2 * π)
⊢ deriv (circleMap c R) θ • (fun z => (z - w)⁻¹ • (z - w) • f z) (circleMap c R θ) =
    deriv (circleMap c R) θ • (fun z => f z) (circleMap c R θ)

Tactic:
change circleMap c R θ ≠ w at hθ

Result:
case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c w : ℂ
R : ℝ
hR : R ≠ 0
this : (circleMap c R ⁻¹' {w}).Countable
θ : ℝ
_' : θ ∈ Ι 0 (2 * π)
hθ : circleMap c R θ ≠ w
⊢ deriv (circleMap c R) θ • (fun z => (z - w)⁻¹ • (z - w) • f z) (circleMap c R θ) =
    deriv (circleMap c R) θ • (fun z => f z) (circleMap c R θ)

Proof state:
case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c w : ℂ
⊢ (∮ (z : ℂ) in C(c, 0), (z - w)⁻¹ • (z - w) • f z) = ∮ (z : ℂ) in C(c, 0), f z

Tactic:
simp only [integral_radius_zero]

Result:
no goals

Proof state:
case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c w : ℂ
R : ℝ
hR : R ≠ 0
this : (circleMap c R ⁻¹' {w}).Countable
⊢ (∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • (z - w) • f z) = ∮ (z : ℂ) in C(c, R), f z

Tactic:
refine intervalIntegral.integral_congr_ae ((this.ae_not_mem _).mono fun θ hθ _' => ?_)

Result:
case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c w : ℂ
R : ℝ
hR : R ≠ 0
this : (circleMap c R ⁻¹' {w}).Countable
θ : ℝ
hθ : θ ∉ circleMap c R ⁻¹' {w}
_' : θ ∈ Ι 0 (2 * π)
⊢ deriv (circleMap c R) θ • (fun z => (z - w)⁻¹ • (z - w) • f z) (circleMap c R θ) =
    deriv (circleMap c R) θ • (fun z => f z) (circleMap c R θ)

Proof state:
case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c w : ℂ
R : ℝ
hR : R ≠ 0
⊢ (∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • (z - w) • f z) = ∮ (z : ℂ) in C(c, R), f z

Tactic:
have : (circleMap c R ⁻¹' {w}).Countable := (countable_singleton _).preimage_circleMap c hR

Result:
case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c w : ℂ
R : ℝ
hR : R ≠ 0
this : (circleMap c R ⁻¹' {w}).Countable
⊢ (∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • (z - w) • f z) = ∮ (z : ℂ) in C(c, R), f z

Proof state:
case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c w : ℂ
R : ℝ
hR : R ≠ 0
this : (circleMap c R ⁻¹' {w}).Countable
θ : ℝ
_' : θ ∈ Ι 0 (2 * π)
hθ : circleMap c R θ ≠ w
⊢ deriv (circleMap c R) θ • (fun z => (z - w)⁻¹ • (z - w) • f z) (circleMap c R θ) =
    deriv (circleMap c R) θ • (fun z => f z) (circleMap c R θ)

Tactic:
simp only [inv_smul_smul₀ (sub_ne_zero.2 <| hθ)]

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c w : ℂ
R : ℝ
⊢ (∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • (z - w) • f z) = ∮ (z : ℂ) in C(c, R), f z

Tactic:
rcases eq_or_ne R 0 with (rfl | hR)

Result:
case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c w : ℂ
⊢ (∮ (z : ℂ) in C(c, 0), (z - w)⁻¹ • (z - w) • f z) = ∮ (z : ℂ) in C(c, 0), f z

case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c w : ℂ
R : ℝ
hR : R ≠ 0
⊢ (∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • (z - w) • f z) = ∮ (z : ℂ) in C(c, R), f z