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

Tactic:
exact re_add_im_mul_mem_ball w_mem

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

Tactic:
rw [← smul_add, intervalIntegral.integral_add_adjacent_intervals]

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

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

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

Tactic:
exact re_add_im_mul_mem_ball w_mem

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₂
hI₁ : I₁ = I₃ + I₇
⊢ (↑w.re : ℂ) + (↑z.im : ℂ) * I ∈ ball c r

Tactic:
mem_of_subset_of_mem z_ball (re_add_im_mul_mem_ball w_in_z_ball)

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

Tactic:
exact mem_of_subset_of_mem z_ball (re_add_im_mul_mem_ball w_in_z_ball)

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

Tactic:
simpa using w_mem
-- 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₇
⊢ 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
-- 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₆
⊢ (↑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)
-- 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
⊢ (↑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
-- 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).re : ℂ) + (↑((↑w.re : ℂ) + (↑z.im : ℂ) * I).im : ℂ) * I ∈ ball c r

Tactic:
simpa using hz