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
f : ℂ → E
U : Set ℂ
hf : DifferentiableOn ℂ f U
z w : ℂ
hzw : z.Rectangle w ⊆ U
⊢ z.wedgeIntegral w f = -w.wedgeIntegral z f
have rw : HSub.hSub (α := E) (∫ (x : ℝ) in z.re..w.re, f ((↑x : ℂ) + (↑z.im : ℂ) * I))
        (∫ (x : ℝ) in z.re..w.re, f ((↑x : ℂ) + (↑w.im : ℂ) * I)) +
      HSMul.hSMul (β := E) I (∫ (y : ℝ) in z.im..w.im, f ((↑w.re : ℂ) + (↑y : ℂ) * I)) -
    HSMul.hSMul (β := E) I (∫ (y : ℝ) in z.im..w.im, f ((↑z.re : ℂ) + (↑y : ℂ) * I)) =
  0
Tactic: rw [← add_eq_zero_iff_eq_neg, wedgeIntegral_add_wedgeIntegral_eq]
-- 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
hf : IsExactOn f U
⊢ DifferentiableOn ℂ f U
have obtain : ∀ (g : ℂ → E) (hg : ∀ z ∈ U, HasDerivAt g (f z) z), DifferentiableOn ℂ f U
Tactic: obtain ⟨g, hg⟩ := hf
Cleared hypotheses: hf
-- 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
g : ℂ → E
hg : ∀ z ∈ U, HasDerivAt g (f z) z
⊢ DifferentiableOn ℂ f U
have hg' : DifferentiableOn ℂ g U
Tactic: have hg' : DifferentiableOn ℂ g U := fun z hz ↦ (hg z hz).differentiableAt.differentiableWithinAt
-- 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 : ℂ) in 𝓝 z, c.wedgeIntegral w f - c.wedgeIntegral z f = z.wedgeIntegral w f
have refine : ∀ (w : ℂ) (w_in_z_ball : w ∈ ball z (r - dist z c)), c.wedgeIntegral w f - c.wedgeIntegral z f = z.wedgeIntegral w f
Tactic: refine eventually_nhds_iff_ball.mpr ⟨r - dist z c, by simpa using hz, fun w 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))
⊢ c.wedgeIntegral w f - c.wedgeIntegral z f = z.wedgeIntegral w f
have z_ball : ball z (r - dist z c) ⊆ ball c r
Tactic: have z_ball : ball z (r - dist z c) ⊆ ball c r := ball_subset_ball' (by simp)
-- 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
⊢ c.wedgeIntegral w f - c.wedgeIntegral z f = z.wedgeIntegral w f
have w_mem : w ∈ ball c r
Tactic: have w_mem : w ∈ ball c r := mem_of_subset_of_mem z_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
⊢ c.wedgeIntegral w f - c.wedgeIntegral z f = z.wedgeIntegral w f
have 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₂
Tactic: have integrableHoriz (a₁ a₂ b : ℝ) (ha₁ : a₁ + b * I ∈ ball c r) (ha₂ : a₂ + b * I ∈ ball c r) :
      IntervalIntegrable (fun x ↦ f (x + b * I)) volume a₁ a₂ :=
    ((f_cont.mono (mem_ball_of_map_re_aux ha₁ ha₂)).comp (by fun_prop)
      (mapsTo_image _ _)).intervalIntegrable
-- 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₂
⊢ c.wedgeIntegral w f - c.wedgeIntegral z f = z.wedgeIntegral w f
have 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₂
Tactic: have integrableVert (a b₁ b₂ : ℝ) (hb₁ : a + b₁ * I ∈ ball c r) (hb₂ : a + b₂ * I ∈ ball c r) :
      IntervalIntegrable (fun y ↦ f (a + y * I)) volume b₁ b₂ :=
    ((f_cont.mono (mem_ball_of_map_im_aux₁ hb₁ hb₂)).comp (by fun_prop)
      (mapsTo_image _ _)).intervalIntegrable
