awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Harmonic.Basic (goal)
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₁ f₂ : E → F
x : E
h₁ : HarmonicAt f₁ x
h₂ : HarmonicAt f₂ x
⊢ Δ (f₁ + f₂) =ᶠ[𝓝 x] 0
have h : ∀ (a : E), Δ (f₁ + f₂) a = (Δ f₁ + Δ f₂) a → Δ f₁ a = 0 a → Δ f₂ a = 0 a → Δ (f₁ + f₂) a = 0 a
Tactic: filter_upwards [h₁.1.laplacian_add_nhds h₂.1, h₁.2, h₂.2]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Harmonic.Basic (goal)
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₁ f₂ : E → F
x : E
h₁ : HarmonicAt f₁ x
h₂ : HarmonicAt f₂ x
⊢ HarmonicAt (f₁ - f₂) x
have left : ContDiffAt ℝ 2 (f₁ - f₂) x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Harmonic.Basic (goal)
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₁ f₂ : E → F
x : E
h₁ : HarmonicAt f₁ x
h₂ : HarmonicAt f₂ x
left : ContDiffAt ℝ 2 (f₁ - f₂) x
⊢ HarmonicAt (f₁ - f₂) x
have right : Δ (f₁ - f₂) =ᶠ[𝓝 x] 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Harmonic.Basic (goal)
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₁ f₂ : E → F
x : E
h₁ : HarmonicAt f₁ x
h₂ : HarmonicAt f₂ x
⊢ Δ (f₁ - f₂) =ᶠ[𝓝 x] 0
have h : ∀ (a : E), Δ (f₁ - f₂) a = (Δ f₁ - Δ f₂) a → Δ f₁ a = 0 a → Δ f₂ a = 0 a → Δ (f₁ - f₂) a = 0 a
Tactic: filter_upwards [h₁.1.laplacian_sub_nhds h₂.1, h₁.2, h₂.2]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Harmonic.Basic (goal)
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 : HarmonicAt f x
⊢ HarmonicAt (-f) x
have left : ContDiffAt ℝ 2 (-f) x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Harmonic.Basic (goal)
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 : HarmonicAt f x
left : ContDiffAt ℝ 2 (-f) x
⊢ HarmonicAt (-f) x
have right : Δ (-f) =ᶠ[𝓝 x] 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Harmonic.Basic (goal)
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 : HarmonicAt f x
⊢ Δ (-f) =ᶠ[𝓝 x] 0
have h₁ : ∀ (x : E) (hx : Δ f x = 0 x), Δ (-f) x = 0 x
Tactic: filter_upwards [h.2] with x hx
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Harmonic.Basic (goal)
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
c : ℝ
h : HarmonicAt f x
⊢ HarmonicAt (c • f) x
have left : ContDiffAt ℝ 2 (c • f) x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Harmonic.Basic (goal)
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
c : ℝ
h : HarmonicAt f x
left : ContDiffAt ℝ 2 (c • f) x
⊢ HarmonicAt (c • f) x
have right : Δ (c • f) =ᶠ[𝓝 x] 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Harmonic.Basic (goal)
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
c : ℝ
h : HarmonicAt f x
⊢ Δ (c • f) =ᶠ[𝓝 x] 0
have h₁ : ∀ (a : E), Δ (c • f) a = (c • Δ f) a → Δ f a = 0 a → Δ (c • f) a = 0 a
Tactic: filter_upwards [laplacian_smul_nhds c h.1, h.2]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Harmonic.Basic (goal)
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
G : Type u_3
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace ℝ G
f : E → F
x : E
h : HarmonicAt f x
l : F →L[ℝ] G
⊢ HarmonicAt.{u_1, u_3} (F := G) ((⇑l : (a : F) → G) ∘ f) x
have left : ContDiffAt.{0, u_1, u_3} ℝ (F := G) 2 ((⇑l : (a : F) → G) ∘ f) x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Harmonic.Basic (goal)
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
G : Type u_3
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace ℝ G
f : E → F
x : E
h : HarmonicAt f x
l : F →L[ℝ] G
left : ContDiffAt.{0, u_1, u_3} ℝ (F := G) 2 ((⇑l : (a : F) → G) ∘ f) x
⊢ HarmonicAt.{u_1, u_3} (F := G) ((⇑l : (a : F) → G) ∘ f) x
have right : Δ (E := E → G) ((⇑l : (a : F) → G) ∘ f) =ᶠ[𝓝 x] 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Harmonic.Basic (goal)
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
G : Type u_3
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace ℝ G
f : E → F
x : E
h : HarmonicAt f x
l : F →L[ℝ] G
⊢ Δ (E := E → G) ((⇑l : (a : F) → G) ∘ f) =ᶠ[𝓝 x] 0
have h₁ : ∀ (a : E),
  Δ (E := E → G) ((⇑l : (a : F) → G) ∘ f) a = ((⇑l : (a : F) → G) ∘ Δ f) a →
    Δ f a = 0 a → Δ (E := E → G) ((⇑l : (a : F) → G) ∘ f) a = 0 a
