awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
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[ℝ] ℂ)
x y : ℝ
⊢ HAdd.hAdd (α := E) (β := E) ((-(I • F' (x, y)) : (a : ℝ × ℝ) → E) (1, 0) : E)
      ((F' (x, y) : (a : ℝ × ℝ) → E) (0, 1) : E) =
    -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:
simp only [F', ContinuousLinearMap.neg_apply, ContinuousLinearMap.smul_apply,
      ContinuousLinearMap.comp_apply, ContinuousLinearEquiv.coe_coe, he₁, he₂, neg_add_eq_sub,
      neg_sub]

Premises used: ContinuousLinearMap.smul_apply, neg_sub, neg_add_eq_sub, ContinuousLinearMap.neg_apply, ContinuousLinearEquiv.coe_coe, ContinuousLinearMap.comp_apply
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
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[ℝ] ℂ)
⊢ ∀ (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)

Tactic:
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 [F', ContinuousLinearMap.neg_apply, ContinuousLinearMap.smul_apply,
      ContinuousLinearMap.comp_apply, ContinuousLinearEquiv.coe_coe, he₁, he₂, neg_add_eq_sub,
      neg_sub]
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
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]] ×ℂ [[w.im, z.im]])
Hd : ∀ 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.{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
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
⊢ (⇑e : (a : ℝ × ℝ) → ℂ) ⁻¹' ([[z.re, w.re]] ×ℂ [[w.im, z.im]]) = R

Tactic:
have hR : e ⁻¹' ([[z.re, w.re]] ×ℂ [[w.im, z.im]]) = R := rfl
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
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]] ×ℂ [[w.im, z.im]])
Hd : ∀ 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.{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
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
hR : (⇑e : (a : ℝ × ℝ) → ℂ) ⁻¹' ([[z.re, w.re]] ×ℂ [[w.im, z.im]]) = R
⊢ ContinuousOn F R

Tactic:
have htc : ContinuousOn F R := Hc.comp e.continuousOn hR.ge
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
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]] ×ℂ [[w.im, z.im]])
Hd : ∀ 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.{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
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
hR : (⇑e : (a : ℝ × ℝ) → ℂ) ⁻¹' ([[z.re, w.re]] ×ℂ [[w.im, z.im]]) = R
htc : ContinuousOn F R
⊢ ∀ 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

Tactic:
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
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
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]] ×ℂ [[w.im, z.im]])
Hd : ∀ 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.{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
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
hR : (⇑e : (a : ℝ × ℝ) → ℂ) ⁻¹' ([[z.re, w.re]] ×ℂ [[w.im, z.im]]) = R
htc : ContinuousOn F R
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
⊢ (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))) +
        ∫ (x : ℝ) in w.im..z.im, -(I • f ((e : (a : ℝ × ℝ) → ℂ) (w.re, x)))) -
      ∫ (x : ℝ) in w.im..z.im, -(I • f ((e : (a : ℝ × ℝ) → ℂ) (z.re, x))) =
    ∫ (x : ℝ) in z.re..w.re,
      ∫ (x_1 : ℝ) in w.im..z.im,
        HAdd.hAdd (α := E) (β := E) ((-(I • F' (x, x_1)) : (a : ℝ × ℝ) → E) (1, 0) : E)
          ((F' (x, x_1) : (a : ℝ × ℝ) → E) (0, 1) : E)

Tactic:
(integral2_divergence_prod_of_hasFDerivAt_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

Premises used: ContinuousOn.neg, Complex.im, MeasureTheory.integral2_divergence_prod_of_hasFDerivAt_off_countable, ContinuousLinearEquiv.injective, Complex.re, HasFDerivAt.const_smul, HSMul.hSMul, Eq.symm, Set.Countable.preimage, ContinuousOn.const_smul, HasFDerivAt.neg, Neg.neg, Complex.I
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
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]] ×ℂ [[w.im, z.im]])
Hd : ∀ 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.{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
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
hR : (⇑e : (a : ℝ × ℝ) → ℂ) ⁻¹' ([[z.re, w.re]] ×ℂ [[w.im, z.im]]) = R
htc : ContinuousOn F R
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
refine :
  IntegrableOn.{0, u} (ε := E) (mα := MeasureSpace.toMeasurableSpace)
    (fun (x : ℝ × ℝ) ↦
      HAdd.hAdd (α := E) (β := E) (((fun (p : ℝ × ℝ) ↦ -(I • F' p)) x : (a : ℝ × ℝ) → E) (1, 0) : E)
        ((F' x : (a : ℝ × ℝ) → E) (0, 1) : E))
    ([[z.re, w.re]] ×ˢ [[w.im, z.im]]) volume
⊢ (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))) +
        ∫ (x : ℝ) in w.im..z.im, -(I • f ((e : (a : ℝ × ℝ) → ℂ) (w.re, x)))) -
      ∫ (x : ℝ) in w.im..z.im, -(I • f ((e : (a : ℝ × ℝ) → ℂ) (z.re, x))) =
    ∫ (x : ℝ) in z.re..w.re,
      ∫ (x_1 : ℝ) in w.im..z.im,
        HAdd.hAdd (α := E) (β := E) ((-(I • F' (x, x_1)) : (a : ℝ × ℝ) → E) (1, 0) : E)
          ((F' (x, x_1) : (a : ℝ × ℝ) → E) (0, 1) : E)

Tactic:
refine (integral2_divergence_prod_of_hasFDerivAt_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

Premises used: ContinuousOn.neg, Complex.im, MeasureTheory.integral2_divergence_prod_of_hasFDerivAt_off_countable, ContinuousLinearEquiv.injective, Complex.re, HasFDerivAt.const_smul, HSMul.hSMul, Eq.symm, Set.Countable.preimage, ContinuousOn.const_smul, HasFDerivAt.neg, Neg.neg, Complex.I
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
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]] ×ℂ [[w.im, z.im]])
Hd : ∀ 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.{0, u} (α := ℝ × ℝ) (ε := E) (mα := Prod.instMeasurableSpace)
    ((fun (z : ℂ) ↦
        HSub.hSub (β := E) (HSMul.hSMul (β := E) I ((f' z : (a : ℂ) → E) 1 : E)) ((f' z : (a : ℂ) → E) I : E)) ∘
      (⇑measurableEquivRealProd.symm : (a : ℝ × ℝ) → ℂ))
    ((⇑measurableEquivRealProd.symm : (a : ℝ × ℝ) → ℂ) ⁻¹' ([[z.re, w.re]] ×ℂ [[w.im, z.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
hR : (⇑e : (a : ℝ × ℝ) → ℂ) ⁻¹' ([[z.re, w.re]] ×ℂ [[w.im, z.im]]) = R
htc : ContinuousOn F R
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
⊢ IntegrableOn.{0, u} (ε := E) (mα := MeasureSpace.toMeasurableSpace)
    (fun (x : ℝ × ℝ) ↦
      HAdd.hAdd (α := E) (β := E) (((fun (p : ℝ × ℝ) ↦ -(I • F' p)) x : (a : ℝ × ℝ) → E) (1, 0) : E)
        ((F' x : (a : ℝ × ℝ) → E) (0, 1) : E))
    ([[z.re, w.re]] ×ˢ [[w.im, z.im]]) volume

Tactic:
simpa only [hF'] using Hi.neg

Premises used: MeasureTheory.IntegrableOn.neg
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
f' : ℂ → ℂ →L[ℝ] E
z w : ℂ
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), 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
⊢ HSub.hSub (α := E) (∫ (x : ℝ) in z.re..w.re, f ((↑x : ℂ) + (↑z.im : ℂ) * I))
          (∫ (x : ℝ) in z.re..w.re, f ((↑x : ℂ) + (↑w.im : ℂ) * I)) +
        HSMul.hSMul (β := E) I (∫ (y : ℝ) in z.im..w.im, f ((↑w.re : ℂ) + (↑y : ℂ) * I)) -
      HSMul.hSMul (β := E) I (∫ (y : ℝ) in z.im..w.im, f ((↑z.re : ℂ) + (↑y : ℂ) * I)) =
    ∫ (x : ℝ) in z.re..w.re,
      ∫ (y : ℝ) in z.im..w.im,
        HSub.hSub (β := E) (HSMul.hSMul (β := E) I ((f' ((↑x : ℂ) + (↑y : ℂ) * I) : (a : ℂ) → E) 1 : E))
          ((f' ((↑x : ℂ) + (↑y : ℂ) * I) : (a : ℂ) → E) I : E)

Tactic:
integral_boundary_rect_of_hasFDerivAt_real_off_countable f f' z w ∅ countable_empty Hc
    (fun x hx => Hd x hx.1) Hi

Premises used: Complex.integral_boundary_rect_of_hasFDerivAt_real_off_countable, And.left, EmptyCollection.emptyCollection, Set.countable_empty
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
z w : ℂ
Hd : DifferentiableOn ℝ f ([[z.re, w.re]] ×ℂ [[z.im, w.im]])
Hi :
  IntegrableOn.{0, u} (ε := E) (mα := MeasureSpace.toMeasurableSpace)
    (fun (z : ℂ) ↦
      HSub.hSub (β := E) (HSMul.hSMul (β := E) I ((fderiv ℝ f z : (a : ℂ) → E) 1 : E))
        ((fderiv ℝ f z : (a : ℂ) → E) I : E))
    ([[z.re, w.re]] ×ℂ [[z.im, w.im]]) volume
x : ℂ
hx : x ∈ Ioo (min z.re w.re) (max z.re w.re) ×ℂ Ioo (min z.im w.im) (max z.im w.im) \ ∅
⊢ [[z.re, w.re]] ×ℂ [[z.im, w.im]] ∈ 𝓝 x

Tactic:
simpa only [← mem_interior_iff_mem_nhds, interior_reProdIm, uIcc, interior_Icc] using hx.1

Premises used: mem_interior_iff_mem_nhds, interior_Icc, Complex.interior_reProdIm, And.left, Set.uIcc
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → 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, DifferentiableAt ℂ f x
⊢ HSub.hSub (α := E) (∫ (x : ℝ) in z.re..w.re, f ((↑x : ℂ) + (↑z.im : ℂ) * I))
          (∫ (x : ℝ) in z.re..w.re, f ((↑x : ℂ) + (↑w.im : ℂ) * I)) +
        HSMul.hSMul (β := E) I (∫ (y : ℝ) in z.im..w.im, f ((↑w.re : ℂ) + (↑y : ℂ) * I)) -
      HSMul.hSMul (β := E) I (∫ (y : ℝ) in z.im..w.im, f ((↑z.re : ℂ) + (↑y : ℂ) * I)) =
    0

Tactic:
(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 ?_

Premises used: Real, ContinuousLinearMap.restrictScalars, HasFDerivAt.restrictScalars, Complex.integral_boundary_rect_of_hasFDerivAt_real_off_countable, fderiv, DifferentiableAt.hasFDerivAt, Complex, Eq.trans
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → 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, DifferentiableAt ℂ f x
refine_1 :
  IntegrableOn.{0, u} (ε := E) (mα := MeasureSpace.toMeasurableSpace)
    (fun (z : ℂ) ↦
      HSub.hSub (β := E)
        (HSMul.hSMul (β := E) I
          (((fun (z : ℂ) ↦ (ContinuousLinearMap.restrictScalars ℝ (fderiv ℂ f z) : ℂ →L[ℝ] E)) z : (a : ℂ) → E) 1 : E))
        (((fun (z : ℂ) ↦ (ContinuousLinearMap.restrictScalars ℝ (fderiv ℂ f z) : ℂ →L[ℝ] E)) z : (a : ℂ) → E) I : E))
    ([[z.re, w.re]] ×ℂ [[z.im, w.im]]) volume
refine_2 :
  Eq.{u + 1} (α := E)
    (∫ (x : ℝ) in z.re..w.re,
      ∫ (y : ℝ) in z.im..w.im,
        HSub.hSub (β := E)
          (HSMul.hSMul (β := E) I
            ((ContinuousLinearMap.restrictScalars ℝ (fderiv ℂ f ((↑x : ℂ) + (↑y : ℂ) * I)) : (a : ℂ) → E) 1 : E))
          ((ContinuousLinearMap.restrictScalars ℝ (fderiv ℂ f ((↑x : ℂ) + (↑y : ℂ) * I)) : (a : ℂ) → E) I : E))
    0
⊢ HSub.hSub (α := E) (∫ (x : ℝ) in z.re..w.re, f ((↑x : ℂ) + (↑z.im : ℂ) * I))
          (∫ (x : ℝ) in z.re..w.re, f ((↑x : ℂ) + (↑w.im : ℂ) * I)) +
        HSMul.hSMul (β := E) I (∫ (y : ℝ) in z.im..w.im, f ((↑w.re : ℂ) + (↑y : ℂ) * I)) -
      HSMul.hSMul (β := E) I (∫ (y : ℝ) in z.im..w.im, f ((↑z.re : ℂ) + (↑y : ℂ) * I)) =
    0

Tactic:
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 ?_

Premises used: Real, ContinuousLinearMap.restrictScalars, HasFDerivAt.restrictScalars, Complex.integral_boundary_rect_of_hasFDerivAt_real_off_countable, fderiv, DifferentiableAt.hasFDerivAt, Complex, Eq.trans
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → 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, DifferentiableAt ℂ f x
⊢ IntegrableOn.{0, u} (ε := E) (mα := MeasureSpace.toMeasurableSpace)
    (fun (z : ℂ) ↦
      HSub.hSub (β := E)
        (HSMul.hSMul (β := E) I
          (((fun (z : ℂ) ↦ (ContinuousLinearMap.restrictScalars ℝ (fderiv ℂ f z) : ℂ →L[ℝ] E)) z : (a : ℂ) → E) 1 : E))
        (((fun (z : ℂ) ↦ (ContinuousLinearMap.restrictScalars ℝ (fderiv ℂ f z) : ℂ →L[ℝ] E)) z : (a : ℂ) → E) I : E))
    ([[z.re, w.re]] ×ℂ [[z.im, w.im]]) volume

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → 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, DifferentiableAt ℂ f x
⊢ Eq.{u + 1} (α := E)
    (∫ (x : ℝ) in z.re..w.re,
      ∫ (y : ℝ) in z.im..w.im,
        HSub.hSub (β := E)
          (HSMul.hSMul (β := E) I
            ((ContinuousLinearMap.restrictScalars ℝ (fderiv ℂ f ((↑x : ℂ) + (↑y : ℂ) * I)) : (a : ℂ) → E) 1 : E))
          ((ContinuousLinearMap.restrictScalars ℝ (fderiv ℂ f ((↑x : ℂ) + (↑y : ℂ) * I)) : (a : ℂ) → E) I : E))
    0

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
z w : ℂ
Hc : ContinuousOn f ([[z.re, w.re]] ×ℂ [[z.im, w.im]])
Hd : DifferentiableOn ℂ f (Ioo (min z.re w.re) (max z.re w.re) ×ℂ Ioo (min z.im w.im) (max z.im w.im))
⊢ HSub.hSub (α := E) (∫ (x : ℝ) in z.re..w.re, f ((↑x : ℂ) + (↑z.im : ℂ) * I))
          (∫ (x : ℝ) in z.re..w.re, f ((↑x : ℂ) + (↑w.im : ℂ) * I)) +
        HSMul.hSMul (β := E) I (∫ (y : ℝ) in z.im..w.im, f ((↑w.re : ℂ) + (↑y : ℂ) * I)) -
      HSMul.hSMul (β := E) I (∫ (y : ℝ) in z.im..w.im, f ((↑z.re : ℂ) + (↑y : ℂ) * I)) =
    0

Tactic:
integral_boundary_rect_eq_zero_of_differentiable_on_off_countable f z w ∅ countable_empty Hc
    fun _x hx => Hd.differentiableAt <| (isOpen_Ioo.reProdIm isOpen_Ioo).mem_nhds hx.1

Premises used: isOpen_Ioo, IsOpen.reProdIm, DifferentiableOn.differentiableAt, And.left, Complex.integral_boundary_rect_eq_zero_of_differentiable_on_off_countable, IsOpen.mem_nhds, EmptyCollection.emptyCollection, Set.countable_empty
-- Module: Mathlib.Analysis.Complex.CauchyIntegral
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
z w : ℂ
H : DifferentiableOn ℂ f ([[z.re, w.re]] ×ℂ [[z.im, w.im]])
⊢ HSub.hSub (α := E) (∫ (x : ℝ) in z.re..w.re, f ((↑x : ℂ) + (↑z.im : ℂ) * I))
          (∫ (x : ℝ) in z.re..w.re, f ((↑x : ℂ) + (↑w.im : ℂ) * I)) +
        HSMul.hSMul (β := E) I (∫ (y : ℝ) in z.im..w.im, f ((↑w.re : ℂ) + (↑y : ℂ) * I)) -
      HSMul.hSMul (β := E) I (∫ (y : ℝ) in z.im..w.im, f ((↑z.re : ℂ) + (↑y : ℂ) * I)) =
    0

Tactic:
integral_boundary_rect_eq_zero_of_continuousOn_of_differentiableOn f z w H.continuousOn <|
    H.mono <|
      inter_subset_inter (preimage_mono Ioo_subset_Icc_self) (preimage_mono Ioo_subset_Icc_self)

Premises used: Set.Ioo_subset_Icc_self, DifferentiableOn.continuousOn, Set.inter_subset_inter, Set.preimage_mono, DifferentiableOn.mono, Complex.integral_boundary_rect_eq_zero_of_continuousOn_of_differentiableOn