awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Complex.Harmonic.Analytic
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) : ℝ)
trans₁ :
  Eq (α := ℝ) ((fderiv ℝ f y : (a : ℂ) → ℝ) (HSMul.hSMul (β := ℂ) x.re 1 + x.im • I) : ℝ)
    ((fderiv ℝ f y : (a : ℂ) → ℝ) x : ℝ)
⊢ Eq (α := ℝ) ((fderiv ℝ (⇑reCLM : (a : ℂ) → ℝ) (F y) ∘SL fderiv ℝ F y : (a : ℂ) → ℝ) x : ℝ)
    ((fderiv ℝ f y : (a : ℂ) → ℝ) x : ℝ)

Tactic:
trans fderiv ℝ f y (x.re • (1 : ℂ) + x.im • (I : ℂ))

Premises used: Real, Complex.im, fderiv, Complex.re, HAdd.hAdd, HSMul.hSMul, OfNat.ofNat, DFunLike.coe, Complex.I
-- Module: Mathlib.Analysis.Complex.Harmonic.Analytic
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 : ℂ
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 : ℝ)
⊢ 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:
simp only [map_smul, map_add]

Premises used: map_add, map_smul
-- Module: Mathlib.Analysis.Complex.Harmonic.Analytic
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 : ℂ
⊢ (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 [(h₁F y).hasFDerivAt.restrictScalars ℝ |>.fderiv, g]

Premises used: Real, HasFDerivAt.restrictScalars, HasDerivAt.hasFDerivAt, HasFDerivAt.fderiv
-- Module: Mathlib.Analysis.Complex.Harmonic.Analytic
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 ℝ f y : (a : ℂ) → ℝ) (HSMul.hSMul (β := ℂ) x.re 1 + x.im • I) : ℝ)
    ((fderiv ℝ f y : (a : ℂ) → ℝ) x : ℝ)

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.Harmonic.Analytic
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 : ℂ
⊢ EqOn (β := ℂ →L[ℝ] ℝ) (fderivWithin ℝ ((⇑reCLM : (a : ℂ) → ℝ) ∘ F) univ) (fderivWithin ℝ f univ) univ

Tactic:
case heq =>
    intro y hy
    simp only [fderivWithin_univ]
    rw [fderiv_comp y (by fun_prop) (by fun_prop)]
    ext x
    trans fderiv ℝ f y (x.re • (1 : ℂ) + x.im • (I : ℂ))
    · simp only [map_smul, map_add]
      simp [(h₁F y).hasFDerivAt.restrictScalars ℝ |>.fderiv, g]
    · simp

Premises used: fderivWithin_univ, map_add, map_smul
-- Module: Mathlib.Analysis.Complex.Harmonic.Analytic
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 : ℂ
⊢ UniqueDiffOn ℝ (E := ℂ) univ

Tactic:
simp_all
-- Module: Mathlib.Analysis.Complex.Harmonic.Analytic
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 : ℂ
⊢ Membership.mem (γ := Set ℂ) univ 0

Tactic:
simp_all
-- Module: Mathlib.Analysis.Complex.Harmonic.Analytic
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 : ℂ
⊢ ((⇑reCLM : (a : ℂ) → ℝ) ∘ F) 0 = f 0

Tactic:
simp_all
-- Module: Mathlib.Analysis.Complex.Harmonic.Analytic
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 : ℂ
⊢ Membership.mem (γ := Set ℂ) univ x

Tactic:
simp_all
-- Module: Mathlib.Analysis.Complex.Harmonic.Analytic
Goal:
f : ℂ → ℝ
x : ℂ
hf : HarmonicAt f x
obtain : ∀ (ε : ℝ) (h₁ε : ε > 0) (h₂ε : ball x ε ⊆ {x : ℂ | HarmonicAt f x}), AnalyticAt ℝ f x
⊢ AnalyticAt ℝ f x

Tactic:
obtain ⟨ε, h₁ε, h₂ε⟩ := isOpen_iff.1 (isOpen_setOf_harmonicAt (f := f)) x hf

