E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
f' : ℂ → ℂ →L[ℝ] 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 → HasFDerivAt f (f' x) x
Hi : IntegrableOn (fun z => I • ↑(f' z) 1 - ↑(f' z) I) ([[z.re, w.re]] ×ℂ [[z.im, w.im]])
e : (ℝ × ℝ) ≃L[ℝ] ℂ := ContinuousLinearEquiv.symm equivRealProdClm
⊢ ((((∫ (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)) =
    ∫ (x : ℝ) in z.re..w.re, ∫ (y : ℝ) in z.im..w.im, I • ↑(f' (↑x + ↑y * I)) 1 - ↑(f' (↑x + ↑y * I)) I
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
f' : ℂ → ℂ →L[ℝ] 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 → 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 (↑w.re + ↑y * I)) -
      I • ∫ (y : ℝ) in z.im..w.im, f (↑z.re + ↑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
set e : (ℝ × ℝ) ≃L[ℝ] ℂ := equivRealProdClm.symm
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
f' : ℂ → ℂ →L[ℝ] 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 → HasFDerivAt f (f' x) x
Hi : IntegrableOn (fun z => I • ↑(f' z) 1 - ↑(f' z) I) ([[z.re, w.re]] ×ℂ [[z.im, w.im]])
e : (ℝ × ℝ) ≃L[ℝ] ℂ := ContinuousLinearEquiv.symm equivRealProdClm
he : ∀ (x y : ℝ), ↑x + ↑y * I = ↑e (x, y)
⊢ ((((∫ (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)) =
    ∫ (x : ℝ) in z.re..w.re, ∫ (y : ℝ) in z.im..w.im, I • ↑(f' (↑x + ↑y * I)) 1 - ↑(f' (↑x + ↑y * I)) I
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
f' : ℂ → ℂ →L[ℝ] 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 → HasFDerivAt f (f' x) x
Hi : IntegrableOn (fun z => I • ↑(f' z) 1 - ↑(f' z) I) ([[z.re, w.re]] ×ℂ [[z.im, w.im]])
e : (ℝ × ℝ) ≃L[ℝ] ℂ := ContinuousLinearEquiv.symm equivRealProdClm
⊢ ((((∫ (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)) =
    ∫ (x : ℝ) in z.re..w.re, ∫ (y : ℝ) in z.im..w.im, I • ↑(f' (↑x + ↑y * I)) 1 - ↑(f' (↑x + ↑y * I)) I
have he : ∀ x y : ℝ, ↑x + ↑y * I = e (x, y) := fun x y => (mk_eq_add_mul_I x y).symm
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
f' : ℂ → ℂ →L[ℝ] 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 → HasFDerivAt f (f' x) x
Hi : IntegrableOn (fun z => I • ↑(f' z) 1 - ↑(f' z) I) ([[z.re, w.re]] ×ℂ [[z.im, w.im]])
e : (ℝ × ℝ) ≃L[ℝ] ℂ := ContinuousLinearEquiv.symm equivRealProdClm
he : ∀ (x y : ℝ), ↑x + ↑y * I = ↑e (x, y)
he₁ : ↑e (1, 0) = 1
⊢ ((((∫ (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)) =
    ∫ (x : ℝ) in z.re..w.re, ∫ (y : ℝ) in z.im..w.im, I • ↑(f' (↑x + ↑y * I)) 1 - ↑(f' (↑x + ↑y * I)) I
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
f' : ℂ → ℂ →L[ℝ] 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 → HasFDerivAt f (f' x) x
Hi : IntegrableOn (fun z => I • ↑(f' z) 1 - ↑(f' z) I) ([[z.re, w.re]] ×ℂ [[z.im, w.im]])
e : (ℝ × ℝ) ≃L[ℝ] ℂ := ContinuousLinearEquiv.symm equivRealProdClm
he : ∀ (x y : ℝ), ↑x + ↑y * I = ↑e (x, y)
⊢ ((((∫ (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)) =
    ∫ (x : ℝ) in z.re..w.re, ∫ (y : ℝ) in z.im..w.im, I • ↑(f' (↑x + ↑y * I)) 1 - ↑(f' (↑x + ↑y * I)) I
have he₁ : e (1, 0) = 1 := rfl
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
f' : ℂ → ℂ →L[ℝ] 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 → HasFDerivAt f (f' x) x
Hi : IntegrableOn (fun z => I • ↑(f' z) 1 - ↑(f' z) I) ([[z.re, w.re]] ×ℂ [[z.im, w.im]])
e : (ℝ × ℝ) ≃L[ℝ] ℂ := ContinuousLinearEquiv.symm equivRealProdClm
he : ∀ (x y : ℝ), ↑x + ↑y * I = ↑e (x, y)
he₁ : ↑e (1, 0) = 1
he₂ : ↑e (0, 1) = 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)) =
    ∫ (x : ℝ) in z.re..w.re, ∫ (y : ℝ) in z.im..w.im, I • ↑(f' (↑x + ↑y * I)) 1 - ↑(f' (↑x + ↑y * I)) I
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
f' : ℂ → ℂ →L[ℝ] 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 → HasFDerivAt f (f' x) x
Hi : IntegrableOn (fun z => I • ↑(f' z) 1 - ↑(f' z) I) ([[z.re, w.re]] ×ℂ [[z.im, w.im]])
e : (ℝ × ℝ) ≃L[ℝ] ℂ := ContinuousLinearEquiv.symm equivRealProdClm
he : ∀ (x y : ℝ), ↑x + ↑y * I = ↑e (x, y)
he₁ : ↑e (1, 0) = 1
⊢ ((((∫ (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)) =
    ∫ (x : ℝ) in z.re..w.re, ∫ (y : ℝ) in z.im..w.im, I • ↑(f' (↑x + ↑y * I)) 1 - ↑(f' (↑x + ↑y * I)) I
have he₂ : e (0, 1) = I := rfl
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
f' : ℂ → ℂ →L[ℝ] 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 → HasFDerivAt f (f' x) x
Hi : IntegrableOn (fun z => I • ↑(f' z) 1 - ↑(f' z) I) ([[z.re, w.re]] ×ℂ [[z.im, w.im]])
e : (ℝ × ℝ) ≃L[ℝ] ℂ := ContinuousLinearEquiv.symm equivRealProdClm
he₁ : ↑(ContinuousLinearEquiv.symm equivRealProdClm) (1, 0) = 1
he₂ : ↑(ContinuousLinearEquiv.symm equivRealProdClm) (0, 1) = I
he : ℝ → ℝ → True
⊢ ((((∫ (x : ℝ) in z.re..w.re, f (↑(ContinuousLinearEquiv.symm equivRealProdClm) (x, z.im))) -
          ∫ (x : ℝ) in z.re..w.re, f (↑(ContinuousLinearEquiv.symm equivRealProdClm) (x, w.im))) +
        I • ∫ (y : ℝ) in z.im..w.im, f (↑(ContinuousLinearEquiv.symm equivRealProdClm) (w.re, y))) -
      I • ∫ (y : ℝ) in z.im..w.im, f (↑(ContinuousLinearEquiv.symm equivRealProdClm) (z.re, y))) =
    ∫ (x : ℝ) in z.re..w.re,
      ∫ (y : ℝ) in z.im..w.im,
        I • ↑(f' (↑(ContinuousLinearEquiv.symm equivRealProdClm) (x, y))) 1 -
          ↑(f' (↑(ContinuousLinearEquiv.symm equivRealProdClm) (x, y))) I
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
f' : ℂ → ℂ →L[ℝ] 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 → HasFDerivAt f (f' x) x
Hi : IntegrableOn (fun z => I • ↑(f' z) 1 - ↑(f' z) I) ([[z.re, w.re]] ×ℂ [[z.im, w.im]])
e : (ℝ × ℝ) ≃L[ℝ] ℂ := ContinuousLinearEquiv.symm equivRealProdClm
he : ∀ (x y : ℝ), ↑x + ↑y * I = ↑e (x, y)
he₁ : ↑e (1, 0) = 1
he₂ : ↑e (0, 1) = 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)) =
    ∫ (x : ℝ) in z.re..w.re, ∫ (y : ℝ) in z.im..w.im, I • ↑(f' (↑x + ↑y * I)) 1 - ↑(f' (↑x + ↑y * I)) I
simp only [he] at *
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
f' : ℂ → ℂ →L[ℝ] 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 → HasFDerivAt f (f' x) x
Hi : IntegrableOn (fun z => I • ↑(f' z) 1 - ↑(f' z) I) ([[z.re, w.re]] ×ℂ [[z.im, w.im]])
e : (ℝ × ℝ) ≃L[ℝ] ℂ := ContinuousLinearEquiv.symm equivRealProdClm
he₁ : ↑(ContinuousLinearEquiv.symm equivRealProdClm) (1, 0) = 1
he₂ : ↑(ContinuousLinearEquiv.symm equivRealProdClm) (0, 1) = I
he : ℝ → ℝ → True
F : ℝ × ℝ → E := f ∘ ↑e
⊢ ((((∫ (x : ℝ) in z.re..w.re, f (↑(ContinuousLinearEquiv.symm equivRealProdClm) (x, z.im))) -
          ∫ (x : ℝ) in z.re..w.re, f (↑(ContinuousLinearEquiv.symm equivRealProdClm) (x, w.im))) +
        I • ∫ (y : ℝ) in z.im..w.im, f (↑(ContinuousLinearEquiv.symm equivRealProdClm) (w.re, y))) -
      I • ∫ (y : ℝ) in z.im..w.im, f (↑(ContinuousLinearEquiv.symm equivRealProdClm) (z.re, y))) =
    ∫ (x : ℝ) in z.re..w.re,
      ∫ (y : ℝ) in z.im..w.im,
        I • ↑(f' (↑(ContinuousLinearEquiv.symm equivRealProdClm) (x, y))) 1 -
          ↑(f' (↑(ContinuousLinearEquiv.symm equivRealProdClm) (x, y))) I
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
f' : ℂ → ℂ →L[ℝ] 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 → HasFDerivAt f (f' x) x
Hi : IntegrableOn (fun z => I • ↑(f' z) 1 - ↑(f' z) I) ([[z.re, w.re]] ×ℂ [[z.im, w.im]])
e : (ℝ × ℝ) ≃L[ℝ] ℂ := ContinuousLinearEquiv.symm equivRealProdClm
he₁ : ↑(ContinuousLinearEquiv.symm equivRealProdClm) (1, 0) = 1
he₂ : ↑(ContinuousLinearEquiv.symm equivRealProdClm) (0, 1) = I
he : ℝ → ℝ → True
⊢ ((((∫ (x : ℝ) in z.re..w.re, f (↑(ContinuousLinearEquiv.symm equivRealProdClm) (x, z.im))) -
          ∫ (x : ℝ) in z.re..w.re, f (↑(ContinuousLinearEquiv.symm equivRealProdClm) (x, w.im))) +
        I • ∫ (y : ℝ) in z.im..w.im, f (↑(ContinuousLinearEquiv.symm equivRealProdClm) (w.re, y))) -
      I • ∫ (y : ℝ) in z.im..w.im, f (↑(ContinuousLinearEquiv.symm equivRealProdClm) (z.re, y))) =
    ∫ (x : ℝ) in z.re..w.re,
      ∫ (y : ℝ) in z.im..w.im,
        I • ↑(f' (↑(ContinuousLinearEquiv.symm equivRealProdClm) (x, y))) 1 -
          ↑(f' (↑(ContinuousLinearEquiv.symm equivRealProdClm) (x, y))) I
set F : ℝ × ℝ → E := f ∘ e
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
f' : ℂ → ℂ →L[ℝ] 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 → HasFDerivAt f (f' x) x
Hi : IntegrableOn (fun z => I • ↑(f' z) 1 - ↑(f' z) I) ([[z.re, w.re]] ×ℂ [[z.im, w.im]])
e : (ℝ × ℝ) ≃L[ℝ] ℂ := ContinuousLinearEquiv.symm equivRealProdClm
he₁ : ↑(ContinuousLinearEquiv.symm equivRealProdClm) (1, 0) = 1
he₂ : ↑(ContinuousLinearEquiv.symm equivRealProdClm) (0, 1) = I
he : ℝ → ℝ → True
F : ℝ × ℝ → E := f ∘ ↑e
F' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E := fun p => ContinuousLinearMap.comp (f' (↑e p)) ↑e
⊢ ((((∫ (x : ℝ) in z.re..w.re, f (↑(ContinuousLinearEquiv.symm equivRealProdClm) (x, z.im))) -
          ∫ (x : ℝ) in z.re..w.re, f (↑(ContinuousLinearEquiv.symm equivRealProdClm) (x, w.im))) +
        I • ∫ (y : ℝ) in z.im..w.im, f (↑(ContinuousLinearEquiv.symm equivRealProdClm) (w.re, y))) -
      I • ∫ (y : ℝ) in z.im..w.im, f (↑(ContinuousLinearEquiv.symm equivRealProdClm) (z.re, y))) =
    ∫ (x : ℝ) in z.re..w.re,
      ∫ (y : ℝ) in z.im..w.im,
        I • ↑(f' (↑(ContinuousLinearEquiv.symm equivRealProdClm) (x, y))) 1 -
          ↑(f' (↑(ContinuousLinearEquiv.symm equivRealProdClm) (x, y))) I
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
f' : ℂ → ℂ →L[ℝ] 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 → HasFDerivAt f (f' x) x
Hi : IntegrableOn (fun z => I • ↑(f' z) 1 - ↑(f' z) I) ([[z.re, w.re]] ×ℂ [[z.im, w.im]])
e : (ℝ × ℝ) ≃L[ℝ] ℂ := ContinuousLinearEquiv.symm equivRealProdClm
he₁ : ↑(ContinuousLinearEquiv.symm equivRealProdClm) (1, 0) = 1
he₂ : ↑(ContinuousLinearEquiv.symm equivRealProdClm) (0, 1) = I
he : ℝ → ℝ → True
F : ℝ × ℝ → E := f ∘ ↑e
⊢ ((((∫ (x : ℝ) in z.re..w.re, f (↑(ContinuousLinearEquiv.symm equivRealProdClm) (x, z.im))) -
          ∫ (x : ℝ) in z.re..w.re, f (↑(ContinuousLinearEquiv.symm equivRealProdClm) (x, w.im))) +
        I • ∫ (y : ℝ) in z.im..w.im, f (↑(ContinuousLinearEquiv.symm equivRealProdClm) (w.re, y))) -
      I • ∫ (y : ℝ) in z.im..w.im, f (↑(ContinuousLinearEquiv.symm equivRealProdClm) (z.re, y))) =
    ∫ (x : ℝ) in z.re..w.re,
      ∫ (y : ℝ) in z.im..w.im,
        I • ↑(f' (↑(ContinuousLinearEquiv.symm equivRealProdClm) (x, y))) 1 -
          ↑(f' (↑(ContinuousLinearEquiv.symm equivRealProdClm) (x, y))) I
set F' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E := fun p => (f' (e p)).comp (e : ℝ × ℝ →L[ℝ] ℂ)
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
f' : ℂ → ℂ →L[ℝ] 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 → HasFDerivAt f (f' x) x
Hi : IntegrableOn (fun z => I • ↑(f' z) 1 - ↑(f' z) I) ([[z.re, w.re]] ×ℂ [[z.im, w.im]])
e : (ℝ × ℝ) ≃L[ℝ] ℂ := ContinuousLinearEquiv.symm equivRealProdClm
he₁ : ↑(ContinuousLinearEquiv.symm equivRealProdClm) (1, 0) = 1
he₂ : ↑(ContinuousLinearEquiv.symm equivRealProdClm) (0, 1) = I
he : ℝ → ℝ → True
F : ℝ × ℝ → E := f ∘ ↑e
F' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E := fun p => ContinuousLinearMap.comp (f' (↑e p)) ↑e
hF' : ∀ (p : ℝ × ℝ), ↑(-(I • F' p)) (1, 0) + ↑(F' p) (0, 1) = -(I • ↑(f' (↑e p)) 1 - ↑(f' (↑e p)) I)
⊢ ((((∫ (x : ℝ) in z.re..w.re, f (↑(ContinuousLinearEquiv.symm equivRealProdClm) (x, z.im))) -
          ∫ (x : ℝ) in z.re..w.re, f (↑(ContinuousLinearEquiv.symm equivRealProdClm) (x, w.im))) +
        I • ∫ (y : ℝ) in z.im..w.im, f (↑(ContinuousLinearEquiv.symm equivRealProdClm) (w.re, y))) -
      I • ∫ (y : ℝ) in z.im..w.im, f (↑(ContinuousLinearEquiv.symm equivRealProdClm) (z.re, y))) =
    ∫ (x : ℝ) in z.re..w.re,
      ∫ (y : ℝ) in z.im..w.im,
        I • ↑(f' (↑(ContinuousLinearEquiv.symm equivRealProdClm) (x, y))) 1 -
          ↑(f' (↑(ContinuousLinearEquiv.symm equivRealProdClm) (x, y))) I
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
f' : ℂ → ℂ →L[ℝ] 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 → HasFDerivAt f (f' x) x
Hi : IntegrableOn (fun z => I • ↑(f' z) 1 - ↑(f' z) I) ([[z.re, w.re]] ×ℂ [[z.im, w.im]])
e : (ℝ × ℝ) ≃L[ℝ] ℂ := ContinuousLinearEquiv.symm equivRealProdClm
he₁ : ↑(ContinuousLinearEquiv.symm equivRealProdClm) (1, 0) = 1
he₂ : ↑(ContinuousLinearEquiv.symm equivRealProdClm) (0, 1) = I
he : ℝ → ℝ → True
F : ℝ × ℝ → E := f ∘ ↑e
F' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E := fun p => ContinuousLinearMap.comp (f' (↑e p)) ↑e
⊢ ((((∫ (x : ℝ) in z.re..w.re, f (↑(ContinuousLinearEquiv.symm equivRealProdClm) (x, z.im))) -
          ∫ (x : ℝ) in z.re..w.re, f (↑(ContinuousLinearEquiv.symm equivRealProdClm) (x, w.im))) +
        I • ∫ (y : ℝ) in z.im..w.im, f (↑(ContinuousLinearEquiv.symm equivRealProdClm) (w.re, y))) -
      I • ∫ (y : ℝ) in z.im..w.im, f (↑(ContinuousLinearEquiv.symm equivRealProdClm) (z.re, y))) =
    ∫ (x : ℝ) in z.re..w.re,
      ∫ (y : ℝ) in z.im..w.im,
        I • ↑(f' (↑(ContinuousLinearEquiv.symm equivRealProdClm) (x, y))) 1 -
          ↑(f' (↑(ContinuousLinearEquiv.symm equivRealProdClm) (x, y))) I
have hF' : ∀ p : ℝ × ℝ, (-(I • F' p)) (1, 0) + F' p (0, 1) = -(I • f' (e p) 1 - f' (e p) I) := by
  rintro ⟨x, y⟩
  simp only [ContinuousLinearMap.neg_apply, ContinuousLinearMap.smul_apply,
    ContinuousLinearMap.comp_apply, ContinuousLinearEquiv.coe_coe, he₁, he₂, neg_add_eq_sub,
    neg_sub]
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
f' : ℂ → ℂ →L[ℝ] 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 → HasFDerivAt f (f' x) x
Hi : IntegrableOn (fun z => I • ↑(f' z) 1 - ↑(f' z) I) ([[z.re, w.re]] ×ℂ [[z.im, w.im]])
e : (ℝ × ℝ) ≃L[ℝ] ℂ := ContinuousLinearEquiv.symm equivRealProdClm
he₁ : ↑(ContinuousLinearEquiv.symm equivRealProdClm) (1, 0) = 1
he₂ : ↑(ContinuousLinearEquiv.symm equivRealProdClm) (0, 1) = I
he : ℝ → ℝ → True
F : ℝ × ℝ → E := f ∘ ↑e
F' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E := fun p => ContinuousLinearMap.comp (f' (↑e p)) ↑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]]
⊢ ((((∫ (x : ℝ) in z.re..w.re, f (↑(ContinuousLinearEquiv.symm equivRealProdClm) (x, z.im))) -
          ∫ (x : ℝ) in z.re..w.re, f (↑(ContinuousLinearEquiv.symm equivRealProdClm) (x, w.im))) +
        I • ∫ (y : ℝ) in z.im..w.im, f (↑(ContinuousLinearEquiv.symm equivRealProdClm) (w.re, y))) -
      I • ∫ (y : ℝ) in z.im..w.im, f (↑(ContinuousLinearEquiv.symm equivRealProdClm) (z.re, y))) =
    ∫ (x : ℝ) in z.re..w.re,
      ∫ (y : ℝ) in z.im..w.im,
        I • ↑(f' (↑(ContinuousLinearEquiv.symm equivRealProdClm) (x, y))) 1 -
          ↑(f' (↑(ContinuousLinearEquiv.symm equivRealProdClm) (x, y))) I
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
f' : ℂ → ℂ →L[ℝ] 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 → HasFDerivAt f (f' x) x
Hi : IntegrableOn (fun z => I • ↑(f' z) 1 - ↑(f' z) I) ([[z.re, w.re]] ×ℂ [[z.im, w.im]])
e : (ℝ × ℝ) ≃L[ℝ] ℂ := ContinuousLinearEquiv.symm equivRealProdClm
he₁ : ↑(ContinuousLinearEquiv.symm equivRealProdClm) (1, 0) = 1
he₂ : ↑(ContinuousLinearEquiv.symm equivRealProdClm) (0, 1) = I
he : ℝ → ℝ → True
F : ℝ × ℝ → E := f ∘ ↑e
F' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E := fun p => ContinuousLinearMap.comp (f' (↑e p)) ↑e
hF' : ∀ (p : ℝ × ℝ), ↑(-(I • F' p)) (1, 0) + ↑(F' p) (0, 1) = -(I • ↑(f' (↑e p)) 1 - ↑(f' (↑e p)) I)
⊢ ((((∫ (x : ℝ) in z.re..w.re, f (↑(ContinuousLinearEquiv.symm equivRealProdClm) (x, z.im))) -
          ∫ (x : ℝ) in z.re..w.re, f (↑(ContinuousLinearEquiv.symm equivRealProdClm) (x, w.im))) +
        I • ∫ (y : ℝ) in z.im..w.im, f (↑(ContinuousLinearEquiv.symm equivRealProdClm) (w.re, y))) -
      I • ∫ (y : ℝ) in z.im..w.im, f (↑(ContinuousLinearEquiv.symm equivRealProdClm) (z.re, y))) =
    ∫ (x : ℝ) in z.re..w.re,
      ∫ (y : ℝ) in z.im..w.im,
        I • ↑(f' (↑(ContinuousLinearEquiv.symm equivRealProdClm) (x, y))) 1 -
          ↑(f' (↑(ContinuousLinearEquiv.symm equivRealProdClm) (x, y))) I
set R : Set (ℝ × ℝ) := [[z.re, w.re]] ×ˢ [[w.im, z.im]]
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
f' : ℂ → ℂ →L[ℝ] 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 → HasFDerivAt f (f' x) x
Hi : IntegrableOn (fun z => I • ↑(f' z) 1 - ↑(f' z) I) ([[z.re, w.re]] ×ℂ [[z.im, w.im]])
e : (ℝ × ℝ) ≃L[ℝ] ℂ := ContinuousLinearEquiv.symm equivRealProdClm
he₁ : ↑(ContinuousLinearEquiv.symm equivRealProdClm) (1, 0) = 1
he₂ : ↑(ContinuousLinearEquiv.symm equivRealProdClm) (0, 1) = I
he : ℝ → ℝ → True
F : ℝ × ℝ → E := f ∘ ↑e
F' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E := fun p => ContinuousLinearMap.comp (f' (↑e p)) ↑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
⊢ ((((∫ (x : ℝ) in z.re..w.re, f (↑(ContinuousLinearEquiv.symm equivRealProdClm) (x, z.im))) -
          ∫ (x : ℝ) in z.re..w.re, f (↑(ContinuousLinearEquiv.symm equivRealProdClm) (x, w.im))) +
        I • ∫ (y : ℝ) in z.im..w.im, f (↑(ContinuousLinearEquiv.symm equivRealProdClm) (w.re, y))) -
      I • ∫ (y : ℝ) in z.im..w.im, f (↑(ContinuousLinearEquiv.symm equivRealProdClm) (z.re, y))) =
    ∫ (x : ℝ) in z.re..w.re,
      ∫ (y : ℝ) in z.im..w.im,
        I • ↑(f' (↑(ContinuousLinearEquiv.symm equivRealProdClm) (x, y))) 1 -
          ↑(f' (↑(ContinuousLinearEquiv.symm equivRealProdClm) (x, y))) I
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
f' : ℂ → ℂ →L[ℝ] 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 → HasFDerivAt f (f' x) x
Hi : IntegrableOn (fun z => I • ↑(f' z) 1 - ↑(f' z) I) ([[z.re, w.re]] ×ℂ [[z.im, w.im]])
e : (ℝ × ℝ) ≃L[ℝ] ℂ := ContinuousLinearEquiv.symm equivRealProdClm
he₁ : ↑(ContinuousLinearEquiv.symm equivRealProdClm) (1, 0) = 1
he₂ : ↑(ContinuousLinearEquiv.symm equivRealProdClm) (0, 1) = I
he : ℝ → ℝ → True
F : ℝ × ℝ → E := f ∘ ↑e
F' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E := fun p => ContinuousLinearMap.comp (f' (↑e p)) ↑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]]
⊢ ((((∫ (x : ℝ) in z.re..w.re, f (↑(ContinuousLinearEquiv.symm equivRealProdClm) (x, z.im))) -
          ∫ (x : ℝ) in z.re..w.re, f (↑(ContinuousLinearEquiv.symm equivRealProdClm) (x, w.im))) +
        I • ∫ (y : ℝ) in z.im..w.im, f (↑(ContinuousLinearEquiv.symm equivRealProdClm) (w.re, y))) -
      I • ∫ (y : ℝ) in z.im..w.im, f (↑(ContinuousLinearEquiv.symm equivRealProdClm) (z.re, y))) =
    ∫ (x : ℝ) in z.re..w.re,
      ∫ (y : ℝ) in z.im..w.im,
        I • ↑(f' (↑(ContinuousLinearEquiv.symm equivRealProdClm) (x, y))) 1 -
          ↑(f' (↑(ContinuousLinearEquiv.symm equivRealProdClm) (x, y))) I
set t : Set (ℝ × ℝ) := e ⁻¹' s
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
f' : ℂ → ℂ →L[ℝ] E
z w : ℂ
s : Set ℂ
hs : Set.Countable s
Hc : ContinuousOn f ([[z.re, w.re]] ×ℂ [[w.im, z.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 → HasFDerivAt f (f' x) x
Hi : IntegrableOn (fun z => I • ↑(f' z) 1 - ↑(f' z) I) ([[z.re, w.re]] ×ℂ [[w.im, z.im]])
e : (ℝ × ℝ) ≃L[ℝ] ℂ := ContinuousLinearEquiv.symm equivRealProdClm
he₁ : ↑(ContinuousLinearEquiv.symm equivRealProdClm) (1, 0) = 1
he₂ : ↑(ContinuousLinearEquiv.symm equivRealProdClm) (0, 1) = I
he : ℝ → ℝ → True
F : ℝ × ℝ → E := f ∘ ↑e
F' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E := fun p => ContinuousLinearMap.comp (f' (↑e p)) ↑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
⊢ ((((∫ (x : ℝ) in z.re..w.re, f (↑(ContinuousLinearEquiv.symm equivRealProdClm) (x, z.im))) -
          ∫ (x : ℝ) in z.re..w.re, f (↑(ContinuousLinearEquiv.symm equivRealProdClm) (x, w.im))) +
        I • ∫ (y : ℝ) in z.im..w.im, f (↑(ContinuousLinearEquiv.symm equivRealProdClm) (w.re, y))) -
      I • ∫ (y : ℝ) in z.im..w.im, f (↑(ContinuousLinearEquiv.symm equivRealProdClm) (z.re, y))) =
    ∫ (x : ℝ) in z.re..w.re,
      ∫ (y : ℝ) in z.im..w.im,
        I • ↑(f' (↑(ContinuousLinearEquiv.symm equivRealProdClm) (x, y))) 1 -
          ↑(f' (↑(ContinuousLinearEquiv.symm equivRealProdClm) (x, y))) I
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
f' : ℂ → ℂ →L[ℝ] 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 → HasFDerivAt f (f' x) x
Hi : IntegrableOn (fun z => I • ↑(f' z) 1 - ↑(f' z) I) ([[z.re, w.re]] ×ℂ [[z.im, w.im]])
e : (ℝ × ℝ) ≃L[ℝ] ℂ := ContinuousLinearEquiv.symm equivRealProdClm
he₁ : ↑(ContinuousLinearEquiv.symm equivRealProdClm) (1, 0) = 1
he₂ : ↑(ContinuousLinearEquiv.symm equivRealProdClm) (0, 1) = I
he : ℝ → ℝ → True
F : ℝ × ℝ → E := f ∘ ↑e
F' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E := fun p => ContinuousLinearMap.comp (f' (↑e p)) ↑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
⊢ ((((∫ (x : ℝ) in z.re..w.re, f (↑(ContinuousLinearEquiv.symm equivRealProdClm) (x, z.im))) -
          ∫ (x : ℝ) in z.re..w.re, f (↑(ContinuousLinearEquiv.symm equivRealProdClm) (x, w.im))) +
        I • ∫ (y : ℝ) in z.im..w.im, f (↑(ContinuousLinearEquiv.symm equivRealProdClm) (w.re, y))) -
      I • ∫ (y : ℝ) in z.im..w.im, f (↑(ContinuousLinearEquiv.symm equivRealProdClm) (z.re, y))) =
    ∫ (x : ℝ) in z.re..w.re,
      ∫ (y : ℝ) in z.im..w.im,
        I • ↑(f' (↑(ContinuousLinearEquiv.symm equivRealProdClm) (x, y))) 1 -
          ↑(f' (↑(ContinuousLinearEquiv.symm equivRealProdClm) (x, y))) I
rw [uIcc_comm z.im] at Hc Hi
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
f' : ℂ → ℂ →L[ℝ] E
z w : ℂ
s : Set ℂ
hs : Set.Countable s
Hc : ContinuousOn f ([[z.re, w.re]] ×ℂ [[w.im, z.im]])
Hd :
  ∀ (x : ℂ), x ∈ Ioo (min z.re w.re) (max z.re w.re) ×ℂ Ioo (min w.im z.im) (max 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]])
e : (ℝ × ℝ) ≃L[ℝ] ℂ := ContinuousLinearEquiv.symm equivRealProdClm
he₁ : ↑(ContinuousLinearEquiv.symm equivRealProdClm) (1, 0) = 1
he₂ : ↑(ContinuousLinearEquiv.symm equivRealProdClm) (0, 1) = I
he : ℝ → ℝ → True
F : ℝ × ℝ → E := f ∘ ↑e
F' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E := fun p => ContinuousLinearMap.comp (f' (↑e p)) ↑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
⊢ ((((∫ (x : ℝ) in z.re..w.re, f (↑(ContinuousLinearEquiv.symm equivRealProdClm) (x, z.im))) -
          ∫ (x : ℝ) in z.re..w.re, f (↑(ContinuousLinearEquiv.symm equivRealProdClm) (x, w.im))) +
        I • ∫ (y : ℝ) in z.im..w.im, f (↑(ContinuousLinearEquiv.symm equivRealProdClm) (w.re, y))) -
      I • ∫ (y : ℝ) in z.im..w.im, f (↑(ContinuousLinearEquiv.symm equivRealProdClm) (z.re, y))) =
    ∫ (x : ℝ) in z.re..w.re,
      ∫ (y : ℝ) in z.im..w.im,
        I • ↑(f' (↑(ContinuousLinearEquiv.symm equivRealProdClm) (x, y))) 1 -
          ↑(f' (↑(ContinuousLinearEquiv.symm equivRealProdClm) (x, y))) I
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
f' : ℂ → ℂ →L[ℝ] E
z w : ℂ
s : Set ℂ
hs : Set.Countable s
Hc : ContinuousOn f ([[z.re, w.re]] ×ℂ [[w.im, z.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 → HasFDerivAt f (f' x) x
Hi : IntegrableOn (fun z => I • ↑(f' z) 1 - ↑(f' z) I) ([[z.re, w.re]] ×ℂ [[w.im, z.im]])
e : (ℝ × ℝ) ≃L[ℝ] ℂ := ContinuousLinearEquiv.symm equivRealProdClm
he₁ : ↑(ContinuousLinearEquiv.symm equivRealProdClm) (1, 0) = 1
he₂ : ↑(ContinuousLinearEquiv.symm equivRealProdClm) (0, 1) = I
he : ℝ → ℝ → True
F : ℝ × ℝ → E := f ∘ ↑e
F' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E := fun p => ContinuousLinearMap.comp (f' (↑e p)) ↑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
⊢ ((((∫ (x : ℝ) in z.re..w.re, f (↑(ContinuousLinearEquiv.symm equivRealProdClm) (x, z.im))) -
          ∫ (x : ℝ) in z.re..w.re, f (↑(ContinuousLinearEquiv.symm equivRealProdClm) (x, w.im))) +
        I • ∫ (y : ℝ) in z.im..w.im, f (↑(ContinuousLinearEquiv.symm equivRealProdClm) (w.re, y))) -
      I • ∫ (y : ℝ) in z.im..w.im, f (↑(ContinuousLinearEquiv.symm equivRealProdClm) (z.re, y))) =
    ∫ (x : ℝ) in z.re..w.re,
      ∫ (y : ℝ) in z.im..w.im,
        I • ↑(f' (↑(ContinuousLinearEquiv.symm equivRealProdClm) (x, y))) 1 -
          ↑(f' (↑(ContinuousLinearEquiv.symm equivRealProdClm) (x, y))) I
rw [min_comm z.im, max_comm z.im] at Hd
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
f' : ℂ → ℂ →L[ℝ] E
z w : ℂ
s : Set ℂ
hs : Set.Countable s
Hc : ContinuousOn f ([[z.re, w.re]] ×ℂ [[w.im, z.im]])
Hd :
  ∀ (x : ℂ), x ∈ Ioo (min z.re w.re) (max z.re w.re) ×ℂ Ioo (min w.im z.im) (max 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]])
e : (ℝ × ℝ) ≃L[ℝ] ℂ := ContinuousLinearEquiv.symm equivRealProdClm
he₁ : ↑(ContinuousLinearEquiv.symm equivRealProdClm) (1, 0) = 1
he₂ : ↑(ContinuousLinearEquiv.symm equivRealProdClm) (0, 1) = I
he : ℝ → ℝ → True
F : ℝ × ℝ → E := f ∘ ↑e
F' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E := fun p => ContinuousLinearMap.comp (f' (↑e p)) ↑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
⊢ ((((∫ (x : ℝ) in z.re..w.re, f (↑(ContinuousLinearEquiv.symm equivRealProdClm) (x, z.im))) -
          ∫ (x : ℝ) in z.re..w.re, f (↑(ContinuousLinearEquiv.symm equivRealProdClm) (x, w.im))) +
        I • ∫ (y : ℝ) in z.im..w.im, f (↑(ContinuousLinearEquiv.symm equivRealProdClm) (w.re, y))) -
      I • ∫ (y : ℝ) in z.im..w.im, f (↑(ContinuousLinearEquiv.symm equivRealProdClm) (z.re, y))) =
    ∫ (x : ℝ) in z.re..w.re,
      ∫ (y : ℝ) in z.im..w.im,
        I • ↑(f' (↑(ContinuousLinearEquiv.symm equivRealProdClm) (x, y))) 1 -
          ↑(f' (↑(ContinuousLinearEquiv.symm equivRealProdClm) (x, y))) I
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
f' : ℂ → ℂ →L[ℝ] E
z w : ℂ
s : Set ℂ
hs : Set.Countable s
Hc : ContinuousOn f ([[z.re, w.re]] ×ℂ [[w.im, z.im]])
Hd :
  ∀ (x : ℂ), x ∈ Ioo (min z.re w.re) (max z.re w.re) ×ℂ Ioo (min w.im z.im) (max 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]])
e : (ℝ × ℝ) ≃L[ℝ] ℂ := ContinuousLinearEquiv.symm equivRealProdClm
he₁ : ↑(ContinuousLinearEquiv.symm equivRealProdClm) (1, 0) = 1
he₂ : ↑(ContinuousLinearEquiv.symm equivRealProdClm) (0, 1) = I
he : ℝ → ℝ → True
F : ℝ × ℝ → E := f ∘ ↑e
F' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E := fun p => ContinuousLinearMap.comp (f' (↑e p)) ↑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
⊢ ((((∫ (x : ℝ) in z.re..w.re, f (↑(ContinuousLinearEquiv.symm equivRealProdClm) (x, z.im))) -
          ∫ (x : ℝ) in z.re..w.re, f (↑(ContinuousLinearEquiv.symm equivRealProdClm) (x, w.im))) +
        I • ∫ (y : ℝ) in z.im..w.im, f (↑(ContinuousLinearEquiv.symm equivRealProdClm) (w.re, y))) -
      I • ∫ (y : ℝ) in z.im..w.im, f (↑(ContinuousLinearEquiv.symm equivRealProdClm) (z.re, y))) =
    ∫ (x : ℝ) in z.re..w.re,
      ∫ (y : ℝ) in z.im..w.im,
        I • ↑(f' (↑(ContinuousLinearEquiv.symm equivRealProdClm) (x, y))) 1 -
          ↑(f' (↑(ContinuousLinearEquiv.symm equivRealProdClm) (x, y))) I
have hR : e ⁻¹' ([[z.re, w.re]] ×ℂ [[w.im, z.im]]) = R := rfl
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
f' : ℂ → ℂ →L[ℝ] E
z w : ℂ
s : Set ℂ
hs : Set.Countable s
Hc : ContinuousOn f ([[z.re, w.re]] ×ℂ [[w.im, z.im]])
Hd :
  ∀ (x : ℂ), x ∈ Ioo (min z.re w.re) (max z.re w.re) ×ℂ Ioo (min w.im z.im) (max 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]])
e : (ℝ × ℝ) ≃L[ℝ] ℂ := ContinuousLinearEquiv.symm equivRealProdClm
he₁ : ↑(ContinuousLinearEquiv.symm equivRealProdClm) (1, 0) = 1
he₂ : ↑(ContinuousLinearEquiv.symm equivRealProdClm) (0, 1) = I
he : ℝ → ℝ → True
F : ℝ × ℝ → E := f ∘ ↑e
F' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E := fun p => ContinuousLinearMap.comp (f' (↑e p)) ↑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
⊢ ((((∫ (x : ℝ) in z.re..w.re, f (↑(ContinuousLinearEquiv.symm equivRealProdClm) (x, z.im))) -
          ∫ (x : ℝ) in z.re..w.re, f (↑(ContinuousLinearEquiv.symm equivRealProdClm) (x, w.im))) +
        I • ∫ (y : ℝ) in z.im..w.im, f (↑(ContinuousLinearEquiv.symm equivRealProdClm) (w.re, y))) -
      I • ∫ (y : ℝ) in z.im..w.im, f (↑(ContinuousLinearEquiv.symm equivRealProdClm) (z.re, y))) =
    ∫ (x : ℝ) in z.re..w.re,
      ∫ (y : ℝ) in z.im..w.im,
        I • ↑(f' (↑(ContinuousLinearEquiv.symm equivRealProdClm) (x, y))) 1 -
          ↑(f' (↑(ContinuousLinearEquiv.symm equivRealProdClm) (x, y))) I
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
f' : ℂ → ℂ →L[ℝ] E
z w : ℂ
s : Set ℂ
hs : Set.Countable s
Hc : ContinuousOn f ([[z.re, w.re]] ×ℂ [[w.im, z.im]])
Hd :
  ∀ (x : ℂ), x ∈ Ioo (min z.re w.re) (max z.re w.re) ×ℂ Ioo (min w.im z.im) (max 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]])
e : (ℝ × ℝ) ≃L[ℝ] ℂ := ContinuousLinearEquiv.symm equivRealProdClm
he₁ : ↑(ContinuousLinearEquiv.symm equivRealProdClm) (1, 0) = 1
he₂ : ↑(ContinuousLinearEquiv.symm equivRealProdClm) (0, 1) = I
he : ℝ → ℝ → True
F : ℝ × ℝ → E := f ∘ ↑e
F' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E := fun p => ContinuousLinearMap.comp (f' (↑e p)) ↑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
⊢ ((((∫ (x : ℝ) in z.re..w.re, f (↑(ContinuousLinearEquiv.symm equivRealProdClm) (x, z.im))) -
          ∫ (x : ℝ) in z.re..w.re, f (↑(ContinuousLinearEquiv.symm equivRealProdClm) (x, w.im))) +
        I • ∫ (y : ℝ) in z.im..w.im, f (↑(ContinuousLinearEquiv.symm equivRealProdClm) (w.re, y))) -
      I • ∫ (y : ℝ) in z.im..w.im, f (↑(ContinuousLinearEquiv.symm equivRealProdClm) (z.re, y))) =
    ∫ (x : ℝ) in z.re..w.re,
      ∫ (y : ℝ) in z.im..w.im,
        I • ↑(f' (↑(ContinuousLinearEquiv.symm equivRealProdClm) (x, y))) 1 -
          ↑(f' (↑(ContinuousLinearEquiv.symm equivRealProdClm) (x, y))) I
have htc : ContinuousOn F R := Hc.comp e.continuousOn hR.ge
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
f' : ℂ → ℂ →L[ℝ] E
z w : ℂ
s : Set ℂ
hs : Set.Countable s
Hc : ContinuousOn f ([[z.re, w.re]] ×ℂ [[w.im, z.im]])
Hd :
  ∀ (x : ℂ), x ∈ Ioo (min z.re w.re) (max z.re w.re) ×ℂ Ioo (min w.im z.im) (max 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]])
e : (ℝ × ℝ) ≃L[ℝ] ℂ := ContinuousLinearEquiv.symm equivRealProdClm
he₁ : ↑(ContinuousLinearEquiv.symm equivRealProdClm) (1, 0) = 1
he₂ : ↑(ContinuousLinearEquiv.symm equivRealProdClm) (0, 1) = I
he : ℝ → ℝ → True
F : ℝ × ℝ → E := f ∘ ↑e
F' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E := fun p => ContinuousLinearMap.comp (f' (↑e p)) ↑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 : ℝ × ℝ),
    p ∈ Ioo (min z.re w.re) (max z.re w.re) ×ˢ Ioo (min w.im z.im) (max w.im z.im) \ t → HasFDerivAt F (F' p) p
⊢ ((((∫ (x : ℝ) in z.re..w.re, f (↑(ContinuousLinearEquiv.symm equivRealProdClm) (x, z.im))) -
          ∫ (x : ℝ) in z.re..w.re, f (↑(ContinuousLinearEquiv.symm equivRealProdClm) (x, w.im))) +
        I • ∫ (y : ℝ) in z.im..w.im, f (↑(ContinuousLinearEquiv.symm equivRealProdClm) (w.re, y))) -
      I • ∫ (y : ℝ) in z.im..w.im, f (↑(ContinuousLinearEquiv.symm equivRealProdClm) (z.re, y))) =
    ∫ (x : ℝ) in z.re..w.re,
      ∫ (y : ℝ) in z.im..w.im,
        I • ↑(f' (↑(ContinuousLinearEquiv.symm equivRealProdClm) (x, y))) 1 -
          ↑(f' (↑(ContinuousLinearEquiv.symm equivRealProdClm) (x, y))) I
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
f' : ℂ → ℂ →L[ℝ] E
z w : ℂ
s : Set ℂ
hs : Set.Countable s
Hc : ContinuousOn f ([[z.re, w.re]] ×ℂ [[w.im, z.im]])
Hd :
  ∀ (x : ℂ), x ∈ Ioo (min z.re w.re) (max z.re w.re) ×ℂ Ioo (min w.im z.im) (max 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]])
e : (ℝ × ℝ) ≃L[ℝ] ℂ := ContinuousLinearEquiv.symm equivRealProdClm
he₁ : ↑(ContinuousLinearEquiv.symm equivRealProdClm) (1, 0) = 1
he₂ : ↑(ContinuousLinearEquiv.symm equivRealProdClm) (0, 1) = I
he : ℝ → ℝ → True
F : ℝ × ℝ → E := f ∘ ↑e
F' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E := fun p => ContinuousLinearMap.comp (f' (↑e p)) ↑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
⊢ ((((∫ (x : ℝ) in z.re..w.re, f (↑(ContinuousLinearEquiv.symm equivRealProdClm) (x, z.im))) -
          ∫ (x : ℝ) in z.re..w.re, f (↑(ContinuousLinearEquiv.symm equivRealProdClm) (x, w.im))) +
        I • ∫ (y : ℝ) in z.im..w.im, f (↑(ContinuousLinearEquiv.symm equivRealProdClm) (w.re, y))) -
      I • ∫ (y : ℝ) in z.im..w.im, f (↑(ContinuousLinearEquiv.symm equivRealProdClm) (z.re, y))) =
    ∫ (x : ℝ) in z.re..w.re,
      ∫ (y : ℝ) in z.im..w.im,
        I • ↑(f' (↑(ContinuousLinearEquiv.symm equivRealProdClm) (x, y))) 1 -
          ↑(f' (↑(ContinuousLinearEquiv.symm equivRealProdClm) (x, y))) I
have htd :
  ∀ p ∈ Ioo (min z.re w.re) (max z.re w.re) ×ˢ Ioo (min w.im z.im) (max w.im z.im) \ t,
    HasFDerivAt F (F' p) p :=
  fun p hp => (Hd (e p) hp).comp p e.hasFDerivAt
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
f' : ℂ → ℂ →L[ℝ] E
z w : ℂ
s : Set ℂ
hs : Set.Countable s
Hc : ContinuousOn f ([[z.re, w.re]] ×ℂ [[w.im, z.im]])
Hd :
  ∀ (x : ℂ), x ∈ Ioo (min z.re w.re) (max z.re w.re) ×ℂ Ioo (min w.im z.im) (max 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]])
e : (ℝ × ℝ) ≃L[ℝ] ℂ := ContinuousLinearEquiv.symm equivRealProdClm
he₁ : ↑(ContinuousLinearEquiv.symm equivRealProdClm) (1, 0) = 1
he₂ : ↑(ContinuousLinearEquiv.symm equivRealProdClm) (0, 1) = I
he : ℝ → ℝ → True
F : ℝ × ℝ → E := f ∘ ↑e
F' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E := fun p => ContinuousLinearMap.comp (f' (↑e p)) ↑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 : ℝ × ℝ),
    p ∈ Ioo (min z.re w.re) (max z.re w.re) ×ˢ Ioo (min w.im z.im) (max w.im z.im) \ t → HasFDerivAt F (F' p) p
⊢ ((((∫ (x : ℝ) in z.re..w.re, f (↑(ContinuousLinearEquiv.symm equivRealProdClm) (x, z.im))) -
          ∫ (x : ℝ) in z.re..w.re, f (↑(ContinuousLinearEquiv.symm equivRealProdClm) (x, w.im))) +
        ∫ (x : ℝ) in w.im..z.im, -(I • f (↑(ContinuousLinearEquiv.symm equivRealProdClm) (w.re, x)))) -
      ∫ (x : ℝ) in w.im..z.im, -(I • f (↑(ContinuousLinearEquiv.symm equivRealProdClm) (z.re, x)))) =
    ∫ (x : ℝ) in z.re..w.re,
      ∫ (x_1 : ℝ) in w.im..z.im,
        ↑(-(I •
                  ContinuousLinearMap.comp (f' (↑(ContinuousLinearEquiv.symm equivRealProdClm) (x, x_1)))
                    ↑(ContinuousLinearEquiv.symm equivRealProdClm)))
            (1, 0) +
          ↑(ContinuousLinearMap.comp (f' (↑(ContinuousLinearEquiv.symm equivRealProdClm) (x, x_1)))
                ↑(ContinuousLinearEquiv.symm equivRealProdClm))
            (0, 1)
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
f' : ℂ → ℂ →L[ℝ] E
z w : ℂ
s : Set ℂ
hs : Set.Countable s
Hc : ContinuousOn f ([[z.re, w.re]] ×ℂ [[w.im, z.im]])
Hd :
  ∀ (x : ℂ), x ∈ Ioo (min z.re w.re) (max z.re w.re) ×ℂ Ioo (min w.im z.im) (max 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]])
e : (ℝ × ℝ) ≃L[ℝ] ℂ := ContinuousLinearEquiv.symm equivRealProdClm
he₁ : ↑(ContinuousLinearEquiv.symm equivRealProdClm) (1, 0) = 1
he₂ : ↑(ContinuousLinearEquiv.symm equivRealProdClm) (0, 1) = I
he : ℝ → ℝ → True
F : ℝ × ℝ → E := f ∘ ↑e
F' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E := fun p => ContinuousLinearMap.comp (f' (↑e p)) ↑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 : ℝ × ℝ),
    p ∈ Ioo (min z.re w.re) (max z.re w.re) ×ˢ Ioo (min w.im z.im) (max w.im z.im) \ t → HasFDerivAt F (F' p) p
⊢ ((((∫ (x : ℝ) in z.re..w.re, f (↑(ContinuousLinearEquiv.symm equivRealProdClm) (x, z.im))) -
          ∫ (x : ℝ) in z.re..w.re, f (↑(ContinuousLinearEquiv.symm equivRealProdClm) (x, w.im))) +
        I • ∫ (y : ℝ) in z.im..w.im, f (↑(ContinuousLinearEquiv.symm equivRealProdClm) (w.re, y))) -
      I • ∫ (y : ℝ) in z.im..w.im, f (↑(ContinuousLinearEquiv.symm equivRealProdClm) (z.re, y))) =
    ∫ (x : ℝ) in z.re..w.re,
      ∫ (y : ℝ) in z.im..w.im,
        I • ↑(f' (↑(ContinuousLinearEquiv.symm equivRealProdClm) (x, y))) 1 -
          ↑(f' (↑(ContinuousLinearEquiv.symm equivRealProdClm) (x, y))) I
simp_rw [← intervalIntegral.integral_smul, intervalIntegral.integral_symm w.im z.im, ←
  intervalIntegral.integral_neg, ← hF']
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
f' : ℂ → ℂ →L[ℝ] E
z w : ℂ
s : Set ℂ
hs : Set.Countable s
Hc : ContinuousOn f ([[z.re, w.re]] ×ℂ [[w.im, z.im]])
Hd :
  ∀ (x : ℂ), x ∈ Ioo (min z.re w.re) (max z.re w.re) ×ℂ Ioo (min w.im z.im) (max 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]])
e : (ℝ × ℝ) ≃L[ℝ] ℂ := ContinuousLinearEquiv.symm equivRealProdClm
he₁ : ↑(ContinuousLinearEquiv.symm equivRealProdClm) (1, 0) = 1
he₂ : ↑(ContinuousLinearEquiv.symm equivRealProdClm) (0, 1) = I
he : ℝ → ℝ → True
F : ℝ × ℝ → E := f ∘ ↑e
F' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E := fun p => ContinuousLinearMap.comp (f' (↑e p)) ↑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 : ℝ × ℝ),
    p ∈ Ioo (min z.re w.re) (max z.re w.re) ×ˢ Ioo (min w.im z.im) (max 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]])
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
f' : ℂ → ℂ →L[ℝ] E
z w : ℂ
s : Set ℂ
hs : Set.Countable s
Hc : ContinuousOn f ([[z.re, w.re]] ×ℂ [[w.im, z.im]])
Hd :
  ∀ (x : ℂ), x ∈ Ioo (min z.re w.re) (max z.re w.re) ×ℂ Ioo (min w.im z.im) (max 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]])
