awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Complex.HasPrimitives
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
c : ℂ
r : ℝ
f : ℂ → E
inst_2 : CompleteSpace E
f_cont : ContinuousOn f (ball c r)
z : ℂ
hz : z ∈ ball c r
⊢ Filter.Tendsto f (𝓝 z) (𝓝 (f z))

Tactic:
f_cont.continuousAt <| _root_.mem_nhds_iff.mpr ⟨ball c r, le_refl _, isOpen_ball, hz⟩

Premises used: Iff.mpr, le_refl, ContinuousAt, mem_nhds_iff, Metric.ball, Metric.isOpen_ball, And.intro, Exists.intro, ContinuousOn.continuousAt
-- Module: Mathlib.Analysis.Complex.HasPrimitives
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
c : ℂ
r : ℝ
f : ℂ → E
inst_2 : CompleteSpace E
f_cont : ContinuousOn f (ball c r)
z : ℂ
hz : z ∈ ball c r
⊢ Filter.Tendsto f (𝓝 z) (𝓝 (f z))

Tactic:
exact f_cont.continuousAt <| _root_.mem_nhds_iff.mpr ⟨ball c r, le_refl _, isOpen_ball, hz⟩

Premises used: Iff.mpr, le_refl, mem_nhds_iff, Metric.ball, Metric.isOpen_ball, And.intro, Exists.intro, ContinuousOn.continuousAt
-- Module: Mathlib.Analysis.Complex.HasPrimitives
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
c : ℂ
r : ℝ
f : ℂ → E
inst_2 : CompleteSpace E
f_cont : ContinuousOn f (ball c r)
z : ℂ
hz : z ∈ ball c r
⊢ Asymptotics.IsLittleO.{0, u_1, 0} (E := E) (F := ℝ) (𝓝 z) (fun (w : ℂ) ↦ f w - f z) fun (x : ℂ) ↦ 1

Tactic:
have : (fun w ↦ f w - f z) =o[𝓝 z] fun _ ↦ (1 : ℝ) := by
    rw [Asymptotics.isLittleO_one_iff, tendsto_sub_nhds_zero_iff]
    exact f_cont.continuousAt <| _root_.mem_nhds_iff.mpr ⟨ball c r, le_refl _, isOpen_ball, hz⟩
-- Module: Mathlib.Analysis.Complex.HasPrimitives
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
c : ℂ
r : ℝ
f : ℂ → E
inst_2 : CompleteSpace E
f_cont : ContinuousOn f (ball c r)
z : ℂ
hz : z ∈ ball c r
this : Asymptotics.IsLittleO.{0, u_1, 0} (E := E) (F := ℝ) (𝓝 z) (fun (w : ℂ) ↦ f w - f z) fun (x : ℂ) ↦ 1
rw :
  ∀
    (this :
      ∀ ⦃c : ℝ⦄,
        0 < c → Asymptotics.IsBigOWith.{0, u_1, 0} (E := E) (F := ℝ) c (𝓝 z) (fun (w : ℂ) ↦ f w - f z) fun (x : ℂ) ↦ 1)
    ⦃c : ℝ⦄,
    0 < c →
      Asymptotics.IsBigOWith.{0, u_1, 0} (E := E) (F := ℂ) c (𝓝 z)
        (fun (w : ℂ) ↦ ∫ (y : ℝ) in z.im..w.im, f ((↑w.re : ℂ) + (↑y : ℂ) * I) - f z) fun (w : ℂ) ↦ w - z
⊢ Asymptotics.IsLittleO.{0, u_1, 0} (E := E) (F := ℂ) (𝓝 z)
    (fun (w : ℂ) ↦ ∫ (y : ℝ) in z.im..w.im, f ((↑w.re : ℂ) + (↑y : ℂ) * I) - f z) fun (w : ℂ) ↦ w - z

Tactic:
rw [Asymptotics.IsLittleO] at this ⊢

Premises used: Asymptotics.IsLittleO
-- Module: Mathlib.Analysis.Complex.HasPrimitives
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
c : ℂ
r : ℝ
f : ℂ → E
inst_2 : CompleteSpace E
f_cont : ContinuousOn f (ball c r)
z : ℂ
hz : z ∈ ball c r
this :
  ∀ ⦃c : ℝ⦄,
    0 < c → Asymptotics.IsBigOWith.{0, u_1, 0} (E := E) (F := ℝ) c (𝓝 z) (fun (w : ℂ) ↦ f w - f z) fun (x : ℂ) ↦ 1
ε : ℝ
ε_pos : 0 < ε
⊢ Asymptotics.IsBigOWith.{0, u_1, 0} (E := E) (F := ℝ) ε (𝓝 z) (fun (w : ℂ) ↦ f w - f z) fun (x : ℂ) ↦ 1

