awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Complex.Harmonic.MeanValue
Goal:
f : ℂ → ℝ
c : ℂ
R : ℝ
hf : HarmonicOnNhd f (closedBall 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 ((⇑Complex.reCLM : (a : ℂ) → ℝ) ∘ F) f (sphere c |R|)
⊢ CircleIntegrable F c R

Tactic:
apply (h₁F.continuousOn.mono (fun _ _ ↦ by simp_all [dist_eq_norm])).circleIntegrable'

Premises used: AnalyticOnNhd.continuousOn, ContinuousOn.mono, ContinuousOn.circleIntegrable'
-- Module: Mathlib.Analysis.Complex.Harmonic.MeanValue
Goal:
f : ℂ → ℝ
c : ℂ
R : ℝ
h₁f : HarmonicContOnCl f (ball c |R|)
pos : ∀ (hR : R = 0), circleAverage f c R = f c
neg : ∀ (hR : ¬R = 0), circleAverage f c R = f c
⊢ circleAverage f c R = f c

Tactic:
by_cases hR : R = 0
-- Module: Mathlib.Analysis.Complex.Harmonic.MeanValue
Goal:
f : ℂ → ℝ
c : ℂ
R : ℝ
h₁f : HarmonicContOnCl f (ball c |R|)
hR : R = 0
⊢ circleAverage f c R = f c

Tactic:
simp_all
-- Module: Mathlib.Analysis.Complex.Harmonic.MeanValue
Goal:
f : ℂ → ℝ
c : ℂ
R : ℝ
h₁f : HarmonicContOnCl f (ball c |R|)
hR : ¬R = 0
⊢ ContinuousOn (circleAverage f c) (Set.Ioc 0 |R|)

Tactic:
(h₁f.2.mono ?_).circleAverage (fun z hz ↦ hz.1.le)

Premises used: Real.ContinuousOn.circleAverage, LT.lt.le, And.left, ContinuousOn.mono, InnerProductSpace.HarmonicContOnCl.continuousOn
-- Module: Mathlib.Analysis.Complex.Harmonic.MeanValue
Goal:
f : ℂ → ℝ
c : ℂ
R : ℝ
h₁f : HarmonicContOnCl f (ball c |R|)
hR : ¬R = 0
refine : {z : ℂ | ‖z - c‖ ∈ Set.Ioc 0 |R|} ⊆ closure (ball c |R|)
⊢ ContinuousOn (circleAverage f c) (Set.Ioc 0 |R|)

Tactic:
refine (h₁f.2.mono ?_).circleAverage (fun z hz ↦ hz.1.le)

Premises used: Real.ContinuousOn.circleAverage, ContinuousOn.mono, InnerProductSpace.HarmonicContOnCl.continuousOn
-- Module: Mathlib.Analysis.Complex.Harmonic.MeanValue
Goal:
f : ℂ → ℝ
c : ℂ
R : ℝ
h₁f : HarmonicContOnCl f (ball c |R|)
hR : ¬R = 0
x : ℂ
hx : Membership.mem (γ := Set ℂ) {z : ℂ | ‖z - c‖ ∈ Set.Ioc 0 |R|} x
⊢ |R| ≠ 0

Tactic:
aesop
-- Module: Mathlib.Analysis.Complex.Harmonic.MeanValue
Goal:
f : ℂ → ℝ
c : ℂ
R : ℝ
h₁f : HarmonicContOnCl f (ball c |R|)
hR : ¬R = 0
x : ℂ
hx : Membership.mem (γ := Set ℂ) {z : ℂ | ‖z - c‖ ∈ Set.Ioc 0 |R|} x
rw : ‖x - c‖ ≤ |R|
⊢ x ∈ closure (ball c |R|)

Tactic:
rw [closure_ball _ (by aesop), mem_closedBall_iff_norm]

Premises used: mem_closedBall_iff_norm, closure_ball
-- Module: Mathlib.Analysis.Complex.Harmonic.MeanValue
Goal:
f : ℂ → ℝ
c : ℂ
R : ℝ
h₁f : HarmonicContOnCl f (ball c |R|)
hR : ¬R = 0
x : ℂ
hx : Membership.mem (γ := Set ℂ) {z : ℂ | ‖z - c‖ ∈ Set.Ioc 0 |R|} x
⊢ ‖x - c‖ ≤ |R|

Tactic:
hx.2

Premises used: And.right
-- Module: Mathlib.Analysis.Complex.Harmonic.MeanValue
Goal:
f : ℂ → ℝ
c : ℂ
R : ℝ
h₁f : HarmonicContOnCl f (ball c |R|)
hR : ¬R = 0
x : ℂ
hx : Membership.mem (γ := Set ℂ) {z : ℂ | ‖z - c‖ ∈ Set.Ioc 0 |R|} x
⊢ ‖x - c‖ ≤ |R|

Tactic:
exact hx.2

Premises used: And.right
-- Module: Mathlib.Analysis.Complex.Harmonic.MeanValue
Goal:
f : ℂ → ℝ
c : ℂ
R : ℝ
h₁f : HarmonicContOnCl f (ball c |R|)
hR : ¬R = 0
⊢ ContinuousOn (circleAverage f c) (Set.Ioc 0 |R|)

Tactic:
have H : ContinuousOn (circleAverage f c) (Set.Ioc 0 |R|) := by
    refine (h₁f.2.mono ?_).circleAverage (fun z hz ↦ hz.1.le)
    intro x hx
    rw [closure_ball _ (by aesop), mem_closedBall_iff_norm]
    exact hx.2
-- Module: Mathlib.Analysis.Complex.Harmonic.MeanValue
Goal:
f : ℂ → ℝ
c : ℂ
R : ℝ
h₁f : HarmonicContOnCl f (ball c |R|)
hR : ¬R = 0
H : ContinuousOn (circleAverage f c) (Set.Ioc 0 |R|)
neg : circleAverage f c |R| = f c
⊢ circleAverage f c R = f c

Tactic:
rw [← circleAverage_abs_radius]

Premises used: Real.circleAverage_abs_radius
-- Module: Mathlib.Analysis.Complex.Harmonic.MeanValue
Goal:
f : ℂ → ℝ
c : ℂ
R : ℝ
h₁f : HarmonicContOnCl f (ball c |R|)
hR : ¬R = 0
H : ContinuousOn (circleAverage f c) (Set.Ioc 0 |R|)
⊢ 0 < |R|

Tactic:
aesop
-- Module: Mathlib.Analysis.Complex.Harmonic.MeanValue
Goal:
f : ℂ → ℝ
c : ℂ
R : ℝ
h₁f : HarmonicContOnCl f (ball c |R|)
hR : ¬R = 0
H : ContinuousOn (circleAverage f c) (Set.Ioc 0 |R|)
neg : Set.EqOn (circleAverage f c) (fun (x : ℝ) ↦ f c) (Set.Ioo 0 |R|)
⊢ circleAverage f c |R| = f c

Tactic:
apply H.eq_of_eqOn_Ioo (by aesop)

Premises used: Real.ContinuousOn.eq_of_eqOn_Ioo
-- Module: Mathlib.Analysis.Complex.Harmonic.MeanValue
Goal:
f : ℂ → ℝ
c : ℂ
R : ℝ
h₁f : HarmonicContOnCl f (ball c |R|)
hR : ¬R = 0
H : ContinuousOn (circleAverage f c) (Set.Ioc 0 |R|)
r : ℝ
hr : r ∈ Set.Ioo 0 |R|
neg : HarmonicOnNhd f (closedBall c |r|)
⊢ circleAverage f c r = (fun (x : ℝ) ↦ f c) r

Tactic:
apply HarmonicOnNhd.circleAverage_eq

Premises used: HarmonicOnNhd.circleAverage_eq
-- Module: Mathlib.Analysis.Complex.Harmonic.MeanValue
Goal:
f : ℂ → ℝ
c : ℂ
R : ℝ
h₁f : HarmonicContOnCl f (ball c |R|)
hR : ¬R = 0
H : ContinuousOn (circleAverage f c) (Set.Ioc 0 |R|)
r : ℝ
hr : r ∈ Set.Ioo 0 |R|
neg : closedBall c |r| ⊆ ball c |R|
⊢ HarmonicOnNhd f (closedBall c |r|)

Tactic:
apply h₁f.1.mono

Premises used: InnerProductSpace.HarmonicContOnCl.harmonicOnNhd, InnerProductSpace.HarmonicOnNhd.mono
-- Module: Mathlib.Analysis.Complex.Harmonic.MeanValue
Goal:
f : ℂ → ℝ
c : ℂ
R : ℝ
h₁f : HarmonicContOnCl f (ball c |R|)
hR : ¬R = 0
H : ContinuousOn (circleAverage f c) (Set.Ioc 0 |R|)
r : ℝ
hr : r ∈ Set.Ioo 0 |R|
neg : closedBall c r ⊆ ball c |R|
⊢ closedBall c |r| ⊆ ball c |R|

Tactic:
rw [abs_of_pos hr.1]

Premises used: And.left, abs_of_pos
-- Module: Mathlib.Analysis.Complex.Harmonic.MeanValue
Goal:
f : ℂ → ℝ
c : ℂ
R : ℝ
h₁f : HarmonicContOnCl f (ball c |R|)
hR : ¬R = 0
H : ContinuousOn (circleAverage f c) (Set.Ioc 0 |R|)
r : ℝ
hr : r ∈ Set.Ioo 0 |R|
⊢ closedBall c r ⊆ ball c |R|

Tactic:
closedBall_subset_ball hr.2

Premises used: Metric.closedBall_subset_ball, And.right
-- Module: Mathlib.Analysis.Complex.Harmonic.MeanValue
Goal:
f : ℂ → ℝ
c : ℂ
R : ℝ
h₁f : HarmonicContOnCl f (ball c |R|)
hR : ¬R = 0
H : ContinuousOn (circleAverage f c) (Set.Ioc 0 |R|)
r : ℝ
hr : r ∈ Set.Ioo 0 |R|
⊢ closedBall c r ⊆ ball c |R|

Tactic:
exact closedBall_subset_ball hr.2

Premises used: Metric.closedBall_subset_ball, And.right
-- Module: Mathlib.Analysis.Complex.Harmonic.Poisson
Goal:
c w : ℂ
R : ℝ
h : w ∈ ball c R
⊢ ∀ (x : ℂ), Membership.mem (γ := Set ℂ) {z : ℂ | ‖z - c‖ ∈ Set.Ioc ‖w - c‖ R} x → x - c - (w - c) ≠ 0

Tactic:
grind [mem_ball, mem_sphere]

Premises used: Metric.mem_ball, Metric.mem_sphere
-- Module: Mathlib.Analysis.Complex.Harmonic.Poisson
Goal:
c w : ℂ
R : ℝ
h : w ∈ ball c R
⊢ ∀ (x : ℂ), Membership.mem (γ := Set ℂ) {z : ℂ | ‖z - c‖ ∈ Set.Ioc ‖w - c‖ R} x → x - c - (w - c) ≠ 0

Tactic:
have : ∀ x ∈ {z | ‖z - c‖ ∈ Set.Ioc ‖w - c‖ R}, x - c - (w - c) ≠ 0 := by
    grind [mem_ball, mem_sphere]
-- Module: Mathlib.Analysis.Complex.Harmonic.Poisson
Goal:
c w : ℂ
R : ℝ
h : w ∈ ball c R
this : ∀ (x : ℂ), Membership.mem (γ := Set ℂ) {z : ℂ | ‖z - c‖ ∈ Set.Ioc ‖w - c‖ R} x → x - c - (w - c) ≠ 0
funProp : HarmonicOnNhd (F := ℝ) (fun (x0 : ℂ) ↦ x0.re) ?t
funProp₁ : ∀ (x : ℂ), Membership.mem (γ := Set ℂ) {z : ℂ | ‖z - c‖ ∈ Set.Ioc ‖w - c‖ R} x → x - c - (w - c) ≠ 0
⊢ ContinuousOn (Y := ℝ) (fun (x : ℂ) ↦ ((x - c + (w - c)) / (x - c - (w - c))).re) {z : ℂ | ‖z - c‖ ∈ Set.Ioc ‖w - c‖ R}

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Complex.Harmonic.Poisson
Goal:
f : ℂ → ℝ
c w : ℂ
R : ℝ
hf : HarmonicOnNhd f (closedBall c R)
hw : w ∈ ball c R
⊢ closedBall c R ⊆ {x : ℂ | HarmonicAt f x}

Tactic:
aesop
-- Module: Mathlib.Analysis.Complex.Harmonic.Poisson
Goal:
f : ℂ → ℝ
c w : ℂ
R : ℝ
hf : HarmonicOnNhd f (closedBall c R)
hw : w ∈ ball c R
obtain :
  ∀ (e : ℝ) (h₁e : 0 < e) (h₂e : thickening e (closedBall c R) ⊆ {x : ℂ | HarmonicAt f x}),
    circleAverage (re ∘ herglotzRieszKernel c w • f) c R = f w
⊢ circleAverage (re ∘ herglotzRieszKernel c w • f) c R = f w

Tactic:
obtain ⟨e, h₁e, h₂e⟩ := (isCompact_closedBall c R).exists_thickening_subset_open
    (isOpen_setOf_harmonicAt f) (by aesop)

Premises used: InnerProductSpace.isOpen_setOf_harmonicAt, ProperSpace.isCompact_closedBall, IsCompact.exists_thickening_subset_open
-- Module: Mathlib.Analysis.Complex.Harmonic.Poisson
Goal:
f : ℂ → ℝ
c w : ℂ
R : ℝ
hf : HarmonicOnNhd f (closedBall c R)
hw : w ∈ ball c R
e : ℝ
h₁e : 0 < e
h₂e : thickening e (closedBall c R) ⊆ {x : ℂ | HarmonicAt f x}
⊢ ball c (e + R) ⊆ {x : ℂ | HarmonicAt f x}

Tactic:
rw [thickening_closedBall h₁e (pos_of_mem_ball hw).le] at h₂e

Premises used: LT.lt.le, thickening_closedBall, Metric.pos_of_mem_ball
-- Module: Mathlib.Analysis.Complex.Harmonic.Poisson
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}
obtain :
  ∀ (F : ℂ → ℂ) (h₁F : AnalyticOnNhd ℂ F (ball c (e + R))) (h₂F : Set.EqOn (fun (z : ℂ) ↦ (F z).re) f (ball c (e + R))),
    circleAverage (re ∘ herglotzRieszKernel c w • f) c R = f w
