awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Complex.Harmonic.Analytic (goal)
Goal:
f : ℂ → ℝ
hf : HarmonicOnNhd f univ
g : ℂ → ℂ :=
  (Function.comp (β := ℝ) (⇑ofRealCLM : (a : ℝ) → ℂ) fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) 1) -
    HSMul.hSMul (β := ℂ → ℂ) I
      (Function.comp (β := ℝ) (⇑ofRealCLM : (a : ℝ) → ℂ) fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) I)
hg : Differentiable ℂ g
F : ℂ → ℂ
hF : F 0 = (↑(f 0) : ℂ) ∧ ∀ (x : ℂ), Membership.mem (γ := Set ℂ) univ x → HasDerivAt F (g x) x
h₁F : ∀ (z₁ : ℂ), HasDerivAt F (g z₁) z₁
h₂F : Differentiable ℂ F
h₃F : Differentiable ℝ F
x_1 y : ℂ
hy : Membership.mem (γ := Set ℂ) univ y
x : ℂ
⊢ Eq (α := ℝ) ((fderiv ℝ (⇑reCLM : (a : ℂ) → ℝ) (F y) ∘SL fderiv ℝ F y : (a : ℂ) → ℝ) x : ℝ)
    ((fderiv ℝ f y : (a : ℂ) → ℝ) x : ℝ)
have trans : Eq (α := ℝ) ((fderiv ℝ (⇑reCLM : (a : ℂ) → ℝ) (F y) ∘SL fderiv ℝ F y : (a : ℂ) → ℝ) x : ℝ)
  ((fderiv ℝ f y : (a : ℂ) → ℝ) (HSMul.hSMul (β := ℂ) x.re 1 + x.im • I) : ℝ)
Tactic: trans fderiv ℝ f y (x.re • (1 : ℂ) + x.im • (I : ℂ))
-- Lean 4 proof step from Mathlib.Analysis.Complex.Harmonic.Analytic (goal)
Goal:
f : ℂ → ℝ
hf : HarmonicOnNhd f univ
g : ℂ → ℂ :=
  (Function.comp (β := ℝ) (⇑ofRealCLM : (a : ℝ) → ℂ) fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) 1) -
    HSMul.hSMul (β := ℂ → ℂ) I
      (Function.comp (β := ℝ) (⇑ofRealCLM : (a : ℝ) → ℂ) fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) I)
hg : Differentiable ℂ g
F : ℂ → ℂ
hF : F 0 = (↑(f 0) : ℂ) ∧ ∀ (x : ℂ), Membership.mem (γ := Set ℂ) univ x → HasDerivAt F (g x) x
h₁F : ∀ (z₁ : ℂ), HasDerivAt F (g z₁) z₁
h₂F : Differentiable ℂ F
h₃F : Differentiable ℝ F
x_1 y : ℂ
hy : Membership.mem (γ := Set ℂ) univ y
x : ℂ
trans :
  Eq (α := ℝ) ((fderiv ℝ (⇑reCLM : (a : ℂ) → ℝ) (F y) ∘SL fderiv ℝ F y : (a : ℂ) → ℝ) x : ℝ)
    ((fderiv ℝ f y : (a : ℂ) → ℝ) (HSMul.hSMul (β := ℂ) x.re 1 + x.im • I) : ℝ)
⊢ Eq (α := ℝ) ((fderiv ℝ (⇑reCLM : (a : ℂ) → ℝ) (F y) ∘SL fderiv ℝ F y : (a : ℂ) → ℝ) x : ℝ)
    ((fderiv ℝ f y : (a : ℂ) → ℝ) x : ℝ)
have trans₁ : Eq (α := ℝ) ((fderiv ℝ f y : (a : ℂ) → ℝ) (HSMul.hSMul (β := ℂ) x.re 1 + x.im • I) : ℝ)
  ((fderiv ℝ f y : (a : ℂ) → ℝ) x : ℝ)