Tactic:
replace := this ε_pos
-- Module: Mathlib.Analysis.Complex.HasPrimitives
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
c : ℂ
r : ℝ
f : ℂ → E
inst_2 : CompleteSpace E
f_cont : ContinuousOn f (ball c r)
z : ℂ
hz : z ∈ ball c r
ε : ℝ
ε_pos : 0 < ε
this : Asymptotics.IsBigOWith.{0, u_1, 0} (E := E) (F := ℝ) ε (𝓝 z) (fun (w : ℂ) ↦ f w - f z) fun (x : ℂ) ↦ 1
simp :
  ∀ (this : ∀ᶠ (x : ℂ) in 𝓝 z, ‖f x - f z‖ ≤ ε),
    ∀ᶠ (x : ℂ) in 𝓝 z, norm.{u_1} (E := E) (∫ (y : ℝ) in z.im..x.im, f ((↑x.re : ℂ) + (↑y : ℂ) * I) - f z) ≤ ε * ‖x - z‖
⊢ Asymptotics.IsBigOWith.{0, u_1, 0} (E := E) (F := ℂ) ε (𝓝 z)
    (fun (w : ℂ) ↦ ∫ (y : ℝ) in z.im..w.im, f ((↑w.re : ℂ) + (↑y : ℂ) * I) - f z) fun (w : ℂ) ↦ w - z

Tactic:
simp only [Asymptotics.isBigOWith_iff, norm_one, mul_one] at this ⊢

Premises used: NormOneClass.norm_one, Asymptotics.isBigOWith_iff, mul_one
-- Module: Mathlib.Analysis.Complex.HasPrimitives
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
c : ℂ
r : ℝ
f : ℂ → E
inst_2 : CompleteSpace E
f_cont : ContinuousOn f (ball c r)
z : ℂ
hz : z ∈ ball c r
ε : ℝ
ε_pos : 0 < ε
this : ∀ᶠ (x : ℂ) in 𝓝 z, ‖f x - f z‖ ≤ ε
rw :
  ∀ (this : ∃ (i : ℝ), 0 < i ∧ ∀ ⦃x : ℂ⦄, x ∈ closedBall z i → ‖f x - f z‖ ≤ ε),
    ∃ (i : ℝ), 0 < i ∧ ∀ ⦃x : ℂ⦄, x ∈ closedBall z i → ∀ y ∈ Ι z.im x.im, ‖f ((↑x.re : ℂ) + (↑y : ℂ) * I) - f z‖ ≤ ε
⊢ ∀ᶠ (w : ℂ) in 𝓝 z, ∀ y ∈ Ι z.im w.im, ‖f ((↑w.re : ℂ) + (↑y : ℂ) * I) - f z‖ ≤ ε

Tactic:
rw [Metric.nhds_basis_closedBall.eventually_iff] at this ⊢

Premises used: Filter.HasBasis.eventually_iff, Metric.nhds_basis_closedBall
-- Module: Mathlib.Analysis.Complex.HasPrimitives
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
c : ℂ
r : ℝ
f : ℂ → E
inst_2 : CompleteSpace E
f_cont : ContinuousOn f (ball c r)
z : ℂ
hz : z ∈ ball c r
ε : ℝ
ε_pos : 0 < ε
this : ∃ (i : ℝ), 0 < i ∧ ∀ ⦃x : ℂ⦄, x ∈ closedBall z i → ‖f x - f z‖ ≤ ε
obtain :
  ∀ (i : ℝ) (i_pos : 0 < i) (hi : ∀ ⦃x : ℂ⦄, x ∈ closedBall z i → ‖f x - f z‖ ≤ ε),
    ∃ (i : ℝ), 0 < i ∧ ∀ ⦃x : ℂ⦄, x ∈ closedBall z i → ∀ y ∈ Ι z.im x.im, ‖f ((↑x.re : ℂ) + (↑y : ℂ) * I) - f z‖ ≤ ε
⊢ ∃ (i : ℝ), 0 < i ∧ ∀ ⦃x : ℂ⦄, x ∈ closedBall z i → ∀ y ∈ Ι z.im x.im, ‖f ((↑x.re : ℂ) + (↑y : ℂ) * I) - f z‖ ≤ ε

Tactic:
obtain ⟨i, i_pos, hi⟩ := this
-- Module: Mathlib.Analysis.Complex.HasPrimitives
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
c : ℂ
r : ℝ
f : ℂ → E
inst_2 : CompleteSpace E
f_cont : ContinuousOn f (ball c r)
z : ℂ
hz : z ∈ ball c r
ε : ℝ
ε_pos : 0 < ε
i : ℝ
i_pos : 0 < i
hi : ∀ ⦃x : ℂ⦄, x ∈ closedBall z i → ‖f x - f z‖ ≤ ε
⊢ ∃ (i : ℝ), 0 < i ∧ ∀ ⦃x : ℂ⦄, x ∈ closedBall z i → ∀ y ∈ Ι z.im x.im, ‖f ((↑x.re : ℂ) + (↑y : ℂ) * I) - f z‖ ≤ ε

Tactic:
⟨i, i_pos, fun w w_in_ball y y_in_I ↦ hi (mem_closedBall_aux w_in_ball y_in_I)⟩

