awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions
Goal:
z : ℂ
g : ℂ → ℂ
h₁g : AnalyticAt ℂ g z
h₂g : g z ≠ 0
h₃g : g z ∈ slitPlane
t₀ : g ⁻¹' (slitPlane ∩ {y : ℂ | y ≠ 0}) ∈ 𝓝 z
⊢ Real.log ∘ (⇑normSq : (a : ℂ) → ℝ) ∘ g =ᶠ[𝓝 z]
    Function.comp (β := ℂ) (⇑reCLM : (a : ℂ) → ℝ) ((⇑ofRealCLM : (a : ℝ) → ℂ) ∘ Real.log ∘ (⇑normSq : (a : ℂ) → ℝ) ∘ g)

Tactic:
aesop
-- Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions
Goal:
z : ℂ
g : ℂ → ℂ
h₁g : AnalyticAt ℂ g z
h₂g : g z ≠ 0
h₃g : g z ∈ slitPlane
t₀ : g ⁻¹' (slitPlane ∩ {y : ℂ | y ≠ 0}) ∈ 𝓝 z
h :
  ∀ (x : ℂ),
    Eq (α := ℝ)
      (Function.comp (β := ℂ) (⇑reCLM : (a : ℂ) → ℝ)
        ((⇑ofRealCLM : (a : ℝ) → ℂ) ∘ Real.log ∘ (⇑normSq : (a : ℂ) → ℝ) ∘ g) x)
      (((⇑reCLM : (a : ℂ) → ℝ) ∘ log ∘ ((⇑conjCLE : (a : ℂ) → ℂ) ∘ g * g)) x)
⊢ (𝓝 z).EventuallyEq (β := ℝ)
    (Function.comp (β := ℂ) (⇑reCLM : (a : ℂ) → ℝ)
      ((⇑ofRealCLM : (a : ℝ) → ℂ) ∘ Real.log ∘ (⇑normSq : (a : ℂ) → ℝ) ∘ g))
    ((⇑reCLM : (a : ℂ) → ℝ) ∘ log ∘ ((⇑conjCLE : (a : ℂ) → ℂ) ∘ g * g))

Tactic:
filter_upwards with x
-- Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions
Goal:
z : ℂ
g : ℂ → ℂ
h₁g : AnalyticAt ℂ g z
h₂g : g z ≠ 0
h₃g : g z ∈ slitPlane
t₀ : g ⁻¹' (slitPlane ∩ {y : ℂ | y ≠ 0}) ∈ 𝓝 z
x : ℂ
h : LE.le (α := ℝ) (0 : ℝ) ((normSq : (a : ℂ) → ℝ) (g x) : ℝ)
⊢ Eq (α := ℝ) ((reCLM : (a : ℂ) → ℝ) (↑(Real.log ((normSq : (a : ℂ) → ℝ) (g x))) : ℂ) : ℝ)
    ((reCLM : (a : ℂ) → ℝ) (log (HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (g x) : ℂ) (g x))) : ℝ)

Tactic:
rw [ofReal_log, normSq_eq_conj_mul_self]

Premises used: Complex.ofReal_log, Complex.normSq_eq_conj_mul_self
-- Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions
Goal:
z : ℂ
g : ℂ → ℂ
h₁g : AnalyticAt ℂ g z
h₂g : g z ≠ 0
h₃g : g z ∈ slitPlane
t₀ : g ⁻¹' (slitPlane ∩ {y : ℂ | y ≠ 0}) ∈ 𝓝 z
x : ℂ
⊢ LE.le (α := ℝ) (0 : ℝ) ((normSq : (a : ℂ) → ℝ) (g x) : ℝ)

Tactic:
normSq_nonneg (g x)

Premises used: Complex.normSq_nonneg
-- Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions
Goal:
z : ℂ
g : ℂ → ℂ
h₁g : AnalyticAt ℂ g z
h₂g : g z ≠ 0
h₃g : g z ∈ slitPlane
t₀ : g ⁻¹' (slitPlane ∩ {y : ℂ | y ≠ 0}) ∈ 𝓝 z
x : ℂ
⊢ LE.le (α := ℝ) (0 : ℝ) ((normSq : (a : ℂ) → ℝ) (g x) : ℝ)

Tactic:
exact normSq_nonneg (g x)

