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
f_cont : ContinuousOn f (ball c r)
z : ℂ
hz : z ∈ ball c r
hf : IsConservativeOn f (ball c r)
w : ℂ
w_in_z_ball : w ∈ ball z (r - dist z c)
I₁ : E := ∫ (x : ℝ) in c.re..w.re, f ((↑x : ℂ) + (↑c.im : ℂ) * I)
I₂ : E := HSMul.hSMul (β := E) I (∫ (y : ℝ) in c.im..w.im, f ((↑w.re : ℂ) + (↑y : ℂ) * I))
I₃ : E := ∫ (x : ℝ) in c.re..z.re, f ((↑x : ℂ) + (↑c.im : ℂ) * I)
I₄ : E := HSMul.hSMul (β := E) I (∫ (y : ℝ) in c.im..z.im, f ((↑z.re : ℂ) + (↑y : ℂ) * I))
I₅ : E := ∫ (x : ℝ) in z.re..w.re, f ((↑x : ℂ) + (↑z.im : ℂ) * I)
I₆ : E := HSMul.hSMul (β := E) I (∫ (y : ℝ) in z.im..w.im, f ((↑w.re : ℂ) + (↑y : ℂ) * I))
I₇ : E := ∫ (x : ℝ) in z.re..w.re, f ((↑x : ℂ) + (↑c.im : ℂ) * I)
I₈ : E := HSMul.hSMul (β := E) I (∫ (y : ℝ) in c.im..z.im, f ((↑w.re : ℂ) + (↑y : ℂ) * I))
z_ball : ball z (r - dist z c) ⊆ ball c r
w_mem : w ∈ ball c r
integrableHoriz :
  ∀ (a₁ a₂ b : ℝ) (ha₁ : (↑a₁ : ℂ) + (↑b : ℂ) * I ∈ ball c r) (ha₂ : (↑a₂ : ℂ) + (↑b : ℂ) * I ∈ ball c r),
    IntervalIntegrable.{u_1} (ε := E) (fun (x : ℝ) ↦ f ((↑x : ℂ) + (↑b : ℂ) * I)) volume a₁ a₂
integrableVert :
  ∀ (a b₁ b₂ : ℝ) (hb₁ : (↑a : ℂ) + (↑b₁ : ℂ) * I ∈ ball c r) (hb₂ : (↑a : ℂ) + (↑b₂ : ℂ) * I ∈ ball c r),
    IntervalIntegrable.{u_1} (ε := E) (fun (y : ℝ) ↦ f ((↑a : ℂ) + (↑y : ℂ) * I)) volume b₁ b₂
hI₁ : I₁ = I₃ + I₇
hI₂ : I₂ = I₈ + I₆
wzInBall : (↑w.re : ℂ) + (↑z.im : ℂ) * I ∈ ball c r
wcInBall : (↑w.re : ℂ) + (↑c.im : ℂ) * I ∈ ball c r
⊢ (↑((↑w.re : ℂ) + (↑z.im : ℂ) * I).re : ℂ) + (↑((↑z.re : ℂ) + (↑c.im : ℂ) * I).im : ℂ) * I ∈ ball c r