Premises used: _private.0.Complex.mem_closedBall_aux, And.intro, Exists.intro
-- Module: Mathlib.Analysis.Complex.HasPrimitives
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
c : ℂ
r : ℝ
f : ℂ → E
inst_2 : CompleteSpace E
f_cont : ContinuousOn f (ball c r)
z : ℂ
hz : z ∈ ball c r
ε : ℝ
ε_pos : 0 < ε
i : ℝ
i_pos : 0 < i
hi : ∀ ⦃x : ℂ⦄, x ∈ closedBall z i → ‖f x - f z‖ ≤ ε
⊢ ∃ (i : ℝ), 0 < i ∧ ∀ ⦃x : ℂ⦄, x ∈ closedBall z i → ∀ y ∈ Ι z.im x.im, ‖f ((↑x.re : ℂ) + (↑y : ℂ) * I) - f z‖ ≤ ε

Tactic:
exact ⟨i, i_pos, fun w w_in_ball y y_in_I ↦ hi (mem_closedBall_aux w_in_ball y_in_I)⟩
-- Module: Mathlib.Analysis.Complex.HasPrimitives
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
c : ℂ
r : ℝ
f : ℂ → E
inst_2 : CompleteSpace E
f_cont : ContinuousOn f (ball c r)
z : ℂ
hz : z ∈ ball c r
ε : ℝ
ε_pos : 0 < ε
this : ∀ᶠ (x : ℂ) in 𝓝 z, ‖f x - f z‖ ≤ ε
⊢ ∀ᶠ (w : ℂ) in 𝓝 z, ∀ y ∈ Ι z.im w.im, ‖f ((↑w.re : ℂ) + (↑y : ℂ) * I) - f z‖ ≤ ε

Tactic:
replace this : ∀ᶠ w in 𝓝 z, ∀ y ∈ Ι z.im w.im, ‖f (w.re + y * I) - f z‖ ≤ ε := by
    rw [Metric.nhds_basis_closedBall.eventually_iff] at this ⊢
    obtain ⟨i, i_pos, hi⟩ := this
    exact ⟨i, i_pos, fun w w_in_ball y y_in_I ↦ hi (mem_closedBall_aux w_in_ball y_in_I)⟩
-- Module: Mathlib.Analysis.Complex.HasPrimitives
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
c : ℂ
r : ℝ
f : ℂ → E
inst_2 : CompleteSpace E
f_cont : ContinuousOn f (ball c r)
z : ℂ
hz : z ∈ ball c r
ε : ℝ
ε_pos : 0 < ε
this : ∀ᶠ (w : ℂ) in 𝓝 z, ∀ y ∈ Ι z.im w.im, ‖f ((↑w.re : ℂ) + (↑y : ℂ) * I) - f z‖ ≤ ε
h :
  ∀ (w : ℂ) (hw : ∀ y ∈ Ι z.im w.im, ‖f ((↑w.re : ℂ) + (↑y : ℂ) * I) - f z‖ ≤ ε),
    norm.{u_1} (E := E) (∫ (y : ℝ) in z.im..w.im, f ((↑w.re : ℂ) + (↑y : ℂ) * I) - f z) ≤ ε * ‖w - z‖
⊢ ∀ᶠ (x : ℂ) in 𝓝 z, norm.{u_1} (E := E) (∫ (y : ℝ) in z.im..x.im, f ((↑x.re : ℂ) + (↑y : ℂ) * I) - f z) ≤ ε * ‖x - z‖

Tactic:
filter_upwards [this] with w hw
-- Module: Mathlib.Analysis.Complex.HasPrimitives
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
c : ℂ
r : ℝ
f : ℂ → E
inst_2 : CompleteSpace E
f_cont : ContinuousOn f (ball c r)
z : ℂ
hz : z ∈ ball c r
ε : ℝ
ε_pos : 0 < ε
this : ∀ᶠ (w : ℂ) in 𝓝 z, ∀ y ∈ Ι z.im w.im, ‖f ((↑w.re : ℂ) + (↑y : ℂ) * I) - f z‖ ≤ ε
w : ℂ
hw : ∀ y ∈ Ι z.im w.im, ‖f ((↑w.re : ℂ) + (↑y : ℂ) * I) - f z‖ ≤ ε
⊢ norm.{u_1} (E := E) (∫ (x : ℝ) in z.im..w.im, f ((↑w.re : ℂ) + (↑x : ℂ) * I) - f z) ≤ ε * ‖w.im - z.im‖

Tactic:
intervalIntegral.norm_integral_le_of_norm_le_const hw