e : (ℝ × ℝ) ≃L[ℝ] ℂ := ContinuousLinearEquiv.symm equivRealProdClm
he₁ : ↑(ContinuousLinearEquiv.symm equivRealProdClm) (1, 0) = 1
he₂ : ↑(ContinuousLinearEquiv.symm equivRealProdClm) (0, 1) = I
he : ℝ → ℝ → True
F : ℝ × ℝ → E := f ∘ ↑e
F' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E := fun p => ContinuousLinearMap.comp (f' (↑e p)) ↑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 : ℝ × ℝ),
    p ∈ Ioo (min z.re w.re) (max z.re w.re) ×ˢ Ioo (min w.im z.im) (max w.im z.im) \ t → HasFDerivAt F (F' p) p
⊢ ((((∫ (x : ℝ) in z.re..w.re, f (↑(ContinuousLinearEquiv.symm equivRealProdClm) (x, z.im))) -
          ∫ (x : ℝ) in z.re..w.re, f (↑(ContinuousLinearEquiv.symm equivRealProdClm) (x, w.im))) +
        ∫ (x : ℝ) in w.im..z.im, -(I • f (↑(ContinuousLinearEquiv.symm equivRealProdClm) (w.re, x)))) -
      ∫ (x : ℝ) in w.im..z.im, -(I • f (↑(ContinuousLinearEquiv.symm equivRealProdClm) (z.re, x)))) =
    ∫ (x : ℝ) in z.re..w.re,
      ∫ (x_1 : ℝ) in w.im..z.im,
        ↑(-(I •
                  ContinuousLinearMap.comp (f' (↑(ContinuousLinearEquiv.symm equivRealProdClm) (x, x_1)))
                    ↑(ContinuousLinearEquiv.symm equivRealProdClm)))
            (1, 0) +
          ↑(ContinuousLinearMap.comp (f' (↑(ContinuousLinearEquiv.symm equivRealProdClm) (x, x_1)))
                ↑(ContinuousLinearEquiv.symm equivRealProdClm))
            (0, 1)
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
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
f' : ℂ → ℂ →L[ℝ] E
z w : ℂ
s : Set ℂ
hs : Set.Countable s
Hc : ContinuousOn f ([[z.re, w.re]] ×ℂ [[w.im, z.im]])
Hd :
  ∀ (x : ℂ), x ∈ Ioo (min z.re w.re) (max z.re w.re) ×ℂ Ioo (min w.im z.im) (max w.im z.im) \ s → HasFDerivAt f (f' x) x
Hi :
  IntegrableOn ((fun z => I • ↑(f' z) 1 - ↑(f' z) I) ∘ ↑(MeasurableEquiv.symm measurableEquivRealProd))
    (↑(MeasurableEquiv.symm measurableEquivRealProd) ⁻¹' ([[z.re, w.re]] ×ℂ [[w.im, z.im]]))
e : (ℝ × ℝ) ≃L[ℝ] ℂ := ContinuousLinearEquiv.symm equivRealProdClm
he₁ : ↑(ContinuousLinearEquiv.symm equivRealProdClm) (1, 0) = 1
he₂ : ↑(ContinuousLinearEquiv.symm equivRealProdClm) (0, 1) = I
he : ℝ → ℝ → True
F : ℝ × ℝ → E := f ∘ ↑e
F' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E := fun p => ContinuousLinearMap.comp (f' (↑e p)) ↑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 : ℝ × ℝ),
    p ∈ Ioo (min z.re w.re) (max z.re w.re) ×ˢ Ioo (min w.im z.im) (max 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]])
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
f' : ℂ → ℂ →L[ℝ] E
z w : ℂ
s : Set ℂ
hs : Set.Countable s
Hc : ContinuousOn f ([[z.re, w.re]] ×ℂ [[w.im, z.im]])
Hd :
  ∀ (x : ℂ), x ∈ Ioo (min z.re w.re) (max z.re w.re) ×ℂ Ioo (min w.im z.im) (max 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]])