Tactic:
simpa using wcInBall
-- Module: Mathlib.Analysis.Complex.HasPrimitives
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
c : ℂ
r : ℝ
f : ℂ → E
f_cont : ContinuousOn f (ball c r)
z : ℂ
hz : z ∈ ball c r
hf : IsConservativeOn f (ball c r)
w : ℂ
w_in_z_ball : w ∈ ball z (r - dist z c)
I₁ : E := ∫ (x : ℝ) in c.re..w.re, f ((↑x : ℂ) + (↑c.im : ℂ) * I)
I₂ : E := HSMul.hSMul (β := E) I (∫ (y : ℝ) in c.im..w.im, f ((↑w.re : ℂ) + (↑y : ℂ) * I))
I₃ : E := ∫ (x : ℝ) in c.re..z.re, f ((↑x : ℂ) + (↑c.im : ℂ) * I)
I₄ : E := HSMul.hSMul (β := E) I (∫ (y : ℝ) in c.im..z.im, f ((↑z.re : ℂ) + (↑y : ℂ) * I))
I₅ : E := ∫ (x : ℝ) in z.re..w.re, f ((↑x : ℂ) + (↑z.im : ℂ) * I)
I₆ : E := HSMul.hSMul (β := E) I (∫ (y : ℝ) in z.im..w.im, f ((↑w.re : ℂ) + (↑y : ℂ) * I))
I₇ : E := ∫ (x : ℝ) in z.re..w.re, f ((↑x : ℂ) + (↑c.im : ℂ) * I)
I₈ : E := HSMul.hSMul (β := E) I (∫ (y : ℝ) in c.im..z.im, f ((↑w.re : ℂ) + (↑y : ℂ) * I))
z_ball : ball z (r - dist z c) ⊆ ball c r
w_mem : w ∈ ball c r
integrableHoriz :
  ∀ (a₁ a₂ b : ℝ) (ha₁ : (↑a₁ : ℂ) + (↑b : ℂ) * I ∈ ball c r) (ha₂ : (↑a₂ : ℂ) + (↑b : ℂ) * I ∈ ball c r),
    IntervalIntegrable.{u_1} (ε := E) (fun (x : ℝ) ↦ f ((↑x : ℂ) + (↑b : ℂ) * I)) volume a₁ a₂
integrableVert :
  ∀ (a b₁ b₂ : ℝ) (hb₁ : (↑a : ℂ) + (↑b₁ : ℂ) * I ∈ ball c r) (hb₂ : (↑a : ℂ) + (↑b₂ : ℂ) * I ∈ ball c r),
    IntervalIntegrable.{u_1} (ε := E) (fun (y : ℝ) ↦ f ((↑a : ℂ) + (↑y : ℂ) * I)) volume b₁ b₂
hI₁ : I₁ = I₃ + I₇
hI₂ : I₂ = I₈ + I₆
wzInBall : (↑w.re : ℂ) + (↑z.im : ℂ) * I ∈ ball c r
wcInBall : (↑w.re : ℂ) + (↑c.im : ℂ) * I ∈ ball c r
⊢ ((↑z.re : ℂ) + (↑c.im : ℂ) * I).Rectangle ((↑w.re : ℂ) + (↑z.im : ℂ) * I) ⊆ ball c r

Tactic:
have hU : Rectangle (z.re + c.im * I) (w.re + z.im * I) ⊆ ball c r :=
      (convex_ball c r).rectangle_subset (re_add_im_mul_mem_ball hz) wzInBall
        (by simpa using hz) (by simpa using wcInBall)
-- Module: Mathlib.Analysis.Complex.HasPrimitives
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
c : ℂ
r : ℝ
f : ℂ → E
f_cont : ContinuousOn f (ball c r)
z : ℂ
hz : z ∈ ball c r
hf : IsConservativeOn f (ball c r)
w : ℂ
w_in_z_ball : w ∈ ball z (r - dist z c)
I₁ : E := ∫ (x : ℝ) in c.re..w.re, f ((↑x : ℂ) + (↑c.im : ℂ) * I)
I₂ : E := HSMul.hSMul (β := E) I (∫ (y : ℝ) in c.im..w.im, f ((↑w.re : ℂ) + (↑y : ℂ) * I))
I₃ : E := ∫ (x : ℝ) in c.re..z.re, f ((↑x : ℂ) + (↑c.im : ℂ) * I)
I₄ : E := HSMul.hSMul (β := E) I (∫ (y : ℝ) in c.im..z.im, f ((↑z.re : ℂ) + (↑y : ℂ) * I))
I₅ : E := ∫ (x : ℝ) in z.re..w.re, f ((↑x : ℂ) + (↑z.im : ℂ) * I)
I₆ : E := HSMul.hSMul (β := E) I (∫ (y : ℝ) in z.im..w.im, f ((↑w.re : ℂ) + (↑y : ℂ) * I))
I₇ : E := ∫ (x : ℝ) in z.re..w.re, f ((↑x : ℂ) + (↑c.im : ℂ) * I)
I₈ : E := HSMul.hSMul (β := E) I (∫ (y : ℝ) in c.im..z.im, f ((↑w.re : ℂ) + (↑y : ℂ) * I))
z_ball : ball z (r - dist z c) ⊆ ball c r
w_mem : w ∈ ball c r
integrableHoriz :
  ∀ (a₁ a₂ b : ℝ) (ha₁ : (↑a₁ : ℂ) + (↑b : ℂ) * I ∈ ball c r) (ha₂ : (↑a₂ : ℂ) + (↑b : ℂ) * I ∈ ball c r),
    IntervalIntegrable.{u_1} (ε := E) (fun (x : ℝ) ↦ f ((↑x : ℂ) + (↑b : ℂ) * I)) volume a₁ a₂
