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
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₇
⊢ IntervalIntegrable.{u_1} (ε := E) (fun (y : ℝ) ↦ f ((↑w.re : ℂ) + (↑y : ℂ) * I)) volume c.im z.im
have hab : (↑w.re : ℂ) + (↑c.im : ℂ) * I ∈ ball c r
Tactic: apply integrableVert
-- 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
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₇
hab : (↑w.re : ℂ) + (↑c.im : ℂ) * I ∈ ball c r
⊢ IntervalIntegrable.{u_1} (ε := E) (fun (y : ℝ) ↦ f ((↑w.re : ℂ) + (↑y : ℂ) * I)) volume c.im z.im
have hab₁ : (↑w.re : ℂ) + (↑z.im : ℂ) * I ∈ ball c r
Tactic: apply integrableVert
-- 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
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₇
⊢ IntervalIntegrable.{u_1} (ε := E) (fun (y : ℝ) ↦ f ((↑w.re : ℂ) + (↑y : ℂ) * I)) volume z.im w.im
have hbc : (↑w.re : ℂ) + (↑z.im : ℂ) * I ∈ ball c r
Tactic: apply integrableVert
-- 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
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₇
hbc : (↑w.re : ℂ) + (↑z.im : ℂ) * I ∈ ball c r
⊢ IntervalIntegrable.{u_1} (ε := E) (fun (y : ℝ) ↦ f ((↑w.re : ℂ) + (↑y : ℂ) * I)) volume z.im w.im
have hbc₁ : (↑w.re : ℂ) + (↑w.im : ℂ) * I ∈ ball c r
Tactic: apply integrableVert
-- 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
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₇
⊢ c.wedgeIntegral w f - c.wedgeIntegral z f = z.wedgeIntegral w f
have hI₂ : I₂ = I₈ + I₆
Tactic: have hI₂ : I₂ = I₈ + I₆ := by
    rw [← smul_add, intervalIntegral.integral_add_adjacent_intervals] <;> apply integrableVert
    · exact re_add_im_mul_mem_ball w_mem
    · exact mem_of_subset_of_mem z_ball (re_add_im_mul_mem_ball w_in_z_ball)
    · exact mem_of_subset_of_mem z_ball (re_add_im_mul_mem_ball w_in_z_ball)
    · simpa using w_mem
-- 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
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
have wzInBall : (↑w.re : ℂ) + (↑z.im : ℂ) * I ∈ ball c r
Tactic: 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)
-- 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
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
⊢ I₇ - I₅ + I₈ - I₄ = 0
have wcInBall : (↑w.re : ℂ) + (↑c.im : ℂ) * I ∈ ball c r
Tactic: have wcInBall : w.re + c.im * I ∈ ball c r := re_add_im_mul_mem_ball w_mem
-- 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
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
⊢ I₇ - I₅ + I₈ - I₄ = 0
have hU : ((↑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)
-- 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
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₆
⊢ c.wedgeIntegral w f - c.wedgeIntegral z f = z.wedgeIntegral w f
have hI₀ : 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
-- 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 : ℂ) ↦ (∫ (x : ℝ) in z.re..w.re, f ((↑x : ℂ) + (↑z.im : ℂ) * I)) - (w - z).re • f z) fun (w : ℂ) ↦ w - z
have 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
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
-- 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
r₁ : ℝ := r - dist z c
⊢ 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
have r₁_pos : 0 < r₁
Tactic: have r₁_pos : 0 < r₁ := by simpa only [mem_ball, sub_pos, r₁] using hz
-- 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
r₁ : ℝ := r - dist z c
r₁_pos : 0 < r₁
s : Set ℝ := Ioo (z.re - r₁) (z.re + r₁)
⊢ 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
have zRe_mem_s : z.re ∈ s
Tactic: have zRe_mem_s : z.re ∈ s := by simp [s, r₁_pos]
-- 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
r₁ : ℝ := r - dist z c
r₁_pos : 0 < r₁
s : Set ℝ := Ioo (z.re - r₁) (z.re + r₁)
zRe_mem_s : z.re ∈ s
⊢ 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
have f_contOn : 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
-- 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
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
⊢ 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
have int1 : 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
-- 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
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
⊢ 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
have int2 : 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
-- 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
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
⊢ 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
have int3 : 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
-- 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 : ℂ) ↦ ∫ (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
have _ : 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: 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
-- 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 : ℂ) ↦ ∫ (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
have 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)
Tactic: refine eventually_nhds_iff_ball.mpr ⟨r - dist z c, by simpa using hz, fun w hw ↦ ?_⟩