e : (ℝ × ℝ) ≃L[ℝ] ℂ := ContinuousLinearEquiv.symm equivRealProdClm
he₁ : ↑(ContinuousLinearEquiv.symm equivRealProdClm) (1, 0) = 1
he₂ : ↑(ContinuousLinearEquiv.symm equivRealProdClm) (0, 1) = I
he : ℝ → ℝ → True
F : ℝ × ℝ → E := f ∘ ↑e
F' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E := fun p => ContinuousLinearMap.comp (f' (↑e p)) ↑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 : ℝ × ℝ),
    p ∈ Ioo (min z.re w.re) (max z.re w.re) ×ˢ Ioo (min w.im z.im) (max 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]])
rw [← (volume_preserving_equiv_real_prod.symm _).integrableOn_comp_preimage
  (MeasurableEquiv.measurableEmbedding _)] at Hi
no goals
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
f' : ℂ → ℂ →L[ℝ] E
z w : ℂ
s : Set ℂ
hs : Set.Countable s
Hc : ContinuousOn f ([[z.re, w.re]] ×ℂ [[w.im, z.im]])
Hd :
  ∀ (x : ℂ), x ∈ Ioo (min z.re w.re) (max z.re w.re) ×ℂ Ioo (min w.im z.im) (max w.im z.im) \ s → HasFDerivAt f (f' x) x
Hi :
  IntegrableOn ((fun z => I • ↑(f' z) 1 - ↑(f' z) I) ∘ ↑(MeasurableEquiv.symm measurableEquivRealProd))
    (↑(MeasurableEquiv.symm measurableEquivRealProd) ⁻¹' ([[z.re, w.re]] ×ℂ [[w.im, z.im]]))
e : (ℝ × ℝ) ≃L[ℝ] ℂ := ContinuousLinearEquiv.symm equivRealProdClm
he₁ : ↑(ContinuousLinearEquiv.symm equivRealProdClm) (1, 0) = 1
he₂ : ↑(ContinuousLinearEquiv.symm equivRealProdClm) (0, 1) = I
he : ℝ → ℝ → True
F : ℝ × ℝ → E := f ∘ ↑e
F' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E := fun p => ContinuousLinearMap.comp (f' (↑e p)) ↑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 : ℝ × ℝ),
    p ∈ Ioo (min z.re w.re) (max z.re w.re) ×ˢ Ioo (min w.im z.im) (max 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]])