integrableVert :
  ∀ (a b₁ b₂ : ℝ) (hb₁ : (↑a : ℂ) + (↑b₁ : ℂ) * I ∈ ball c r) (hb₂ : (↑a : ℂ) + (↑b₂ : ℂ) * I ∈ ball c r),
    IntervalIntegrable.{u_1} (ε := E) (fun (y : ℝ) ↦ f ((↑a : ℂ) + (↑y : ℂ) * I)) volume b₁ b₂
hI₁ : I₁ = I₃ + I₇
hI₂ : I₂ = I₈ + I₆
wzInBall : (↑w.re : ℂ) + (↑z.im : ℂ) * I ∈ ball c r
wcInBall : (↑w.re : ℂ) + (↑c.im : ℂ) * I ∈ ball c r
hU : ((↑z.re : ℂ) + (↑c.im : ℂ) * I).Rectangle ((↑w.re : ℂ) + (↑z.im : ℂ) * I) ⊆ ball c r
⊢ I₇ - I₅ + I₈ - I₄ = 0

Tactic:
simpa [← add_eq_zero_iff_eq_neg, wedgeIntegral_add_wedgeIntegral_eq] using
      hf (z.re + c.im * I) (w.re + z.im * I) hU

Premises used: HMul.hMul, Complex.im, add_eq_zero_iff_eq_neg, Complex.ofReal, Complex.re, HAdd.hAdd, Complex.wedgeIntegral_add_wedgeIntegral_eq, Complex.I
-- Module: Mathlib.Analysis.Complex.HasPrimitives
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
c : ℂ
r : ℝ
f : ℂ → E
f_cont : ContinuousOn f (ball c r)
z : ℂ
hz : z ∈ ball c r
hf : IsConservativeOn f (ball c r)
w : ℂ
w_in_z_ball : w ∈ ball z (r - dist z c)
I₁ : E := ∫ (x : ℝ) in c.re..w.re, f ((↑x : ℂ) + (↑c.im : ℂ) * I)
I₂ : E := HSMul.hSMul (β := E) I (∫ (y : ℝ) in c.im..w.im, f ((↑w.re : ℂ) + (↑y : ℂ) * I))
I₃ : E := ∫ (x : ℝ) in c.re..z.re, f ((↑x : ℂ) + (↑c.im : ℂ) * I)
I₄ : E := HSMul.hSMul (β := E) I (∫ (y : ℝ) in c.im..z.im, f ((↑z.re : ℂ) + (↑y : ℂ) * I))
I₅ : E := ∫ (x : ℝ) in z.re..w.re, f ((↑x : ℂ) + (↑z.im : ℂ) * I)
I₆ : E := HSMul.hSMul (β := E) I (∫ (y : ℝ) in z.im..w.im, f ((↑w.re : ℂ) + (↑y : ℂ) * I))
I₇ : E := ∫ (x : ℝ) in z.re..w.re, f ((↑x : ℂ) + (↑c.im : ℂ) * I)
I₈ : E := HSMul.hSMul (β := E) I (∫ (y : ℝ) in c.im..z.im, f ((↑w.re : ℂ) + (↑y : ℂ) * I))
z_ball : ball z (r - dist z c) ⊆ ball c r
w_mem : w ∈ ball c r
integrableHoriz :
  ∀ (a₁ a₂ b : ℝ) (ha₁ : (↑a₁ : ℂ) + (↑b : ℂ) * I ∈ ball c r) (ha₂ : (↑a₂ : ℂ) + (↑b : ℂ) * I ∈ ball c r),
    IntervalIntegrable.{u_1} (ε := E) (fun (x : ℝ) ↦ f ((↑x : ℂ) + (↑b : ℂ) * I)) volume a₁ a₂