Tactic: trans fderiv ℝ f y (x.re • (1 : ℂ) + x.im • (I : ℂ))
-- Lean 4 proof step from Mathlib.Analysis.Complex.Harmonic.Analytic (goal)
Goal:
f : ℂ → ℝ
hf : HarmonicOnNhd f univ
g : ℂ → ℂ :=
  (Function.comp (β := ℝ) (⇑ofRealCLM : (a : ℝ) → ℂ) fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) 1) -
    HSMul.hSMul (β := ℂ → ℂ) I
      (Function.comp (β := ℝ) (⇑ofRealCLM : (a : ℝ) → ℂ) fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) I)
hg : Differentiable ℂ g
F : ℂ → ℂ
hF : F 0 = (↑(f 0) : ℂ) ∧ ∀ (x : ℂ), Membership.mem (γ := Set ℂ) univ x → HasDerivAt F (g x) x
h₁F : ∀ (z₁ : ℂ), HasDerivAt F (g z₁) z₁
h₂F : Differentiable ℂ F
h₃F : Differentiable ℝ F
x_1 y : ℂ
hy : Membership.mem (γ := Set ℂ) univ y
x : ℂ
⊢ Eq (α := ℝ) ((fderiv ℝ (⇑reCLM : (a : ℂ) → ℝ) (F y) ∘SL fderiv ℝ F y : (a : ℂ) → ℝ) x : ℝ)
    ((fderiv ℝ f y : (a : ℂ) → ℝ) (HSMul.hSMul (β := ℂ) x.re 1 + x.im • I) : ℝ)
have simp : (fderiv ℝ (⇑reCLM : (a : ℂ) → ℝ) (F y) ∘SL fderiv ℝ F y : (a : ℂ) → ℝ) x =
  HSMul.hSMul (β := ℝ) x.re ((fderiv ℝ f y : (a : ℂ) → ℝ) 1 : ℝ) +
    HSMul.hSMul (β := ℝ) x.im ((fderiv ℝ f y : (a : ℂ) → ℝ) I : ℝ)
Tactic: simp only [map_smul, map_add]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Harmonic.Analytic (goal)
Goal:
f : ℂ → ℝ
x : ℂ
hf : HarmonicAt f x
⊢ AnalyticAt ℝ f x
have obtain : ∀ (ε : ℝ) (h₁ε : ε > 0) (h₂ε : ball x ε ⊆ {x : ℂ | HarmonicAt f x}), AnalyticAt ℝ f x
Tactic: obtain ⟨ε, h₁ε, h₂ε⟩ := isOpen_iff.1 (isOpen_setOf_harmonicAt (f := f)) x hf
-- Lean 4 proof step from Mathlib.Analysis.Complex.Harmonic.Analytic (goal)
Goal:
f : ℂ → ℝ
x : ℂ
hf : HarmonicAt f x
ε : ℝ
h₁ε : ε > 0
h₂ε : ball x ε ⊆ {x : ℂ | HarmonicAt f x}
⊢ AnalyticAt ℝ f x
have obtain : ∀ (F : ℂ → ℂ) (h₁F : AnalyticOnNhd ℂ F (ball x ε)) (h₂F : EqOn (fun (z : ℂ) ↦ (F z).re) f (ball x ε)), AnalyticAt ℝ f x
Tactic: obtain ⟨F, h₁F, h₂F⟩ := InnerProductSpace.HarmonicOnNhd.exists_analyticOnNhd_ball_re_eq
    (fun _ hy ↦ h₂ε hy)
