-- Lean 4 proof step from Mathlib.Analysis.Complex.CauchyIntegral (goal)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ 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 (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.{0, u} (ε := E) (mα := MeasureSpace.toMeasurableSpace)
    (fun (z : ℂ) ↦
      HSub.hSub (β := E) (HSMul.hSMul (β := E) I ((f' z : (a : ℂ) → E) 1 : E)) ((f' z : (a : ℂ) → E) I : E))
    ([[z.re, w.re]] ×ℂ [[z.im, w.im]]) volume
e : (ℝ × ℝ) ≃L[ℝ] ℂ := equivRealProdCLM.symm
he₁ : Eq (α := ℂ) ((e : (a : ℝ × ℝ) → ℂ) (1, 0) : ℂ) (1 : ℂ)
he₂ : (e : (a : ℝ × ℝ) → ℂ) (0, 1) = I
he : ∀ (x y : ℝ), True
F : ℝ × ℝ → E := f ∘ (⇑e : (a : ℝ × ℝ) → ℂ)
F' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E := fun (p : ℝ × ℝ) ↦ f' ((e : (a : ℝ × ℝ) → ℂ) p) ∘SL (↑e : ℝ × ℝ →L[ℝ] ℂ)
hF' :
  ∀ (p : ℝ × ℝ),
    HAdd.hAdd (α := E) (β := E) ((-(I • F' p) : (a : ℝ × ℝ) → E) (1, 0) : E) ((F' p : (a : ℝ × ℝ) → E) (0, 1) : E) =
      -HSub.hSub (β := E) (HSMul.hSMul (β := E) I ((f' ((e : (a : ℝ × ℝ) → ℂ) p) : (a : ℂ) → E) 1 : E))
          ((f' ((e : (a : ℝ × ℝ) → ℂ) p) : (a : ℂ) → E) I : E)
R : Set (ℝ × ℝ) := [[z.re, w.re]] ×ˢ [[w.im, z.im]]
t : Set (ℝ × ℝ) := (⇑e : (a : ℝ × ℝ) → ℂ) ⁻¹' s
⊢ HSub.hSub (α := E) (∫ (x : ℝ) in z.re..w.re, f ((e : (a : ℝ × ℝ) → ℂ) (x, z.im)))
          (∫ (x : ℝ) in z.re..w.re, f ((e : (a : ℝ × ℝ) → ℂ) (x, w.im))) +
        HSMul.hSMul (β := E) I (∫ (y : ℝ) in z.im..w.im, f ((e : (a : ℝ × ℝ) → ℂ) (w.re, y))) -
      HSMul.hSMul (β := E) I (∫ (y : ℝ) in z.im..w.im, f ((e : (a : ℝ × ℝ) → ℂ) (z.re, y))) =
    ∫ (x : ℝ) in z.re..w.re,
      ∫ (y : ℝ) in z.im..w.im,
        HSub.hSub (β := E) (HSMul.hSMul (β := E) I ((f' ((e : (a : ℝ × ℝ) → ℂ) (x, y)) : (a : ℂ) → E) 1 : E))
          ((f' ((e : (a : ℝ × ℝ) → ℂ) (x, y)) : (a : ℂ) → E) I : E)
have rw : ∀ (Hc : ContinuousOn f ([[z.re, w.re]] ×ℂ [[w.im, z.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.{0, u} (ε := E) (mα := MeasureSpace.toMeasurableSpace)
      (fun (z : ℂ) ↦
        HSub.hSub (β := E) (HSMul.hSMul (β := E) I ((f' z : (a : ℂ) → E) 1 : E)) ((f' z : (a : ℂ) → E) I : E))
      ([[z.re, w.re]] ×ℂ [[w.im, z.im]]) volume),
  let e := equivRealProdCLM.symm;
  ∀ (he₁ : Eq (α := ℂ) ((e : (a : ℝ × ℝ) → ℂ) (1, 0) : ℂ) (1 : ℂ)) (he₂ : (e : (a : ℝ × ℝ) → ℂ) (0, 1) = I)
    (he : ∀ (x y : ℝ), True),
    let F' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E := fun (p : ℝ × ℝ) ↦ f' ((e : (a : ℝ × ℝ) → ℂ) p) ∘SL (↑e : ℝ × ℝ →L[ℝ] ℂ);
    ∀
      (hF' :
        ∀ (p : ℝ × ℝ),
          HAdd.hAdd (α := E) (β := E) ((-(I • F' p) : (a : ℝ × ℝ) → E) (1, 0) : E)
              ((F' p : (a : ℝ × ℝ) → E) (0, 1) : E) =
            -HSub.hSub (β := E) (HSMul.hSMul (β := E) I ((f' ((e : (a : ℝ × ℝ) → ℂ) p) : (a : ℂ) → E) 1 : E))
                ((f' ((e : (a : ℝ × ℝ) → ℂ) p) : (a : ℂ) → E) I : E)),
      HSub.hSub (α := E) (∫ (x : ℝ) in z.re..w.re, f ((e : (a : ℝ × ℝ) → ℂ) (x, z.im)))
              (∫ (x : ℝ) in z.re..w.re, f ((e : (a : ℝ × ℝ) → ℂ) (x, w.im))) +
            HSMul.hSMul (β := E) I (∫ (y : ℝ) in z.im..w.im, f ((e : (a : ℝ × ℝ) → ℂ) (w.re, y))) -
          HSMul.hSMul (β := E) I (∫ (y : ℝ) in z.im..w.im, f ((e : (a : ℝ × ℝ) → ℂ) (z.re, y))) =
        ∫ (x : ℝ) in z.re..w.re,
          ∫ (y : ℝ) in z.im..w.im,
            HSub.hSub (β := E) (HSMul.hSMul (β := E) I ((f' ((e : (a : ℝ × ℝ) → ℂ) (x, y)) : (a : ℂ) → E) 1 : E))
              ((f' ((e : (a : ℝ × ℝ) → ℂ) (x, y)) : (a : ℂ) → E) I : E)
Tactic: rw [uIcc_comm z.im] at Hc Hi
Cleared hypotheses: Hc, Hd, Hi, e, he₁, he₂, he, F, F', hF', R, t