E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
z w : ℂ
s : Set ℂ
hs : Set.Countable s
Hc : ContinuousOn f ([[z.re, w.re]] ×ℂ [[z.im, w.im]])
Hd :
  ∀ (x : ℂ), x ∈ Ioo (min z.re w.re) (max z.re w.re) ×ℂ Ioo (min z.im w.im) (max z.im w.im) \ s → DifferentiableAt ℂ f x
this :
  ∀ (z : ℂ),
    I • ↑(ContinuousLinearMap.restrictScalars ℝ (fderiv ℂ f z)) 1 =
      ↑(ContinuousLinearMap.restrictScalars ℝ (fderiv ℂ f z)) I
⊢ ((((∫ (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 (↑w.re + ↑y * I)) -
      I • ∫ (y : ℝ) in z.im..w.im, f (↑z.re + ↑y * I)) =
    0
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
z w : ℂ
s : Set ℂ
hs : Set.Countable s
Hc : ContinuousOn f ([[z.re, w.re]] ×ℂ [[z.im, w.im]])
Hd :
  ∀ (x : ℂ), x ∈ Ioo (min z.re w.re) (max z.re w.re) ×ℂ Ioo (min z.im w.im) (max z.im w.im) \ s → DifferentiableAt ℂ f x
⊢ ((((∫ (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 (↑w.re + ↑y * I)) -
      I • ∫ (y : ℝ) in z.im..w.im, f (↑z.re + ↑y * I)) =
    0
have : ∀ z, I • (fderiv ℂ f z).restrictScalars ℝ 1 = (fderiv ℂ f z).restrictScalars ℝ I := fun z ↦
  by rw [(fderiv ℂ f _).coe_restrictScalars', ← (fderiv ℂ f _).map_smul, smul_eq_mul, mul_one]
no goals
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
z w : ℂ
s : Set ℂ
hs : Set.Countable s
Hc : ContinuousOn f ([[z.re, w.re]] ×ℂ [[z.im, w.im]])
Hd :
  ∀ (x : ℂ), x ∈ Ioo (min z.re w.re) (max z.re w.re) ×ℂ Ioo (min z.im w.im) (max z.im w.im) \ s → DifferentiableAt ℂ f x
this :
  ∀ (z : ℂ),
    I • ↑(ContinuousLinearMap.restrictScalars ℝ (fderiv ℂ f z)) 1 =
      ↑(ContinuousLinearMap.restrictScalars ℝ (fderiv ℂ f z)) I
⊢ ((((∫ (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 (↑w.re + ↑y * I)) -
      I • ∫ (y : ℝ) in z.im..w.im, f (↑z.re + ↑y * I)) =
    0
refine (integral_boundary_rect_of_hasFDerivAt_real_off_countable f
  (fun z => (fderiv ℂ f z).restrictScalars ℝ) z w s hs Hc
  (fun x hx => (Hd x hx).hasFDerivAt.restrictScalars ℝ) ?_).trans ?_ <;> simp [this]
no goals
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
z✝ w : ℂ
s : Set ℂ
hs : Set.Countable s
Hc : ContinuousOn f ([[z✝.re, w.re]] ×ℂ [[z✝.im, w.im]])
Hd :
  ∀ (x : ℂ),
    x ∈ Ioo (min z✝.re w.re) (max z✝.re w.re) ×ℂ Ioo (min z✝.im w.im) (max z✝.im w.im) \ s → DifferentiableAt ℂ f x
z : ℂ
⊢ I • ↑(ContinuousLinearMap.restrictScalars ℝ (fderiv ℂ f z)) 1 =
    ↑(ContinuousLinearMap.restrictScalars ℝ (fderiv ℂ f z)) I
rw [(fderiv ℂ f _).coe_restrictScalars', ← (fderiv ℂ f _).map_smul, smul_eq_mul, mul_one]