Premises used: Metric.isOpen_iff, Iff.mp, InnerProductSpace.isOpen_setOf_harmonicAt
-- Module: Mathlib.Analysis.Complex.Harmonic.Analytic
Goal:
f : ℂ → ℝ
x : ℂ
hf : HarmonicAt f x
ε : ℝ
h₁ε : ε > 0
h₂ε : ball x ε ⊆ {x : ℂ | HarmonicAt f x}
obtain :
  ∀ (F : ℂ → ℂ) (h₁F : AnalyticOnNhd ℂ F (ball x ε)) (h₂F : EqOn (fun (z : ℂ) ↦ (F z).re) f (ball x ε)),
    AnalyticAt ℝ f x
⊢ AnalyticAt ℝ f x

Tactic:
obtain ⟨F, h₁F, h₂F⟩ := InnerProductSpace.HarmonicOnNhd.exists_analyticOnNhd_ball_re_eq
    (fun _ hy ↦ h₂ε hy)

Premises used: InnerProductSpace.HarmonicOnNhd.exists_analyticOnNhd_ball_re_eq
-- Module: Mathlib.Analysis.Complex.Harmonic.Analytic
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 ε)
rw : AnalyticAt ℝ (F := ℝ) (fun (y : ℂ) ↦ (F y).re) x
⊢ AnalyticAt ℝ f x

Tactic:
rw [analyticAt_congr (Filter.eventually_of_mem (ball_mem_nhds x h₁ε) (fun y hy ↦ h₂F.symm hy))]

Premises used: Filter.eventually_of_mem, Metric.ball_mem_nhds, Set.EqOn.symm, analyticAt_congr
-- Module: Mathlib.Analysis.Complex.Harmonic.Analytic
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 := ℝ) (fun (y : ℂ) ↦ (F y).re) x

Tactic:
(reCLM.analyticAt (F x)).comp (h₁F x (mem_ball_self h₁ε)).restrictScalars

Premises used: ContinuousLinearMap.analyticAt, Metric.mem_ball_self, AnalyticAt.restrictScalars, Complex.reCLM, AnalyticAt.comp
-- Module: Mathlib.Analysis.Complex.Harmonic.Analytic
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 := ℝ) (fun (y : ℂ) ↦ (F y).re) x

Tactic:
exact (reCLM.analyticAt (F x)).comp (h₁F x (mem_ball_self h₁ε)).restrictScalars

Premises used: ContinuousLinearMap.analyticAt, Metric.mem_ball_self, AnalyticAt.restrictScalars, Complex.reCLM, AnalyticAt.comp
-- Module: Mathlib.Analysis.Complex.Harmonic.Liouville
Goal:
f : ℂ → ℝ
h_harm : HarmonicOnNhd f univ
h_bound : IsBounded (range f)
obtain : ∀ (F : ℂ → ℂ) (hF_diff : AnalyticOnNhd ℂ F univ) (hF_re : (fun (z : ℂ) ↦ (F z).re) = f) (z w : ℂ), f z = f w
⊢ ∀ (z w : ℂ), f z = f w

Tactic:
obtain ⟨F, hF_diff, hF_re⟩ := h_harm.exists_analyticOnNhd_univ_re_eq

Premises used: InnerProductSpace.HarmonicOnNhd.exists_analyticOnNhd_univ_re_eq
-- Module: Mathlib.Analysis.Complex.Harmonic.Liouville
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
this : ∀ (z w : ℂ), cexp (F z) = cexp (F w)
⊢ ∀ (z w : ℂ), f z = f w

Tactic:
grind
-- Module: Mathlib.Analysis.Complex.Harmonic.Liouville
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
suffices : ∀ (z w : ℂ), cexp (F z) = cexp (F w)
⊢ ∀ (z w : ℂ), f z = f w

Tactic:
suffices ∀ z w, Complex.exp (F z) = Complex.exp (F w) by grind
-- Module: Mathlib.Analysis.Complex.Harmonic.Liouville
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)
hb : IsBounded (α := ℂ) (range fun (z : ℂ) ↦ cexp (F z))
⊢ ∀ (z w : ℂ), cexp (F z) = cexp (F w)

Tactic:
apply Differentiable.apply_eq_apply_of_bounded