Premises used: Complex.normSq_nonneg
-- Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions
Goal:
z : ℂ
g : ℂ → ℂ
h₁g : AnalyticAt ℂ g z
h₂g : g z ≠ 0
h₃g : g z ∈ slitPlane
t₀ : g ⁻¹' (slitPlane ∩ {y : ℂ | y ≠ 0}) ∈ 𝓝 z
h :
  ∀ (x : ℂ) (hx : x ∈ g ⁻¹' (slitPlane ∩ {y : ℂ | y ≠ 0})),
    Eq (α := ℝ) (((⇑reCLM : (a : ℂ) → ℝ) ∘ log ∘ ((⇑conjCLE : (a : ℂ) → ℂ) ∘ g * g)) x)
      (((⇑reCLM : (a : ℂ) → ℝ) ∘ (log ∘ (⇑conjCLE : (a : ℂ) → ℂ) ∘ g + log ∘ g)) x)
⊢ (𝓝 z).EventuallyEq (β := ℝ) ((⇑reCLM : (a : ℂ) → ℝ) ∘ log ∘ ((⇑conjCLE : (a : ℂ) → ℂ) ∘ g * g))
    ((⇑reCLM : (a : ℂ) → ℝ) ∘ (log ∘ (⇑conjCLE : (a : ℂ) → ℂ) ∘ g + log ∘ g))

Tactic:
filter_upwards [t₀] with x hx
-- Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions
Goal:
z : ℂ
g : ℂ → ℂ
h₁g : AnalyticAt ℂ g z
h₂g : g z ≠ 0
h₃g : g z ∈ slitPlane
t₀ : g ⁻¹' (slitPlane ∩ {y : ℂ | y ≠ 0}) ∈ 𝓝 z
x : ℂ
hx : x ∈ g ⁻¹' (slitPlane ∩ {y : ℂ | y ≠ 0})
h :
  log (HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (g x) : ℂ) (g x)) =
    log ((starRingEnd ℂ : (a : ℂ) → ℂ) (g x)) + log (g x)
⊢ Eq (α := ℝ) ((reCLM : (a : ℂ) → ℝ) (log (HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (g x) : ℂ) (g x))) : ℝ)
    ((reCLM : (a : ℂ) → ℝ) (log ((starRingEnd ℂ : (a : ℂ) → ℂ) (g x)) + log (g x)) : ℝ)

Tactic:
congr
-- Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions
Goal:
z : ℂ
g : ℂ → ℂ
h₁g : AnalyticAt ℂ g z
h₂g : g z ≠ 0
h₃g : g z ∈ slitPlane
t₀ : g ⁻¹' (slitPlane ∩ {y : ℂ | y ≠ 0}) ∈ 𝓝 z
x : ℂ
hx : x ∈ g ⁻¹' (slitPlane ∩ {y : ℂ | y ≠ 0})
h : (if (g x).arg = Real.pi then Real.pi else -(g x).arg) + (g x).arg ∈ Set.Ioc (-Real.pi) Real.pi
rw : Ne (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (g x) : ℂ) (0 : ℂ)
⊢ log (HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (g x) : ℂ) (g x)) =
    log ((starRingEnd ℂ : (a : ℂ) → ℂ) (g x)) + log (g x)

Tactic:
rw [Complex.log_mul_eq_add_log_iff _ hx.2, Complex.arg_conj]

Premises used: Complex.arg_conj, Complex.log_mul_eq_add_log_iff, And.right
-- Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions
Goal:
z : ℂ
g : ℂ → ℂ
h₁g : AnalyticAt ℂ g z
h₂g : g z ≠ 0
h₃g : g z ∈ slitPlane
t₀ : g ⁻¹' (slitPlane ∩ {y : ℂ | y ≠ 0}) ∈ 𝓝 z
x : ℂ
hx : x ∈ g ⁻¹' (slitPlane ∩ {y : ℂ | y ≠ 0})
⊢ (if (g x).arg = Real.pi then Real.pi else -(g x).arg) + (g x).arg ∈ Set.Ioc (-Real.pi) Real.pi

Tactic:
simp [Complex.slitPlane_arg_ne_pi hx.1, Real.pi_pos, Real.pi_nonneg]

Premises used: Real.pi_nonneg, Real.pi_pos, And.left, Complex.slitPlane_arg_ne_pi
-- Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions
Goal:
z : ℂ
g : ℂ → ℂ
h₁g : AnalyticAt ℂ g z
h₂g : g z ≠ 0
h₃g : g z ∈ slitPlane
t₀ : g ⁻¹' (slitPlane ∩ {y : ℂ | y ≠ 0}) ∈ 𝓝 z
x : ℂ
hx : x ∈ g ⁻¹' (slitPlane ∩ {y : ℂ | y ≠ 0})
⊢ Ne (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (g x) : ℂ) (0 : ℂ)

Tactic:
simpa [ne_eq, map_eq_zero] using hx.2