-- Lean 4 proof step from Mathlib.Analysis.Complex.Harmonic.Analytic (goal)
Goal:
f : ℂ → ℝ
x : ℂ
hf : HarmonicAt f x
ε : ℝ
h₁ε : ε > 0
h₂ε : ball x ε ⊆ {x : ℂ | HarmonicAt f x}
F : ℂ → ℂ
h₁F : AnalyticOnNhd ℂ F (ball x ε)
h₂F : EqOn (fun (z : ℂ) ↦ (F z).re) f (ball x ε)
⊢ AnalyticAt ℝ f x
have rw : AnalyticAt ℝ (F := ℝ) (fun (y : ℂ) ↦ (F y).re) x
Tactic: rw [analyticAt_congr (Filter.eventually_of_mem (ball_mem_nhds x h₁ε) (fun y hy ↦ h₂F.symm hy))]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Harmonic.Liouville (goal)
Goal:
f : ℂ → ℝ
h_harm : HarmonicOnNhd f univ
h_bound : IsBounded (range f)
⊢ ∀ (z w : ℂ), f z = f w
have obtain : ∀ (F : ℂ → ℂ) (hF_diff : AnalyticOnNhd ℂ F univ) (hF_re : (fun (z : ℂ) ↦ (F z).re) = f) (z w : ℂ), f z = f w
Tactic: obtain ⟨F, hF_diff, hF_re⟩ := h_harm.exists_analyticOnNhd_univ_re_eq
-- Lean 4 proof step from Mathlib.Analysis.Complex.Harmonic.Liouville (goal)
Goal:
f : ℂ → ℝ
h_harm : HarmonicOnNhd f univ
h_bound : IsBounded (range f)
F : ℂ → ℂ
hF_diff : AnalyticOnNhd ℂ F univ
hF_re : (fun (z : ℂ) ↦ (F z).re) = f
⊢ ∀ (z w : ℂ), f z = f w
have suffices : ∀ (z w : ℂ), cexp (F z) = cexp (F w)
Tactic: suffices ∀ z w, Complex.exp (F z) = Complex.exp (F w) by grind
-- Lean 4 proof step from Mathlib.Analysis.Complex.Harmonic.Liouville (goal)
Goal:
f : ℂ → ℝ
h_harm : HarmonicOnNhd f univ
h_bound : IsBounded (range f)
F : ℂ → ℂ
hF_diff : AnalyticOnNhd ℂ F univ
hF_re : (fun (z : ℂ) ↦ (F z).re) = f
⊢ ∀ (z w : ℂ), cexp (F z) = cexp (F w)
have hf : Differentiable ℂ (F := ℂ) fun (z : ℂ) ↦ cexp (F z)
Tactic: apply Differentiable.apply_eq_apply_of_bounded
-- Lean 4 proof step from Mathlib.Analysis.Complex.Harmonic.Liouville (goal)
Goal:
f : ℂ → ℝ
h_harm : HarmonicOnNhd f univ
h_bound : IsBounded (range f)
F : ℂ → ℂ
hF_diff : AnalyticOnNhd ℂ F univ
hF_re : (fun (z : ℂ) ↦ (F z).re) = f
hf : Differentiable ℂ (F := ℂ) fun (z : ℂ) ↦ cexp (F z)
⊢ ∀ (z w : ℂ), cexp (F z) = cexp (F w)
have hb : IsBounded (α := ℂ) (range fun (z : ℂ) ↦ cexp (F z))
Tactic: apply Differentiable.apply_eq_apply_of_bounded
-- Lean 4 proof step from Mathlib.Analysis.Complex.Harmonic.Liouville (goal)
Goal:
f : ℂ → ℝ
h_harm : HarmonicOnNhd f univ
h_bound : IsBounded (range f)
F : ℂ → ℂ
hF_diff : AnalyticOnNhd ℂ F univ
hF_re : (fun (z : ℂ) ↦ (F z).re) = f
⊢ IsBounded (α := ℂ) (range fun (z : ℂ) ↦ cexp (F z))
have hb : ∀ (h_bound : ∃ (C : ℝ), ∀ x ∈ range f, ‖x‖ ≤ C) (F : ℂ → ℂ) (hF_diff : AnalyticOnNhd ℂ F univ)
  (hF_re : (fun (z : ℂ) ↦ (F z).re) = f),
  ∃ (C : ℝ), ∀ (x : ℂ), Membership.mem (γ := Set ℂ) (range fun (z : ℂ) ↦ cexp (F z)) x → ‖x‖ ≤ C
Tactic: rw [isBounded_iff_forall_norm_le] at *
Cleared hypotheses: h_bound, F, hF_diff, hF_re
-- Lean 4 proof step from Mathlib.Analysis.Complex.Harmonic.Liouville (goal)
Goal:
f : ℂ → ℝ
h_harm : HarmonicOnNhd f univ
h_bound : ∃ (C : ℝ), ∀ x ∈ range f, ‖x‖ ≤ C
F : ℂ → ℂ
hF_diff : AnalyticOnNhd ℂ F univ
hF_re : (fun (z : ℂ) ↦ (F z).re) = f
⊢ ∃ (C : ℝ), ∀ (x : ℂ), Membership.mem (γ := Set ℂ) (range fun (z : ℂ) ↦ cexp (F z)) x → ‖x‖ ≤ C
have hb : ∀ (M : ℝ) (hM : ∀ x ∈ range f, ‖x‖ ≤ M),
  ∃ (C : ℝ), ∀ (x : ℂ), Membership.mem (γ := Set ℂ) (range fun (z : ℂ) ↦ cexp (F z)) x → ‖x‖ ≤ C