⊢ circleAverage (re ∘ herglotzRieszKernel c w • f) c R = f w

Tactic:
obtain ⟨F, h₁F, h₂F⟩ := HarmonicOnNhd.exists_analyticOnNhd_ball_re_eq h₂e

Premises used: InnerProductSpace.HarmonicOnNhd.exists_analyticOnNhd_ball_re_eq
-- Module: Mathlib.Analysis.Complex.Harmonic.Poisson
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))
x : ℂ
hx : x ∈ closure (ball c R)
apply : x ∈ ball c (e + R)
⊢ DifferentiableWithinAt ℂ F (closure (ball c R)) x

Tactic:
apply (h₁F x _).differentiableWithinAt

Premises used: AnalyticAt.differentiableWithinAt
-- Module: Mathlib.Analysis.Complex.Harmonic.Poisson
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))
x : ℂ
hx : x ∈ closure (ball c R)
⊢ x ∈ ball c (e + R)

Tactic:
grind [mem_ball, mem_closedBall.1 (closure_ball_subset_closedBall hx)]

Premises used: Metric.mem_ball, Metric.closure_ball_subset_closedBall, Iff.mp, Metric.mem_closedBall
-- Module: Mathlib.Analysis.Complex.Harmonic.Poisson
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))
⊢ DifferentiableOn ℂ F (closure (ball c R))

