-- Mathlib/Analysis/Complex/CauchyIntegral.lean
theorem circleIntegral_sub_center_inv_smul_eq_of_differentiable_on_annulus_off_countable {c : ℂ}
    {r R : ℝ} (h0 : 0 < r) (hle : r ≤ R) {f : ℂ → E} {s : Set ℂ} (hs : s.Countable)
    (hc : ContinuousOn f (closedBall c R \ ball c r))
    (hd : ∀ z ∈ (ball c R \ closedBall c r) \ s, DifferentiableAt ℂ f z) :
    (∮ z in C(c, R), (z - c)⁻¹ • f z) = ∮ z in C(c, r), (z - c)⁻¹ • f z

Proof state:
case intro.intro
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
c : ℂ
f : ℂ → E
s : Set ℂ
a : ℝ
h0 : 0 < rexp a
b : ℝ
hle : a ≤ b
hd : ∀ z ∈ (ball c (rexp b) \ closedBall c (rexp a)) \ s, DifferentiableAt ℂ f z
A : Set ℂ := closedBall c (rexp b) \ ball c (rexp a)
hc : ContinuousOn f A
R : Set ℂ := [[a, b]] ×ℂ [[0, 2 * π]]
g : ℂ → ℂ := fun x => c + cexp x
hdg : Differentiable ℂ g
hs : (g ⁻¹' s).Countable
h_maps : MapsTo g R A
⊢ ∫ (θ : ℝ) in 0 ..2 * π, I • f (circleMap c (rexp b) θ) = ∫ (θ : ℝ) in 0 ..2 * π, I • f (circleMap c (rexp a) θ)

Tactic:
replace hc : ContinuousOn (f ∘ g) R := hc.comp hdg.continuous.continuousOn h_maps

Result:
case intro.intro
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
c : ℂ
f : ℂ → E
s : Set ℂ
a : ℝ
h0 : 0 < rexp a
b : ℝ
hle : a ≤ b
hd : ∀ z ∈ (ball c (rexp b) \ closedBall c (rexp a)) \ s, DifferentiableAt ℂ f z
A : Set ℂ := closedBall c (rexp b) \ ball c (rexp a)
R : Set ℂ := [[a, b]] ×ℂ [[0, 2 * π]]
g : ℂ → ℂ := fun x => c + cexp x
hdg : Differentiable ℂ g
hs : (g ⁻¹' s).Countable
h_maps : MapsTo g R A
hc : ContinuousOn (f ∘ g) R
⊢ ∫ (θ : ℝ) in 0 ..2 * π, I • f (circleMap c (rexp b) θ) = ∫ (θ : ℝ) in 0 ..2 * π, I • f (circleMap c (rexp a) θ)

Proof state:
case intro.intro
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
c : ℂ
f : ℂ → E
s : Set ℂ
a : ℝ
h0 : 0 < rexp a
b : ℝ
hle : a ≤ b
hd : ∀ z ∈ (ball c (rexp b) \ closedBall c (rexp a)) \ s, DifferentiableAt ℂ f z
A : Set ℂ := closedBall c (rexp b) \ ball c (rexp a)
hc : ContinuousOn f A
R : Set ℂ := [[a, b]] ×ℂ [[0, 2 * π]]
g : ℂ → ℂ := fun x => c + cexp x
hdg : Differentiable ℂ g
hs : (g ⁻¹' s).Countable
⊢ ∫ (θ : ℝ) in 0 ..2 * π, I • f (circleMap c (rexp b) θ) = ∫ (θ : ℝ) in 0 ..2 * π, I • f (circleMap c (rexp a) θ)

Tactic:
have h_maps : MapsTo g R A := by
  rintro z ⟨h, -⟩; simpa [g, A, dist_eq, norm_exp, hle] using h.symm

Result:
case intro.intro
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
c : ℂ
f : ℂ → E
s : Set ℂ
a : ℝ
h0 : 0 < rexp a
b : ℝ
hle : a ≤ b
hd : ∀ z ∈ (ball c (rexp b) \ closedBall c (rexp a)) \ s, DifferentiableAt ℂ f z
A : Set ℂ := closedBall c (rexp b) \ ball c (rexp a)
hc : ContinuousOn f A
R : Set ℂ := [[a, b]] ×ℂ [[0, 2 * π]]
g : ℂ → ℂ := fun x => c + cexp x
hdg : Differentiable ℂ g
hs : (g ⁻¹' s).Countable
h_maps : MapsTo g R A
⊢ ∫ (θ : ℝ) in 0 ..2 * π, I • f (circleMap c (rexp b) θ) = ∫ (θ : ℝ) in 0 ..2 * π, I • f (circleMap c (rexp a) θ)

Proof state:
case intro.intro
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
c : ℂ
f : ℂ → E
s : Set ℂ
a : ℝ
h0 : 0 < rexp a
b : ℝ
hle : a ≤ b
A : Set ℂ := closedBall c (rexp b) \ ball c (rexp a)
R : Set ℂ := [[a, b]] ×ℂ [[0, 2 * π]]
g : ℂ → ℂ := fun x => c + cexp x
hdg : Differentiable ℂ g
hs : (g ⁻¹' s).Countable
h_maps : MapsTo g R A
hc : ContinuousOn (f ∘ g) R
hd : ∀ z ∈ Ioo (a ⊓ b) (a ⊔ b) ×ℂ Ioo (0 ⊓ 2 * π) (0 ⊔ 2 * π) \ g ⁻¹' s, DifferentiableAt ℂ (f ∘ g) z
⊢ ∫ (θ : ℝ) in 0 ..2 * π, I • f (circleMap c (rexp b) θ) = ∫ (θ : ℝ) in 0 ..2 * π, I • f (circleMap c (rexp a) θ)

Tactic:
simpa [g, circleMap, exp_periodic _, sub_eq_zero, ← exp_add] using
  integral_boundary_rect_eq_zero_of_differentiable_on_off_countable _ ⟨a, 0⟩ ⟨b, 2 * π⟩ _ hs hc hd

Result:
no goals

Proof state:
case intro.intro
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
c : ℂ
f : ℂ → E
s : Set ℂ
hs : s.Countable
a : ℝ
h0 : 0 < rexp a
b : ℝ
hle : a ≤ b
hd : ∀ z ∈ (ball c (rexp b) \ closedBall c (rexp a)) \ s, DifferentiableAt ℂ f z
A : Set ℂ := closedBall c (rexp b) \ ball c (rexp a)
hc : ContinuousOn f A
R : Set ℂ := [[a, b]] ×ℂ [[0, 2 * π]]
g : ℂ → ℂ := fun x => c + cexp x
hdg : Differentiable ℂ g
⊢ ∫ (θ : ℝ) in 0 ..2 * π, I • f (circleMap c (rexp b) θ) = ∫ (θ : ℝ) in 0 ..2 * π, I • f (circleMap c (rexp a) θ)

Tactic:
replace hs : (g ⁻¹' s).Countable := (hs.preimage (add_right_injective c)).preimage_cexp

Result:
case intro.intro
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
c : ℂ
f : ℂ → E
s : Set ℂ
a : ℝ
h0 : 0 < rexp a
b : ℝ
hle : a ≤ b
hd : ∀ z ∈ (ball c (rexp b) \ closedBall c (rexp a)) \ s, DifferentiableAt ℂ f z
A : Set ℂ := closedBall c (rexp b) \ ball c (rexp a)
hc : ContinuousOn f A
R : Set ℂ := [[a, b]] ×ℂ [[0, 2 * π]]
g : ℂ → ℂ := fun x => c + cexp x
hdg : Differentiable ℂ g
hs : (g ⁻¹' s).Countable
⊢ ∫ (θ : ℝ) in 0 ..2 * π, I • f (circleMap c (rexp b) θ) = ∫ (θ : ℝ) in 0 ..2 * π, I • f (circleMap c (rexp a) θ)

Proof state:
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
c : ℂ
r R : ℝ
h0 : 0 < r
hle : r ≤ R
f : ℂ → E
s : Set ℂ
hs : s.Countable
hd : ∀ z ∈ (ball c R \ closedBall c r) \ s, DifferentiableAt ℂ f z
A : Set ℂ := closedBall c R \ ball c r
hc : ContinuousOn f A
⊢ (∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z) = ∮ (z : ℂ) in C(c, r), (z - c)⁻¹ • f z

Tactic:
obtain ⟨a, rfl⟩ : ∃ a, Real.exp a = r := ⟨Real.log r, Real.exp_log h0⟩

Result:
case intro
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
c : ℂ
R : ℝ
f : ℂ → E
s : Set ℂ
hs : s.Countable
a : ℝ
h0 : 0 < rexp a
hle : rexp a ≤ R
hd : ∀ z ∈ (ball c R \ closedBall c (rexp a)) \ s, DifferentiableAt ℂ f z
A : Set ℂ := closedBall c R \ ball c (rexp a)
hc : ContinuousOn f A
⊢ (∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z) = ∮ (z : ℂ) in C(c, rexp a), (z - c)⁻¹ • f z

Proof state:
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
c : ℂ
f : ℂ → E
s : Set ℂ
a : ℝ
h0 : 0 < rexp a
b : ℝ
hle : a ≤ b
hd : ∀ z ∈ (ball c (rexp b) \ closedBall c (rexp a)) \ s, DifferentiableAt ℂ f z
A : Set ℂ := closedBall c (rexp b) \ ball c (rexp a)
hc : ContinuousOn f A
R : Set ℂ := [[a, b]] ×ℂ [[0, 2 * π]]
g : ℂ → ℂ := fun x => c + cexp x
hdg : Differentiable ℂ g
hs : (g ⁻¹' s).Countable
⊢ MapsTo g R A

Tactic:
rintro z ⟨h, -⟩

Result:
case intro
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
c : ℂ
f : ℂ → E
s : Set ℂ
a : ℝ
h0 : 0 < rexp a
b : ℝ
hle : a ≤ b
hd : ∀ z ∈ (ball c (rexp b) \ closedBall c (rexp a)) \ s, DifferentiableAt ℂ f z
A : Set ℂ := closedBall c (rexp b) \ ball c (rexp a)
hc : ContinuousOn f A
R : Set ℂ := [[a, b]] ×ℂ [[0, 2 * π]]
g : ℂ → ℂ := fun x => c + cexp x
hdg : Differentiable ℂ g
hs : (g ⁻¹' s).Countable
z : ℂ
h : z ∈ re ⁻¹' [[a, b]]
⊢ g z ∈ A

Proof state:
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
c : ℂ
f : ℂ → E
s : Set ℂ
hs : s.Countable
a : ℝ
h0 : 0 < rexp a
b : ℝ
hle : a ≤ b
hd : ∀ z ∈ (ball c (rexp b) \ closedBall c (rexp a)) \ s, DifferentiableAt ℂ f z
A : Set ℂ := closedBall c (rexp b) \ ball c (rexp a)
hc : ContinuousOn f A
this : ∫ (θ : ℝ) in 0 ..2 * π, I • f (circleMap c (rexp b) θ) = ∫ (θ : ℝ) in 0 ..2 * π, I • f (circleMap c (rexp a) θ)
⊢ (∮ (z : ℂ) in C(c, rexp b), (z - c)⁻¹ • f z) = ∮ (z : ℂ) in C(c, rexp a), (z - c)⁻¹ • f z

Tactic:
simpa only [circleIntegral, add_sub_cancel_left, ofReal_exp, ← exp_add, smul_smul, ←
  div_eq_mul_inv, mul_div_cancel_left₀ _ (circleMap_ne_center (Real.exp_pos _).ne'),
  circleMap_sub_center, deriv_circleMap]

Result:
no goals