Premises used: intervalIntegral.norm_integral_le_of_norm_le_const
-- Module: Mathlib.Analysis.Complex.HasPrimitives
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
c : ℂ
r : ℝ
f : ℂ → E
inst_2 : CompleteSpace E
f_cont : ContinuousOn f (ball c r)
z : ℂ
hz : z ∈ ball c r
ε : ℝ
ε_pos : 0 < ε
this : ∀ᶠ (w : ℂ) in 𝓝 z, ∀ y ∈ Ι z.im w.im, ‖f ((↑w.re : ℂ) + (↑y : ℂ) * I) - f z‖ ≤ ε
w : ℂ
hw : ∀ y ∈ Ι z.im w.im, ‖f ((↑w.re : ℂ) + (↑y : ℂ) * I) - f z‖ ≤ ε
⊢ ε * ‖w.im - z.im‖ = ε * ‖(w - z).im‖

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.HasPrimitives
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
c : ℂ
r : ℝ
f : ℂ → E
inst_2 : CompleteSpace E
f_cont : ContinuousOn f (ball c r)
z : ℂ
hz : z ∈ ball c r
ε : ℝ
ε_pos : 0 < ε
this : ∀ᶠ (w : ℂ) in 𝓝 z, ∀ y ∈ Ι z.im w.im, ‖f ((↑w.re : ℂ) + (↑y : ℂ) * I) - f z‖ ≤ ε
w : ℂ
hw : ∀ y ∈ Ι z.im w.im, ‖f ((↑w.re : ℂ) + (↑y : ℂ) * I) - f z‖ ≤ ε
⊢ ε * ‖(w - z).im‖ ≤ ε * ‖w - z‖

Tactic:
(mul_le_mul_iff_of_pos_left ε_pos).mpr (abs_im_le_norm _)

Premises used: Iff.mpr, Complex.abs_im_le_norm, mul_le_mul_iff_of_pos_left
-- Module: Mathlib.Analysis.Complex.HasPrimitives
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
c : ℂ
r : ℝ
f : ℂ → E
inst_2 : CompleteSpace E
f_cont : ContinuousOn f (ball c r)
z : ℂ
hz : z ∈ ball c r
ε : ℝ
ε_pos : 0 < ε
this : ∀ᶠ (w : ℂ) in 𝓝 z, ∀ y ∈ Ι z.im w.im, ‖f ((↑w.re : ℂ) + (↑y : ℂ) * I) - f z‖ ≤ ε
w : ℂ
hw : ∀ y ∈ Ι z.im w.im, ‖f ((↑w.re : ℂ) + (↑y : ℂ) * I) - f z‖ ≤ ε
_ : ε * ‖w.im - z.im‖ = ε * ‖(w - z).im‖
⊢ norm.{u_1} (E := E) (∫ (y : ℝ) in z.im..w.im, f ((↑w.re : ℂ) + (↑y : ℂ) * I) - f z) ≤ ε * ‖w - z‖

Tactic:
calc
    _ ≤ ε * ‖w.im - z.im‖ := intervalIntegral.norm_integral_le_of_norm_le_const hw
    _ = ε * ‖(w - z).im‖ := by simp
    _ ≤ ε * ‖w - z‖ := (mul_le_mul_iff_of_pos_left ε_pos).mpr (abs_im_le_norm _)