Tactic:
have h₃F : DifferentiableOn ℂ F (closure (ball c R)) := by
    intro x hx
    apply (h₁F x _).differentiableWithinAt
    grind [mem_ball, mem_closedBall.1 (closure_ball_subset_closedBall hx)]
-- Module: Mathlib.Analysis.Complex.Harmonic.Poisson
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))
x : ℂ
hx : x ∈ sphere c R
⊢ (re ∘ herglotzRieszKernel c w • f) x =
    Function.comp (β := ℂ) (⇑reCLM : (a : ℂ) → ℝ) (fun (z : ℂ) ↦ ((z - c + (w - c)) / (z - c - (w - c))).re • F z) x

Tactic:
simp [h₂F (sphere_subset_ball (lt_add_of_pos_left R h₁e) hx), herglotzRieszKernel_def]

Premises used: herglotzRieszKernel_def, Metric.sphere_subset_ball, lt_add_of_pos_left
-- Module: Mathlib.Analysis.Complex.Harmonic.Poisson
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))
⊢ 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:
have h₄F : Set.EqOn (re ∘ herglotzRieszKernel c w • f)
      (reCLM ∘ (fun z ↦ ((z - c + (w - c)) / (z - c - (w - c))).re • F z))
      (sphere c R) := by
    intro x hx
    simp [h₂F (sphere_subset_ball (lt_add_of_pos_left R h₁e) hx), herglotzRieszKernel_def]