integrableVert :
  ∀ (a b₁ b₂ : ℝ) (hb₁ : (↑a : ℂ) + (↑b₁ : ℂ) * I ∈ ball c r) (hb₂ : (↑a : ℂ) + (↑b₂ : ℂ) * I ∈ ball c r),
    IntervalIntegrable.{u_1} (ε := E) (fun (y : ℝ) ↦ f ((↑a : ℂ) + (↑y : ℂ) * I)) volume b₁ b₂
hI₁ : I₁ = I₃ + I₇
hI₂ : I₂ = I₈ + I₆
⊢ I₇ - I₅ + I₈ - I₄ = 0

Tactic:
have hI₀ : I₇ - I₅ + I₈ - I₄ = 0 := by
    have wzInBall : w.re + z.im * I ∈ ball c r :=
      mem_of_subset_of_mem z_ball (re_add_im_mul_mem_ball w_in_z_ball)
    have wcInBall : w.re + c.im * I ∈ ball c r := re_add_im_mul_mem_ball w_mem
    have hU : Rectangle (z.re + c.im * I) (w.re + z.im * I) ⊆ ball c r :=
      (convex_ball c r).rectangle_subset (re_add_im_mul_mem_ball hz) wzInBall
        (by simpa using hz) (by simpa using wcInBall)
    simpa [← add_eq_zero_iff_eq_neg, wedgeIntegral_add_wedgeIntegral_eq] using
      hf (z.re + c.im * I) (w.re + z.im * I) hU
-- Module: Mathlib.Analysis.Complex.HasPrimitives
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
c : ℂ
r : ℝ
f : ℂ → E
f_cont : ContinuousOn f (ball c r)
z : ℂ
hz : z ∈ ball c r
hf : IsConservativeOn f (ball c r)
w : ℂ
w_in_z_ball : w ∈ ball z (r - dist z c)
I₁ : E := ∫ (x : ℝ) in c.re..w.re, f ((↑x : ℂ) + (↑c.im : ℂ) * I)
I₂ : E := HSMul.hSMul (β := E) I (∫ (y : ℝ) in c.im..w.im, f ((↑w.re : ℂ) + (↑y : ℂ) * I))
I₃ : E := ∫ (x : ℝ) in c.re..z.re, f ((↑x : ℂ) + (↑c.im : ℂ) * I)
I₄ : E := HSMul.hSMul (β := E) I (∫ (y : ℝ) in c.im..z.im, f ((↑z.re : ℂ) + (↑y : ℂ) * I))
I₅ : E := ∫ (x : ℝ) in z.re..w.re, f ((↑x : ℂ) + (↑z.im : ℂ) * I)
I₆ : E := HSMul.hSMul (β := E) I (∫ (y : ℝ) in z.im..w.im, f ((↑w.re : ℂ) + (↑y : ℂ) * I))
I₇ : E := ∫ (x : ℝ) in z.re..w.re, f ((↑x : ℂ) + (↑c.im : ℂ) * I)
I₈ : E := HSMul.hSMul (β := E) I (∫ (y : ℝ) in c.im..z.im, f ((↑w.re : ℂ) + (↑y : ℂ) * I))
z_ball : ball z (r - dist z c) ⊆ ball c r
w_mem : w ∈ ball c r
integrableHoriz :
  ∀ (a₁ a₂ b : ℝ) (ha₁ : (↑a₁ : ℂ) + (↑b : ℂ) * I ∈ ball c r) (ha₂ : (↑a₂ : ℂ) + (↑b : ℂ) * I ∈ ball c r),
    IntervalIntegrable.{u_1} (ε := E) (fun (x : ℝ) ↦ f ((↑x : ℂ) + (↑b : ℂ) * I)) volume a₁ a₂