Premises used: map_eq_zero, ne_eq, And.right
-- Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions
Goal:
z : ℂ
g : ℂ → ℂ
h₁g : AnalyticAt ℂ g z
h₂g : g z ≠ 0
h₃g : g z ∈ slitPlane
t₀ : g ⁻¹' (slitPlane ∩ {y : ℂ | y ≠ 0}) ∈ 𝓝 z
apply :
  ∃ s ∈ 𝓝 z,
    Set.EqOn (β := ℝ) ((⇑reCLM : (a : ℂ) → ℝ) ∘ (log ∘ (⇑conjCLE : (a : ℂ) → ℂ) ∘ g + log ∘ g))
      ((⇑reCLM : (a : ℂ) → ℝ) ∘ ((⇑conjCLE : (a : ℂ) → ℂ) ∘ log ∘ g + log ∘ g)) s
⊢ (𝓝 z).EventuallyEq (β := ℝ) ((⇑reCLM : (a : ℂ) → ℝ) ∘ (log ∘ (⇑conjCLE : (a : ℂ) → ℂ) ∘ g + log ∘ g))
    ((⇑reCLM : (a : ℂ) → ℝ) ∘ ((⇑conjCLE : (a : ℂ) → ℂ) ∘ log ∘ g + log ∘ g))

Tactic:
apply Filter.eventuallyEq_iff_exists_mem.2