-- Module: Mathlib.Analysis.Complex.Harmonic.Poisson
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)
⊢ 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

Premises used: abs_of_pos, Metric.pos_of_mem_ball
-- Module: Mathlib.Analysis.Complex.Harmonic.Poisson
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
rw₁ : CircleIntegrable (E := ℂ) (fun (z : ℂ) ↦ ((z - c + (w - c)) / (z - c - (w - c))).re • F z) c R
⊢ circleAverage (re ∘ herglotzRieszKernel c w • f) c R = f w

Tactic:
rw [circleAverage_congr_sphere h₄F, reCLM.circleAverage_comp_comm,
    h₃F.diffContOnCl.circleAverage_re_herglotzRieszKernel_smul' hw]

Premises used: Real.circleAverage_congr_sphere, DiffContOnCl.circleAverage_re_herglotzRieszKernel_smul', DifferentiableOn.diffContOnCl, Complex.reCLM, ContinuousLinearMap.circleAverage_comp_comm
-- Module: Mathlib.Analysis.Complex.Harmonic.Poisson
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|)
a : w ∈ ball c (e + R)
⊢ (reCLM : (a : ℂ) → ℝ) (F w) = f w

Tactic:
apply h₂F
-- Module: Mathlib.Analysis.Complex.Harmonic.Poisson
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|)
⊢ w ∈ ball c (e + R)