Premises used: Iff.mpr, Complex.im, HSub.hSub, Complex.abs_im_le_norm, mul_le_mul_iff_of_pos_left, intervalIntegral.norm_integral_le_of_norm_le_const
-- Module: Mathlib.Analysis.Complex.HasPrimitives
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
c : ℂ
r : ℝ
f : ℂ → E
inst_2 : CompleteSpace E
f_cont : ContinuousOn f (ball c r)
z : ℂ
hz : z ∈ ball c r
h : IsConservativeOn f (ball c r)
rw :
  Asymptotics.IsLittleO.{0, u_1, 0} (E := E) (F := ℂ) (𝓝 z)
    (fun (x' : ℂ) ↦ c.wedgeIntegral x' f - c.wedgeIntegral z f - (x' - z) • f z) fun (x' : ℂ) ↦ x' - z
⊢ HasDerivAt (fun (w : ℂ) ↦ c.wedgeIntegral w f) (f z) z

Tactic:
rw [hasDerivAt_iff_isLittleO]

Premises used: hasDerivAt_iff_isLittleO
-- Module: Mathlib.Analysis.Complex.HasPrimitives
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
c : ℂ
r : ℝ
f : ℂ → E
inst_2 : CompleteSpace E
f_cont : ContinuousOn f (ball c r)
z : ℂ
hz : z ∈ ball c r
h : IsConservativeOn f (ball c r)
⊢ Filter.EventuallyEq.{0, u_1} (β := E) (𝓝 z)
    (fun (x' : ℂ) ↦ c.wedgeIntegral x' f - c.wedgeIntegral z f - (x' - z) • f z) fun (w : ℂ) ↦
    z.wedgeIntegral w f - (w - z) • f z

Tactic:
?_
-- Module: Mathlib.Analysis.Complex.HasPrimitives
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
c : ℂ
r : ℝ
f : ℂ → E
inst_2 : CompleteSpace E
f_cont : ContinuousOn f (ball c r)
z : ℂ
hz : z ∈ ball c r
h : IsConservativeOn f (ball c r)
⊢ (fun (w : ℂ) ↦ z.wedgeIntegral w f - (w - z) • f z) =
    (fun (w : ℂ) ↦ (∫ (x : ℝ) in z.re..w.re, f ((↑x : ℂ) + (↑z.im : ℂ) * I)) - (w - z).re • f z) +
      HSMul.hSMul (β := (w : ℂ) → E) I fun (w : ℂ) ↦
        (∫ (y : ℝ) in z.im..w.im, f ((↑w.re : ℂ) + (↑y : ℂ) * I)) - (w - z).im • f z

Tactic:
?_
-- Module: Mathlib.Analysis.Complex.HasPrimitives
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
c : ℂ
r : ℝ
f : ℂ → E
inst_2 : CompleteSpace E
f_cont : ContinuousOn f (ball c r)
z : ℂ
hz : z ∈ ball c r
h : IsConservativeOn f (ball c r)
⊢ Asymptotics.IsLittleO (F := ℂ) (𝓝 z)
    ((fun (w : ℂ) ↦ (∫ (x : ℝ) in z.re..w.re, f ((↑x : ℂ) + (↑z.im : ℂ) * I)) - (w - z).re • f z) +
      HSMul.hSMul (β := (w : ℂ) → E) I fun (w : ℂ) ↦
        (∫ (y : ℝ) in z.im..w.im, f ((↑w.re : ℂ) + (↑y : ℂ) * I)) - (w - z).im • f z)
    fun (w : ℂ) ↦ w - z

Tactic:
(hasDerivAt_wedgeIntegral_re_aux f_cont hz).add
        ((hasDerivAt_wedgeIntegral_im_aux f_cont hz).const_smul_left I)

Premises used: _private.0.Complex.hasDerivAt_wedgeIntegral_im_aux, _private.0.Complex.hasDerivAt_wedgeIntegral_re_aux, Asymptotics.IsLittleO.add, Asymptotics.IsLittleO.const_smul_left, Complex.I
-- Module: Mathlib.Analysis.Complex.HasPrimitives
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
c : ℂ
r : ℝ
f : ℂ → E
inst_2 : CompleteSpace E
f_cont : ContinuousOn f (ball c r)
z : ℂ
hz : z ∈ ball c r
h : IsConservativeOn f (ball c r)
calc_1 :
  Filter.EventuallyEq.{0, u_1} (β := E) (𝓝 z)
    (fun (x' : ℂ) ↦ c.wedgeIntegral x' f - c.wedgeIntegral z f - (x' - z) • f z) fun (w : ℂ) ↦
    z.wedgeIntegral w f - (w - z) • f z
calc_2 :
  (fun (w : ℂ) ↦ z.wedgeIntegral w f - (w - z) • f z) =
    (fun (w : ℂ) ↦ (∫ (x : ℝ) in z.re..w.re, f ((↑x : ℂ) + (↑z.im : ℂ) * I)) - (w - z).re • f z) +
      HSMul.hSMul (β := (w : ℂ) → E) I fun (w : ℂ) ↦
        (∫ (y : ℝ) in z.im..w.im, f ((↑w.re : ℂ) + (↑y : ℂ) * I)) - (w - z).im • f z
⊢ Asymptotics.IsLittleO.{0, u_1, 0} (E := E) (F := ℂ) (𝓝 z)
    (fun (x' : ℂ) ↦ c.wedgeIntegral x' f - c.wedgeIntegral z f - (x' - z) • f z) fun (x' : ℂ) ↦ x' - z

Tactic:
calc
    _ =ᶠ[𝓝 z] (fun w ↦ wedgeIntegral z w f - (w - z) • f z) := ?_
    _ = (fun w ↦ (∫ x in z.re..w.re, f (x + z.im * I)) - (w - z).re • f z)
        + I • (fun w ↦ (∫ y in z.im..w.im, f (w.re + y * I)) - (w - z).im • f z) := ?_
    _ =o[𝓝 z] fun w ↦ w - z := (hasDerivAt_wedgeIntegral_re_aux f_cont hz).add
        ((hasDerivAt_wedgeIntegral_im_aux f_cont hz).const_smul_left I)

Premises used: _private.0.Complex.hasDerivAt_wedgeIntegral_im_aux, HMul.hMul, _private.0.Complex.hasDerivAt_wedgeIntegral_re_aux, Complex.wedgeIntegral, Complex.im, HSub.hSub, intervalIntegral, nhds, Complex.ofReal, Complex.re, MeasureTheory.MeasureSpace.volume, HAdd.hAdd, Asymptotics.IsLittleO.add, HSMul.hSMul, Asymptotics.IsLittleO.const_smul_left, Complex.I
-- Module: Mathlib.Analysis.Complex.HasPrimitives
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
c : ℂ
r : ℝ
f : ℂ → E
inst_2 : CompleteSpace E
f_cont : ContinuousOn f (ball c r)
z : ℂ
hz : z ∈ ball c r
h : IsConservativeOn f (ball c r)
⊢ ∀ (x : ℂ),
    c.wedgeIntegral x f - c.wedgeIntegral z f = z.wedgeIntegral x f →
      Eq.{u_1 + 1} (α := E) ((fun (x' : ℂ) ↦ c.wedgeIntegral x' f - c.wedgeIntegral z f - (x' - z) • f z) x)
        ((fun (w : ℂ) ↦ z.wedgeIntegral w f - (w - z) • f z) x)

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.HasPrimitives
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
c : ℂ
r : ℝ
f : ℂ → E
inst_2 : CompleteSpace E
f_cont : ContinuousOn f (ball c r)
z : ℂ
hz : z ∈ ball c r
h : IsConservativeOn f (ball c r)
⊢ Filter.EventuallyEq.{0, u_1} (β := E) (𝓝 z)
    (fun (x' : ℂ) ↦ c.wedgeIntegral x' f - c.wedgeIntegral z f - (x' - z) • f z) fun (w : ℂ) ↦
    z.wedgeIntegral w f - (w - z) • f z

Tactic:
exact (h.eventually_nhds_wedgeIntegral_sub_wedgeIntegral f_cont hz).mono <| by simp

Premises used: Filter.Eventually.mono, Complex.IsConservativeOn.eventually_nhds_wedgeIntegral_sub_wedgeIntegral
-- Module: Mathlib.Analysis.Complex.HasPrimitives
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
c : ℂ
r : ℝ
f : ℂ → E
inst_2 : CompleteSpace E
f_cont : ContinuousOn f (ball c r)
z : ℂ
hz : z ∈ ball c r
h : IsConservativeOn f (ball c r)
calc_2 :
  ∀ (w : ℂ),
    z.wedgeIntegral w f - (w - z) • f z =
      HAdd.hAdd (α := (w : ℂ) → E)
        (fun (w : ℂ) ↦ (∫ (x : ℝ) in z.re..w.re, f ((↑x : ℂ) + (↑z.im : ℂ) * I)) - (w - z).re • f z)
        (HSMul.hSMul (β := (w : ℂ) → E) I fun (w : ℂ) ↦
          (∫ (y : ℝ) in z.im..w.im, f ((↑w.re : ℂ) + (↑y : ℂ) * I)) - (w - z).im • f z)
        w
⊢ (fun (w : ℂ) ↦ z.wedgeIntegral w f - (w - z) • f z) =
    (fun (w : ℂ) ↦ (∫ (x : ℝ) in z.re..w.re, f ((↑x : ℂ) + (↑z.im : ℂ) * I)) - (w - z).re • f z) +
      HSMul.hSMul (β := (w : ℂ) → E) I fun (w : ℂ) ↦
        (∫ (y : ℝ) in z.im..w.im, f ((↑w.re : ℂ) + (↑y : ℂ) * I)) - (w - z).im • f z

Tactic:
ext w
-- Module: Mathlib.Analysis.Complex.HasPrimitives
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
c : ℂ
r : ℝ
f : ℂ → E
inst_2 : CompleteSpace E
f_cont : ContinuousOn f (ball c r)
z : ℂ
hz : z ∈ ball c r
h : IsConservativeOn f (ball c r)
w : ℂ
I₁ : E := ∫ (x : ℝ) in z.re..w.re, f ((↑x : ℂ) + (↑z.im : ℂ) * I)
I₂ : E := ∫ (y : ℝ) in z.im..w.im, f ((↑w.re : ℂ) + (↑y : ℂ) * I)
e_a : w - z = (↑(w - z).re : ℂ) + (↑(w - z).im : ℂ) * I
⊢ z.wedgeIntegral w f - (w - z) • f z = I₁ + I • I₂ - ((↑(w - z).re : ℂ) + (↑(w - z).im : ℂ) * I) • f z

Tactic:
congr
-- Module: Mathlib.Analysis.Complex.HasPrimitives
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
c : ℂ
r : ℝ
f : ℂ → E
inst_2 : CompleteSpace E
f_cont : ContinuousOn f (ball c r)
z : ℂ
hz : z ∈ ball c r
h : IsConservativeOn f (ball c r)
w : ℂ
I₁ : E := ∫ (x : ℝ) in z.re..w.re, f ((↑x : ℂ) + (↑z.im : ℂ) * I)
I₂ : E := ∫ (y : ℝ) in z.im..w.im, f ((↑w.re : ℂ) + (↑y : ℂ) * I)
e_a e_a₁ : w - z = w - z
⊢ w - z = (↑(w - z).re : ℂ) + (↑(w - z).im : ℂ) * I

Tactic:
rw [re_add_im]

Premises used: Complex.re_add_im
-- Module: Mathlib.Analysis.Complex.HasPrimitives
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
c : ℂ
r : ℝ
f : ℂ → E
inst_2 : CompleteSpace E
f_cont : ContinuousOn f (ball c r)
z : ℂ
hz : z ∈ ball c r
h : IsConservativeOn f (ball c r)
w : ℂ
I₁ : E := ∫ (x : ℝ) in z.re..w.re, f ((↑x : ℂ) + (↑z.im : ℂ) * I)
I₂ : E := ∫ (y : ℝ) in z.im..w.im, f ((↑w.re : ℂ) + (↑y : ℂ) * I)
⊢ I₁ + I • I₂ - ((↑(w - z).re : ℂ) + (↑(w - z).im : ℂ) * I) • f z =
    I₁ + I • I₂ - ((↑w.re : ℂ) - (↑z.re : ℂ) + ((↑w.im : ℂ) - (↑z.im : ℂ)) * I) • f z

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.HasPrimitives
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
c : ℂ
r : ℝ
f : ℂ → E
inst_2 : CompleteSpace E
f_cont : ContinuousOn f (ball c r)
z : ℂ
hz : z ∈ ball c r
h : IsConservativeOn f (ball c r)
w : ℂ
I₁ : E := ∫ (x : ℝ) in z.re..w.re, f ((↑x : ℂ) + (↑z.im : ℂ) * I)
I₂ : E := ∫ (y : ℝ) in z.im..w.im, f ((↑w.re : ℂ) + (↑y : ℂ) * I)
⊢ I₁ + I • I₂ - ((↑w.re : ℂ) - (↑z.re : ℂ) + ((↑w.im : ℂ) - (↑z.im : ℂ)) * I) • f z =
    I₁ - ((↑w.re : ℂ) - (↑z.re : ℂ)) • f z + I • (I₂ - ((↑w.im : ℂ) - (↑z.im : ℂ)) • f z)

Tactic:
?_
-- Module: Mathlib.Analysis.Complex.HasPrimitives
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
c : ℂ
r : ℝ
f : ℂ → E
inst_2 : CompleteSpace E
f_cont : ContinuousOn f (ball c r)
z : ℂ
hz : z ∈ ball c r
h : IsConservativeOn f (ball c r)
w : ℂ
I₁ : E := ∫ (x : ℝ) in z.re..w.re, f ((↑x : ℂ) + (↑z.im : ℂ) * I)
I₂ : E := ∫ (y : ℝ) in z.im..w.im, f ((↑w.re : ℂ) + (↑y : ℂ) * I)
calc_2 :
  I₁ + I • I₂ - ((↑w.re : ℂ) - (↑z.re : ℂ) + ((↑w.im : ℂ) - (↑z.im : ℂ)) * I) • f z =
    I₁ - ((↑w.re : ℂ) - (↑z.re : ℂ)) • f z + I • (I₂ - ((↑w.im : ℂ) - (↑z.im : ℂ)) • f z)
calc_2₁ :
  I₁ - ((↑w.re : ℂ) - (↑z.re : ℂ)) • f z + I • (I₂ - ((↑w.im : ℂ) - (↑z.im : ℂ)) • f z) =
    HAdd.hAdd (α := (w : ℂ) → E)
      (fun (w : ℂ) ↦ (∫ (x : ℝ) in z.re..w.re, f ((↑x : ℂ) + (↑z.im : ℂ) * I)) - (w - z).re • f z)
      (HSMul.hSMul (β := (w : ℂ) → E) I fun (w : ℂ) ↦
        (∫ (y : ℝ) in z.im..w.im, f ((↑w.re : ℂ) + (↑y : ℂ) * I)) - (w - z).im • f z)
      w
⊢ z.wedgeIntegral w f - (w - z) • f z =
    HAdd.hAdd (α := (w : ℂ) → E)
      (fun (w : ℂ) ↦ (∫ (x : ℝ) in z.re..w.re, f ((↑x : ℂ) + (↑z.im : ℂ) * I)) - (w - z).re • f z)
      (HSMul.hSMul (β := (w : ℂ) → E) I fun (w : ℂ) ↦
        (∫ (y : ℝ) in z.im..w.im, f ((↑w.re : ℂ) + (↑y : ℂ) * I)) - (w - z).im • f z)
      w

Tactic:
calc
    _ = I₁ + I • I₂ - ((w - z).re + (w - z).im * I) • f z := by congr; rw [re_add_im]
    _ = I₁ + I • I₂ - ((w.re - z.re : ℂ) + (w.im - z.im) * I) • f z := by simp
    _ = I₁ - (w.re - z.re : ℂ) • f z + I • (I₂ - (w.im - z.im : ℂ) • f z) := ?_

Premises used: HMul.hMul, Complex.im, HSub.hSub, Complex.ofReal, Complex.re, HAdd.hAdd, HSMul.hSMul, Complex.I
-- Module: Mathlib.Analysis.Complex.HasPrimitives
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
c : ℂ
r : ℝ
f : ℂ → E
inst_2 : CompleteSpace E
f_cont : ContinuousOn f (ball c r)
z : ℂ
hz : z ∈ ball c r
h : IsConservativeOn f (ball c r)
w : ℂ
I₁ : E := ∫ (x : ℝ) in z.re..w.re, f ((↑x : ℂ) + (↑z.im : ℂ) * I)
I₂ : E := ∫ (y : ℝ) in z.im..w.im, f ((↑w.re : ℂ) + (↑y : ℂ) * I)
calc_2 :
  I₁ + I • I₂ - (((↑w.re : ℂ) - (↑z.re : ℂ)) • f z + (((↑w.im : ℂ) - (↑z.im : ℂ)) * I) • f z) =
    I₁ - ((↑w.re : ℂ) - (↑z.re : ℂ)) • f z + (I • I₂ - (((↑w.im : ℂ) - (↑z.im : ℂ)) * I) • f z)
⊢ I₁ + I • I₂ - ((↑w.re : ℂ) - (↑z.re : ℂ) + ((↑w.im : ℂ) - (↑z.im : ℂ)) * I) • f z =
    I₁ - ((↑w.re : ℂ) - (↑z.re : ℂ)) • f z + I • (I₂ - ((↑w.im : ℂ) - (↑z.im : ℂ)) • f z)

Tactic:
rw [add_smul, smul_sub, smul_smul, mul_comm I]

Premises used: smul_smul, smul_sub, add_smul, mul_comm, Complex.I
-- Module: Mathlib.Analysis.Complex.HasPrimitives
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
c : ℂ
r : ℝ
f : ℂ → E
inst_2 : CompleteSpace E
f_cont : ContinuousOn f (ball c r)
z : ℂ
hz : z ∈ ball c r
h : IsConservativeOn f (ball c r)
w : ℂ
I₁ : E := ∫ (x : ℝ) in z.re..w.re, f ((↑x : ℂ) + (↑z.im : ℂ) * I)
I₂ : E := ∫ (y : ℝ) in z.im..w.im, f ((↑w.re : ℂ) + (↑y : ℂ) * I)
⊢ I₁ + I • I₂ - (((↑w.re : ℂ) - (↑z.re : ℂ)) • f z + (((↑w.im : ℂ) - (↑z.im : ℂ)) * I) • f z) =
    I₁ - ((↑w.re : ℂ) - (↑z.re : ℂ)) • f z + (I • I₂ - (((↑w.im : ℂ) - (↑z.im : ℂ)) * I) • f z)

Tactic:
abel
-- Module: Mathlib.Analysis.Complex.HasPrimitives
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
c : ℂ
r : ℝ
f : ℂ → E
inst_2 : CompleteSpace E
f_cont : ContinuousOn f (ball c r)
z : ℂ
hz : z ∈ ball c r
h : IsConservativeOn f (ball c r)
w : ℂ
I₁ : E := ∫ (x : ℝ) in z.re..w.re, f ((↑x : ℂ) + (↑z.im : ℂ) * I)
I₂ : E := ∫ (y : ℝ) in z.im..w.im, f ((↑w.re : ℂ) + (↑y : ℂ) * I)
calc_2 :
  (↑w.re : ℂ) - (↑z.re : ℂ) = ((↑(RingHom.toMonoidWithZeroHom (algebraMap ℝ ℂ)) : ZeroHom ℝ ℂ) : (a : ℝ) → ℂ) (w - z).re
calc_2₁ :
  (↑w.im : ℂ) - (↑z.im : ℂ) = ((↑(RingHom.toMonoidWithZeroHom (algebraMap ℝ ℂ)) : ZeroHom ℝ ℂ) : (a : ℝ) → ℂ) (w - z).im
⊢ I₁ - ((↑w.re : ℂ) - (↑z.re : ℂ)) • f z + I • (I₂ - ((↑w.im : ℂ) - (↑z.im : ℂ)) • f z) =
    HAdd.hAdd (α := (w : ℂ) → E)
      (fun (w : ℂ) ↦ (∫ (x : ℝ) in z.re..w.re, f ((↑x : ℂ) + (↑z.im : ℂ) * I)) - (w - z).re • f z)
      (HSMul.hSMul (β := (w : ℂ) → E) I fun (w : ℂ) ↦
        (∫ (y : ℝ) in z.im..w.im, f ((↑w.re : ℂ) + (↑y : ℂ) * I)) - (w - z).im • f z)
      w

Tactic:
congr
-- Module: Mathlib.Analysis.Complex.HasPrimitives
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
c : ℂ
r : ℝ
f : ℂ → E
inst_2 : CompleteSpace E
f_cont : ContinuousOn f (ball c r)
z : ℂ
hz : z ∈ ball c r
h : IsConservativeOn f (ball c r)
w : ℂ
I₁ : E := ∫ (x : ℝ) in z.re..w.re, f ((↑x : ℂ) + (↑z.im : ℂ) * I)
I₂ : E := ∫ (y : ℝ) in z.im..w.im, f ((↑w.re : ℂ) + (↑y : ℂ) * I)
⊢ (↑w.re : ℂ) - (↑z.re : ℂ) = ((↑(RingHom.toMonoidWithZeroHom (algebraMap ℝ ℂ)) : ZeroHom ℝ ℂ) : (a : ℝ) → ℂ) (w - z).re

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.HasPrimitives
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
c : ℂ
r : ℝ
f : ℂ → E
inst_2 : CompleteSpace E
f_cont : ContinuousOn f (ball c r)
z : ℂ
hz : z ∈ ball c r
h : IsConservativeOn f (ball c r)
w : ℂ
I₁ : E := ∫ (x : ℝ) in z.re..w.re, f ((↑x : ℂ) + (↑z.im : ℂ) * I)
I₂ : E := ∫ (y : ℝ) in z.im..w.im, f ((↑w.re : ℂ) + (↑y : ℂ) * I)
⊢ (↑w.im : ℂ) - (↑z.im : ℂ) = ((↑(RingHom.toMonoidWithZeroHom (algebraMap ℝ ℂ)) : ZeroHom ℝ ℂ) : (a : ℝ) → ℂ) (w - z).im

Tactic:
simp