Tactic: obtain ⟨M, hM⟩ := h_bound
Cleared hypotheses: h_bound
-- Lean 4 proof step from Mathlib.Analysis.Complex.Harmonic.Liouville (goal)
Goal:
f : ℂ → ℝ
h_harm : HarmonicOnNhd f univ
F : ℂ → ℂ
hF_diff : AnalyticOnNhd ℂ F univ
hF_re : (fun (z : ℂ) ↦ (F z).re) = f
M : ℝ
hM : ∀ x ∈ range f, ‖x‖ ≤ M
⊢ ∃ (C : ℝ), ∀ (x : ℂ), Membership.mem (γ := Set ℂ) (range fun (z : ℂ) ↦ cexp (F z)) x → ‖x‖ ≤ C
have h : ∀ (x : ℂ), Membership.mem (γ := Set ℂ) (range fun (z : ℂ) ↦ cexp (F z)) x → ‖x‖ ≤ rexp M
Tactic: use Real.exp M
-- Lean 4 proof step from Mathlib.Analysis.Complex.Harmonic.Liouville (goal)
Goal:
f : ℂ → ℝ
h_harm : HarmonicOnNhd f univ
F : ℂ → ℂ
hF_diff : AnalyticOnNhd ℂ F univ
hF_re : (fun (z : ℂ) ↦ (F z).re) = f
M : ℝ
hM : ∀ x ∈ range f, ‖x‖ ≤ M
⊢ ∀ (x : ℂ), Membership.mem (γ := Set ℂ) (range fun (z : ℂ) ↦ cexp (F z)) x → ‖x‖ ≤ rexp M
have h : ∀ (hM : ∀ (a : ℂ), |f a| ≤ M) (a : ℂ), (F a).re ≤ M
Tactic: simp_all only [mem_range, norm_eq_abs, forall_exists_index, forall_apply_eq_imp_iff,
    norm_exp, exp_le_exp]