integrableVert :
  ∀ (a b₁ b₂ : ℝ) (hb₁ : (↑a : ℂ) + (↑b₁ : ℂ) * I ∈ ball c r) (hb₂ : (↑a : ℂ) + (↑b₂ : ℂ) * I ∈ ball c r),
    IntervalIntegrable.{u_1} (ε := E) (fun (y : ℝ) ↦ f ((↑a : ℂ) + (↑y : ℂ) * I)) volume b₁ b₂
hI₁ : I₁ = I₃ + I₇
hI₂ : I₂ = I₈ + I₆
hI₀ : I₇ - I₅ + I₈ - I₄ = 0
⊢ c.wedgeIntegral w f - c.wedgeIntegral z f = z.wedgeIntegral w f

Tactic:
grind [wedgeIntegral]

Premises used: Complex.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
suffices :
  Asymptotics.IsLittleO.{0, u_1, 0} (E := E) (F := ℝ) (𝓝 z.re)
    (fun (x : ℝ) ↦ (∫ (t : ℝ) in z.re..x, f ((↑t : ℂ) + (↑z.im : ℂ) * I)) - (x - z.re) • f z) fun (x : ℝ) ↦ x - z.re
⊢ Asymptotics.IsLittleO.{0, u_1, 0} (E := E) (F := ℂ) (𝓝 z)
    (fun (w : ℂ) ↦ (∫ (x : ℝ) in z.re..w.re, f ((↑x : ℂ) + (↑z.im : ℂ) * I)) - (w - z).re • f z) fun (w : ℂ) ↦ w - z

Tactic:
suffices (fun x ↦ (∫ t in z.re..x, f (t + z.im * I)) - (x - z.re) • f z) =o[𝓝 z.re]
      fun x ↦ x - z.re from
    this.comp_tendsto (continuous_re.tendsto z) |>.trans_isBigO isBigO_re_sub_re
-- 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
r₁ : ℝ := r - dist z c
⊢ 0 < r₁

Tactic:
simpa only [mem_ball, sub_pos, r₁] using hz

Premises used: sub_pos, Metric.mem_ball
-- 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
r₁ : ℝ := r - dist z c
⊢ 0 < r₁

Tactic:
have r₁_pos : 0 < r₁ := by simpa only [mem_ball, sub_pos, r₁] using 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
r₁ : ℝ := r - dist z c
r₁_pos : 0 < r₁
s : Set ℝ := Ioo (z.re - r₁) (z.re + r₁)
⊢ z.re ∈ s

