awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Complex.HasPrimitives (goal)
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 : ℂ) ↦ (∫ (y : ℝ) in z.im..w.im, f ((↑w.re : ℂ) + (↑y : ℂ) * I)) - (w - z).im • f z) fun (w : ℂ) ↦ w - z
have suffices : 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: suffices (fun w ↦ ∫ y in z.im..w.im, f (w.re + y * I) - f z) =o[𝓝 z] fun w ↦ w - z by
    calc
      _ = fun w ↦ (∫ y in z.im..w.im, f (w.re + y * I)) - (∫ _ in z.im..w.im, f z) := by simp
      _ =ᶠ[𝓝 z] fun w ↦ ∫ y in z.im..w.im, f (w.re + y * I) - f z := ?_
      _ =o[𝓝 z] fun w ↦ w - z := this
    refine eventually_nhds_iff_ball.mpr ⟨r - dist z c, by simpa using hz, fun w hw ↦ ?_⟩
    exact (intervalIntegral.integral_sub
      ((f_cont.mono (mem_ball_of_map_im_aux₂ hw)).comp (by fun_prop)
        (mapsTo_image _ _)).intervalIntegrable intervalIntegrable_const).symm
-- Lean 4 proof step from Mathlib.Analysis.Complex.HasPrimitives (goal)
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
have rw : Filter.Tendsto f (𝓝 z) (𝓝 (f z))
Tactic: rw [Asymptotics.isLittleO_one_iff, tendsto_sub_nhds_zero_iff]
-- Lean 4 proof step from Mathlib.Analysis.Complex.HasPrimitives (hypothesis)
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 : ℂ) ↦ ∫ (y : ℝ) in z.im..w.im, f ((↑w.re : ℂ) + (↑y : ℂ) * I) - f z) fun (w : ℂ) ↦ w - z
have this : 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⟩
-- Lean 4 proof step from Mathlib.Analysis.Complex.HasPrimitives (goal)
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
⊢ 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
have 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
Tactic: rw [Asymptotics.IsLittleO] at this ⊢
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Complex.HasPrimitives (hypothesis)
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 : ℂ) ↦ ∫ (y : ℝ) in z.im..w.im, f ((↑w.re : ℂ) + (↑y : ℂ) * I) - f z) fun (w : ℂ) ↦ w - z
have this₁ : Asymptotics.IsBigOWith.{0, u_1, 0} (E := E) (F := ℝ) ε (𝓝 z) (fun (w : ℂ) ↦ f w - f z) fun (x : ℂ) ↦ 1
Tactic: replace := this ε_pos
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Complex.HasPrimitives (goal)
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
⊢ 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
have 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‖
Tactic: simp only [Asymptotics.isBigOWith_iff, norm_one, mul_one] at this ⊢
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Complex.HasPrimitives (goal)
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‖ ≤ ε
have 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‖ ≤ ε
Tactic: rw [Metric.nhds_basis_closedBall.eventually_iff] at this ⊢
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Complex.HasPrimitives (goal)
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‖ ≤ ε
⊢ ∃ (i : ℝ), 0 < i ∧ ∀ ⦃x : ℂ⦄, x ∈ closedBall z i → ∀ y ∈ Ι z.im x.im, ‖f ((↑x.re : ℂ) + (↑y : ℂ) * I) - f z‖ ≤ ε
have 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‖ ≤ ε
Tactic: obtain ⟨i, i_pos, hi⟩ := this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Complex.HasPrimitives (hypothesis)
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‖ ≤ ε
⊢ ∀ᶠ (x : ℂ) in 𝓝 z, norm.{u_1} (E := E) (∫ (y : ℝ) in z.im..x.im, f ((↑x.re : ℂ) + (↑y : ℂ) * I) - f z) ≤ ε * ‖x - z‖
have this₁ : ∀ᶠ (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)⟩
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Complex.HasPrimitives (goal)
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‖ ≤ ε
⊢ ∀ᶠ (x : ℂ) in 𝓝 z, norm.{u_1} (E := E) (∫ (y : ℝ) in z.im..x.im, f ((↑x.re : ℂ) + (↑y : ℂ) * I) - f z) ≤ ε * ‖x - z‖
have 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‖
Tactic: filter_upwards [this] with w hw
-- Lean 4 proof step from Mathlib.Analysis.Complex.HasPrimitives (goal)
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) (∫ (y : ℝ) in z.im..w.im, f ((↑w.re : ℂ) + (↑y : ℂ) * I) - f z) ≤ ε * ‖w - z‖
have _ : ε * ‖w.im - z.im‖ = ε * ‖(w - z).im‖
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 _)
-- Lean 4 proof step from Mathlib.Analysis.Complex.HasPrimitives (goal)
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)
⊢ HasDerivAt (fun (w : ℂ) ↦ c.wedgeIntegral w f) (f z) z
have 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
Tactic: rw [hasDerivAt_iff_isLittleO]
-- Lean 4 proof step from Mathlib.Analysis.Complex.HasPrimitives (goal)
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.{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
have 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
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)
-- Lean 4 proof step from Mathlib.Analysis.Complex.HasPrimitives (goal)
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
⊢ 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
have 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
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)
-- Lean 4 proof step from Mathlib.Analysis.Complex.HasPrimitives (goal)
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
have 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
Tactic: ext w
-- Lean 4 proof step from Mathlib.Analysis.Complex.HasPrimitives (goal)
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)
⊢ z.wedgeIntegral w f - (w - z) • f z = I₁ + I • I₂ - ((↑(w - z).re : ℂ) + (↑(w - z).im : ℂ) * I) • f z
have e_a : w - z = (↑(w - z).re : ℂ) + (↑(w - z).im : ℂ) * I
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.Complex.HasPrimitives (goal)
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 - z = (↑(w - z).re : ℂ) + (↑(w - z).im : ℂ) * I
have e_a : w - z = w - z
Tactic: rw [re_add_im]
-- Lean 4 proof step from Mathlib.Analysis.Complex.HasPrimitives (goal)
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)
⊢ 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
have 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)
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) := ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.HasPrimitives (goal)
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)
⊢ 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
have 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
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) := ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.HasPrimitives (goal)
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)
have 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)
Tactic: rw [add_smul, smul_sub, smul_smul, mul_comm I]
-- Lean 4 proof step from Mathlib.Analysis.Complex.HasPrimitives (goal)
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₁ - ((↑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
have calc_2 : (↑w.re : ℂ) - (↑z.re : ℂ) = ((↑(RingHom.toMonoidWithZeroHom (algebraMap ℝ ℂ)) : ZeroHom ℝ ℂ) : (a : ℝ) → ℂ) (w - z).re
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.Complex.HasPrimitives (goal)
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
⊢ 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
have calc_2₁ : (↑w.im : ℂ) - (↑z.im : ℂ) = ((↑(RingHom.toMonoidWithZeroHom (algebraMap ℝ ℂ)) : ZeroHom ℝ ℂ) : (a : ℝ) → ℂ) (w - z).im
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.Complex.HasPrimitives (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
inst_2 : CompleteSpace E
U : Set ℂ
hU : IsOpen U
⊢ IsConservativeOn f U ∧ ContinuousOn f U ↔ DifferentiableOn ℂ f U
have refine : IsConservativeOn f U ∧ ContinuousOn f U →
  ∀ (z : ℂ) (hz : z ∈ U) (hf : IsConservativeOn f U) (hf' : ContinuousOn f U), DifferentiableWithinAt ℂ f U z
Tactic: refine ⟨fun ⟨hf, hf'⟩ z hz ↦ ?_, fun hf ↦ ⟨hf.isConservativeOn, hf.continuousOn⟩⟩
-- Lean 4 proof step from Mathlib.Analysis.Complex.HasPrimitives (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
inst_2 : CompleteSpace E
U : Set ℂ
hU : IsOpen U
h : IsConservativeOn f U ∧ ContinuousOn f U
z : ℂ
hz : z ∈ U
hf : IsConservativeOn f U
hf' : ContinuousOn f U
⊢ DifferentiableWithinAt ℂ f U z
have obtain : ∀ (r : ℝ) (h₀ : r > 0) (h₁ : ball z r ⊆ U), DifferentiableWithinAt ℂ f U z
Tactic: obtain ⟨r, h₀, h₁⟩ : ∃ r > 0, ball z r ⊆ U := Metric.isOpen_iff.mp hU z hz
-- Lean 4 proof step from Mathlib.Analysis.Complex.HasPrimitives (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
inst_2 : CompleteSpace E
U : Set ℂ
hU : IsOpen U
h : IsConservativeOn f U ∧ ContinuousOn f U
z : ℂ
hz : z ∈ U
hf : IsConservativeOn f U
hf' : ContinuousOn f U
r : ℝ
h₀ : r > 0
h₁ : ball z r ⊆ U
⊢ DifferentiableWithinAt ℂ f U z
have this : DifferentiableOn ℂ f (ball z r)
Tactic: have : DifferentiableOn ℂ f (ball z r) :=
    (IsConservativeOn.isExactOn_ball (hf'.mono h₁) (hf.mono h₁)).differentiableOn isOpen_ball
-- Lean 4 proof step from Mathlib.Analysis.Complex.HasPrimitives (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
inst_2 : CompleteSpace E
U : Set ℂ
hU : IsOpen U
h : IsConservativeOn f U ∧ ContinuousOn f U
z : ℂ
hz : z ∈ U
hf : IsConservativeOn f U
hf' : ContinuousOn f U
r : ℝ
h₀ : r > 0
h₁ : ball z r ⊆ U
this : DifferentiableOn ℂ f (ball z r)
⊢ DifferentiableWithinAt ℂ f U z
have apply : ball z r ∈ 𝓝[U] z
Tactic: apply (this z (mem_ball_self h₀)).mono_of_mem_nhdsWithin
-- Lean 4 proof step from Mathlib.Analysis.Complex.HasPrimitives (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
inst_2 : CompleteSpace E
h₁ : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
h₂ : IsConservativeOn f univ
⊢ IsExactOn f univ
have h : ∀ (z : ℂ), Membership.mem (γ := Set ℂ) univ z → HasDerivAt (fun (x : ℂ) ↦ wedgeIntegral 0 x f) (f z) z
Tactic: use (wedgeIntegral 0 · f)
-- Lean 4 proof step from Mathlib.Analysis.Complex.HasPrimitives (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
inst_2 : CompleteSpace E
h₁ : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
h₂ : IsConservativeOn f univ
z : ℂ
h : Membership.mem (γ := Set ℂ) univ z
⊢ HasDerivAt (fun (x : ℂ) ↦ wedgeIntegral 0 x f) (f z) z
have h₃ : IsConservativeOn f (ball 0 (‖z‖ + 1))
Tactic: have h₃ : IsConservativeOn f (ball 0 (‖z‖ + 1)) := h₂.mono (subset_univ _)
-- Lean 4 proof step from Mathlib.Analysis.Complex.IntegerCompl (goal)
Goal:
x : ℂ
a : ℤ
⊢ x + (↑a : ℂ) ∈ ℂ_ℤ ↔ x ∈ ℂ_ℤ
have simp : (∃ (n : ℤ), (↑n : ℂ) = x + (↑a : ℂ)) ↔ ∃ (n : ℤ), (↑n : ℂ) = x
Tactic: simp only [mem_integerComplement_iff, not_iff_not]
-- Lean 4 proof step from Mathlib.Analysis.Complex.IntegerCompl (hypothesis)
Goal:
x : ℂ
hx : x ∈ ℂ_ℤ
n : ℤ
⊢ HPow.hPow (β := ℕ) x 2 ≠ HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2
have this : ¬(↑n : ℂ) = x
Tactic: have := not_exists.mp hx n
-- Lean 4 proof step from Mathlib.Analysis.Complex.IntegerCompl (hypothesis)
Goal:
x : ℂ
hx : x ∈ ℂ_ℤ
n : ℤ
this : ¬(↑n : ℂ) = x
⊢ HPow.hPow (β := ℕ) x 2 ≠ HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2
have this₁ : ¬(↑(-n) : ℂ) = x
Tactic: have := not_exists.mp hx (-n)
-- Lean 4 proof step from Mathlib.Analysis.Complex.IntegerCompl (goal)
Goal:
⊢ {z : ℂ | 0 < z.im} ∩ ℂ_ℤ = {z : ℂ | 0 < z.im}
have a : {z : ℂ | 0 < z.im} ⊆ ℂ_ℤ
Tactic: apply Set.inter_eq_self_of_subset_left
-- Lean 4 proof step from Mathlib.Analysis.Complex.IntegerCompl (hypothesis)
Goal:
z : ℍ
n : ℤ
hn : n ≠ 0
w : ℤ
hm : (↑w : ℂ) = (↑n : ℂ) / (↑z : ℂ)
⊢ False
have this : ((↑n : ℂ) / (↑z : ℂ)).im ≠ 0
Tactic: have : (n / (z : ℂ)).im ≠ 0 := by simp [div_im, z.ne_zero, hn, z.im_ne_zero]
-- Lean 4 proof step from Mathlib.Analysis.Complex.IsIntegral (goal)
Goal:
⊢ IsIntegral ℤ I
have refine : eval₂ (algebraMap ℤ ℂ) I (HPow.hPow (α := ℤ[X]) (β := ℕ) X 2 + (C : (a : ℤ) → ℤ[X]) 1) = 0
Tactic: refine ⟨X ^ 2 + C 1, monic_X_pow_add_C _ two_ne_zero, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Complex.IsIntegral (goal)
Goal:
⊢ eval₂ (algebraMap ℤ ℂ) I (HPow.hPow (α := ℤ[X]) (β := ℕ) X 2 + (C : (a : ℤ) → ℤ[X]) 1) = 0
have rw : eval₂ (algebraMap ℤ ℂ) I (HPow.hPow (α := ℤ[X]) (β := ℕ) X 2) + eval₂ (algebraMap ℤ ℂ) I ((C : (a : ℤ) → ℤ[X]) 1) = 0
Tactic: rw [eval₂_add, eval₂_X_pow, eval₂_C, I_sq, eq_intCast, Int.cast_one, neg_add_cancel]