Tactic:
grind [mem_ball]

Premises used: Metric.mem_ball
-- Module: Mathlib.Analysis.Complex.Harmonic.Poisson
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|)
apply₁ : ContinuousOn F (sphere c |R|)
⊢ CircleIntegrable (E := ℂ) (fun (z : ℂ) ↦ ((z - c + (w - c)) / (z - c - (w - c))).re • F z) c R

Tactic:
apply (ContinuousOn.smul _ _).circleIntegrable'

Premises used: ContinuousOn.smul, ContinuousOn.circleIntegrable'
-- Module: Mathlib.Analysis.Complex.Harmonic.Poisson
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 : sphere c |R| ⊆ {z : ℂ | ‖z - c‖ ∈ Set.Ioc ‖w - c‖ R}
⊢ ContinuousOn (Y := ℝ) (fun (x : ℂ) ↦ ((x - c + (w - c)) / (x - c - (w - c))).re) (sphere c |R|)

Tactic:
apply (continuousOn_herglotz_riesz hw).mono

Premises used: _private.0.InnerProductSpace.continuousOn_herglotz_riesz, ContinuousOn.mono
-- Module: Mathlib.Analysis.Complex.Harmonic.Poisson
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|)
⊢ sphere c |R| ⊆ {z : ℂ | ‖z - c‖ ∈ Set.Ioc ‖w - c‖ R}

