awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Complex.Harmonic.Poisson (hypothesis)
Goal:
f : ℂ → ℝ
c w : ℂ
R : ℝ
hf : HarmonicOnNhd f (closedBall c R)
hw : w ∈ ball c R
e : ℝ
h₁e : 0 < e
h₂e : ball c (e + R) ⊆ {x : ℂ | HarmonicAt f x}
F : ℂ → ℂ
h₁F : AnalyticOnNhd ℂ F (ball c (e + R))
h₂F : Set.EqOn (fun (z : ℂ) ↦ (F z).re) f (ball c (e + R))
h₃F : DifferentiableOn ℂ F (closure (ball c R))
h₄F :
  Set.EqOn (re ∘ herglotzRieszKernel c w • f)
    (Function.comp (β := ℂ) (⇑reCLM : (a : ℂ) → ℝ) fun (z : ℂ) ↦ ((z - c + (w - c)) / (z - c - (w - c))).re • F z)
    (sphere c R)
⊢ circleAverage (re ∘ herglotzRieszKernel c w • f) c R = f w
have h₄F₁ : Set.EqOn (re ∘ herglotzRieszKernel c w • f)
  (Function.comp (β := ℂ) (⇑reCLM : (a : ℂ) → ℝ) fun (z : ℂ) ↦ ((z - c + (w - c)) / (z - c - (w - c))).re • F z)
  (sphere c |R|)
Tactic: rw [← abs_of_pos (pos_of_mem_ball hw)] at h₄F
Cleared hypotheses: h₄F
-- Lean 4 proof step from Mathlib.Analysis.Complex.Harmonic.Poisson (goal)
Goal:
f : ℂ → ℝ
c w : ℂ
R : ℝ
hf : HarmonicOnNhd f (closedBall c R)
hw : w ∈ ball c R
e : ℝ
h₁e : 0 < e
h₂e : ball c (e + R) ⊆ {x : ℂ | HarmonicAt f x}
F : ℂ → ℂ
h₁F : AnalyticOnNhd ℂ F (ball c (e + R))
h₂F : Set.EqOn (fun (z : ℂ) ↦ (F z).re) f (ball c (e + R))
h₃F : DifferentiableOn ℂ F (closure (ball c R))
h₄F :
  Set.EqOn (re ∘ herglotzRieszKernel c w • f)
    (Function.comp (β := ℂ) (⇑reCLM : (a : ℂ) → ℝ) fun (z : ℂ) ↦ ((z - c + (w - c)) / (z - c - (w - c))).re • F z)
    (sphere c |R|)
