-- 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 ℂ
hs : s.Countable
a : ℝ
h0 : 0 < rexp a
b : ℝ
hle : rexp a ≤ rexp 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
⊢ (∮ (z : ℂ) in C(c, rexp b), (z - c)⁻¹ • f z) = ∮ (z : ℂ) in C(c, rexp a), (z - c)⁻¹ • f z

Tactic:
rw [Real.exp_le_exp] at hle

Result:
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
⊢ (∮ (z : ℂ) in C(c, rexp b), (z - c)⁻¹ • f z) = ∮ (z : ℂ) in C(c, rexp a), (z - c)⁻¹ • f z

Proof state:
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

Tactic:
simpa [g, A, dist_eq, norm_exp, hle] using h.symm

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
⊢ (∮ (z : ℂ) in C(c, rexp b), (z - c)⁻¹ • f z) = ∮ (z : ℂ) in C(c, rexp a), (z - c)⁻¹ • f z

Tactic:
suffices
  (∫ θ in (0)..2 * π, I • f (circleMap c (Real.exp b) θ)) =
    ∫ θ in (0)..2 * π, I • f (circleMap c (Real.exp a) θ) by
  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:
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
⊢ ∫ (θ : ℝ) in 0 ..2 * π, I • f (circleMap c (rexp b) θ) = ∫ (θ : ℝ) in 0 ..2 * π, I • f (circleMap c (rexp a) θ)