Tactic:
grind [mem_ball, dist_eq_norm, mem_sphere_iff_norm, (pos_of_mem_ball hw)]

Premises used: dist_eq_norm, Metric.mem_ball, mem_sphere_iff_norm, Metric.pos_of_mem_ball
-- Module: Mathlib.Analysis.Complex.Harmonic.Poisson
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 : sphere c |R| ⊆ ball c (e + R)
⊢ ContinuousOn F (sphere c |R|)

Tactic:
apply (h₁F.mono _).continuousOn (𝕜 := ℂ)

Premises used: AnalyticOnNhd.continuousOn, AnalyticOnNhd.mono
-- Module: Mathlib.Analysis.Complex.Harmonic.Poisson
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|)
⊢ sphere c |R| ⊆ ball c (e + R)

Tactic:
grind [mem_sphere, mem_ball, (pos_of_mem_ball hw)]

Premises used: Metric.mem_ball, Metric.mem_sphere, Metric.pos_of_mem_ball
-- Module: Mathlib.Analysis.Complex.Harmonic.Poisson
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
h₂f : Set.EqOn (circleAverage (re ∘ herglotzRieszKernel c w • f) c) (fun (x : ℝ) ↦ f w) (Set.Ioo ‖w - c‖ R)
⊢ circleAverage (re ∘ herglotzRieszKernel c w • f) c R = f w

Tactic:
apply ContinuousOn.eq_of_eqOn_Ioo (r := ‖w - c‖)

Premises used: Real.ContinuousOn.eq_of_eqOn_Ioo
-- Module: Mathlib.Analysis.Complex.Harmonic.Poisson
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}
h₁f₁ : ∀ r ∈ Set.Ioc ‖w - c‖ R, 0 ≤ r
⊢ ContinuousOn (circleAverage (re ∘ herglotzRieszKernel c w • f) c) (Set.Ioc ‖w - c‖ R)

Tactic:
apply ContinuousOn.circleAverage

Premises used: Real.ContinuousOn.circleAverage
-- Module: Mathlib.Analysis.Complex.Harmonic.Poisson
Goal:
f : ℂ → ℝ
c w : ℂ
R : ℝ
hf : HarmonicContOnCl f (ball c R)
hw : w ∈ ball c R
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}
⊢ ContinuousOn (re ∘ herglotzRieszKernel c w • f) {z : ℂ | ‖z - c‖ ∈ Set.Ioc ‖w - c‖ R}

Tactic:
rw [herglotzRieszKernel_fun_def]

Premises used: herglotzRieszKernel_fun_def
-- Module: Mathlib.Analysis.Complex.Harmonic.Poisson
Goal:
f : ℂ → ℝ
c w : ℂ
R : ℝ
hf : HarmonicContOnCl f (ball c R)
hw : w ∈ ball c R
apply : {z : ℂ | ‖z - c‖ ∈ Set.Ioc ‖w - c‖ R} ⊆ closure (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}

Tactic:
apply (continuousOn_herglotz_riesz hw).smul (hf.2.mono _)

Premises used: _private.0.InnerProductSpace.continuousOn_herglotz_riesz, ContinuousOn.smul, ContinuousOn.mono, InnerProductSpace.HarmonicContOnCl.continuousOn
-- Module: Mathlib.Analysis.Complex.Harmonic.Poisson
Goal:
f : ℂ → ℝ
c w : ℂ
R : ℝ
hf : HarmonicContOnCl f (ball c R)
hw : w ∈ ball c R
⊢ {z : ℂ | ‖z - c‖ ∈ Set.Ioc ‖w - c‖ R} ⊆ closure (ball c R)