Premises used: Iff.mpr, Filter.eventuallyEq_iff_exists_mem
-- Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions
Goal:
z : ℂ
g : ℂ → ℂ
h₁g : AnalyticAt ℂ g z
h₂g : g z ≠ 0
h₃g : g z ∈ slitPlane
t₀ : g ⁻¹' (slitPlane ∩ {y : ℂ | y ≠ 0}) ∈ 𝓝 z
right :
  Set.EqOn (β := ℝ) ((⇑reCLM : (a : ℂ) → ℝ) ∘ (log ∘ (⇑conjCLE : (a : ℂ) → ℂ) ∘ g + log ∘ g))
    ((⇑reCLM : (a : ℂ) → ℝ) ∘ ((⇑conjCLE : (a : ℂ) → ℂ) ∘ log ∘ g + log ∘ g)) (g ⁻¹' (slitPlane ∩ {0}ᶜ))
⊢ ∃ s ∈ 𝓝 z,
    Set.EqOn (β := ℝ) ((⇑reCLM : (a : ℂ) → ℝ) ∘ (log ∘ (⇑conjCLE : (a : ℂ) → ℂ) ∘ g + log ∘ g))
      ((⇑reCLM : (a : ℂ) → ℝ) ∘ ((⇑conjCLE : (a : ℂ) → ℂ) ∘ log ∘ g + log ∘ g)) s

Tactic:
use g ⁻¹' (Complex.slitPlane ∩ {0}ᶜ), t₀

Premises used: Compl.compl, Inter.inter, Singleton.singleton, OfNat.ofNat, Complex.slitPlane
-- Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions
Goal:
z : ℂ
g : ℂ → ℂ
h₁g : AnalyticAt ℂ g z
h₂g : g z ≠ 0
h₃g : g z ∈ slitPlane
t₀ : g ⁻¹' (slitPlane ∩ {y : ℂ | y ≠ 0}) ∈ 𝓝 z
x : ℂ
hx : x ∈ g ⁻¹' (slitPlane ∩ {0}ᶜ)
right :
  log ((starRingEnd ℂ : (a : ℂ) → ℂ) (g x)) + log (g x) =
    HAdd.hAdd (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (log (g x)) : ℂ) (log (g x))
⊢ Eq (α := ℝ) ((reCLM : (a : ℂ) → ℝ) (log ((starRingEnd ℂ : (a : ℂ) → ℂ) (g x)) + log (g x)) : ℝ)
    ((reCLM : (a : ℂ) → ℝ) (HAdd.hAdd (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (log (g x)) : ℂ) (log (g x))) : ℝ)

Tactic:
congr 1
-- Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions
Goal:
z : ℂ
g : ℂ → ℂ
h₁g : AnalyticAt ℂ g z
h₂g : g z ≠ 0
h₃g : g z ∈ slitPlane
t₀ : g ⁻¹' (slitPlane ∩ {y : ℂ | y ≠ 0}) ∈ 𝓝 z
x : ℂ
hx : x ∈ g ⁻¹' (slitPlane ∩ {0}ᶜ)
right : (g x).arg ≠ Real.pi
⊢ log ((starRingEnd ℂ : (a : ℂ) → ℂ) (g x)) + log (g x) =
    HAdd.hAdd (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (log (g x)) : ℂ) (log (g x))

Tactic:
rw [← Complex.log_conj]

Premises used: Complex.log_conj
-- Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions
Goal:
z : ℂ
g : ℂ → ℂ
h₁g : AnalyticAt ℂ g z
h₂g : g z ≠ 0
h₃g : g z ∈ slitPlane
t₀ : g ⁻¹' (slitPlane ∩ {y : ℂ | y ≠ 0}) ∈ 𝓝 z
x : ℂ
hx : x ∈ g ⁻¹' (slitPlane ∩ {0}ᶜ)
⊢ (g x).arg ≠ Real.pi

Tactic:
simp [Complex.slitPlane_arg_ne_pi hx.1]

Premises used: And.left, Complex.slitPlane_arg_ne_pi
-- Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions
Goal:
z : ℂ
g : ℂ → ℂ
h₁g : AnalyticAt ℂ g z
h₂g : g z ≠ 0
h₃g : g z ∈ slitPlane
t₀ : g ⁻¹' (slitPlane ∩ {y : ℂ | y ≠ 0}) ∈ 𝓝 z
calc :
  Real.log ∘ (⇑normSq : (a : ℂ) → ℝ) ∘ g =ᶠ[𝓝 z]
    Function.comp (β := ℂ) (⇑reCLM : (a : ℂ) → ℝ) ((⇑ofRealCLM : (a : ℝ) → ℂ) ∘ Real.log ∘ (⇑normSq : (a : ℂ) → ℝ) ∘ g)
calc₁ :
  (𝓝 z).EventuallyEq (β := ℝ)
    (Function.comp (β := ℂ) (⇑reCLM : (a : ℂ) → ℝ)
      ((⇑ofRealCLM : (a : ℝ) → ℂ) ∘ Real.log ∘ (⇑normSq : (a : ℂ) → ℝ) ∘ g))
    ((⇑reCLM : (a : ℂ) → ℝ) ∘ log ∘ ((⇑conjCLE : (a : ℂ) → ℂ) ∘ g * g))
calc₂ :
  (𝓝 z).EventuallyEq (β := ℝ) ((⇑reCLM : (a : ℂ) → ℝ) ∘ log ∘ ((⇑conjCLE : (a : ℂ) → ℂ) ∘ g * g))
    ((⇑reCLM : (a : ℂ) → ℝ) ∘ (log ∘ (⇑conjCLE : (a : ℂ) → ℂ) ∘ g + log ∘ g))
calc₃ :
  (𝓝 z).EventuallyEq (β := ℝ) ((⇑reCLM : (a : ℂ) → ℝ) ∘ (log ∘ (⇑conjCLE : (a : ℂ) → ℂ) ∘ g + log ∘ g))
    ((⇑reCLM : (a : ℂ) → ℝ) ∘ ((⇑conjCLE : (a : ℂ) → ℂ) ∘ log ∘ g + log ∘ g))
⊢ Real.log ∘ (⇑normSq : (a : ℂ) → ℝ) ∘ g =ᶠ[𝓝 z] (⇑reCLM : (a : ℂ) → ℝ) ∘ ((⇑conjCLE : (a : ℂ) → ℂ) ∘ log ∘ g + log ∘ g)

Tactic:
calc Real.log ∘ normSq ∘ g
    _ =ᶠ[𝓝 z] reCLM ∘ ofRealCLM ∘ Real.log ∘ normSq ∘ g := by aesop
    _ =ᶠ[𝓝 z] reCLM ∘ log ∘ ((conjCLE ∘ g) * g) := by
      filter_upwards with x
      simp only [Function.comp_apply, ofRealCLM_apply, Pi.mul_apply, conjCLE_apply]
      rw [ofReal_log, normSq_eq_conj_mul_self]
      exact normSq_nonneg (g x)
    _ =ᶠ[𝓝 z] reCLM ∘ (log ∘ conjCLE ∘ g + log ∘ g) := by
      filter_upwards [t₀] with x hx
      simp only [Function.comp_apply, Pi.mul_apply, conjCLE_apply, Pi.add_apply]
      congr
      rw [Complex.log_mul_eq_add_log_iff _ hx.2, Complex.arg_conj]
      · simp [Complex.slitPlane_arg_ne_pi hx.1, Real.pi_pos, Real.pi_nonneg]
      · simpa [ne_eq, map_eq_zero] using hx.2
    _ =ᶠ[𝓝 z] ⇑reCLM ∘ (⇑conjCLE ∘ log ∘ g + log ∘ g) := by
      apply Filter.eventuallyEq_iff_exists_mem.2
      use g ⁻¹' (Complex.slitPlane ∩ {0}ᶜ), t₀
      intro x hx
      simp only [Function.comp_apply, Pi.add_apply, conjCLE_apply]
      congr 1
      rw [← Complex.log_conj]
      simp [Complex.slitPlane_arg_ne_pi hx.1]

Premises used: Complex.log, HMul.hMul, Function.comp, nhds, Complex.normSq, Complex.ofRealCLM, Real.log, HAdd.hAdd, Complex.conjCLE, Complex.reCLM, DFunLike.coe
-- Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions
Goal:
f : ℂ → ℂ
z : ℂ
h₁f : AnalyticAt ℂ f z
h₂f : f z ≠ 0
h : ∀ (z : ℂ), Real.log ‖f z‖ = HSMul.hSMul (α := ℝ) 2⁻¹ (Real.log ∘ (⇑normSq : (a : ℂ) → ℝ) ∘ f) z
⊢ (fun (x : ℂ) ↦ Real.log ‖f x‖) = HSMul.hSMul (α := ℝ) 2⁻¹ (Real.log ∘ (⇑normSq : (a : ℂ) → ℝ) ∘ f)

Tactic:
funext z
-- Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions
Goal:
f : ℂ → ℂ
z_1 : ℂ
h₁f : AnalyticAt ℂ f z_1
h₂f : f z_1 ≠ 0
z : ℂ
h : Real.log ((normSq : (a : ℂ) → ℝ) (f z)) / 2 = 2⁻¹ * Real.log ((normSq : (a : ℂ) → ℝ) (f z))
h₁ : LE.le (α := ℝ) (0 : ℝ) ((normSq : (a : ℂ) → ℝ) (f z) : ℝ)
⊢ Real.log ‖f z‖ = 2⁻¹ * Real.log ((normSq : (a : ℂ) → ℝ) (f z))

Tactic:
rw [Complex.norm_def, Real.log_sqrt]

Premises used: Real.log_sqrt, Complex.norm_def
-- Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions
Goal:
f : ℂ → ℂ
z_1 : ℂ
h₁f : AnalyticAt ℂ f z_1
h₂f : f z_1 ≠ 0
z : ℂ
linarith : Real.log ((normSq : (a : ℂ) → ℝ) (f z)) / 2 < 2⁻¹ * Real.log ((normSq : (a : ℂ) → ℝ) (f z)) → 2 / 2 = 1
linarith₁ :
  Real.log ((normSq : (a : ℂ) → ℝ) (f z)) / 2 < 2⁻¹ * Real.log ((normSq : (a : ℂ) → ℝ) (f z)) →
    HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : Real.log ((normSq : (a : ℂ) → ℝ) (f z)) / 2 < 2⁻¹ * Real.log ((normSq : (a : ℂ) → ℝ) (f z)) → 2 / 2 = 1
linarith₃ :
  Real.log ((normSq : (a : ℂ) → ℝ) (f z)) / 2 < 2⁻¹ * Real.log ((normSq : (a : ℂ) → ℝ) (f z)) →
    HMul.hMul (α := ℝ) 1 2 = 2
linarith₄ :
  Real.log ((normSq : (a : ℂ) → ℝ) (f z)) / 2 < 2⁻¹ * Real.log ((normSq : (a : ℂ) → ℝ) (f z)) →
    HMul.hMul (α := ℝ) 2 1 = 2
linarith₅ :
  Real.log ((normSq : (a : ℂ) → ℝ) (f z)) / 2 < 2⁻¹ * Real.log ((normSq : (a : ℂ) → ℝ) (f z)) → GT.gt (α := ℝ) 2 0
linarith₆ :
  Real.log ((normSq : (a : ℂ) → ℝ) (f z)) / 2 < 2⁻¹ * Real.log ((normSq : (a : ℂ) → ℝ) (f z)) →
    1 * Real.log ((normSq : (a : ℂ) → ℝ) (f z)) -
        HMul.hMul (α := ℝ) 1 1 * (1 * Real.log ((normSq : (a : ℂ) → ℝ) (f z))) =
      0
linarith₇ : 2⁻¹ * Real.log ((normSq : (a : ℂ) → ℝ) (f z)) < Real.log ((normSq : (a : ℂ) → ℝ) (f z)) / 2 → 2 / 2 = 1
linarith₈ :
  2⁻¹ * Real.log ((normSq : (a : ℂ) → ℝ) (f z)) < Real.log ((normSq : (a : ℂ) → ℝ) (f z)) / 2 →
    HMul.hMul (α := ℝ) 1 2 = 2
linarith₉ :
  2⁻¹ * Real.log ((normSq : (a : ℂ) → ℝ) (f z)) < Real.log ((normSq : (a : ℂ) → ℝ) (f z)) / 2 →
    HMul.hMul (α := ℝ) 2 1 = 2
linarith₁₀ : 2⁻¹ * Real.log ((normSq : (a : ℂ) → ℝ) (f z)) < Real.log ((normSq : (a : ℂ) → ℝ) (f z)) / 2 → 2 / 2 = 1
linarith₁₁ :
  2⁻¹ * Real.log ((normSq : (a : ℂ) → ℝ) (f z)) < Real.log ((normSq : (a : ℂ) → ℝ) (f z)) / 2 →
    HMul.hMul (α := ℝ) 1 2 = 2
linarith₁₂ :
  2⁻¹ * Real.log ((normSq : (a : ℂ) → ℝ) (f z)) < Real.log ((normSq : (a : ℂ) → ℝ) (f z)) / 2 → GT.gt (α := ℝ) 2 0
linarith₁₃ :
  2⁻¹ * Real.log ((normSq : (a : ℂ) → ℝ) (f z)) < Real.log ((normSq : (a : ℂ) → ℝ) (f z)) / 2 →
    HMul.hMul (α := ℝ) 1 1 * (1 * Real.log ((normSq : (a : ℂ) → ℝ) (f z))) -
        1 * Real.log ((normSq : (a : ℂ) → ℝ) (f z)) =
      0
⊢ Real.log ((normSq : (a : ℂ) → ℝ) (f z)) / 2 = 2⁻¹ * Real.log ((normSq : (a : ℂ) → ℝ) (f z))

Tactic:
linarith
-- Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions
Goal:
f : ℂ → ℂ
z_1 : ℂ
h₁f : AnalyticAt ℂ f z_1
h₂f : f z_1 ≠ 0
z : ℂ
⊢ LE.le (α := ℝ) (0 : ℝ) ((normSq : (a : ℂ) → ℝ) (f z) : ℝ)

Tactic:
(f z).normSq_nonneg

Premises used: Complex.normSq_nonneg
-- Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions
Goal:
f : ℂ → ℂ
z_1 : ℂ
h₁f : AnalyticAt ℂ f z_1
h₂f : f z_1 ≠ 0
z : ℂ
⊢ LE.le (α := ℝ) (0 : ℝ) ((normSq : (a : ℂ) → ℝ) (f z) : ℝ)

Tactic:
exact (f z).normSq_nonneg

Premises used: Complex.normSq_nonneg
-- Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions
Goal:
f : ℂ → ℂ
z : ℂ
h₁f : AnalyticAt ℂ f z
h₂f : f z ≠ 0
⊢ (fun (x : ℂ) ↦ Real.log ‖f x‖) = HSMul.hSMul (α := ℝ) 2⁻¹ (Real.log ∘ (⇑normSq : (a : ℂ) → ℝ) ∘ f)

Tactic:
have : (Real.log ‖f ·‖) = (2 : ℝ)⁻¹ • (Real.log ∘ Complex.normSq ∘ f) := by
    funext z
    simp only [Pi.smul_apply, Function.comp_apply, smul_eq_mul]
    rw [Complex.norm_def, Real.log_sqrt]
    · linarith
    exact (f z).normSq_nonneg
-- Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions
Goal:
f : ℂ → ℂ
z : ℂ
h₁f : AnalyticAt ℂ f z
h₂f : f z ≠ 0
this : (fun (x : ℂ) ↦ Real.log ‖f x‖) = HSMul.hSMul (α := ℝ) 2⁻¹ (Real.log ∘ (⇑normSq : (a : ℂ) → ℝ) ∘ f)
rw : HarmonicAt (HSMul.hSMul (α := ℝ) 2⁻¹ (Real.log ∘ (⇑normSq : (a : ℂ) → ℝ) ∘ f)) z
⊢ HarmonicAt (F := ℝ) (fun (x : ℂ) ↦ Real.log ‖f x‖) z

Tactic:
rw [this]
-- Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions
Goal:
f : ℂ → ℂ
z : ℂ
h₁f : AnalyticAt ℂ f z
h₂f : f z ≠ 0
this : (fun (x : ℂ) ↦ Real.log ‖f x‖) = HSMul.hSMul (α := ℝ) 2⁻¹ (Real.log ∘ (⇑normSq : (a : ℂ) → ℝ) ∘ f)
h : HarmonicAt (Real.log ∘ (⇑normSq : (a : ℂ) → ℝ) ∘ f) z
⊢ HarmonicAt (HSMul.hSMul (α := ℝ) 2⁻¹ (Real.log ∘ (⇑normSq : (a : ℂ) → ℝ) ∘ f)) z

Tactic:
apply HarmonicAt.const_smul

Premises used: InnerProductSpace.HarmonicAt.const_smul
-- Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions
Goal:
f : ℂ → ℂ
z : ℂ
h₁f : AnalyticAt ℂ f z
h₂f : f z ≠ 0
this : (fun (x : ℂ) ↦ Real.log ‖f x‖) = HSMul.hSMul (α := ℝ) 2⁻¹ (Real.log ∘ (⇑normSq : (a : ℂ) → ℝ) ∘ f)
pos : ∀ (h₃f : f z ∈ slitPlane), HarmonicAt (Real.log ∘ (⇑normSq : (a : ℂ) → ℝ) ∘ f) z
neg : ∀ (h₃f : f z ∉ slitPlane), HarmonicAt (Real.log ∘ (⇑normSq : (a : ℂ) → ℝ) ∘ f) z
⊢ HarmonicAt (Real.log ∘ (⇑normSq : (a : ℂ) → ℝ) ∘ f) z

Tactic:
by_cases h₃f : f z ∈ Complex.slitPlane

Premises used: Complex.slitPlane
-- Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions
Goal:
f : ℂ → ℂ
z : ℂ
h₁f : AnalyticAt ℂ f z
h₂f : f z ≠ 0
this : (fun (x : ℂ) ↦ Real.log ‖f x‖) = HSMul.hSMul (α := ℝ) 2⁻¹ (Real.log ∘ (⇑normSq : (a : ℂ) → ℝ) ∘ f)
h₃f : f z ∈ slitPlane
⊢ HarmonicAt (Real.log ∘ (⇑normSq : (a : ℂ) → ℝ) ∘ f) z

Tactic:
analyticAt_harmonicAt_log_normSq h₁f h₂f h₃f

Premises used: _private.0.analyticAt_harmonicAt_log_normSq
-- Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions
Goal:
f : ℂ → ℂ
z : ℂ
h₁f : AnalyticAt ℂ f z
h₂f : f z ≠ 0
this : (fun (x : ℂ) ↦ Real.log ‖f x‖) = HSMul.hSMul (α := ℝ) 2⁻¹ (Real.log ∘ (⇑normSq : (a : ℂ) → ℝ) ∘ f)
h₃f : f z ∈ slitPlane
⊢ HarmonicAt (Real.log ∘ (⇑normSq : (a : ℂ) → ℝ) ∘ f) z

Tactic:
exact analyticAt_harmonicAt_log_normSq h₁f h₂f h₃f

Premises used: _private.0.analyticAt_harmonicAt_log_normSq
-- Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions
Goal:
f : ℂ → ℂ
z : ℂ
h₁f : AnalyticAt ℂ f z
h₂f : f z ≠ 0
this : (fun (x : ℂ) ↦ Real.log ‖f x‖) = HSMul.hSMul (α := ℝ) 2⁻¹ (Real.log ∘ (⇑normSq : (a : ℂ) → ℝ) ∘ f)
h₃f : f z ∉ slitPlane
⊢ Eq (α := ℂ → ℝ) ((⇑normSq : (a : ℂ) → ℝ) ∘ f) ((⇑normSq : (a : ℂ) → ℝ) ∘ (-f))

Tactic:
aesop
-- Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions
Goal:
f : ℂ → ℂ
z : ℂ
h₁f : AnalyticAt ℂ f z
h₂f : f z ≠ 0
this : (fun (x : ℂ) ↦ Real.log ‖f x‖) = HSMul.hSMul (α := ℝ) 2⁻¹ (Real.log ∘ (⇑normSq : (a : ℂ) → ℝ) ∘ f)
h₃f : f z ∉ slitPlane
neg : HarmonicAt (Real.log ∘ (⇑normSq : (a : ℂ) → ℝ) ∘ (-f)) z
⊢ HarmonicAt (Real.log ∘ (⇑normSq : (a : ℂ) → ℝ) ∘ f) z

Tactic:
rw [(by aesop : Complex.normSq ∘ f = Complex.normSq ∘ (-f))]
-- Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions
Goal:
f : ℂ → ℂ
z : ℂ
h₁f : AnalyticAt ℂ f z
h₂f : f z ≠ 0
this : (fun (x : ℂ) ↦ Real.log ‖f x‖) = HSMul.hSMul (α := ℝ) 2⁻¹ (Real.log ∘ (⇑normSq : (a : ℂ) → ℝ) ∘ f)
h₃f : f z ∉ slitPlane
⊢ (-f) z ≠ 0

Tactic:
simpa
-- Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions
Goal:
f : ℂ → ℂ
z : ℂ
h₁f : AnalyticAt ℂ f z
h₂f : f z ≠ 0
this : (fun (x : ℂ) ↦ Real.log ‖f x‖) = HSMul.hSMul (α := ℝ) 2⁻¹ (Real.log ∘ (⇑normSq : (a : ℂ) → ℝ) ∘ f)
h₃f : f z ∉ slitPlane
⊢ HarmonicAt (Real.log ∘ (⇑normSq : (a : ℂ) → ℝ) ∘ (-f)) z

Tactic:
exact analyticAt_harmonicAt_log_normSq h₁f.neg (by simpa)
      ((mem_slitPlane_or_neg_mem_slitPlane h₂f).resolve_left h₃f)

Premises used: _private.0.analyticAt_harmonicAt_log_normSq, Or.resolve_left, AnalyticAt.neg, Complex.mem_slitPlane_or_neg_mem_slitPlane
-- Module: Mathlib.Analysis.InnerProductSpace.Harmonic.HarmonicContOnCl
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
f : E → F
s : Set E
h : HarmonicOnNhd f (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s)
⊢ HarmonicContOnCl f s

Tactic:
⟨h.mono subset_closure, h.continuousOn⟩

Premises used: subset_closure, InnerProductSpace.HarmonicContOnCl.mk, InnerProductSpace.HarmonicOnNhd.continuousOn, InnerProductSpace.HarmonicOnNhd.mono
-- Module: Mathlib.Analysis.InnerProductSpace.Harmonic.HarmonicContOnCl
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
f : E → F
s : Set E
hs : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
h : HarmonicOnNhd f s
⊢ HarmonicOnNhd f (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s)

Tactic:
rw [← hs.closure_eq] at h

Premises used: IsClosed.closure_eq
-- Module: Mathlib.Analysis.InnerProductSpace.Harmonic.HarmonicContOnCl
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
f : E → F
s : Set E
hs : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
h : HarmonicOnNhd f (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s)
⊢ HarmonicContOnCl f s

Tactic:
h.harmonicContOnCl

Premises used: InnerProductSpace.HarmonicOnNhd.harmonicContOnCl
-- Module: Mathlib.Analysis.InnerProductSpace.Harmonic.HarmonicContOnCl
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
f : E → F
s : Set E
hs : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
h : HarmonicOnNhd f (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s)
⊢ HarmonicContOnCl f s

Tactic:
exact h.harmonicContOnCl

Premises used: InnerProductSpace.HarmonicOnNhd.harmonicContOnCl
-- Module: Mathlib.Analysis.InnerProductSpace.Harmonic.HarmonicContOnCl
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
s : Set E
c : F
⊢ HarmonicContOnCl.{u_1, u_2} (F := F) (fun (x : E) ↦ c) s

Tactic:
⟨harmonicOnNhd_const c, continuousOn_const⟩

Premises used: InnerProductSpace.harmonicOnNhd_const, continuousOn_const, InnerProductSpace.HarmonicContOnCl.mk
-- Module: Mathlib.Analysis.InnerProductSpace.Harmonic.HarmonicContOnCl
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
f : E → F
x : E
r : ℝ
h : HarmonicContOnCl f (ball x r)
inl : ∀ (h : HarmonicContOnCl f (ball x 0)), ContinuousOn f (closedBall x 0)
inr : ∀ (hr : r ≠ 0), ContinuousOn f (closedBall x r)
⊢ ContinuousOn f (closedBall x r)

Tactic:
rcases eq_or_ne r 0 with (rfl | hr)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.InnerProductSpace.Harmonic.HarmonicContOnCl
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
f : E → F
x : E
h : HarmonicContOnCl f (ball x 0)
inl : ContinuousOn f {x}
⊢ ContinuousOn f (closedBall x 0)

Tactic:
rw [closedBall_zero]

Premises used: Metric.closedBall_zero
-- Module: Mathlib.Analysis.InnerProductSpace.Harmonic.HarmonicContOnCl
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
f : E → F
x : E
h : HarmonicContOnCl f (ball x 0)
⊢ ContinuousOn f {x}

Tactic:
continuousOn_singleton f x

Premises used: continuousOn_singleton
-- Module: Mathlib.Analysis.InnerProductSpace.Harmonic.HarmonicContOnCl
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
f : E → F
x : E
h : HarmonicContOnCl f (ball x 0)
⊢ ContinuousOn f {x}

Tactic:
exact continuousOn_singleton f x

Premises used: continuousOn_singleton
-- Module: Mathlib.Analysis.InnerProductSpace.Harmonic.HarmonicContOnCl
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
f : E → F
x : E
r : ℝ
h : HarmonicContOnCl f (ball x r)
hr : r ≠ 0
inr : ContinuousOn f (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball x r))
⊢ ContinuousOn f (closedBall x r)

Tactic:
rw [← closure_ball x hr]

Premises used: closure_ball
-- Module: Mathlib.Analysis.InnerProductSpace.Harmonic.HarmonicContOnCl
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
f : E → F
x : E
r : ℝ
h : HarmonicContOnCl f (ball x r)
hr : r ≠ 0
⊢ ContinuousOn f (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball x r))

Tactic:
h.continuousOn

Premises used: InnerProductSpace.HarmonicContOnCl.continuousOn
-- Module: Mathlib.Analysis.InnerProductSpace.Harmonic.HarmonicContOnCl
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
f : E → F
x : E
r : ℝ
h : HarmonicContOnCl f (ball x r)
hr : r ≠ 0
⊢ ContinuousOn f (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball x r))

Tactic:
exact h.continuousOn

Premises used: InnerProductSpace.HarmonicContOnCl.continuousOn