-- 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₂
⊢ I₁ = I₃ + I₇
have hab : IntervalIntegrable.{u_1} (ε := E) (fun (x : ℝ) ↦ f ((↑x : ℂ) + (↑c.im : ℂ) * I)) volume c.re z.re
Tactic: rw [intervalIntegral.integral_add_adjacent_intervals]
-- 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₂
hab : IntervalIntegrable.{u_1} (ε := E) (fun (x : ℝ) ↦ f ((↑x : ℂ) + (↑c.im : ℂ) * I)) volume c.re z.re
⊢ I₁ = I₃ + I₇
have hbc : IntervalIntegrable.{u_1} (ε := E) (fun (x : ℝ) ↦ f ((↑x : ℂ) + (↑c.im : ℂ) * I)) volume z.re w.re
Tactic: rw [intervalIntegral.integral_add_adjacent_intervals]
-- 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₂
⊢ IntervalIntegrable.{u_1} (ε := E) (fun (x : ℝ) ↦ f ((↑x : ℂ) + (↑c.im : ℂ) * I)) volume c.re z.re
have hab : (↑c.re : ℂ) + (↑c.im : ℂ) * I ∈ ball c r
Tactic: apply integrableHoriz
-- 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₂
hab : (↑c.re : ℂ) + (↑c.im : ℂ) * I ∈ ball c r
⊢ IntervalIntegrable.{u_1} (ε := E) (fun (x : ℝ) ↦ f ((↑x : ℂ) + (↑c.im : ℂ) * I)) volume c.re z.re
have hab₁ : (↑z.re : ℂ) + (↑c.im : ℂ) * I ∈ ball c r
Tactic: apply integrableHoriz
-- 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₂
⊢ IntervalIntegrable.{u_1} (ε := E) (fun (x : ℝ) ↦ f ((↑x : ℂ) + (↑c.im : ℂ) * I)) volume z.re w.re
have hbc : (↑z.re : ℂ) + (↑c.im : ℂ) * I ∈ ball c r
Tactic: apply integrableHoriz
-- 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₂
hbc : (↑z.re : ℂ) + (↑c.im : ℂ) * I ∈ ball c r
⊢ IntervalIntegrable.{u_1} (ε := E) (fun (x : ℝ) ↦ f ((↑x : ℂ) + (↑c.im : ℂ) * I)) volume z.re w.re
have hbc₁ : (↑w.re : ℂ) + (↑c.im : ℂ) * I ∈ ball c r
Tactic: apply integrableHoriz
-- 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₂
⊢ 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 [intervalIntegral.integral_add_adjacent_intervals] <;> apply integrableHoriz
    · exact re_add_im_mul_mem_ball <| mem_ball_self (pos_of_mem_ball hz)
    · exact re_add_im_mul_mem_ball hz
    · exact re_add_im_mul_mem_ball hz
    · exact re_add_im_mul_mem_ball w_mem
-- 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₇
⊢ I₂ = I₈ + I₆
have hab : IntervalIntegrable.{u_1} (ε := E) (fun (y : ℝ) ↦ f ((↑w.re : ℂ) + (↑y : ℂ) * I)) volume c.im z.im
Tactic: rw [← smul_add, intervalIntegral.integral_add_adjacent_intervals]
-- 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 : IntervalIntegrable.{u_1} (ε := E) (fun (y : ℝ) ↦ f ((↑w.re : ℂ) + (↑y : ℂ) * I)) volume c.im z.im
⊢ I₂ = I₈ + I₆
have hbc : IntervalIntegrable.{u_1} (ε := E) (fun (y : ℝ) ↦ f ((↑w.re : ℂ) + (↑y : ℂ) * I)) volume z.im w.im
Tactic: rw [← smul_add, intervalIntegral.integral_add_adjacent_intervals]