Tactic: filter_upwards [h.1.laplacian_CLM_comp_left_nhds (l := l), h.2]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Harmonic.Basic (goal)
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
G : Type u_3
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace ℝ G
f : E → F
x : E
l : F ≃L[ℝ] G
⊢ HarmonicAt.{u_1, u_3} (F := G) ((⇑l : (a : F) → G) ∘ f) x ↔ HarmonicAt f x
have mp : HarmonicAt.{u_1, u_3} (F := G) ((⇑l : (a : F) → G) ∘ f) x → HarmonicAt f x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Harmonic.Basic (goal)
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
G : Type u_3
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace ℝ G
f : E → F
x : E
l : F ≃L[ℝ] G
mp : HarmonicAt.{u_1, u_3} (F := G) ((⇑l : (a : F) → G) ∘ f) x → HarmonicAt f x
⊢ HarmonicAt.{u_1, u_3} (F := G) ((⇑l : (a : F) → G) ∘ f) x ↔ HarmonicAt f x
have mpr : HarmonicAt f x → HarmonicAt.{u_1, u_3} (F := G) ((⇑l : (a : F) → G) ∘ f) x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions (goal)
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℂ F
f : ℂ → F
x : ℂ
h : ContDiffAt ℂ 2 f x
⊢ HarmonicAt f x
have refine : Laplacian.laplacian f =ᶠ[𝓝 x] 0
Tactic: refine ⟨h.restrict_scalars ℝ, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions (goal)
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℂ F
f : ℂ → F
x : ℂ
h : ContDiffAt ℂ 2 f x
⊢ Laplacian.laplacian f =ᶠ[𝓝 x] 0
have h₁ : ∀ (a : ℂ)
  (ha :
    Eq (α := ContinuousMultilinearMap ℝ (fun (i : Fin 2) ↦ ℂ) F)
      (Function.comp (β := ContinuousMultilinearMap ℂ (fun (i : Fin 2) ↦ ℂ) F)
        (ContinuousMultilinearMap.restrictScalars ℝ (M₁ := fun (i : Fin 2) ↦ ℂ)) (iteratedFDeriv ℂ 2 f) a)
      (iteratedFDeriv ℝ 2 f a)),
  Laplacian.laplacian f a = 0 a
Tactic: filter_upwards [h.restrictScalars_iteratedFDeriv_eventuallyEq (𝕜 := ℝ)] with a ha
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions (hypothesis)
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℂ F
f : ℂ → F
x : ℂ
h : ContDiffAt ℂ 2 f x
a : ℂ
ha :
  Eq (α := ContinuousMultilinearMap ℝ (fun (i : Fin 2) ↦ ℂ) F)
    (Function.comp (β := ContinuousMultilinearMap ℂ (fun (i : Fin 2) ↦ ℂ) F)
      (ContinuousMultilinearMap.restrictScalars ℝ (M₁ := fun (i : Fin 2) ↦ ℂ)) (iteratedFDeriv ℂ 2 f) a)
    (iteratedFDeriv ℝ 2 f a)
⊢ Laplacian.laplacian f a = 0 a
have this : (iteratedFDeriv ℂ 2 f a : (a : (i : Fin 2) → ℂ) → F) (HSMul.hSMul (β := Fin (Nat.succ 0).succ → ℂ) I ![1, 1]) =
  HSMul.hSMul (α := ℂ) (β := F) (∏ i : Fin 2, I) ((iteratedFDeriv ℂ 2 f a : (a : (i : Fin 2) → ℂ) → F) ![1, 1] : F)
