awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Complex.HasPrimitives
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
hg' : DifferentiableOn ℂ g U
⊢ DifferentiableOn ℂ f U

Tactic:
exact (differentiableOn_congr <| fun z hz ↦ (hg z hz).deriv).mp <| hg'.deriv hU

Premises used: DifferentiableOn.deriv, HasDerivAt.deriv, Iff.mp, differentiableOn_congr
-- 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)
⊢ 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
f_cont : ContinuousOn f (ball c r)
z : ℂ
hz : z ∈ ball c r
hf : IsConservativeOn f (ball c r)
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
⊢ ∀ᶠ (w : ℂ) in 𝓝 z, 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 ↦ ?_⟩

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
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))
⊢ r - dist z c + dist z c ≤ r

Tactic:
simp
-- 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))
⊢ 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)
-- 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 ∈ ball c r

Tactic:
have w_mem : w ∈ ball c r := mem_of_subset_of_mem z_ball w_in_z_ball
-- 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
a₁ a₂ b : ℝ
ha₁ : (↑a₁ : ℂ) + (↑b : ℂ) * I ∈ ball c r
ha₂ : (↑a₂ : ℂ) + (↑b : ℂ) * I ∈ ball c r
⊢ ContinuousOn (Y := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) + (↑b : ℂ) * I) [[a₁, a₂]]

Tactic:
fun_prop
-- 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
⊢ ∀ (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
-- 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₂
a b₁ b₂ : ℝ
hb₁ : (↑a : ℂ) + (↑b₁ : ℂ) * I ∈ ball c r
hb₂ : (↑a : ℂ) + (↑b₂ : ℂ) * I ∈ ball c r
⊢ ContinuousOn (Y := ℂ) (fun (y : ℝ) ↦ (↑a : ℂ) + (↑y : ℂ) * I) [[b₁, b₂]]

Tactic:
fun_prop
-- 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₂
⊢ ∀ (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
-- 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₂
hab : IntervalIntegrable.{u_1} (ε := E) (fun (x : ℝ) ↦ f ((↑x : ℂ) + (↑c.im : ℂ) * I)) volume c.re z.re
hbc : IntervalIntegrable.{u_1} (ε := E) (fun (x : ℝ) ↦ f ((↑x : ℂ) + (↑c.im : ℂ) * I)) volume z.re w.re
⊢ I₁ = I₃ + I₇

Tactic:
rw [intervalIntegral.integral_add_adjacent_intervals]

Premises used: intervalIntegral.integral_add_adjacent_intervals
-- 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₂
hab : (↑c.re : ℂ) + (↑c.im : ℂ) * I ∈ ball c r
hab₁ : (↑z.re : ℂ) + (↑c.im : ℂ) * I ∈ ball c r
⊢ IntervalIntegrable.{u_1} (ε := E) (fun (x : ℝ) ↦ f ((↑x : ℂ) + (↑c.im : ℂ) * I)) volume c.re z.re

Tactic:
apply integrableHoriz
-- 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₂
hbc : (↑z.re : ℂ) + (↑c.im : ℂ) * I ∈ ball c r
hbc₁ : (↑w.re : ℂ) + (↑c.im : ℂ) * I ∈ ball c r
⊢ IntervalIntegrable.{u_1} (ε := E) (fun (x : ℝ) ↦ f ((↑x : ℂ) + (↑c.im : ℂ) * I)) volume z.re w.re

Tactic:
apply integrableHoriz
-- 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₂
⊢ (↑c.re : ℂ) + (↑c.im : ℂ) * I ∈ ball c r

Tactic:
re_add_im_mul_mem_ball <| mem_ball_self (pos_of_mem_ball hz)

Premises used: _private.0.Complex.re_add_im_mul_mem_ball, Metric.mem_ball_self, Metric.pos_of_mem_ball
-- 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₂
⊢ (↑c.re : ℂ) + (↑c.im : ℂ) * I ∈ ball c r

Tactic:
exact re_add_im_mul_mem_ball <| mem_ball_self (pos_of_mem_ball hz)

Premises used: _private.0.Complex.re_add_im_mul_mem_ball, Metric.mem_ball_self, Metric.pos_of_mem_ball
-- 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₂
⊢ (↑z.re : ℂ) + (↑c.im : ℂ) * I ∈ ball c r

Tactic:
re_add_im_mul_mem_ball hz

Premises used: _private.0.Complex.re_add_im_mul_mem_ball
-- 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₂
⊢ (↑z.re : ℂ) + (↑c.im : ℂ) * I ∈ ball c r

Tactic:
exact re_add_im_mul_mem_ball hz

Premises used: _private.0.Complex.re_add_im_mul_mem_ball
-- 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₂
⊢ (↑w.re : ℂ) + (↑c.im : ℂ) * I ∈ ball c r

Tactic:
re_add_im_mul_mem_ball w_mem

Premises used: _private.0.Complex.re_add_im_mul_mem_ball