Tactic:
simp [s, r₁_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
r₁ : ℝ := r - dist z c
r₁_pos : 0 < r₁
s : Set ℝ := Ioo (z.re - r₁) (z.re + r₁)
⊢ z.re ∈ s

Tactic:
have zRe_mem_s : z.re ∈ s := by simp [s, r₁_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
r₁ : ℝ := r - dist z c
r₁_pos : 0 < r₁
s : Set ℝ := Ioo (z.re - r₁) (z.re + r₁)
zRe_mem_s : z.re ∈ s
⊢ ContinuousOn.{0, u_1} (Y := E) (fun (x : ℝ) ↦ f ((↑x : ℂ) + (↑z.im : ℂ) * I)) s

Tactic:
have f_contOn : ContinuousOn (fun (x : ℝ) ↦ f (x + z.im * I)) s :=
    f_cont.comp ((continuous_add_const _).comp continuous_ofReal).continuousOn <|
      fun _ ↦ mem_ball_re_aux
-- 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
r₁ : ℝ := r - dist z c
r₁_pos : 0 < r₁
s : Set ℝ := Ioo (z.re - r₁) (z.re + r₁)
zRe_mem_s : z.re ∈ s
f_contOn : ContinuousOn.{0, u_1} (Y := E) (fun (x : ℝ) ↦ f ((↑x : ℂ) + (↑z.im : ℂ) * I)) s
⊢ [[z.re, z.re]] ⊆ s

Tactic:
simpa
-- 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
r₁ : ℝ := r - dist z c
r₁_pos : 0 < r₁
s : Set ℝ := Ioo (z.re - r₁) (z.re + r₁)
zRe_mem_s : z.re ∈ s
f_contOn : ContinuousOn.{0, u_1} (Y := E) (fun (x : ℝ) ↦ f ((↑x : ℂ) + (↑z.im : ℂ) * I)) s
⊢ IntervalIntegrable.{u_1} (ε := E) (fun (x : ℝ) ↦ f ((↑x : ℂ) + (↑z.im : ℂ) * I)) volume z.re z.re

Tactic:
have int1 : IntervalIntegrable (fun (x : ℝ) ↦ f (x + z.im * I)) volume z.re z.re :=
    ContinuousOn.intervalIntegrable <| f_contOn.mono <| by simpa
-- 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
r₁ : ℝ := r - dist z c
r₁_pos : 0 < r₁
s : Set ℝ := Ioo (z.re - r₁) (z.re + r₁)
zRe_mem_s : z.re ∈ s
f_contOn : ContinuousOn.{0, u_1} (Y := E) (fun (x : ℝ) ↦ f ((↑x : ℂ) + (↑z.im : ℂ) * I)) s
int1 : IntervalIntegrable.{u_1} (ε := E) (fun (x : ℝ) ↦ f ((↑x : ℂ) + (↑z.im : ℂ) * I)) volume z.re z.re
⊢ StronglyMeasurableAtFilter.{0, u_1} (β := E) (mα := MeasureSpace.toMeasurableSpace)
    (fun (x : ℝ) ↦ f ((↑x : ℂ) + (↑z.im : ℂ) * I)) (𝓝 z.re) volume

Tactic:
have int2 : StronglyMeasurableAtFilter (fun (x : ℝ) ↦ f (x + z.im * I)) (𝓝 z.re) :=
    f_contOn.stronglyMeasurableAtFilter isOpen_Ioo _ zRe_mem_s
-- 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
r₁ : ℝ := r - dist z c
r₁_pos : 0 < r₁
s : Set ℝ := Ioo (z.re - r₁) (z.re + r₁)
zRe_mem_s : z.re ∈ s
f_contOn : ContinuousOn.{0, u_1} (Y := E) (fun (x : ℝ) ↦ f ((↑x : ℂ) + (↑z.im : ℂ) * I)) s
int1 : IntervalIntegrable.{u_1} (ε := E) (fun (x : ℝ) ↦ f ((↑x : ℂ) + (↑z.im : ℂ) * I)) volume z.re z.re
int2 :
  StronglyMeasurableAtFilter.{0, u_1} (β := E) (mα := MeasureSpace.toMeasurableSpace)
    (fun (x : ℝ) ↦ f ((↑x : ℂ) + (↑z.im : ℂ) * I)) (𝓝 z.re) volume
⊢ ContinuousAt.{0, u_1} (Y := E) (fun (x : ℝ) ↦ f ((↑x : ℂ) + (↑z.im : ℂ) * I)) z.re

Tactic:
have int3 : ContinuousAt (fun (x : ℝ) ↦ f (x + z.im * I)) z.re :=
    isOpen_Ioo.continuousOn_iff.mp f_contOn zRe_mem_s
-- 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
r₁ : ℝ := r - dist z c
r₁_pos : 0 < r₁
s : Set ℝ := Ioo (z.re - r₁) (z.re + r₁)
zRe_mem_s : z.re ∈ s
f_contOn : ContinuousOn.{0, u_1} (Y := E) (fun (x : ℝ) ↦ f ((↑x : ℂ) + (↑z.im : ℂ) * I)) s
int1 : IntervalIntegrable.{u_1} (ε := E) (fun (x : ℝ) ↦ f ((↑x : ℂ) + (↑z.im : ℂ) * I)) volume z.re z.re
int2 :
  StronglyMeasurableAtFilter.{0, u_1} (β := E) (mα := MeasureSpace.toMeasurableSpace)
    (fun (x : ℝ) ↦ f ((↑x : ℂ) + (↑z.im : ℂ) * I)) (𝓝 z.re) volume
int3 : ContinuousAt.{0, u_1} (Y := E) (fun (x : ℝ) ↦ f ((↑x : ℂ) + (↑z.im : ℂ) * I)) z.re
⊢ Asymptotics.IsLittleO.{0, u_1, 0} (E := E) (F := ℝ) (𝓝 z.re)
    (fun (x : ℝ) ↦ (∫ (t : ℝ) in z.re..x, f ((↑t : ℂ) + (↑z.im : ℂ) * I)) - (x - z.re) • f z) fun (x : ℝ) ↦ x - z.re

Tactic:
simpa using intervalIntegral.integral_hasDerivAt_right int1 int2 int3 |>.isLittleO

Premises used: HasDerivAt.isLittleO, intervalIntegral.integral_hasDerivAt_right
-- 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 : ℂ) ↦ ∫ (y : ℝ) in z.im..w.im, f ((↑w.re : ℂ) + (↑y : ℂ) * I) - f z) fun (w : ℂ) ↦ w - z
⊢ Eq.{max (u_1 + 1) 1} (α := (w : ℂ) → E)
    (fun (w : ℂ) ↦ (∫ (y : ℝ) in z.im..w.im, f ((↑w.re : ℂ) + (↑y : ℂ) * I)) - (w - z).im • f z) fun (w : ℂ) ↦
    HSub.hSub (α := E) (∫ (y : ℝ) in z.im..w.im, f ((↑w.re : ℂ) + (↑y : ℂ) * I)) (∫ (x : ℝ) in z.im..w.im, 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
this :
  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
⊢ Filter.EventuallyEq.{0, u_1} (β := E) (𝓝 z)
    (fun (w : ℂ) ↦
      HSub.hSub (α := E) (∫ (y : ℝ) in z.im..w.im, f ((↑w.re : ℂ) + (↑y : ℂ) * I)) (∫ (x : ℝ) in z.im..w.im, f z))
    fun (w : ℂ) ↦ ∫ (y : ℝ) in z.im..w.im, f ((↑w.re : ℂ) + (↑y : ℂ) * I) - 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
this :
  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
⊢ 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:
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
this :
  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
_ :
  Filter.EventuallyEq.{0, u_1} (β := E) (𝓝 z)
    (fun (w : ℂ) ↦
      HSub.hSub (α := E) (∫ (y : ℝ) in z.im..w.im, f ((↑w.re : ℂ) + (↑y : ℂ) * I)) (∫ (x : ℝ) in z.im..w.im, f z))
    fun (w : ℂ) ↦ ∫ (y : ℝ) in z.im..w.im, f ((↑w.re : ℂ) + (↑y : ℂ) * I) - f z
⊢ 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

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

Premises used: HMul.hMul, Complex.im, HSub.hSub, intervalIntegral, nhds, Complex.ofReal, MeasureTheory.MeasureSpace.volume, HAdd.hAdd, 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
this :
  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
⊢ r - dist z c > 0

Tactic:
simpa using 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 : ℂ) ↦ ∫ (y : ℝ) in z.im..w.im, f ((↑w.re : ℂ) + (↑y : ℂ) * I) - f z) fun (w : ℂ) ↦ w - z
refine :
  ∀ (w : ℂ) (hw : w ∈ ball z (r - dist z c)),
    Eq.{u_1 + 1} (α := E)
      ((fun (w : ℂ) ↦
          HSub.hSub (α := E) (∫ (y : ℝ) in z.im..w.im, f ((↑w.re : ℂ) + (↑y : ℂ) * I)) (∫ (x : ℝ) in z.im..w.im, f z))
        w)
      ((fun (w : ℂ) ↦ (∫ (y : ℝ) in z.im..w.im, f ((↑w.re : ℂ) + (↑y : ℂ) * I) - f z : E)) w)