Tactic: have : (iteratedFDeriv ℂ 2 f a) (I • ![1, 1])
      = (∏ i, I) • ((iteratedFDeriv ℂ 2 f a) ![1, 1]) :=
    (iteratedFDeriv ℂ 2 f a).map_smul_univ (fun _ ↦ I) ![1, 1]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions (goal)
Goal:
z : ℂ
g : ℂ → ℂ
h₁g : AnalyticAt ℂ g z
h₂g : g z ≠ 0
h₃g : g z ∈ slitPlane
⊢ HarmonicAt (Real.log ∘ (⇑normSq : (a : ℂ) → ℝ) ∘ g) z
have rw : HarmonicAt (F := ℝ) ((⇑reCLM : (a : ℂ) → ℝ) ∘ ((⇑conjCLE : (a : ℂ) → ℂ) ∘ log ∘ g + log ∘ g)) z
Tactic: rw [harmonicAt_congr_nhds (f₂ := reCLM ∘ (conjCLE ∘ log ∘ g + log ∘ g))]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions (goal)
Goal:
z : ℂ
g : ℂ → ℂ
h₁g : AnalyticAt ℂ g z
h₂g : g z ≠ 0
h₃g : g z ∈ slitPlane
rw : HarmonicAt (F := ℝ) ((⇑reCLM : (a : ℂ) → ℝ) ∘ ((⇑conjCLE : (a : ℂ) → ℂ) ∘ log ∘ g + log ∘ g)) z
⊢ HarmonicAt (Real.log ∘ (⇑normSq : (a : ℂ) → ℝ) ∘ g) z
have rw₁ : Real.log ∘ (⇑normSq : (a : ℂ) → ℝ) ∘ g =ᶠ[𝓝 z] (⇑reCLM : (a : ℂ) → ℝ) ∘ ((⇑conjCLE : (a : ℂ) → ℂ) ∘ log ∘ g + log ∘ g)
Tactic: rw [harmonicAt_congr_nhds (f₂ := reCLM ∘ (conjCLE ∘ log ∘ g + log ∘ g))]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions (hypothesis)
Goal:
z : ℂ
g : ℂ → ℂ
h₁g : AnalyticAt ℂ g z
h₂g : g z ≠ 0
h₃g : g z ∈ slitPlane
⊢ Real.log ∘ (⇑normSq : (a : ℂ) → ℝ) ∘ g =ᶠ[𝓝 z] (⇑reCLM : (a : ℂ) → ℝ) ∘ ((⇑conjCLE : (a : ℂ) → ℂ) ∘ log ∘ g + log ∘ g)
have t₀ : g ⁻¹' (slitPlane ∩ {y : ℂ | y ≠ 0}) ∈ 𝓝 z
Tactic: have t₀ := h₁g.differentiableAt.continuousAt.preimage_mem_nhds
      ((isOpen_slitPlane.inter isOpen_ne).mem_nhds ⟨h₃g, h₂g⟩)
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions (goal)
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
⊢ (𝓝 z).EventuallyEq (β := ℝ)
    (Function.comp (β := ℂ) (⇑reCLM : (a : ℂ) → ℝ)
      ((⇑ofRealCLM : (a : ℝ) → ℂ) ∘ Real.log ∘ (⇑normSq : (a : ℂ) → ℝ) ∘ g))
    ((⇑reCLM : (a : ℂ) → ℝ) ∘ log ∘ ((⇑conjCLE : (a : ℂ) → ℂ) ∘ g * g))
have h : ∀ (x : ℂ),
  Eq (α := ℝ)
    (Function.comp (β := ℂ) (⇑reCLM : (a : ℂ) → ℝ) ((⇑ofRealCLM : (a : ℝ) → ℂ) ∘ Real.log ∘ (⇑normSq : (a : ℂ) → ℝ) ∘ g)
      x)
    (((⇑reCLM : (a : ℂ) → ℝ) ∘ log ∘ ((⇑conjCLE : (a : ℂ) → ℂ) ∘ g * g)) x)