simpa only [hF'] using Hi.neg
case mk
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
f' : ℂ → ℂ →L[ℝ] 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 → HasFDerivAt f (f' x) x
Hi : IntegrableOn (fun z => I • ↑(f' z) 1 - ↑(f' z) I) ([[z.re, w.re]] ×ℂ [[z.im, w.im]])
e : (ℝ × ℝ) ≃L[ℝ] ℂ := ContinuousLinearEquiv.symm equivRealProdClm
he₁ : ↑(ContinuousLinearEquiv.symm equivRealProdClm) (1, 0) = 1
he₂ : ↑(ContinuousLinearEquiv.symm equivRealProdClm) (0, 1) = I
he : ℝ → ℝ → True
F : ℝ × ℝ → E := f ∘ ↑e
F' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E := fun p => ContinuousLinearMap.comp (f' (↑e p)) ↑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)
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
f' : ℂ → ℂ →L[ℝ] 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 → HasFDerivAt f (f' x) x
Hi : IntegrableOn (fun z => I • ↑(f' z) 1 - ↑(f' z) I) ([[z.re, w.re]] ×ℂ [[z.im, w.im]])
e : (ℝ × ℝ) ≃L[ℝ] ℂ := ContinuousLinearEquiv.symm equivRealProdClm
he₁ : ↑(ContinuousLinearEquiv.symm equivRealProdClm) (1, 0) = 1
he₂ : ↑(ContinuousLinearEquiv.symm equivRealProdClm) (0, 1) = I
he : ℝ → ℝ → True
F : ℝ × ℝ → E := f ∘ ↑e
F' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E := fun p => ContinuousLinearMap.comp (f' (↑e p)) ↑e
⊢ ∀ (p : ℝ × ℝ), ↑(-(I • F' p)) (1, 0) + ↑(F' p) (0, 1) = -(I • ↑(f' (↑e p)) 1 - ↑(f' (↑e p)) I)
rintro ⟨x, y⟩
no goals
case mk
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
f' : ℂ → ℂ →L[ℝ] 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 → HasFDerivAt f (f' x) x
Hi : IntegrableOn (fun z => I • ↑(f' z) 1 - ↑(f' z) I) ([[z.re, w.re]] ×ℂ [[z.im, w.im]])
e : (ℝ × ℝ) ≃L[ℝ] ℂ := ContinuousLinearEquiv.symm equivRealProdClm
he₁ : ↑(ContinuousLinearEquiv.symm equivRealProdClm) (1, 0) = 1
he₂ : ↑(ContinuousLinearEquiv.symm equivRealProdClm) (0, 1) = I
he : ℝ → ℝ → True
F : ℝ × ℝ → E := f ∘ ↑e
F' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E := fun p => ContinuousLinearMap.comp (f' (↑e p)) ↑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)
simp only [ContinuousLinearMap.neg_apply, ContinuousLinearMap.smul_apply,
  ContinuousLinearMap.comp_apply, ContinuousLinearEquiv.coe_coe, he₁, he₂, neg_add_eq_sub,
  neg_sub]