Cleared hypotheses: hM
-- Lean 4 proof step from Mathlib.Analysis.Complex.Harmonic.Liouville (hypothesis)
Goal:
f : ℂ → ℝ
h_harm : HarmonicOnNhd f univ
F : ℂ → ℂ
hF_diff : AnalyticOnNhd ℂ F univ
hF_re : (fun (z : ℂ) ↦ (F z).re) = f
M : ℝ
hM : ∀ (a : ℂ), |f a| ≤ M
⊢ ∀ (a : ℂ), (F a).re ≤ M
have hM₁ : ∀ (a : ℂ), |(fun (z : ℂ) ↦ (F z).re) a| ≤ M
Tactic: rw [← hF_re] at hM
Cleared hypotheses: hM
-- Lean 4 proof step from Mathlib.Analysis.Complex.Harmonic.Liouville (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℂ → E
h_harm : HarmonicOnNhd f univ
h_bound : IsBounded (range f)
z w : ℂ
⊢ f z = f w
have obtain : ∀ (ℓ : StrongDual ℝ E) (h₁ℓ : ‖ℓ‖ ≤ 1) (h₂ℓ : Eq (α := ℝ) ((ℓ : (a : E) → ℝ) (f z - f w) : ℝ) ((↑‖f z - f w‖ : ℝ) : ℝ)),
  f z = f w
Tactic: obtain ⟨ℓ, h₁ℓ, h₂ℓ⟩ := exists_dual_vector'' ℝ (f z - f w)
-- Lean 4 proof step from Mathlib.Analysis.Complex.Harmonic.Liouville (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℂ → E
h_harm : HarmonicOnNhd f univ
h_bound : IsBounded (range f)
z w : ℂ
ℓ : StrongDual ℝ E
h₁ℓ : ‖ℓ‖ ≤ 1
h₂ℓ : Eq (α := ℝ) ((ℓ : (a : E) → ℝ) (f z - f w) : ℝ) ((↑‖f z - f w‖ : ℝ) : ℝ)
⊢ f z = f w
have h₂ℓ₁ : HSub.hSub (α := ℝ) (β := ℝ) ((ℓ : (a : E) → ℝ) (f z) : ℝ) ((ℓ : (a : E) → ℝ) (f w) : ℝ) = ‖f z - f w‖
Tactic: rw [map_sub, RCLike.ofReal_real_eq_id, id_eq] at h₂ℓ
Cleared hypotheses: h₂ℓ
-- Lean 4 proof step from Mathlib.Analysis.Complex.Harmonic.Liouville (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℂ → E
h_harm : HarmonicOnNhd f univ
h_bound : IsBounded (range f)
z w : ℂ
ℓ : StrongDual ℝ E
h₁ℓ : ‖ℓ‖ ≤ 1
h₂ℓ : HSub.hSub (α := ℝ) (β := ℝ) ((ℓ : (a : E) → ℝ) (f z) : ℝ) ((ℓ : (a : E) → ℝ) (f w) : ℝ) = ‖f z - f w‖
⊢ f z = f w
have η₁ : IsBounded (α := ℝ) (range ((⇑ℓ : (a : E) → ℝ) ∘ f))
Tactic: have η₁ : Bornology.IsBounded (range (ℓ ∘ f)) := by
    simpa [range_comp] using IsBounded.image ℓ h_bound
-- Lean 4 proof step from Mathlib.Analysis.Complex.Harmonic.Liouville (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℂ → E
h_harm : HarmonicOnNhd f univ
h_bound : IsBounded (range f)
z w : ℂ
ℓ : StrongDual ℝ E
h₁ℓ : ‖ℓ‖ ≤ 1
h₂ℓ : HSub.hSub (α := ℝ) (β := ℝ) ((ℓ : (a : E) → ℝ) (f z) : ℝ) ((ℓ : (a : E) → ℝ) (f w) : ℝ) = ‖f z - f w‖
η₁ : IsBounded (α := ℝ) (range ((⇑ℓ : (a : E) → ℝ) ∘ f))
⊢ f z = f w
have rw : HSub.hSub (α := ℝ) (β := ℝ) ((ℓ : (a : E) → ℝ) (f z) : ℝ) ((ℓ : (a : E) → ℝ) (f w) : ℝ) = 0
Tactic: rw [← sub_eq_zero, ← norm_eq_zero, ← h₂ℓ]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Harmonic.MeanValue (goal)
Goal:
f : ℂ → ℝ
c : ℂ
R : ℝ
hf : HarmonicOnNhd f (closedBall c |R|)
⊢ circleAverage f c R = f c
have obtain : ∀ (e : ℝ) (h₁e : 0 < e) (h₂e : thickening e (closedBall c |R|) ⊆ {x : ℂ | HarmonicAt f x}), circleAverage f c R = f c
Tactic: obtain ⟨e, h₁e, h₂e⟩ := (isCompact_closedBall c |R|).exists_thickening_subset_open
    (isOpen_setOf_harmonicAt f) hf
-- Lean 4 proof step from Mathlib.Analysis.Complex.Harmonic.MeanValue (hypothesis)
Goal:
f : ℂ → ℝ
c : ℂ
R : ℝ
hf : HarmonicOnNhd f (closedBall c |R|)
e : ℝ
h₁e : 0 < e
h₂e : thickening e (closedBall c |R|) ⊆ {x : ℂ | HarmonicAt f x}
⊢ circleAverage f c R = f c
have h₂e₁ : ball c (e + |R|) ⊆ {x : ℂ | HarmonicAt f x}
Tactic: rw [thickening_closedBall h₁e (abs_nonneg R)] at h₂e
Cleared hypotheses: h₂e
-- Lean 4 proof step from Mathlib.Analysis.Complex.Harmonic.MeanValue (goal)
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}
⊢ circleAverage f c R = f c
have 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 f c R = f c
Tactic: obtain ⟨F, h₁F, h₂F⟩ := InnerProductSpace.HarmonicOnNhd.exists_analyticOnNhd_ball_re_eq h₂e
-- Lean 4 proof step from Mathlib.Analysis.Complex.Harmonic.MeanValue (goal)
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|))
x : ℂ
hx : x ∈ closure (ball c |R|)
⊢ DifferentiableWithinAt ℂ F (closure (ball c |R|)) x
have apply : x ∈ ball c (e + |R|)
Tactic: apply (h₁F x _).differentiableWithinAt
-- Lean 4 proof step from Mathlib.Analysis.Complex.Harmonic.MeanValue (hypothesis)
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|))
⊢ circleAverage f c R = f c
have h₃F : 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)]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Harmonic.MeanValue (hypothesis)
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|))
⊢ circleAverage f c R = f c
have h₄F : Set.EqOn ((⇑Complex.reCLM : (a : ℂ) → ℝ) ∘ F) f (sphere c |R|)
Tactic: have h₄F : Set.EqOn (Complex.reCLM ∘ F) f (sphere c |R|) :=
    fun x hx ↦ h₂F (sphere_subset_ball (lt_add_of_pos_left |R| h₁e) hx)