Tactic: filter_upwards with x
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions (goal)
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 : ℂ
⊢ Eq (α := ℝ) ((reCLM : (a : ℂ) → ℝ) (↑(Real.log ((normSq : (a : ℂ) → ℝ) (g x))) : ℂ) : ℝ)
    ((reCLM : (a : ℂ) → ℝ) (log (HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (g x) : ℂ) (g x))) : ℝ)
have h : LE.le (α := ℝ) (0 : ℝ) ((normSq : (a : ℂ) → ℝ) (g x) : ℝ)
Tactic: rw [ofReal_log, normSq_eq_conj_mul_self]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions (goal)
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
⊢ (𝓝 z).EventuallyEq (β := ℝ) ((⇑reCLM : (a : ℂ) → ℝ) ∘ log ∘ ((⇑conjCLE : (a : ℂ) → ℂ) ∘ g * g))
    ((⇑reCLM : (a : ℂ) → ℝ) ∘ (log ∘ (⇑conjCLE : (a : ℂ) → ℂ) ∘ g + log ∘ g))
have 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)
Tactic: filter_upwards [t₀] with x hx
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions (goal)
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})
⊢ Eq (α := ℝ) ((reCLM : (a : ℂ) → ℝ) (log (HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (g x) : ℂ) (g x))) : ℝ)
    ((reCLM : (a : ℂ) → ℝ) (log ((starRingEnd ℂ : (a : ℂ) → ℂ) (g x)) + log (g x)) : ℝ)
have h : log (HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (g x) : ℂ) (g x)) =
  log ((starRingEnd ℂ : (a : ℂ) → ℂ) (g x)) + log (g x)
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions (goal)
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})
⊢ log (HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (g x) : ℂ) (g x)) =
    log ((starRingEnd ℂ : (a : ℂ) → ℂ) (g x)) + log (g x)
have h : (if (g x).arg = Real.pi then Real.pi else -(g x).arg) + (g x).arg ∈ Set.Ioc (-Real.pi) Real.pi
Tactic: rw [Complex.log_mul_eq_add_log_iff _ hx.2, Complex.arg_conj]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions (goal)
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
⊢ log (HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (g x) : ℂ) (g x)) =
    log ((starRingEnd ℂ : (a : ℂ) → ℂ) (g x)) + log (g x)
have rw : Ne (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (g x) : ℂ) (0 : ℂ)
Tactic: rw [Complex.log_mul_eq_add_log_iff _ hx.2, Complex.arg_conj]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions (goal)
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
⊢ (𝓝 z).EventuallyEq (β := ℝ) ((⇑reCLM : (a : ℂ) → ℝ) ∘ (log ∘ (⇑conjCLE : (a : ℂ) → ℂ) ∘ g + log ∘ g))
    ((⇑reCLM : (a : ℂ) → ℝ) ∘ ((⇑conjCLE : (a : ℂ) → ℂ) ∘ log ∘ g + log ∘ g))
have apply : ∃ s ∈ 𝓝 z,
  Set.EqOn (β := ℝ) ((⇑reCLM : (a : ℂ) → ℝ) ∘ (log ∘ (⇑conjCLE : (a : ℂ) → ℂ) ∘ g + log ∘ g))
    ((⇑reCLM : (a : ℂ) → ℝ) ∘ ((⇑conjCLE : (a : ℂ) → ℂ) ∘ log ∘ g + log ∘ g)) s
Tactic: apply Filter.eventuallyEq_iff_exists_mem.2
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions (goal)
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
⊢ ∃ s ∈ 𝓝 z,
    Set.EqOn (β := ℝ) ((⇑reCLM : (a : ℂ) → ℝ) ∘ (log ∘ (⇑conjCLE : (a : ℂ) → ℂ) ∘ g + log ∘ g))
      ((⇑reCLM : (a : ℂ) → ℝ) ∘ ((⇑conjCLE : (a : ℂ) → ℂ) ∘ log ∘ g + log ∘ g)) s