Premises used: Differentiable.apply_eq_apply_of_bounded
-- Module: Mathlib.Analysis.Complex.Harmonic.Liouville
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
⊢ Differentiable ℂ (F := ℂ) fun (z : ℂ) ↦ cexp (F z)

Tactic:
apply (differentiable_exp.comp (fun x ↦ (hF_diff x (mem_univ x)).differentiableAt))

Premises used: Complex.differentiable_exp, AnalyticAt.differentiableAt, Set.mem_univ, Differentiable.comp
-- Module: Mathlib.Analysis.Complex.Harmonic.Liouville
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
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
⊢ IsBounded (α := ℂ) (range fun (z : ℂ) ↦ cexp (F z))

Tactic:
rw [isBounded_iff_forall_norm_le] at *

Premises used: isBounded_iff_forall_norm_le
-- Module: Mathlib.Analysis.Complex.Harmonic.Liouville
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
hb :
  ∀ (M : ℝ) (hM : ∀ x ∈ range f, ‖x‖ ≤ M),
    ∃ (C : ℝ), ∀ (x : ℂ), Membership.mem (γ := Set ℂ) (range fun (z : ℂ) ↦ cexp (F z)) x → ‖x‖ ≤ C
⊢ ∃ (C : ℝ), ∀ (x : ℂ), Membership.mem (γ := Set ℂ) (range fun (z : ℂ) ↦ cexp (F z)) x → ‖x‖ ≤ C

Tactic:
obtain ⟨M, hM⟩ := h_bound
-- Module: Mathlib.Analysis.Complex.Harmonic.Liouville
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
h : ∀ (x : ℂ), Membership.mem (γ := Set ℂ) (range fun (z : ℂ) ↦ cexp (F z)) x → ‖x‖ ≤ rexp M
⊢ ∃ (C : ℝ), ∀ (x : ℂ), Membership.mem (γ := Set ℂ) (range fun (z : ℂ) ↦ cexp (F z)) x → ‖x‖ ≤ C

Tactic:
use Real.exp M

Premises used: Real.exp
-- Module: Mathlib.Analysis.Complex.Harmonic.Liouville
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
h : ∀ (hM : ∀ (a : ℂ), |f a| ≤ M) (a : ℂ), (F a).re ≤ M
⊢ ∀ (x : ℂ), Membership.mem (γ := Set ℂ) (range fun (z : ℂ) ↦ cexp (F z)) x → ‖x‖ ≤ rexp M

Tactic:
simp_all only [mem_range, norm_eq_abs, forall_exists_index, forall_apply_eq_imp_iff,
    norm_exp, exp_le_exp]

Premises used: Set.mem_range, forall_exists_index, Real.exp_le_exp, Complex.norm_exp, forall_apply_eq_imp_iff, Real.norm_eq_abs
-- Module: Mathlib.Analysis.Complex.Harmonic.Liouville
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 : ℂ), |(fun (z : ℂ) ↦ (F z).re) a| ≤ M

Tactic:
rw [← hF_re] at hM
-- Module: Mathlib.Analysis.Complex.Harmonic.Liouville
Goal:
f : ℂ → ℝ
h_harm : HarmonicOnNhd f univ
F : ℂ → ℂ
hF_diff : AnalyticOnNhd ℂ F univ
hF_re : (fun (z : ℂ) ↦ (F z).re) = f
M : ℝ
hM : ∀ (a : ℂ), |(fun (z : ℂ) ↦ (F z).re) a| ≤ M
⊢ ∀ (a : ℂ), (F a).re ≤ M

Tactic:
grind
-- Module: Mathlib.Analysis.Complex.Harmonic.Liouville
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 : ℂ
obtain :
  ∀ (ℓ : StrongDual ℝ E) (h₁ℓ : ‖ℓ‖ ≤ 1)
    (h₂ℓ : Eq (α := ℝ) ((ℓ : (a : E) → ℝ) (f z - f w) : ℝ) ((↑‖f z - f w‖ : ℝ) : ℝ)), f z = f w
⊢ f z = f w

Tactic:
obtain ⟨ℓ, h₁ℓ, h₂ℓ⟩ := exists_dual_vector'' ℝ (f z - f w)