⊢ Filter.EventuallyEq.{0, u_1} (β := E) (𝓝 z)
    (fun (w : ℂ) ↦
      HSub.hSub (α := E) (∫ (y : ℝ) in z.im..w.im, f ((↑w.re : ℂ) + (↑y : ℂ) * I)) (∫ (x : ℝ) in z.im..w.im, f z))
    fun (w : ℂ) ↦ ∫ (y : ℝ) in z.im..w.im, f ((↑w.re : ℂ) + (↑y : ℂ) * I) - f z

Tactic:
refine eventually_nhds_iff_ball.mpr ⟨r - dist z c, by simpa using hz, fun w hw ↦ ?_⟩

Premises used: Iff.mpr, HSub.hSub, And.intro, Exists.intro, Metric.eventually_nhds_iff_ball, Dist.dist
-- 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 : ℂ) ↦ ∫ (y : ℝ) in z.im..w.im, f ((↑w.re : ℂ) + (↑y : ℂ) * I) - f z) fun (w : ℂ) ↦ w - z
w : ℂ
hw : w ∈ ball z (r - dist z c)
⊢ ContinuousOn (Y := ℂ) (fun (y : ℝ) ↦ (↑w.re : ℂ) + (↑y : ℂ) * I) [[z.im, w.im]]