Tactic:
grind [closure_ball c (pos_of_mem_ball hw).ne', mem_closedBall_iff_norm]

Premises used: mem_closedBall_iff_norm, LT.lt.ne', closure_ball, Metric.pos_of_mem_ball
-- Module: Mathlib.Analysis.Complex.Harmonic.Poisson
Goal:
f : ℂ → ℝ
c w : ℂ
R : ℝ
hf : HarmonicContOnCl f (ball c R)
hw : w ∈ ball c R
⊢ ∀ r ∈ Set.Ioc ‖w - c‖ R, 0 ≤ r

Tactic:
grind [norm_nonneg (w - c)]

Premises used: HSub.hSub, norm_nonneg
-- Module: Mathlib.Analysis.Complex.Harmonic.Poisson
Goal:
f : ℂ → ℝ
c w : ℂ
R : ℝ
hf : HarmonicContOnCl f (ball c R)
hw : w ∈ ball c R
⊢ ‖w - c‖ < R

Tactic:
grind [mem_ball_iff_norm]

Premises used: mem_ball_iff_norm
-- Module: Mathlib.Analysis.Complex.Harmonic.Poisson
Goal:
f : ℂ → ℝ
c w : ℂ
R : ℝ
hf : HarmonicContOnCl f (ball c R)
hw : w ∈ ball c R
r : ℝ
hr : r ∈ Set.Ioo ‖w - c‖ R
⊢ w ∈ ball c r

Tactic:
grind [mem_ball_iff_norm]

Premises used: mem_ball_iff_norm
-- Module: Mathlib.Analysis.Complex.Harmonic.Poisson
Goal:
f : ℂ → ℝ
c w : ℂ
R : ℝ
hf : HarmonicContOnCl f (ball c R)
hw : w ∈ ball c R
r : ℝ
hr : r ∈ Set.Ioo ‖w - c‖ R
h₂f h₂f₁ : f w = (fun (x : ℝ) ↦ f w) r
⊢ circleAverage (re ∘ herglotzRieszKernel c w • f) c r = (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])]

Premises used: Metric.closedBall_subset_ball, And.right, InnerProductSpace.HarmonicContOnCl.harmonicOnNhd, InnerProductSpace.HarmonicOnNhd.circleAverage_re_herglotzRieszKernel_smul, InnerProductSpace.HarmonicOnNhd.mono
-- Module: Mathlib.Analysis.Complex.Harmonic.Poisson
Goal:
f : ℂ → ℝ
c w : ℂ
R : ℝ
hf : HarmonicOnNhd f (closedBall c R)
hw : w ∈ ball c R
rw : circleAverage (poissonKernel c w • f) c R = circleAverage (re ∘ herglotzRieszKernel c w • f) c R
⊢ circleAverage (poissonKernel c w • f) c R = f w

Tactic:
rw [← hf.circleAverage_re_herglotzRieszKernel_smul hw]

Premises used: InnerProductSpace.HarmonicOnNhd.circleAverage_re_herglotzRieszKernel_smul
-- Module: Mathlib.Analysis.Complex.Harmonic.Poisson
Goal:
f : ℂ → ℝ
c w : ℂ
R : ℝ
hf : HarmonicOnNhd f (closedBall c R)
hw : w ∈ ball c R
x : ℂ
h : x ∈ sphere c |R|
⊢ (poissonKernel c w • f) x = (re ∘ herglotzRieszKernel c w • f) x

Tactic:
simp_rw [← poissonKernel_eq_re_herglotzRieszKernel]

Premises used: poissonKernel_eq_re_herglotzRieszKernel
-- Module: Mathlib.Analysis.Complex.Harmonic.Poisson
Goal:
f : ℂ → ℝ
c w : ℂ
R : ℝ
hf : HarmonicOnNhd f (closedBall c R)
hw : w ∈ ball c R
⊢ circleAverage (poissonKernel c w • f) c R = circleAverage (re ∘ herglotzRieszKernel c w • f) c R

Tactic:
apply circleAverage_congr_sphere
    (fun _ _ ↦ by simp_rw [← poissonKernel_eq_re_herglotzRieszKernel])

Premises used: Real.circleAverage_congr_sphere