awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Complex.CauchyIntegral (hypothesis)
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[ℝ] ℂ)
⊢ 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 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)
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]
-- Lean 4 proof step from Mathlib.Analysis.Complex.CauchyIntegral (hypothesis)
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
⊢ 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 hR : (⇑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
-- Lean 4 proof step from Mathlib.Analysis.Complex.CauchyIntegral (hypothesis)
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
⊢ 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 htc : ContinuousOn F R
Tactic: have htc : ContinuousOn F R := Hc.comp e.continuousOn hR.ge
-- Lean 4 proof step from Mathlib.Analysis.Complex.CauchyIntegral (hypothesis)
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
⊢ 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 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
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
-- 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]] ×ℂ [[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)
have 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
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
-- Lean 4 proof step from Mathlib.Analysis.Complex.CauchyIntegral (goal)
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
have 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
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 ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.CauchyIntegral (goal)
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
⊢ 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
have 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
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 ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.CauchyIntegral (goal)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
c : ℂ
r R : ℝ
h0 : 0 < r
hle : r ≤ R
f : ℂ → E
s : Set ℂ
hs : s.Countable
hd : ∀ z ∈ (ball c R \ closedBall c r) \ s, DifferentiableAt ℂ f z
A : Set ℂ := closedBall c R \ ball c r
hc : ContinuousOn f A
⊢ Eq.{u + 1} (α := E) (∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z) (∮ (z : ℂ) in C(c, r), (z - c)⁻¹ • f z)
have obtain : ∀ (a : ℝ) (h0 : 0 < rexp a) (hle : rexp a ≤ R)
  (hd : ∀ z ∈ (ball c R \ closedBall c (rexp a)) \ s, DifferentiableAt ℂ f z),
  let A := closedBall c R \ ball c (rexp a);
  ∀ (hc : ContinuousOn f A),
    Eq.{u + 1} (α := E) (∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z) (∮ (z : ℂ) in C(c, rexp a), (z - c)⁻¹ • f z)
Tactic: obtain ⟨a, rfl⟩ : ∃ a, Real.exp a = r := ⟨Real.log r, Real.exp_log h0⟩
Cleared hypotheses: r, h0, hle, hd, A, hc
-- Lean 4 proof step from Mathlib.Analysis.Complex.CauchyIntegral (goal)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
c : ℂ
R : ℝ
f : ℂ → E
s : Set ℂ
hs : s.Countable
a : ℝ
h0 : 0 < rexp a
hle : rexp a ≤ R
hd : ∀ z ∈ (ball c R \ closedBall c (rexp a)) \ s, DifferentiableAt ℂ f z
A : Set ℂ := closedBall c R \ ball c (rexp a)
hc : ContinuousOn f A
⊢ Eq.{u + 1} (α := E) (∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z) (∮ (z : ℂ) in C(c, rexp a), (z - c)⁻¹ • f z)
have obtain : ∀ (b : ℝ) (hle : rexp a ≤ rexp b) (hd : ∀ z ∈ (ball c (rexp b) \ closedBall c (rexp a)) \ s, DifferentiableAt ℂ f z),
  let A := closedBall c (rexp b) \ ball c (rexp a);
  ∀ (hc : ContinuousOn f A),
    Eq.{u + 1} (α := E) (∮ (z : ℂ) in C(c, rexp b), (z - c)⁻¹ • f z) (∮ (z : ℂ) in C(c, rexp a), (z - c)⁻¹ • f z)
Tactic: obtain ⟨b, rfl⟩ : ∃ b, Real.exp b = R := ⟨Real.log R, Real.exp_log (h0.trans_le hle)⟩
Cleared hypotheses: R, hle, hd, A, hc
-- Lean 4 proof step from Mathlib.Analysis.Complex.CauchyIntegral (hypothesis)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
c : ℂ
f : ℂ → E
s : Set ℂ
hs : s.Countable
a : ℝ
h0 : 0 < rexp a
b : ℝ
hle : rexp a ≤ rexp b
hd : ∀ z ∈ (ball c (rexp b) \ closedBall c (rexp a)) \ s, DifferentiableAt ℂ f z
A : Set ℂ := closedBall c (rexp b) \ ball c (rexp a)
hc : ContinuousOn f A
⊢ Eq.{u + 1} (α := E) (∮ (z : ℂ) in C(c, rexp b), (z - c)⁻¹ • f z) (∮ (z : ℂ) in C(c, rexp a), (z - c)⁻¹ • f z)
have hle₁ : a ≤ b
Tactic: rw [Real.exp_le_exp] at hle
Cleared hypotheses: hle, hd, A, hc
-- Lean 4 proof step from Mathlib.Analysis.Complex.CauchyIntegral (goal)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
c : ℂ
f : ℂ → E
s : Set ℂ
hs : s.Countable
a : ℝ
h0 : 0 < rexp a
b : ℝ
hle : a ≤ b
hd : ∀ z ∈ (ball c (rexp b) \ closedBall c (rexp a)) \ s, DifferentiableAt ℂ f z
A : Set ℂ := closedBall c (rexp b) \ ball c (rexp a)
hc : ContinuousOn f A
⊢ Eq.{u + 1} (α := E) (∮ (z : ℂ) in C(c, rexp b), (z - c)⁻¹ • f z) (∮ (z : ℂ) in C(c, rexp a), (z - c)⁻¹ • f z)
have θ : Eq.{u + 1} (α := E) (∫ (θ : ℝ) in 0..2 * π, I • f (circleMap c (rexp b) θ))
  (∫ (θ : ℝ) in 0..2 * π, I • f (circleMap c (rexp a) θ))
Tactic: suffices
    (∫ θ in 0..2 * π, I • f (circleMap c (Real.exp b) θ)) =
      ∫ θ in 0..2 * π, I • f (circleMap c (Real.exp a) θ) by
    simpa only [circleIntegral, add_sub_cancel_left, ofReal_exp, ← exp_add, smul_smul, ←
      div_eq_mul_inv, mul_div_cancel_left₀ _ (circleMap_ne_center (Real.exp_pos _).ne'),
      circleMap_sub_center, deriv_circleMap]
-- Lean 4 proof step from Mathlib.Analysis.Complex.CauchyIntegral (hypothesis)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
c : ℂ
f : ℂ → E
s : Set ℂ
hs : s.Countable
a : ℝ
h0 : 0 < rexp a
b : ℝ
hle : a ≤ b
hd : ∀ z ∈ (ball c (rexp b) \ closedBall c (rexp a)) \ s, DifferentiableAt ℂ f z
A : Set ℂ := closedBall c (rexp b) \ ball c (rexp a)
hc : ContinuousOn f A
R : Set ℂ := [[a, b]] ×ℂ [[0, 2 * π]]
g : ℂ → ℂ := fun (x : ℂ) ↦ c + cexp x
⊢ Eq.{u + 1} (α := E) (∫ (θ : ℝ) in 0..2 * π, I • f (circleMap c (rexp b) θ))
    (∫ (θ : ℝ) in 0..2 * π, I • f (circleMap c (rexp a) θ))
have hdg : Differentiable ℂ g
Tactic: have hdg : Differentiable ℂ g := differentiable_exp.const_add _
-- Lean 4 proof step from Mathlib.Analysis.Complex.CauchyIntegral (hypothesis)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
c : ℂ
f : ℂ → E
s : Set ℂ
hs : s.Countable
a : ℝ
h0 : 0 < rexp a
b : ℝ
hle : a ≤ b
hd : ∀ z ∈ (ball c (rexp b) \ closedBall c (rexp a)) \ s, DifferentiableAt ℂ f z
A : Set ℂ := closedBall c (rexp b) \ ball c (rexp a)
hc : ContinuousOn f A
R : Set ℂ := [[a, b]] ×ℂ [[0, 2 * π]]
g : ℂ → ℂ := fun (x : ℂ) ↦ c + cexp x
hdg : Differentiable ℂ g
⊢ Eq.{u + 1} (α := E) (∫ (θ : ℝ) in 0..2 * π, I • f (circleMap c (rexp b) θ))
    (∫ (θ : ℝ) in 0..2 * π, I • f (circleMap c (rexp a) θ))
have hs₁ : (g ⁻¹' s).Countable
Tactic: replace hs : (g ⁻¹' s).Countable := (hs.preimage (add_right_injective c)).preimage_cexp
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Analysis.Complex.CauchyIntegral (hypothesis)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
c : ℂ
f : ℂ → E
s : Set ℂ
a : ℝ
h0 : 0 < rexp a
b : ℝ
hle : a ≤ b
hd : ∀ z ∈ (ball c (rexp b) \ closedBall c (rexp a)) \ s, DifferentiableAt ℂ f z
A : Set ℂ := closedBall c (rexp b) \ ball c (rexp a)
hc : ContinuousOn f A
R : Set ℂ := [[a, b]] ×ℂ [[0, 2 * π]]
g : ℂ → ℂ := fun (x : ℂ) ↦ c + cexp x
hdg : Differentiable ℂ g
hs : (g ⁻¹' s).Countable
⊢ Eq.{u + 1} (α := E) (∫ (θ : ℝ) in 0..2 * π, I • f (circleMap c (rexp b) θ))
    (∫ (θ : ℝ) in 0..2 * π, I • f (circleMap c (rexp a) θ))
have h_maps : MapsTo g R A
Tactic: have h_maps : MapsTo g R A := by
    rintro z ⟨h, -⟩; simpa [g, A, dist_eq, norm_exp, hle] using h.symm
-- Lean 4 proof step from Mathlib.Analysis.Complex.CauchyIntegral (hypothesis)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
c : ℂ
f : ℂ → E
s : Set ℂ
a : ℝ
h0 : 0 < rexp a
b : ℝ
hle : a ≤ b
hd : ∀ z ∈ (ball c (rexp b) \ closedBall c (rexp a)) \ s, DifferentiableAt ℂ f z
A : Set ℂ := closedBall c (rexp b) \ ball c (rexp a)
hc : ContinuousOn f A
R : Set ℂ := [[a, b]] ×ℂ [[0, 2 * π]]
g : ℂ → ℂ := fun (x : ℂ) ↦ c + cexp x
hdg : Differentiable ℂ g
hs : (g ⁻¹' s).Countable
h_maps : MapsTo g R A
⊢ Eq.{u + 1} (α := E) (∫ (θ : ℝ) in 0..2 * π, I • f (circleMap c (rexp b) θ))
    (∫ (θ : ℝ) in 0..2 * π, I • f (circleMap c (rexp a) θ))
have hc₁ : ContinuousOn (f ∘ g) R
Tactic: replace hc : ContinuousOn (f ∘ g) R := hc.comp hdg.continuous.continuousOn h_maps
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.Analysis.Complex.CauchyIntegral (goal)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
c : ℂ
f : ℂ → E
s : Set ℂ
a : ℝ
h0 : 0 < rexp a
b : ℝ
hle : a ≤ b
hd : ∀ z ∈ (ball c (rexp b) \ closedBall c (rexp a)) \ s, DifferentiableAt ℂ f z
A : Set ℂ := closedBall c (rexp b) \ ball c (rexp a)
R : Set ℂ := [[a, b]] ×ℂ [[0, 2 * π]]
g : ℂ → ℂ := fun (x : ℂ) ↦ c + cexp x
hdg : Differentiable ℂ g
hs : (g ⁻¹' s).Countable
h_maps : MapsTo g R A
hc : ContinuousOn (f ∘ g) R
⊢ ∀ z ∈ Ioo (min a b) (max a b) ×ℂ Ioo (min 0 (2 * π)) (max 0 (2 * π)) \ g ⁻¹' s, DifferentiableAt ℂ (f ∘ g) z
have refine : ∀ (z : ℂ) (hz : z ∈ Ioo (min a b) (max a b) ×ℂ Ioo (min 0 (2 * π)) (max 0 (2 * π)) \ g ⁻¹' s),
  g z ∈ ball c (rexp b) \ closedBall c (rexp a)
Tactic: refine fun z hz => (hd (g z) ⟨?_, hz.2⟩).comp z (hdg _)
-- Lean 4 proof step from Mathlib.Analysis.Complex.CauchyIntegral (hypothesis)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
c : ℂ
f : ℂ → E
s : Set ℂ
a : ℝ
h0 : 0 < rexp a
b : ℝ
hle : a ≤ b
hd : ∀ z ∈ (ball c (rexp b) \ closedBall c (rexp a)) \ s, DifferentiableAt ℂ f z
A : Set ℂ := closedBall c (rexp b) \ ball c (rexp a)
R : Set ℂ := [[a, b]] ×ℂ [[0, 2 * π]]
g : ℂ → ℂ := fun (x : ℂ) ↦ c + cexp x
hdg : Differentiable ℂ g
hs : (g ⁻¹' s).Countable
h_maps : MapsTo g R A
hc : ContinuousOn (f ∘ g) R
⊢ Eq.{u + 1} (α := E) (∫ (θ : ℝ) in 0..2 * π, I • f (circleMap c (rexp b) θ))
    (∫ (θ : ℝ) in 0..2 * π, I • f (circleMap c (rexp a) θ))
have hd₁ : ∀ z ∈ Ioo (min a b) (max a b) ×ℂ Ioo (min 0 (2 * π)) (max 0 (2 * π)) \ g ⁻¹' s, DifferentiableAt ℂ (f ∘ g) z
Tactic: replace hd : ∀ z ∈ Ioo (min a b) (max a b) ×ℂ Ioo (min 0 (2 * π)) (max 0 (2 * π)) \ g ⁻¹' s,
      DifferentiableAt ℂ (f ∘ g) z := by
    refine fun z hz => (hd (g z) ⟨?_, hz.2⟩).comp z (hdg _)
    simpa [g, dist_eq, norm_exp, hle, and_comm] using hz.1.1
Cleared hypotheses: hd
-- Lean 4 proof step from Mathlib.Analysis.Complex.CauchyIntegral (goal)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → E
y : E
s : Set ℂ
hs : s.Countable
hc : ContinuousOn f (closedBall c R \ {c})
hd : ∀ z ∈ (ball c R \ {c}) \ s, DifferentiableAt ℂ f z
hy : Tendsto f (𝓝[≠] c) (𝓝 y)
⊢ ∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z = (2 * (↑π : ℂ) * I) • y
have rw : ‖(∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z) - (2 * (↑π : ℂ) * I) • y‖ ≤ 0
Tactic: rw [← sub_eq_zero, ← norm_le_zero_iff]
-- Lean 4 proof step from Mathlib.Analysis.Complex.CauchyIntegral (goal)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → E
y : E
s : Set ℂ
hs : s.Countable
hc : ContinuousOn f (closedBall c R \ {c})
hd : ∀ z ∈ (ball c R \ {c}) \ s, DifferentiableAt ℂ f z
hy : Tendsto f (𝓝[≠] c) (𝓝 y)
⊢ ‖(∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z) - (2 * (↑π : ℂ) * I) • y‖ ≤ 0
have refine : ∀ (ε : ℝ) (ε0 : 0 < ε), ‖(∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z) - (2 * (↑π : ℂ) * I) • y‖ ≤ ε
Tactic: refine le_of_forall_gt_imp_ge_of_dense fun ε ε0 => ?_