⊢ circleAverage (re ∘ herglotzRieszKernel c w • f) c R = f w
have rw : (reCLM : (a : ℂ) → ℝ) (F w) = f w
Tactic: rw [circleAverage_congr_sphere h₄F, reCLM.circleAverage_comp_comm,
    h₃F.diffContOnCl.circleAverage_re_herglotzRieszKernel_smul' hw]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Harmonic.Poisson (goal)
Goal:
f : ℂ → ℝ
c w : ℂ
R : ℝ
hf : HarmonicOnNhd f (closedBall c R)
hw : w ∈ ball c R
e : ℝ
h₁e : 0 < e
h₂e : ball c (e + R) ⊆ {x : ℂ | HarmonicAt f x}
F : ℂ → ℂ
h₁F : AnalyticOnNhd ℂ F (ball c (e + R))
h₂F : Set.EqOn (fun (z : ℂ) ↦ (F z).re) f (ball c (e + R))
h₃F : DifferentiableOn ℂ F (closure (ball c R))
h₄F :
  Set.EqOn (re ∘ herglotzRieszKernel c w • f)
    (Function.comp (β := ℂ) (⇑reCLM : (a : ℂ) → ℝ) fun (z : ℂ) ↦ ((z - c + (w - c)) / (z - c - (w - c))).re • F z)
    (sphere c |R|)
rw : (reCLM : (a : ℂ) → ℝ) (F w) = f w
⊢ circleAverage (re ∘ herglotzRieszKernel c w • f) c R = f w
have rw₁ : CircleIntegrable (E := ℂ) (fun (z : ℂ) ↦ ((z - c + (w - c)) / (z - c - (w - c))).re • F z) c R
Tactic: rw [circleAverage_congr_sphere h₄F, reCLM.circleAverage_comp_comm,
    h₃F.diffContOnCl.circleAverage_re_herglotzRieszKernel_smul' hw]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Harmonic.Poisson (goal)
Goal:
f : ℂ → ℝ
c w : ℂ
R : ℝ
hf : HarmonicOnNhd f (closedBall c R)
hw : w ∈ ball c R
e : ℝ
h₁e : 0 < e
h₂e : ball c (e + R) ⊆ {x : ℂ | HarmonicAt f x}
F : ℂ → ℂ
h₁F : AnalyticOnNhd ℂ F (ball c (e + R))
h₂F : Set.EqOn (fun (z : ℂ) ↦ (F z).re) f (ball c (e + R))
h₃F : DifferentiableOn ℂ F (closure (ball c R))
h₄F :
  Set.EqOn (re ∘ herglotzRieszKernel c w • f)
    (Function.comp (β := ℂ) (⇑reCLM : (a : ℂ) → ℝ) fun (z : ℂ) ↦ ((z - c + (w - c)) / (z - c - (w - c))).re • F z)
    (sphere c |R|)
⊢ (reCLM : (a : ℂ) → ℝ) (F w) = f w
have a : w ∈ ball c (e + R)
Tactic: apply h₂F
-- Lean 4 proof step from Mathlib.Analysis.Complex.Harmonic.Poisson (goal)
Goal:
f : ℂ → ℝ
c w : ℂ
R : ℝ
hf : HarmonicOnNhd f (closedBall c R)
hw : w ∈ ball c R
e : ℝ
h₁e : 0 < e
h₂e : ball c (e + R) ⊆ {x : ℂ | HarmonicAt f x}
F : ℂ → ℂ
h₁F : AnalyticOnNhd ℂ F (ball c (e + R))
h₂F : Set.EqOn (fun (z : ℂ) ↦ (F z).re) f (ball c (e + R))
h₃F : DifferentiableOn ℂ F (closure (ball c R))
h₄F :
  Set.EqOn (re ∘ herglotzRieszKernel c w • f)
    (Function.comp (β := ℂ) (⇑reCLM : (a : ℂ) → ℝ) fun (z : ℂ) ↦ ((z - c + (w - c)) / (z - c - (w - c))).re • F z)
    (sphere c |R|)
⊢ CircleIntegrable (E := ℂ) (fun (z : ℂ) ↦ ((z - c + (w - c)) / (z - c - (w - c))).re • F z) c R
have apply : ContinuousOn (Y := ℝ) (fun (x : ℂ) ↦ ((x - c + (w - c)) / (x - c - (w - c))).re) (sphere c |R|)
Tactic: apply (ContinuousOn.smul _ _).circleIntegrable'
-- Lean 4 proof step from Mathlib.Analysis.Complex.Harmonic.Poisson (goal)
Goal:
f : ℂ → ℝ
c w : ℂ
R : ℝ
hf : HarmonicOnNhd f (closedBall c R)
hw : w ∈ ball c R
e : ℝ
h₁e : 0 < e
h₂e : ball c (e + R) ⊆ {x : ℂ | HarmonicAt f x}
F : ℂ → ℂ
h₁F : AnalyticOnNhd ℂ F (ball c (e + R))
h₂F : Set.EqOn (fun (z : ℂ) ↦ (F z).re) f (ball c (e + R))
h₃F : DifferentiableOn ℂ F (closure (ball c R))
h₄F :
  Set.EqOn (re ∘ herglotzRieszKernel c w • f)
    (Function.comp (β := ℂ) (⇑reCLM : (a : ℂ) → ℝ) fun (z : ℂ) ↦ ((z - c + (w - c)) / (z - c - (w - c))).re • F z)
    (sphere c |R|)
apply : ContinuousOn (Y := ℝ) (fun (x : ℂ) ↦ ((x - c + (w - c)) / (x - c - (w - c))).re) (sphere c |R|)
⊢ CircleIntegrable (E := ℂ) (fun (z : ℂ) ↦ ((z - c + (w - c)) / (z - c - (w - c))).re • F z) c R
have apply₁ : ContinuousOn F (sphere c |R|)
Tactic: apply (ContinuousOn.smul _ _).circleIntegrable'
-- Lean 4 proof step from Mathlib.Analysis.Complex.Harmonic.Poisson (goal)
Goal:
f : ℂ → ℝ
c w : ℂ
R : ℝ
hf : HarmonicOnNhd f (closedBall c R)
hw : w ∈ ball c R
e : ℝ
h₁e : 0 < e
h₂e : ball c (e + R) ⊆ {x : ℂ | HarmonicAt f x}
F : ℂ → ℂ
h₁F : AnalyticOnNhd ℂ F (ball c (e + R))
h₂F : Set.EqOn (fun (z : ℂ) ↦ (F z).re) f (ball c (e + R))
h₃F : DifferentiableOn ℂ F (closure (ball c R))
h₄F :
  Set.EqOn (re ∘ herglotzRieszKernel c w • f)
    (Function.comp (β := ℂ) (⇑reCLM : (a : ℂ) → ℝ) fun (z : ℂ) ↦ ((z - c + (w - c)) / (z - c - (w - c))).re • F z)
    (sphere c |R|)
⊢ ContinuousOn (Y := ℝ) (fun (x : ℂ) ↦ ((x - c + (w - c)) / (x - c - (w - c))).re) (sphere c |R|)
have apply : sphere c |R| ⊆ {z : ℂ | ‖z - c‖ ∈ Set.Ioc ‖w - c‖ R}
Tactic: apply (continuousOn_herglotz_riesz hw).mono
-- Lean 4 proof step from Mathlib.Analysis.Complex.Harmonic.Poisson (goal)
Goal:
f : ℂ → ℝ
c w : ℂ
R : ℝ
hf : HarmonicOnNhd f (closedBall c R)
hw : w ∈ ball c R
e : ℝ
h₁e : 0 < e
h₂e : ball c (e + R) ⊆ {x : ℂ | HarmonicAt f x}
F : ℂ → ℂ
h₁F : AnalyticOnNhd ℂ F (ball c (e + R))
h₂F : Set.EqOn (fun (z : ℂ) ↦ (F z).re) f (ball c (e + R))
h₃F : DifferentiableOn ℂ F (closure (ball c R))
h₄F :
  Set.EqOn (re ∘ herglotzRieszKernel c w • f)
    (Function.comp (β := ℂ) (⇑reCLM : (a : ℂ) → ℝ) fun (z : ℂ) ↦ ((z - c + (w - c)) / (z - c - (w - c))).re • F z)
    (sphere c |R|)
⊢ ContinuousOn F (sphere c |R|)
have apply : sphere c |R| ⊆ ball c (e + R)
Tactic: apply (h₁F.mono _).continuousOn (𝕜 := ℂ)
-- Lean 4 proof step from Mathlib.Analysis.Complex.Harmonic.Poisson (goal)
Goal:
f : ℂ → ℝ
c w : ℂ
R : ℝ
hf : HarmonicContOnCl f (ball c R)
hw : w ∈ ball c R
⊢ circleAverage (re ∘ herglotzRieszKernel c w • f) c R = f w
have h₁f : ContinuousOn (circleAverage (re ∘ herglotzRieszKernel c w • f) c) (Set.Ioc ‖w - c‖ R)
Tactic: apply ContinuousOn.eq_of_eqOn_Ioo (r := ‖w - c‖)
-- Lean 4 proof step from Mathlib.Analysis.Complex.Harmonic.Poisson (goal)
Goal:
f : ℂ → ℝ
c w : ℂ
R : ℝ
hf : HarmonicContOnCl f (ball c R)
hw : w ∈ ball c R
h₁f : ContinuousOn (circleAverage (re ∘ herglotzRieszKernel c w • f) c) (Set.Ioc ‖w - c‖ R)
⊢ circleAverage (re ∘ herglotzRieszKernel c w • f) c R = f w
have hR : ‖w - c‖ < R
Tactic: apply ContinuousOn.eq_of_eqOn_Ioo (r := ‖w - c‖)
-- Lean 4 proof step from Mathlib.Analysis.Complex.Harmonic.Poisson (goal)
Goal:
f : ℂ → ℝ
c w : ℂ
R : ℝ
hf : HarmonicContOnCl f (ball c R)
hw : w ∈ ball c R
h₁f : ContinuousOn (circleAverage (re ∘ herglotzRieszKernel c w • f) c) (Set.Ioc ‖w - c‖ R)
hR : ‖w - c‖ < R
⊢ circleAverage (re ∘ herglotzRieszKernel c w • f) c R = f w
have h₂f : Set.EqOn (circleAverage (re ∘ herglotzRieszKernel c w • f) c) (fun (x : ℝ) ↦ f w) (Set.Ioo ‖w - c‖ R)
Tactic: apply ContinuousOn.eq_of_eqOn_Ioo (r := ‖w - c‖)
-- Lean 4 proof step from Mathlib.Analysis.Complex.Harmonic.Poisson (goal)
Goal:
f : ℂ → ℝ
c w : ℂ
R : ℝ
hf : HarmonicContOnCl f (ball c R)
hw : w ∈ ball c R
⊢ ContinuousOn (circleAverage (re ∘ herglotzRieszKernel c w • f) c) (Set.Ioc ‖w - c‖ R)
have h₁f : ContinuousOn (re ∘ herglotzRieszKernel c w • f) {z : ℂ | ‖z - c‖ ∈ Set.Ioc ‖w - c‖ R}
Tactic: apply ContinuousOn.circleAverage
-- Lean 4 proof step from Mathlib.Analysis.Complex.Harmonic.Poisson (goal)
Goal:
f : ℂ → ℝ
c w : ℂ
R : ℝ
hf : HarmonicContOnCl f (ball c R)
hw : w ∈ ball c R
h₁f : ContinuousOn (re ∘ herglotzRieszKernel c w • f) {z : ℂ | ‖z - c‖ ∈ Set.Ioc ‖w - c‖ R}
⊢ ContinuousOn (circleAverage (re ∘ herglotzRieszKernel c w • f) c) (Set.Ioc ‖w - c‖ R)
have h₁f₁ : ∀ r ∈ Set.Ioc ‖w - c‖ R, 0 ≤ r
Tactic: apply ContinuousOn.circleAverage
-- Lean 4 proof step from Mathlib.Analysis.Complex.Harmonic.Poisson (goal)
Goal:
f : ℂ → ℝ
c w : ℂ
R : ℝ
hf : HarmonicContOnCl f (ball c R)
hw : w ∈ ball c R
⊢ ContinuousOn (re ∘ herglotzRieszKernel c w • f) {z : ℂ | ‖z - c‖ ∈ Set.Ioc ‖w - c‖ R}
have h₁f : ContinuousOn (HSMul.hSMul (α := ℂ → ℝ) (re ∘ fun (z : ℂ) ↦ (z - c + (w - c)) / (z - c - (w - c))) f)
  {z : ℂ | ‖z - c‖ ∈ Set.Ioc ‖w - c‖ R}
Tactic: rw [herglotzRieszKernel_fun_def]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Harmonic.Poisson (goal)
Goal:
f : ℂ → ℝ
c w : ℂ
R : ℝ
hf : HarmonicContOnCl f (ball c R)
hw : w ∈ ball c R
⊢ ContinuousOn (HSMul.hSMul (α := ℂ → ℝ) (re ∘ fun (z : ℂ) ↦ (z - c + (w - c)) / (z - c - (w - c))) f)
    {z : ℂ | ‖z - c‖ ∈ Set.Ioc ‖w - c‖ R}
have apply : {z : ℂ | ‖z - c‖ ∈ Set.Ioc ‖w - c‖ R} ⊆ closure (ball c R)
Tactic: apply (continuousOn_herglotz_riesz hw).smul (hf.2.mono _)
-- Lean 4 proof step from Mathlib.Analysis.Complex.Harmonic.Poisson (goal)
Goal:
f : ℂ → ℝ
c w : ℂ
R : ℝ
hf : HarmonicContOnCl f (ball c R)
hw : w ∈ ball c R
r : ℝ
hr : r ∈ Set.Ioo ‖w - c‖ R
⊢ circleAverage (re ∘ herglotzRieszKernel c w • f) c r = (fun (x : ℝ) ↦ f w) r
have h₂f : f w = (fun (x : ℝ) ↦ f w) r
Tactic: rw [HarmonicOnNhd.circleAverage_re_herglotzRieszKernel_smul
      (hf.1.mono (closedBall_subset_ball hr.2)) (by grind [mem_ball_iff_norm])]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Harmonic.Poisson (goal)
Goal:
f : ℂ → ℝ
c w : ℂ
R : ℝ
hf : HarmonicOnNhd f (closedBall c R)
hw : w ∈ ball c R
⊢ circleAverage (poissonKernel c w • f) c R = f w
have rw : circleAverage (poissonKernel c w • f) c R = circleAverage (re ∘ herglotzRieszKernel c w • f) c R
Tactic: rw [← hf.circleAverage_re_herglotzRieszKernel_smul hw]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Harmonic.Poisson (goal)
Goal:
f : ℂ → ℝ
c w : ℂ
R : ℝ
hf : HarmonicContOnCl f (ball c R)
hw : w ∈ ball c R
⊢ circleAverage (poissonKernel c w • f) c R = f w
have rw : circleAverage (poissonKernel c w • f) c R = circleAverage (re ∘ herglotzRieszKernel c w • f) c R
Tactic: rw [← hf.circleAverage_re_herglotzRieszKernel_smul hw]
-- Lean 4 proof step from Mathlib.Analysis.Complex.HasPrimitives (goal)
Goal:
c z : ℂ
r : ℝ
hz : z ∈ ball c r
⊢ (↑z.re : ℂ) + (↑c.im : ℂ) * I ∈ ball c r
have suffices : dist ((↑z.re : ℂ) + (↑c.im : ℂ) * I) c ≤ dist z c
Tactic: suffices dist (z.re + c.im * I) c ≤ dist z c from lt_of_le_of_lt this hz
-- Lean 4 proof step from Mathlib.Analysis.Complex.HasPrimitives (goal)
Goal:
c z : ℂ
r : ℝ
hz : z ∈ ball c r
⊢ dist ((↑z.re : ℂ) + (↑c.im : ℂ) * I) c ≤ dist z c
have rw : HPow.hPow (β := ℕ) (((↑z.re : ℂ) + (↑c.im : ℂ) * I).re - c.re) 2 +
    HPow.hPow (β := ℕ) (((↑z.re : ℂ) + (↑c.im : ℂ) * I).im - c.im) 2 ≤
  HPow.hPow (β := ℕ) (z.re - c.re) 2 + HPow.hPow (β := ℕ) (z.im - c.im) 2
Tactic: rw [dist_eq_re_im, dist_eq_re_im, Real.le_sqrt (by positivity) (by positivity),
    Real.sq_sqrt (by positivity)]
-- Lean 4 proof step from Mathlib.Analysis.Complex.HasPrimitives (goal)
Goal:
c z : ℂ
r x : ℝ
r₁ : ℝ := r - dist z c
s : Set ℝ := Ioo (z.re - r₁) (z.re + r₁)
hx : x ∈ s
y : ℂ
yRe : y.re ∈ s
yIm : y.im = z.im
⊢ y ∈ ball z r₁
have rw : |y.re - z.re| < r₁
Tactic: rw [mem_ball, dist_eq_re_im, yIm, sub_self, zero_pow two_ne_zero, add_zero, Real.sqrt_sq_eq_abs]
-- Lean 4 proof step from Mathlib.Analysis.Complex.HasPrimitives (hypothesis)
Goal:
c z : ℂ
r x : ℝ
r₁ : ℝ := r - dist z c
s : Set ℝ := Ioo (z.re - r₁) (z.re + r₁)
hx : x ∈ s
⊢ (↑x : ℂ) + (↑z.im : ℂ) * I ∈ ball c r
have s_ball₁ : s ×ℂ {z.im} ⊆ ball z r₁
Tactic: have s_ball₁ : s ×ℂ {z.im} ⊆ ball z r₁ := by
    rintro y ⟨yRe : y.re ∈ s, yIm : y.im = z.im⟩
    rw [mem_ball, dist_eq_re_im, yIm, sub_self, zero_pow two_ne_zero, add_zero, Real.sqrt_sq_eq_abs]
    grind [abs_lt]
-- Lean 4 proof step from Mathlib.Analysis.Complex.HasPrimitives (goal)
Goal:
c z : ℂ
r x : ℝ
r₁ : ℝ := r - dist z c
s : Set ℝ := Ioo (z.re - r₁) (z.re + r₁)
hx : x ∈ s
s_ball₁ : s ×ℂ {z.im} ⊆ ball z r₁
⊢ (↑x : ℂ) + (↑z.im : ℂ) * I ∈ ball c r
have suffices : s ×ℂ {z.im} ⊆ ball c r
Tactic: suffices s ×ℂ {z.im} ⊆ ball c r from this <| by simp [mem_reProdIm, hx]
-- Lean 4 proof step from Mathlib.Analysis.Complex.HasPrimitives (goal)
Goal:
c z : ℂ
r y : ℝ
z_in_ball : z ∈ closedBall c r
y_in_I : y ∈ Ι c.im z.im
⊢ (↑z.re : ℂ) + (↑y : ℂ) * I ∈ closedBall c r
have refine : dist ((↑z.re : ℂ) + (↑y : ℂ) * I) c ≤ dist z c
Tactic: refine le_trans ?_ (mem_closedBall.mp z_in_ball)
-- Lean 4 proof step from Mathlib.Analysis.Complex.HasPrimitives (goal)
Goal:
c z : ℂ
r y : ℝ
z_in_ball : z ∈ closedBall c r
y_in_I : y ∈ Ι c.im z.im
⊢ dist ((↑z.re : ℂ) + (↑y : ℂ) * I) c ≤ dist z c
have rw : HPow.hPow (β := ℕ) (((↑z.re : ℂ) + (↑y : ℂ) * I).re - c.re) 2 +
    HPow.hPow (β := ℕ) (((↑z.re : ℂ) + (↑y : ℂ) * I).im - c.im) 2 ≤
  HPow.hPow (β := ℕ) (z.re - c.re) 2 + HPow.hPow (β := ℕ) (z.im - c.im) 2
Tactic: rw [dist_eq_re_im, dist_eq_re_im, Real.le_sqrt (by positivity) (by positivity),
    Real.sq_sqrt (by positivity)]
-- Lean 4 proof step from Mathlib.Analysis.Complex.HasPrimitives (goal)
Goal:
c z : ℂ
r y : ℝ
z_in_ball : z ∈ closedBall c r
y_in_I : y ∈ Ι c.im z.im
⊢ HPow.hPow (β := ℕ) (((↑z.re : ℂ) + (↑y : ℂ) * I).re - c.re) 2 +
      HPow.hPow (β := ℕ) (((↑z.re : ℂ) + (↑y : ℂ) * I).im - c.im) 2 ≤
    HPow.hPow (β := ℕ) (z.re - c.re) 2 + HPow.hPow (β := ℕ) (z.im - c.im) 2
have suffices : HPow.hPow (β := ℕ) (y - c.im) 2 ≤ HPow.hPow (β := ℕ) (z.im - c.im) 2
Tactic: suffices (y - c.im) ^ 2 ≤ (z.im - c.im) ^ 2 by simpa
-- Lean 4 proof step from Mathlib.Analysis.Complex.HasPrimitives (goal)
Goal:
c z : ℂ
r y : ℝ
z_in_ball : z ∈ closedBall c r
y_in_I : y ∈ Ι c.im z.im
⊢ HPow.hPow (β := ℕ) (y - c.im) 2 ≤ HPow.hPow (β := ℕ) (z.im - c.im) 2
have inl : c.im < y ∧ y ≤ z.im → HPow.hPow (β := ℕ) (y - c.im) 2 ≤ HPow.hPow (β := ℕ) (z.im - c.im) 2
Tactic: cases mem_uIoc.mp y_in_I
-- Lean 4 proof step from Mathlib.Analysis.Complex.HasPrimitives (goal)
Goal:
c z : ℂ
r y : ℝ
z_in_ball : z ∈ closedBall c r
y_in_I : y ∈ Ι c.im z.im
inl : c.im < y ∧ y ≤ z.im → HPow.hPow (β := ℕ) (y - c.im) 2 ≤ HPow.hPow (β := ℕ) (z.im - c.im) 2
⊢ HPow.hPow (β := ℕ) (y - c.im) 2 ≤ HPow.hPow (β := ℕ) (z.im - c.im) 2
have inr : z.im < y ∧ y ≤ c.im → HPow.hPow (β := ℕ) (y - c.im) 2 ≤ HPow.hPow (β := ℕ) (z.im - c.im) 2
Tactic: cases mem_uIoc.mp y_in_I
-- Lean 4 proof step from Mathlib.Analysis.Complex.HasPrimitives (goal)
Goal:
c z : ℂ
r y : ℝ
z_in_ball : z ∈ closedBall c r
y_in_I : y ∈ Ι c.im z.im
h : c.im < y ∧ y ≤ z.im
⊢ HPow.hPow (β := ℕ) (y - c.im) 2 ≤ HPow.hPow (β := ℕ) (z.im - c.im) 2
have nlinarith : HPow.hPow (β := ℕ) (z.im - c.im) 2 < HPow.hPow (β := ℕ) (y - c.im) 2 →
  HPow.hPow (β := ℕ) (z.im - c.im) 2 - HPow.hPow (β := ℕ) (y - c.im) 2 + 2 * (0 - (c.im - y) * (y - z.im)) +
      (0 - (y - z.im) * (y - z.im)) =
    0
Tactic: nlinarith
-- Lean 4 proof step from Mathlib.Analysis.Complex.HasPrimitives (goal)
Goal:
c z : ℂ
r y : ℝ
z_in_ball : z ∈ closedBall c r
y_in_I : y ∈ Ι c.im z.im
h : c.im < y ∧ y ≤ z.im
nlinarith :
  HPow.hPow (β := ℕ) (z.im - c.im) 2 < HPow.hPow (β := ℕ) (y - c.im) 2 →
    HPow.hPow (β := ℕ) (z.im - c.im) 2 - HPow.hPow (β := ℕ) (y - c.im) 2 + 2 * (0 - (c.im - y) * (y - z.im)) +
        (0 - (y - z.im) * (y - z.im)) =
      0
⊢ HPow.hPow (β := ℕ) (y - c.im) 2 ≤ HPow.hPow (β := ℕ) (z.im - c.im) 2
have nlinarith₁ : HPow.hPow (β := ℕ) (z.im - c.im) 2 < HPow.hPow (β := ℕ) (y - c.im) 2 → GT.gt (α := ℝ) 2 0
Tactic: nlinarith
-- Lean 4 proof step from Mathlib.Analysis.Complex.HasPrimitives (goal)
Goal:
c z : ℂ
r y : ℝ
z_in_ball : z ∈ closedBall c r
y_in_I : y ∈ Ι c.im z.im
h : z.im < y ∧ y ≤ c.im
⊢ HPow.hPow (β := ℕ) (y - c.im) 2 ≤ HPow.hPow (β := ℕ) (z.im - c.im) 2
have nlinarith : HPow.hPow (β := ℕ) (z.im - c.im) 2 < HPow.hPow (β := ℕ) (y - c.im) 2 →
  HPow.hPow (β := ℕ) (z.im - c.im) 2 - HPow.hPow (β := ℕ) (y - c.im) 2 + (0 - (z.im - y) * (z.im - y)) +
      2 * (0 - (z.im - y) * (y - c.im)) =
    0
Tactic: nlinarith
-- Lean 4 proof step from Mathlib.Analysis.Complex.HasPrimitives (goal)
Goal:
c z : ℂ
r y : ℝ
z_in_ball : z ∈ closedBall c r
y_in_I : y ∈ Ι c.im z.im
h : z.im < y ∧ y ≤ c.im
nlinarith :
  HPow.hPow (β := ℕ) (z.im - c.im) 2 < HPow.hPow (β := ℕ) (y - c.im) 2 →
    HPow.hPow (β := ℕ) (z.im - c.im) 2 - HPow.hPow (β := ℕ) (y - c.im) 2 + (0 - (z.im - y) * (z.im - y)) +
        2 * (0 - (z.im - y) * (y - c.im)) =
      0
⊢ HPow.hPow (β := ℕ) (y - c.im) 2 ≤ HPow.hPow (β := ℕ) (z.im - c.im) 2
have nlinarith₁ : HPow.hPow (β := ℕ) (z.im - c.im) 2 < HPow.hPow (β := ℕ) (y - c.im) 2 → GT.gt (α := ℝ) 2 0
Tactic: nlinarith
-- Lean 4 proof step from Mathlib.Analysis.Complex.HasPrimitives (goal)
Goal:
c : ℂ
r a₁ a₂ b : ℝ
ha₁ : (↑a₁ : ℂ) + (↑b : ℂ) * I ∈ ball c r
ha₂ : (↑a₂ : ℂ) + (↑b : ℂ) * I ∈ ball c r
⊢ (fun (x : ℝ) ↦ (↑x : ℂ) + (↑b : ℂ) * I) '' [[a₁, a₂]] ⊆ ball c r
have h : (fun (x : ℝ) ↦ (↑x : ℂ) + (↑b : ℂ) * I) '' [[a₁, a₂]] = ((↑a₁ : ℂ) + (↑b : ℂ) * I).Rectangle ((↑a₂ : ℂ) + (↑b : ℂ) * I)
Tactic: convert! Convex.rectangle_subset (convex_ball c r) ha₁ ha₂ ?_ ?_ using 1
-- Lean 4 proof step from Mathlib.Analysis.Complex.HasPrimitives (goal)
Goal:
c : ℂ
r a₁ a₂ b : ℝ
ha₁ : (↑a₁ : ℂ) + (↑b : ℂ) * I ∈ ball c r
ha₂ : (↑a₂ : ℂ) + (↑b : ℂ) * I ∈ ball c r
h :
  (fun (x : ℝ) ↦ (↑x : ℂ) + (↑b : ℂ) * I) '' [[a₁, a₂]] =
    ((↑a₁ : ℂ) + (↑b : ℂ) * I).Rectangle ((↑a₂ : ℂ) + (↑b : ℂ) * I)
⊢ (fun (x : ℝ) ↦ (↑x : ℂ) + (↑b : ℂ) * I) '' [[a₁, a₂]] ⊆ ball c r
have convert_1 : (↑((↑a₁ : ℂ) + (↑b : ℂ) * I).re : ℂ) + (↑((↑a₂ : ℂ) + (↑b : ℂ) * I).im : ℂ) * I ∈ ball c r
Tactic: convert! Convex.rectangle_subset (convex_ball c r) ha₁ ha₂ ?_ ?_ using 1
-- Lean 4 proof step from Mathlib.Analysis.Complex.HasPrimitives (goal)
Goal:
c : ℂ
r a₁ a₂ b : ℝ
ha₁ : (↑a₁ : ℂ) + (↑b : ℂ) * I ∈ ball c r
ha₂ : (↑a₂ : ℂ) + (↑b : ℂ) * I ∈ ball c r
h :
  (fun (x : ℝ) ↦ (↑x : ℂ) + (↑b : ℂ) * I) '' [[a₁, a₂]] =
    ((↑a₁ : ℂ) + (↑b : ℂ) * I).Rectangle ((↑a₂ : ℂ) + (↑b : ℂ) * I)
convert_1 : (↑((↑a₁ : ℂ) + (↑b : ℂ) * I).re : ℂ) + (↑((↑a₂ : ℂ) + (↑b : ℂ) * I).im : ℂ) * I ∈ ball c r
⊢ (fun (x : ℝ) ↦ (↑x : ℂ) + (↑b : ℂ) * I) '' [[a₁, a₂]] ⊆ ball c r
have convert_2 : (↑((↑a₂ : ℂ) + (↑b : ℂ) * I).re : ℂ) + (↑((↑a₁ : ℂ) + (↑b : ℂ) * I).im : ℂ) * I ∈ ball c r
Tactic: convert! Convex.rectangle_subset (convex_ball c r) ha₁ ha₂ ?_ ?_ using 1
-- Lean 4 proof step from Mathlib.Analysis.Complex.HasPrimitives (goal)
Goal:
c : ℂ
r a b₁ b₂ : ℝ
hb₁ : (↑a : ℂ) + (↑b₁ : ℂ) * I ∈ ball c r
hb₂ : (↑a : ℂ) + (↑b₂ : ℂ) * I ∈ ball c r
⊢ (fun (y : ℝ) ↦ (↑a : ℂ) + (↑y : ℂ) * I) '' [[b₁, b₂]] ⊆ ball c r
have h : (fun (y : ℝ) ↦ (↑a : ℂ) + (↑y : ℂ) * I) '' [[b₁, b₂]] = ((↑a : ℂ) + (↑b₁ : ℂ) * I).Rectangle ((↑a : ℂ) + (↑b₂ : ℂ) * I)
Tactic: convert! Convex.rectangle_subset (convex_ball c r) hb₁ hb₂ ?_ ?_ using 1
-- Lean 4 proof step from Mathlib.Analysis.Complex.HasPrimitives (goal)
Goal:
c : ℂ
r a b₁ b₂ : ℝ
hb₁ : (↑a : ℂ) + (↑b₁ : ℂ) * I ∈ ball c r
hb₂ : (↑a : ℂ) + (↑b₂ : ℂ) * I ∈ ball c r
h :
  (fun (y : ℝ) ↦ (↑a : ℂ) + (↑y : ℂ) * I) '' [[b₁, b₂]] =
    ((↑a : ℂ) + (↑b₁ : ℂ) * I).Rectangle ((↑a : ℂ) + (↑b₂ : ℂ) * I)
⊢ (fun (y : ℝ) ↦ (↑a : ℂ) + (↑y : ℂ) * I) '' [[b₁, b₂]] ⊆ ball c r
have convert_1 : (↑((↑a : ℂ) + (↑b₁ : ℂ) * I).re : ℂ) + (↑((↑a : ℂ) + (↑b₂ : ℂ) * I).im : ℂ) * I ∈ ball c r
Tactic: convert! Convex.rectangle_subset (convex_ball c r) hb₁ hb₂ ?_ ?_ using 1
-- Lean 4 proof step from Mathlib.Analysis.Complex.HasPrimitives (goal)
Goal:
c : ℂ
r a b₁ b₂ : ℝ
hb₁ : (↑a : ℂ) + (↑b₁ : ℂ) * I ∈ ball c r
hb₂ : (↑a : ℂ) + (↑b₂ : ℂ) * I ∈ ball c r
h :
  (fun (y : ℝ) ↦ (↑a : ℂ) + (↑y : ℂ) * I) '' [[b₁, b₂]] =
    ((↑a : ℂ) + (↑b₁ : ℂ) * I).Rectangle ((↑a : ℂ) + (↑b₂ : ℂ) * I)
convert_1 : (↑((↑a : ℂ) + (↑b₁ : ℂ) * I).re : ℂ) + (↑((↑a : ℂ) + (↑b₂ : ℂ) * I).im : ℂ) * I ∈ ball c r
⊢ (fun (y : ℝ) ↦ (↑a : ℂ) + (↑y : ℂ) * I) '' [[b₁, b₂]] ⊆ ball c r
have convert_2 : (↑((↑a : ℂ) + (↑b₂ : ℂ) * I).re : ℂ) + (↑((↑a : ℂ) + (↑b₁ : ℂ) * I).im : ℂ) * I ∈ ball c r
Tactic: convert! Convex.rectangle_subset (convex_ball c r) hb₁ hb₂ ?_ ?_ using 1
-- Lean 4 proof step from Mathlib.Analysis.Complex.HasPrimitives (goal)
Goal:
c z : ℂ
r : ℝ
w : ℂ
hw : w ∈ ball z (r - dist z c)
⊢ (fun (y : ℝ) ↦ (↑w.re : ℂ) + (↑y : ℂ) * I) '' [[z.im, w.im]] ⊆ ball c r
have hb₁ : (↑w.re : ℂ) + (↑z.im : ℂ) * I ∈ ball c r
Tactic: apply mem_ball_of_map_im_aux₁
-- Lean 4 proof step from Mathlib.Analysis.Complex.HasPrimitives (goal)
Goal:
c z : ℂ
r : ℝ
w : ℂ
hw : w ∈ ball z (r - dist z c)
hb₁ : (↑w.re : ℂ) + (↑z.im : ℂ) * I ∈ ball c r
⊢ (fun (y : ℝ) ↦ (↑w.re : ℂ) + (↑y : ℂ) * I) '' [[z.im, w.im]] ⊆ ball c r
have hb₂ : (↑w.re : ℂ) + (↑w.im : ℂ) * I ∈ ball c r
Tactic: apply mem_ball_of_map_im_aux₁
-- Lean 4 proof step from Mathlib.Analysis.Complex.HasPrimitives (goal)
Goal:
c z : ℂ
r : ℝ
w : ℂ
hw : w ∈ ball z (r - dist z c)
⊢ (↑w.re : ℂ) + (↑z.im : ℂ) * I ∈ ball c r
have hb₁ : (↑w.re : ℂ) + (↑z.im : ℂ) * I ∈ ball z (r - dist z c)
Tactic: apply mem_of_subset_of_mem (ball_subset_ball' (by simp) : ball z (r - dist z c) ⊆ ball c r)
-- Lean 4 proof step from Mathlib.Analysis.Complex.HasPrimitives (goal)
Goal:
c z : ℂ
r : ℝ
w : ℂ
hw : w ∈ ball z (r - dist z c)
⊢ (↑w.re : ℂ) + (↑w.im : ℂ) * I ∈ ball c r
have hb₂ : (↑w.re : ℂ) + (↑w.im : ℂ) * I ∈ ball z (r - dist z c)
Tactic: apply mem_of_subset_of_mem (ball_subset_ball' (by simp) : ball z (r - dist z c) ⊆ ball c r)
-- Lean 4 proof step from Mathlib.Analysis.Complex.HasPrimitives (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
z w : ℂ
f : ℂ → E
⊢ z.wedgeIntegral w f + w.wedgeIntegral z f =
    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))
have simp : (∫ (x : ℝ) in z.re..w.re, f ((↑x : ℂ) + (↑z.im : ℂ) * I)) +
      HSMul.hSMul (β := E) I (∫ (y : ℝ) in z.im..w.im, f ((↑w.re : ℂ) + (↑y : ℂ) * I)) +
    ((-∫ (x : ℝ) in z.re..w.re, f ((↑x : ℂ) + (↑w.im : ℂ) * I)) +
      -HSMul.hSMul (β := E) I (∫ (y : ℝ) in z.im..w.im, f ((↑z.re : ℂ) + (↑y : ℂ) * I))) =
  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))
Tactic: simp only [wedgeIntegral, intervalIntegral.integral_symm z.re w.re,
    intervalIntegral.integral_symm z.im w.im, smul_neg]
-- Lean 4 proof step from Mathlib.Analysis.Complex.HasPrimitives (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
s : Set ℂ
h : IsExactOn f s
x₀ : ℂ
y : E
⊢ ∃ (g : ℂ → E), g x₀ = y ∧ ∀ x ∈ s, HasDerivAt g (f x) x
have obtain : ∀ (η : ℂ → E) (hη : ∀ z ∈ s, HasDerivAt η (f z) z), ∃ (g : ℂ → E), g x₀ = y ∧ ∀ x ∈ s, HasDerivAt g (f x) x
Tactic: obtain ⟨η, hη⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Complex.HasPrimitives (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
s : Set ℂ
x₀ : ℂ
y : E
η : ℂ → E
hη : ∀ z ∈ s, HasDerivAt η (f z) z
w : ℂ → E
⊢ ∃ (g : ℂ → E), g x₀ = y ∧ ∀ x ∈ s, HasDerivAt g (f x) x
have left : η x₀ - η x₀ + y = y
Tactic: use fun z ↦ η z - η x₀ + y, by simp, by simpa using hη
-- Lean 4 proof step from Mathlib.Analysis.Complex.HasPrimitives (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
s : Set ℂ
x₀ : ℂ
y : E
η : ℂ → E
hη : ∀ z ∈ s, HasDerivAt η (f z) z
w : ℂ → E
left : η x₀ - η x₀ + y = y
⊢ ∃ (g : ℂ → E), g x₀ = y ∧ ∀ x ∈ s, HasDerivAt g (f x) x
have right : ∀ x ∈ s, HasDerivAt (fun (z : ℂ) ↦ η z - η x₀ + y) (f x) x
Tactic: use fun z ↦ η z - η x₀ + y, by simp, by simpa using hη