Premises used: Real, HSub.hSub, exists_dual_vector''
-- Module: Mathlib.Analysis.Complex.Harmonic.Liouville
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‖ : ℝ) : ℝ)
⊢ 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₂ℓ

Premises used: map_sub, RCLike.ofReal_real_eq_id, id_eq
-- Module: Mathlib.Analysis.Complex.Harmonic.Liouville
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))

Tactic:
simpa [range_comp] using IsBounded.image ℓ h_bound

Premises used: Bornology.IsBounded.image, Set.range_comp
-- Module: Mathlib.Analysis.Complex.Harmonic.Liouville
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))

Tactic:
have η₁ : Bornology.IsBounded (range (ℓ ∘ f)) := by
    simpa [range_comp] using IsBounded.image ℓ h_bound
-- Module: Mathlib.Analysis.Complex.Harmonic.Liouville
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))
rw : HSub.hSub (α := ℝ) (β := ℝ) ((ℓ : (a : E) → ℝ) (f z) : ℝ) ((ℓ : (a : E) → ℝ) (f w) : ℝ) = 0
⊢ f z = f w

Tactic:
rw [← sub_eq_zero, ← norm_eq_zero, ← h₂ℓ]

Premises used: norm_eq_zero, sub_eq_zero
-- Module: Mathlib.Analysis.Complex.Harmonic.Liouville
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))
⊢ HSub.hSub (α := ℝ) (β := ℝ) ((ℓ : (a : E) → ℝ) (f z) : ℝ) ((ℓ : (a : E) → ℝ) (f w) : ℝ) = 0

Tactic:
grind [bounded_harmonic_on_complex_plane_is_constant_aux (ℓ ∘ f) (h_harm.comp_CLM ℓ) η₁]

Premises used: InnerProductSpace.HarmonicOnNhd.comp_CLM, Function.comp, _private.0.InnerProductSpace.bounded_harmonic_on_complex_plane_is_constant_aux, DFunLike.coe
-- Module: Mathlib.Analysis.Complex.Harmonic.MeanValue
Goal:
f : ℂ → ℝ
c : ℂ
R : ℝ
hf : HarmonicOnNhd f (closedBall c |R|)
obtain :
  ∀ (e : ℝ) (h₁e : 0 < e) (h₂e : thickening e (closedBall c |R|) ⊆ {x : ℂ | HarmonicAt f x}), circleAverage f c R = f c
⊢ 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

Premises used: abs, InnerProductSpace.isOpen_setOf_harmonicAt, ProperSpace.isCompact_closedBall, IsCompact.exists_thickening_subset_open
-- Module: Mathlib.Analysis.Complex.Harmonic.MeanValue
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}
⊢ ball c (e + |R|) ⊆ {x : ℂ | HarmonicAt f x}

Tactic:
rw [thickening_closedBall h₁e (abs_nonneg R)] at h₂e

Premises used: thickening_closedBall, abs_nonneg
-- 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}
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
⊢ circleAverage f c R = f c

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

Premises used: InnerProductSpace.HarmonicOnNhd.exists_analyticOnNhd_ball_re_eq
-- 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|))
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.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|))
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.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|))
⊢ 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.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|))
⊢ 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)
-- 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|)
rw : (Complex.reCLM : (a : ℂ) → ℝ) (F c) = f c
rw₁ : CircleIntegrable F c R
⊢ circleAverage f c R = f c

Tactic:
rw [← circleAverage_congr_sphere h₄F, Complex.reCLM.circleAverage_comp_comm,
    h₃F.diffContOnCl.circleAverage]

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

Tactic:
apply h₂F
-- 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|)
⊢ c ∈ ball c (e + |R|)

Tactic:
simp [mem_ball, dist_self, add_pos_of_pos_of_nonneg h₁e (abs_nonneg R)]

Premises used: Metric.mem_ball, dist_self, abs_nonneg, add_pos_of_pos_of_nonneg
-- 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|)
x : ℂ
h : x ∈ sphere c |R|
⊢ x ∈ ball c (e + |R|)

Tactic:
simp_all [dist_eq_norm]

Premises used: dist_eq_norm