Tactic:
fun_prop
-- 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 : ℂ) ↦ ∫ (y : ℝ) in z.im..w.im, f ((↑w.re : ℂ) + (↑y : ℂ) * I) - f z) fun (w : ℂ) ↦ w - z
w : ℂ
hw : w ∈ ball z (r - dist z c)
⊢ Eq.{u_1 + 1} (α := E)
    ((fun (w : ℂ) ↦
        HSub.hSub (α := E) (∫ (y : ℝ) in z.im..w.im, f ((↑w.re : ℂ) + (↑y : ℂ) * I)) (∫ (x : ℝ) in z.im..w.im, f z))
      w)
    ((fun (w : ℂ) ↦ (∫ (y : ℝ) in z.im..w.im, f ((↑w.re : ℂ) + (↑y : ℂ) * I) - f z : E)) w)

Tactic:
exact (intervalIntegral.integral_sub
      ((f_cont.mono (mem_ball_of_map_im_aux₂ hw)).comp (by fun_prop)
        (mapsTo_image _ _)).intervalIntegrable intervalIntegrable_const).symm

Premises used: Set.mapsTo_image, ContinuousOn.comp, intervalIntegral.integral_sub, intervalIntegrable_const, _private.0.Complex.mem_ball_of_map_im_aux₂, ContinuousOn.mono, ContinuousOn.intervalIntegrable, Eq.symm
-- 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
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
⊢ 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

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
-- 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
rw : Filter.Tendsto f (𝓝 z) (𝓝 (f z))
⊢ Asymptotics.IsLittleO.{0, u_1, 0} (E := E) (F := ℝ) (𝓝 z) (fun (w : ℂ) ↦ f w - f z) fun (x : ℂ) ↦ 1

Tactic:
rw [Asymptotics.isLittleO_one_iff, tendsto_sub_nhds_zero_iff]

Premises used: Asymptotics.isLittleO_one_iff, tendsto_sub_nhds_zero_iff