have right : Set.EqOn (β := ℝ) ((⇑reCLM : (a : ℂ) → ℝ) ∘ (log ∘ (⇑conjCLE : (a : ℂ) → ℂ) ∘ g + log ∘ g))
  ((⇑reCLM : (a : ℂ) → ℝ) ∘ ((⇑conjCLE : (a : ℂ) → ℂ) ∘ log ∘ g + log ∘ g)) (g ⁻¹' (slitPlane ∩ {0}ᶜ))
Tactic: use g ⁻¹' (Complex.slitPlane ∩ {0}ᶜ), t₀
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions (goal)
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}ᶜ)
⊢ Eq (α := ℝ) ((reCLM : (a : ℂ) → ℝ) (log ((starRingEnd ℂ : (a : ℂ) → ℂ) (g x)) + log (g x)) : ℝ)
    ((reCLM : (a : ℂ) → ℝ) (HAdd.hAdd (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (log (g x)) : ℂ) (log (g x))) : ℝ)
have right : log ((starRingEnd ℂ : (a : ℂ) → ℂ) (g x)) + log (g x) =
  HAdd.hAdd (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (log (g x)) : ℂ) (log (g x))
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions (goal)
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}ᶜ)
⊢ log ((starRingEnd ℂ : (a : ℂ) → ℂ) (g x)) + log (g x) =
    HAdd.hAdd (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (log (g x)) : ℂ) (log (g x))
have right : (g x).arg ≠ Real.pi
Tactic: rw [← Complex.log_conj]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions (goal)
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] (⇑reCLM : (a : ℂ) → ℝ) ∘ ((⇑conjCLE : (a : ℂ) → ℂ) ∘ log ∘ g + log ∘ g)
have calc : Real.log ∘ (⇑normSq : (a : ℂ) → ℝ) ∘ g =ᶠ[𝓝 z]
  Function.comp (β := ℂ) (⇑reCLM : (a : ℂ) → ℝ) ((⇑ofRealCLM : (a : ℝ) → ℂ) ∘ Real.log ∘ (⇑normSq : (a : ℂ) → ℝ) ∘ 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]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions (goal)
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)
⊢ Real.log ∘ (⇑normSq : (a : ℂ) → ℝ) ∘ g =ᶠ[𝓝 z] (⇑reCLM : (a : ℂ) → ℝ) ∘ ((⇑conjCLE : (a : ℂ) → ℂ) ∘ log ∘ g + log ∘ g)
have calc₁ : (𝓝 z).EventuallyEq (β := ℝ)
  (Function.comp (β := ℂ) (⇑reCLM : (a : ℂ) → ℝ) ((⇑ofRealCLM : (a : ℝ) → ℂ) ∘ Real.log ∘ (⇑normSq : (a : ℂ) → ℝ) ∘ g))
  ((⇑reCLM : (a : ℂ) → ℝ) ∘ log ∘ ((⇑conjCLE : (a : ℂ) → ℂ) ∘ g * 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]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions (goal)
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))
⊢ Real.log ∘ (⇑normSq : (a : ℂ) → ℝ) ∘ g =ᶠ[𝓝 z] (⇑reCLM : (a : ℂ) → ℝ) ∘ ((⇑conjCLE : (a : ℂ) → ℂ) ∘ log ∘ g + log ∘ g)
have calc₂ : (𝓝 z).EventuallyEq (β := ℝ) ((⇑reCLM : (a : ℂ) → ℝ) ∘ log ∘ ((⇑conjCLE : (a : ℂ) → ℂ) ∘ g * g))
  ((⇑reCLM : (a : ℂ) → ℝ) ∘ (log ∘ (⇑conjCLE : (a : ℂ) → ℂ) ∘ 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]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions (goal)
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))
⊢ Real.log ∘ (⇑normSq : (a : ℂ) → ℝ) ∘ g =ᶠ[𝓝 z] (⇑reCLM : (a : ℂ) → ℝ) ∘ ((⇑conjCLE : (a : ℂ) → ℂ) ∘ log ∘ g + log ∘ g)
have calc₃ : (𝓝 z).EventuallyEq (β := ℝ) ((⇑reCLM : (a : ℂ) → ℝ) ∘ (log ∘ (⇑conjCLE : (a : ℂ) → ℂ) ∘ g + log ∘ g))
  ((⇑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]