-- Lean 4 proof step from Mathlib.Analysis.Complex.Harmonic.MeanValue (goal)
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|)
⊢ circleAverage f c R = f c
have rw : (Complex.reCLM : (a : ℂ) → ℝ) (F c) = f c
Tactic: rw [← circleAverage_congr_sphere h₄F, Complex.reCLM.circleAverage_comp_comm,
    h₃F.diffContOnCl.circleAverage]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Harmonic.MeanValue (goal)
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|)
rw : (Complex.reCLM : (a : ℂ) → ℝ) (F c) = f c
⊢ circleAverage f c R = f c
have rw₁ : CircleIntegrable F c R
Tactic: rw [← circleAverage_congr_sphere h₄F, Complex.reCLM.circleAverage_comp_comm,
    h₃F.diffContOnCl.circleAverage]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Harmonic.MeanValue (goal)
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|)
⊢ (Complex.reCLM : (a : ℂ) → ℝ) (F c) = f c
have a : c ∈ ball c (e + |R|)
Tactic: apply h₂F
-- Lean 4 proof step from Mathlib.Analysis.Complex.Harmonic.MeanValue (goal)
Goal:
f : ℂ → ℝ
c : ℂ
R : ℝ
h₁f : HarmonicContOnCl f (ball c |R|)
⊢ circleAverage f c R = f c
have pos : ∀ (hR : R = 0), circleAverage f c R = f c
Tactic: by_cases hR : R = 0
-- Lean 4 proof step from Mathlib.Analysis.Complex.Harmonic.MeanValue (goal)
Goal:
f : ℂ → ℝ
c : ℂ
R : ℝ
h₁f : HarmonicContOnCl f (ball c |R|)
pos : ∀ (hR : R = 0), circleAverage f c R = f c
⊢ circleAverage f c R = f c
have neg : ∀ (hR : ¬R = 0), circleAverage f c R = f c
Tactic: by_cases hR : R = 0
-- Lean 4 proof step from Mathlib.Analysis.Complex.Harmonic.MeanValue (goal)
Goal:
f : ℂ → ℝ
c : ℂ
R : ℝ
h₁f : HarmonicContOnCl f (ball c |R|)
hR : ¬R = 0
⊢ ContinuousOn (circleAverage f c) (Set.Ioc 0 |R|)
have refine : {z : ℂ | ‖z - c‖ ∈ Set.Ioc 0 |R|} ⊆ closure (ball c |R|)
Tactic: refine (h₁f.2.mono ?_).circleAverage (fun z hz ↦ hz.1.le)
-- Lean 4 proof step from Mathlib.Analysis.Complex.Harmonic.MeanValue (goal)
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 ∈ closure (ball c |R|)
have rw : ‖x - c‖ ≤ |R|
Tactic: rw [closure_ball _ (by aesop), mem_closedBall_iff_norm]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Harmonic.MeanValue (hypothesis)
Goal:
f : ℂ → ℝ
c : ℂ
R : ℝ
h₁f : HarmonicContOnCl f (ball c |R|)
hR : ¬R = 0
⊢ circleAverage f c R = f c
have H : 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
-- Lean 4 proof step from Mathlib.Analysis.Complex.Harmonic.MeanValue (goal)
Goal:
f : ℂ → ℝ
c : ℂ
R : ℝ
h₁f : HarmonicContOnCl f (ball c |R|)
hR : ¬R = 0
H : ContinuousOn (circleAverage f c) (Set.Ioc 0 |R|)
⊢ circleAverage f c R = f c
have neg : circleAverage f c |R| = f c
Tactic: rw [← circleAverage_abs_radius]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Harmonic.MeanValue (goal)
Goal:
f : ℂ → ℝ
c : ℂ
R : ℝ
h₁f : HarmonicContOnCl f (ball c |R|)
hR : ¬R = 0
H : ContinuousOn (circleAverage f c) (Set.Ioc 0 |R|)
⊢ circleAverage f c |R| = f c
have neg : Set.EqOn (circleAverage f c) (fun (x : ℝ) ↦ f c) (Set.Ioo 0 |R|)
Tactic: apply H.eq_of_eqOn_Ioo (by aesop)
-- Lean 4 proof step from Mathlib.Analysis.Complex.Harmonic.MeanValue (goal)
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|
⊢ circleAverage f c r = (fun (x : ℝ) ↦ f c) r
have neg : HarmonicOnNhd f (closedBall c |r|)
Tactic: apply HarmonicOnNhd.circleAverage_eq
-- Lean 4 proof step from Mathlib.Analysis.Complex.Harmonic.MeanValue (goal)
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|
⊢ HarmonicOnNhd f (closedBall c |r|)
have neg : closedBall c |r| ⊆ ball c |R|
Tactic: apply h₁f.1.mono
-- Lean 4 proof step from Mathlib.Analysis.Complex.Harmonic.MeanValue (goal)
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|
have neg : closedBall c r ⊆ ball c |R|
Tactic: rw [abs_of_pos hr.1]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Harmonic.Poisson (hypothesis)
Goal:
c w : ℂ
R : ℝ
h : w ∈ ball c R
⊢ ContinuousOn (Y := ℝ) (fun (x : ℂ) ↦ ((x - c + (w - c)) / (x - c - (w - c))).re) {z : ℂ | ‖z - c‖ ∈ Set.Ioc ‖w - c‖ R}
have this : ∀ (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]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Harmonic.Poisson (goal)
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
⊢ ContinuousOn (Y := ℝ) (fun (x : ℂ) ↦ ((x - c + (w - c)) / (x - c - (w - c))).re) {z : ℂ | ‖z - c‖ ∈ Set.Ioc ‖w - c‖ R}
have funProp : HarmonicOnNhd (F := ℝ) (fun (x0 : ℂ) ↦ x0.re) ?t
Tactic: fun_prop
-- 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 (re ∘ herglotzRieszKernel c w • f) c R = f w
have 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
Tactic: obtain ⟨e, h₁e, h₂e⟩ := (isCompact_closedBall c R).exists_thickening_subset_open
    (isOpen_setOf_harmonicAt f) (by aesop)
-- 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 : thickening e (closedBall c R) ⊆ {x : ℂ | HarmonicAt f x}
⊢ circleAverage (re ∘ herglotzRieszKernel c w • f) c R = f w
have h₂e₁ : ball c (e + R) ⊆ {x : ℂ | HarmonicAt f x}
Tactic: rw [thickening_closedBall h₁e (pos_of_mem_ball hw).le] at h₂e
Cleared hypotheses: h₂e
-- 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}
⊢ circleAverage (re ∘ herglotzRieszKernel c w • f) c R = f w
have 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
Tactic: obtain ⟨F, h₁F, h₂F⟩ := HarmonicOnNhd.exists_analyticOnNhd_ball_re_eq h₂e
-- 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))
x : ℂ
hx : x ∈ closure (ball c R)
⊢ DifferentiableWithinAt ℂ F (closure (ball c R)) x
have apply : x ∈ ball c (e + R)
Tactic: apply (h₁F x _).differentiableWithinAt
-- 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))
⊢ circleAverage (re ∘ herglotzRieszKernel c w • f) c R = f w
have h₃F : 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)]
-- 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))
⊢ 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: 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]