-- Mathlib/Analysis/Complex/CauchyIntegral.lean
theorem integral_boundary_rect_of_hasFDerivAt_real_off_countable (f : ℂ → E) (f' : ℂ → ℂ →L[ℝ] E)
    (z w : ℂ) (s : Set ℂ) (hs : s.Countable)
    (Hc : ContinuousOn f ([[z.re, w.re]] ×ℂ [[z.im, w.im]]))
    (Hd : ∀ x ∈ Ioo (min z.re w.re) (max z.re w.re) ×ℂ Ioo (min z.im w.im) (max z.im w.im) \ s,
      HasFDerivAt f (f' x) x)
    (Hi : IntegrableOn (fun z => I • f' z 1 - f' z I) ([[z.re, w.re]] ×ℂ [[z.im, w.im]])) :
    (∫ x : ℝ in z.re..w.re, f (x + z.im * I)) - (∫ x : ℝ in z.re..w.re, f (x + w.im * I)) +
      I • (∫ y : ℝ in z.im..w.im, f (re w + y * I)) -
      I • ∫ y : ℝ in z.im..w.im, f (re z + y * I) =
      ∫ x : ℝ in z.re..w.re, ∫ y : ℝ in z.im..w.im, I • f' (x + y * I) 1 - f' (x + y * I) I

Proof state:
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
f' : ℂ → ℂ →L[ℝ] E
z w : ℂ
s : Set ℂ
hs : s.Countable
Hc : ContinuousOn f ([[z.re, w.re]] ×ℂ [[w.im, z.im]])
Hd : ∀ x ∈ Ioo (z.re ⊓ w.re) (z.re ⊔ w.re) ×ℂ Ioo (w.im ⊓ z.im) (w.im ⊔ z.im) \ s, HasFDerivAt f (f' x) x
Hi : IntegrableOn (fun z => I • (f' z) 1 - (f' z) I) ([[z.re, w.re]] ×ℂ [[w.im, z.im]]) volume
e : (ℝ × ℝ) ≃L[ℝ] ℂ := equivRealProdCLM.symm
he₁ : e (1, 0) = 1
he₂ : e (0, 1) = I
he : ℝ → ℝ → True
F : ℝ × ℝ → E := f ∘ ⇑e
F' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E := fun p => (f' (e p)).comp ↑e
hF' : ∀ (p : ℝ × ℝ), (-(I • F' p)) (1, 0) + (F' p) (0, 1) = -(I • (f' (e p)) 1 - (f' (e p)) I)
R : Set (ℝ × ℝ) := [[z.re, w.re]] ×ˢ [[w.im, z.im]]
t : Set (ℝ × ℝ) := ⇑e ⁻¹' s
hR : ⇑e ⁻¹' ([[z.re, w.re]] ×ℂ [[w.im, z.im]]) = R
htc : ContinuousOn F R
htd : ∀ p ∈ Ioo (z.re ⊓ w.re) (z.re ⊔ w.re) ×ˢ Ioo (w.im ⊓ z.im) (w.im ⊔ z.im) \ t, HasFDerivAt F (F' p) p
⊢ (((∫ (x : ℝ) in z.re..w.re, f (e (x, z.im))) - ∫ (x : ℝ) in z.re..w.re, f (e (x, w.im))) +
        ∫ (x : ℝ) in w.im..z.im, -(I • f (e (w.re, x)))) -
      ∫ (x : ℝ) in w.im..z.im, -(I • f (e (z.re, x))) =
    ∫ (x : ℝ) in z.re..w.re, ∫ (x_1 : ℝ) in w.im..z.im, (-(I • F' (x, x_1))) (1, 0) + (F' (x, x_1)) (0, 1)

Tactic:
refine (integral2_divergence_prod_of_hasFDerivWithinAt_off_countable (fun p => -(I • F p)) F
  (fun p => -(I • F' p)) F' z.re w.im w.re z.im t (hs.preimage e.injective)
  (htc.const_smul _).neg htc (fun p hp => ((htd p hp).const_smul I).neg) htd ?_).symm

Result:
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
f' : ℂ → ℂ →L[ℝ] E
z w : ℂ
s : Set ℂ
hs : s.Countable
Hc : ContinuousOn f ([[z.re, w.re]] ×ℂ [[w.im, z.im]])
Hd : ∀ x ∈ Ioo (z.re ⊓ w.re) (z.re ⊔ w.re) ×ℂ Ioo (w.im ⊓ z.im) (w.im ⊔ z.im) \ s, HasFDerivAt f (f' x) x
Hi : IntegrableOn (fun z => I • (f' z) 1 - (f' z) I) ([[z.re, w.re]] ×ℂ [[w.im, z.im]]) volume
e : (ℝ × ℝ) ≃L[ℝ] ℂ := equivRealProdCLM.symm
he₁ : e (1, 0) = 1
he₂ : e (0, 1) = I
he : ℝ → ℝ → True
F : ℝ × ℝ → E := f ∘ ⇑e
F' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E := fun p => (f' (e p)).comp ↑e
hF' : ∀ (p : ℝ × ℝ), (-(I • F' p)) (1, 0) + (F' p) (0, 1) = -(I • (f' (e p)) 1 - (f' (e p)) I)
R : Set (ℝ × ℝ) := [[z.re, w.re]] ×ˢ [[w.im, z.im]]
t : Set (ℝ × ℝ) := ⇑e ⁻¹' s
hR : ⇑e ⁻¹' ([[z.re, w.re]] ×ℂ [[w.im, z.im]]) = R
htc : ContinuousOn F R
htd : ∀ p ∈ Ioo (z.re ⊓ w.re) (z.re ⊔ w.re) ×ˢ Ioo (w.im ⊓ z.im) (w.im ⊔ z.im) \ t, HasFDerivAt F (F' p) p
⊢ IntegrableOn (fun x => ((fun p => -(I • F' p)) x) (1, 0) + (F' x) (0, 1)) ([[z.re, w.re]] ×ˢ [[w.im, z.im]]) volume

Proof state:
case mk
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
f' : ℂ → ℂ →L[ℝ] E
z w : ℂ
s : Set ℂ
hs : s.Countable
Hc : ContinuousOn f ([[z.re, w.re]] ×ℂ [[z.im, w.im]])
Hd : ∀ x ∈ Ioo (z.re ⊓ w.re) (z.re ⊔ w.re) ×ℂ Ioo (z.im ⊓ w.im) (z.im ⊔ w.im) \ s, HasFDerivAt f (f' x) x
Hi : IntegrableOn (fun z => I • (f' z) 1 - (f' z) I) ([[z.re, w.re]] ×ℂ [[z.im, w.im]]) volume
e : (ℝ × ℝ) ≃L[ℝ] ℂ := equivRealProdCLM.symm
he₁ : e (1, 0) = 1
he₂ : e (0, 1) = I
he : ℝ → ℝ → True
F : ℝ × ℝ → E := f ∘ ⇑e
F' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E := fun p => (f' (e p)).comp ↑e
x y : ℝ
⊢ (-(I • F' (x, y))) (1, 0) + (F' (x, y)) (0, 1) = -(I • (f' (e (x, y))) 1 - (f' (e (x, y))) I)

Tactic:
simp only [F', ContinuousLinearMap.neg_apply, ContinuousLinearMap.smul_apply,
  ContinuousLinearMap.comp_apply, ContinuousLinearEquiv.coe_coe, he₁, he₂, neg_add_eq_sub,
  neg_sub]

Result:
no goals

Proof state:
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
f' : ℂ → ℂ →L[ℝ] E
z w : ℂ
s : Set ℂ
hs : s.Countable
Hc : ContinuousOn f ([[z.re, w.re]] ×ℂ [[w.im, z.im]])
Hd : ∀ x ∈ Ioo (z.re ⊓ w.re) (z.re ⊔ w.re) ×ℂ Ioo (w.im ⊓ z.im) (w.im ⊔ z.im) \ s, HasFDerivAt f (f' x) x
Hi : IntegrableOn (fun z => I • (f' z) 1 - (f' z) I) ([[z.re, w.re]] ×ℂ [[w.im, z.im]]) volume
e : (ℝ × ℝ) ≃L[ℝ] ℂ := equivRealProdCLM.symm
he₁ : e (1, 0) = 1
he₂ : e (0, 1) = I
he : ℝ → ℝ → True
F : ℝ × ℝ → E := f ∘ ⇑e
F' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E := fun p => (f' (e p)).comp ↑e
hF' : ∀ (p : ℝ × ℝ), (-(I • F' p)) (1, 0) + (F' p) (0, 1) = -(I • (f' (e p)) 1 - (f' (e p)) I)
R : Set (ℝ × ℝ) := [[z.re, w.re]] ×ˢ [[w.im, z.im]]
t : Set (ℝ × ℝ) := ⇑e ⁻¹' s
hR : ⇑e ⁻¹' ([[z.re, w.re]] ×ℂ [[w.im, z.im]]) = R
htc : ContinuousOn F R
htd : ∀ p ∈ Ioo (z.re ⊓ w.re) (z.re ⊔ w.re) ×ˢ Ioo (w.im ⊓ z.im) (w.im ⊔ z.im) \ t, HasFDerivAt F (F' p) p
⊢ (((∫ (x : ℝ) in z.re..w.re, f (e (x, z.im))) - ∫ (x : ℝ) in z.re..w.re, f (e (x, w.im))) +
        I • ∫ (y : ℝ) in z.im..w.im, f (e (w.re, y))) -
      I • ∫ (y : ℝ) in z.im..w.im, f (e (z.re, y)) =
    ∫ (x : ℝ) in z.re..w.re, ∫ (y : ℝ) in z.im..w.im, I • (f' (e (x, y))) 1 - (f' (e (x, y))) I

Tactic:
simp_rw [← intervalIntegral.integral_smul, intervalIntegral.integral_symm w.im z.im, ←
  intervalIntegral.integral_neg, ← hF']

Result:
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
f' : ℂ → ℂ →L[ℝ] E
z w : ℂ
s : Set ℂ
hs : s.Countable
Hc : ContinuousOn f ([[z.re, w.re]] ×ℂ [[w.im, z.im]])
Hd : ∀ x ∈ Ioo (z.re ⊓ w.re) (z.re ⊔ w.re) ×ℂ Ioo (w.im ⊓ z.im) (w.im ⊔ z.im) \ s, HasFDerivAt f (f' x) x
Hi : IntegrableOn (fun z => I • (f' z) 1 - (f' z) I) ([[z.re, w.re]] ×ℂ [[w.im, z.im]]) volume
e : (ℝ × ℝ) ≃L[ℝ] ℂ := equivRealProdCLM.symm
he₁ : e (1, 0) = 1
he₂ : e (0, 1) = I
he : ℝ → ℝ → True
F : ℝ × ℝ → E := f ∘ ⇑e
F' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E := fun p => (f' (e p)).comp ↑e
hF' : ∀ (p : ℝ × ℝ), (-(I • F' p)) (1, 0) + (F' p) (0, 1) = -(I • (f' (e p)) 1 - (f' (e p)) I)
R : Set (ℝ × ℝ) := [[z.re, w.re]] ×ˢ [[w.im, z.im]]
t : Set (ℝ × ℝ) := ⇑e ⁻¹' s
hR : ⇑e ⁻¹' ([[z.re, w.re]] ×ℂ [[w.im, z.im]]) = R
htc : ContinuousOn F R
htd : ∀ p ∈ Ioo (z.re ⊓ w.re) (z.re ⊔ w.re) ×ˢ Ioo (w.im ⊓ z.im) (w.im ⊔ z.im) \ t, HasFDerivAt F (F' p) p
⊢ (((∫ (x : ℝ) in z.re..w.re, f (e (x, z.im))) - ∫ (x : ℝ) in z.re..w.re, f (e (x, w.im))) +
        ∫ (x : ℝ) in w.im..z.im, -(I • f (e (w.re, x)))) -
      ∫ (x : ℝ) in w.im..z.im, -(I • f (e (z.re, x))) =
    ∫ (x : ℝ) in z.re..w.re, ∫ (x_1 : ℝ) in w.im..z.im, (-(I • F' (x, x_1))) (1, 0) + (F' (x, x_1)) (0, 1)