awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Basic
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
x : E
h : x ∈ s
⊢ HarmonicAt.{u_1, u_2} (F := F) (fun (x : E) ↦ c) x

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Basic
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
⊢ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {x : E | HarmonicAt f x}

Tactic:
isOpen_iff_mem_nhds.2 (fun _ hx ↦ hx.eventually)

Premises used: Iff.mpr, InnerProductSpace.HarmonicAt.eventually, isOpen_iff_mem_nhds
-- Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Basic
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 t : Set E
h : HarmonicOnNhd f s
hst : t ⊆ s
⊢ HarmonicOnNhd f t

Tactic:
fun x hx ↦ h x (hst hx)

Premises used: InnerProductSpace.HarmonicOnNhd
-- Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Basic
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 s
⊢ ContinuousOn f s

Tactic:
fun x hx ↦ (h x hx).1.continuousAt.continuousWithinAt (s := s)

Premises used: ContinuousAt.continuousWithinAt, And.left, ContinuousOn, ContDiffAt.continuousAt
-- Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Basic
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
right : Δ (f₁ + f₂) =ᶠ[𝓝 x] 0
⊢ HarmonicAt (f₁ + f₂) x

Tactic:
constructor
-- Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Basic
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
⊢ ContDiffAt ℝ 2 (f₁ + f₂) x

Tactic:
h₁.1.add h₂.1

Premises used: ContDiffAt.add, And.left
-- Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Basic
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
⊢ ContDiffAt ℝ 2 (f₁ + f₂) x

Tactic:
exact h₁.1.add h₂.1

Premises used: ContDiffAt.add, And.left
-- Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Basic
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
h : ∀ (a : E), Δ (f₁ + f₂) a = (Δ f₁ + Δ f₂) a → Δ f₁ a = 0 a → Δ f₂ a = 0 a → Δ (f₁ + f₂) a = 0 a
⊢ Δ (f₁ + f₂) =ᶠ[𝓝 x] 0

Tactic:
filter_upwards [h₁.1.laplacian_add_nhds h₂.1, h₁.2, h₂.2]

Premises used: ContDiffAt.laplacian_add_nhds, And.right, And.left
-- Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Basic
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
⊢ ∀ (a : E), Δ (f₁ + f₂) a = (Δ f₁ + Δ f₂) a → Δ f₁ a = 0 a → Δ f₂ a = 0 a → Δ (f₁ + f₂) a = 0 a

Tactic:
simp_all
-- Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Basic
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
right : Δ (f₁ - f₂) =ᶠ[𝓝 x] 0
⊢ HarmonicAt (f₁ - f₂) x

Tactic:
constructor
-- Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Basic
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
⊢ ContDiffAt ℝ 2 (f₁ - f₂) x

Tactic:
h₁.1.sub h₂.1

Premises used: And.left, ContDiffAt.sub
-- Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Basic
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
⊢ ContDiffAt ℝ 2 (f₁ - f₂) x

Tactic:
exact h₁.1.sub h₂.1

Premises used: And.left, ContDiffAt.sub
-- Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Basic
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
h : ∀ (a : E), Δ (f₁ - f₂) a = (Δ f₁ - Δ f₂) a → Δ f₁ a = 0 a → Δ f₂ a = 0 a → Δ (f₁ - f₂) a = 0 a
⊢ Δ (f₁ - f₂) =ᶠ[𝓝 x] 0

Tactic:
filter_upwards [h₁.1.laplacian_sub_nhds h₂.1, h₁.2, h₂.2]

Premises used: And.right, And.left, ContDiffAt.laplacian_sub_nhds
-- Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Basic
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
⊢ ∀ (a : E), Δ (f₁ - f₂) a = (Δ f₁ - Δ f₂) a → Δ f₁ a = 0 a → Δ f₂ a = 0 a → Δ (f₁ - f₂) a = 0 a

Tactic:
simp_all
-- Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Basic
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
s : Set E
h₁ : HarmonicOnNhd f₁ s
h₂ : HarmonicOnNhd f₂ s
⊢ HarmonicOnNhd (f₁ + f₂) s

Tactic:
fun x hx ↦ (h₁ x hx).add (h₂ x hx)

Premises used: InnerProductSpace.HarmonicOnNhd, InnerProductSpace.HarmonicAt.add
-- Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Basic
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
s : Set E
h₁ : HarmonicOnNhd f₁ s
h₂ : HarmonicOnNhd f₂ s
⊢ HarmonicOnNhd (f₁ - f₂) s

Tactic:
fun x hx ↦ (h₁ x hx).sub (h₂ x hx)

Premises used: InnerProductSpace.HarmonicOnNhd, InnerProductSpace.HarmonicAt.sub
-- Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Basic
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
right : Δ (-f) =ᶠ[𝓝 x] 0
⊢ HarmonicAt (-f) x

Tactic:
constructor
-- Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Basic
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
⊢ ContDiffAt ℝ 2 (-f) x

Tactic:
simpa using h.1.neg

Premises used: And.left, ContDiffAt.neg
-- Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Basic
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
h₁ : ∀ (x : E) (hx : Δ f x = 0 x), Δ (-f) x = 0 x
⊢ Δ (-f) =ᶠ[𝓝 x] 0

Tactic:
filter_upwards [h.2] with x hx

Premises used: And.right
-- Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Basic
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_1 : E
h : HarmonicAt f x_1
x : E
hx : Δ f x = 0 x
⊢ Δ (-f) x = 0 x

Tactic:
simp_all [laplacian_neg]

Premises used: InnerProductSpace.laplacian_neg
-- Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Basic
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 s
⊢ HarmonicOnNhd (-f) s

Tactic:
fun x hx ↦ (h x hx).neg

Premises used: InnerProductSpace.HarmonicOnNhd, InnerProductSpace.HarmonicAt.neg
-- Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Basic
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
right : Δ (c • f) =ᶠ[𝓝 x] 0
⊢ HarmonicAt (c • f) x

Tactic:
constructor
-- Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Basic
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
⊢ ContDiffAt ℝ 2 (c • f) x

Tactic:
h.1.const_smul c

Premises used: ContDiffAt.const_smul, And.left
-- Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Basic
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
⊢ ContDiffAt ℝ 2 (c • f) x

Tactic:
exact h.1.const_smul c

Premises used: ContDiffAt.const_smul, And.left
-- Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Basic
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
h₁ : ∀ (a : E), Δ (c • f) a = (c • Δ f) a → Δ f a = 0 a → Δ (c • f) a = 0 a
⊢ Δ (c • f) =ᶠ[𝓝 x] 0

Tactic:
filter_upwards [laplacian_smul_nhds c h.1, h.2]

Premises used: And.right, And.left, InnerProductSpace.laplacian_smul_nhds
-- Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Basic
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
⊢ ∀ (a : E), Δ (c • f) a = (c • Δ f) a → Δ f a = 0 a → Δ (c • f) a = 0 a

Tactic:
simp_all
-- Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Basic
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
c : ℝ
h : HarmonicOnNhd f s
⊢ HarmonicOnNhd (c • f) s

Tactic:
fun x hx ↦ (h x hx).const_smul

Premises used: InnerProductSpace.HarmonicAt.const_smul, InnerProductSpace.HarmonicOnNhd
-- Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Basic
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
right : Δ (E := E → G) ((⇑l : (a : F) → G) ∘ f) =ᶠ[𝓝 x] 0
⊢ HarmonicAt.{u_1, u_3} (F := G) ((⇑l : (a : F) → G) ∘ f) x

Tactic:
constructor
-- Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Basic
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
⊢ ContDiffAt.{0, u_1, u_3} ℝ (F := G) 2 ((⇑l : (a : F) → G) ∘ f) x

Tactic:
h.1.continuousLinearMap_comp l

Premises used: And.left, ContDiffAt.continuousLinearMap_comp
-- Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Basic
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
⊢ ContDiffAt.{0, u_1, u_3} ℝ (F := G) 2 ((⇑l : (a : F) → G) ∘ f) x

Tactic:
exact h.1.continuousLinearMap_comp l

Premises used: And.left, ContDiffAt.continuousLinearMap_comp
-- Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Basic
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
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
⊢ Δ (E := E → G) ((⇑l : (a : F) → G) ∘ f) =ᶠ[𝓝 x] 0

Tactic:
filter_upwards [h.1.laplacian_CLM_comp_left_nhds (l := l), h.2]

Premises used: And.right, And.left, ContDiffAt.laplacian_CLM_comp_left_nhds
-- Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Basic
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
⊢ ∀ (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:
simp_all
-- Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Basic
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
s : Set E
h : HarmonicOnNhd f s
l : F →L[ℝ] G
⊢ HarmonicOnNhd.{u_1, u_3} (F := G) ((⇑l : (a : F) → G) ∘ f) s

Tactic:
fun x hx ↦ (h x hx).comp_CLM l

Premises used: InnerProductSpace.HarmonicOnNhd, InnerProductSpace.HarmonicAt.comp_CLM
-- Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Basic
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
mpr : HarmonicAt f x → HarmonicAt.{u_1, u_3} (F := G) ((⇑l : (a : F) → G) ∘ f) x
⊢ HarmonicAt.{u_1, u_3} (F := G) ((⇑l : (a : F) → G) ∘ f) x ↔ HarmonicAt f x

Tactic:
constructor
-- Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Basic
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
h : HarmonicAt.{u_1, u_3} (F := G) ((⇑l : (a : F) → G) ∘ f) x
⊢ HarmonicAt f x

Tactic:
simpa [Function.comp_def] using h.comp_CLM l.symm.toContinuousLinearMap

Premises used: ContinuousLinearEquiv.symm, Function.comp_def, InnerProductSpace.HarmonicAt.comp_CLM, ContinuousLinearEquiv.toContinuousLinearMap
-- Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Basic
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
h : HarmonicAt f x
⊢ HarmonicAt.{u_1, u_3} (F := G) ((⇑l : (a : F) → G) ∘ f) x

Tactic:
h.comp_CLM l.toContinuousLinearMap

Premises used: InnerProductSpace.HarmonicAt.comp_CLM, ContinuousLinearEquiv.toContinuousLinearMap
-- Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Basic
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
h : HarmonicAt f x
⊢ HarmonicAt.{u_1, u_3} (F := G) ((⇑l : (a : F) → G) ∘ f) x

Tactic:
exact h.comp_CLM l.toContinuousLinearMap

Premises used: InnerProductSpace.HarmonicAt.comp_CLM, ContinuousLinearEquiv.toContinuousLinearMap
-- Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Basic
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
s : Set E
l : F ≃L[ℝ] G
⊢ HarmonicOnNhd.{u_1, u_3} (F := G) ((⇑l : (a : F) → G) ∘ f) s ↔ HarmonicOnNhd f s

Tactic:
forall₂_congr fun _ _ ↦ harmonicAt_comp_CLE_iff l

Premises used: InnerProductSpace.HarmonicOnNhd, InnerProductSpace.harmonicAt_comp_CLE_iff, forall₂_congr
-- Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℂ F
f : ℂ → F
x : ℂ
h : ContDiffAt ℂ 2 f x
⊢ HarmonicAt f x

Tactic:
⟨h.restrict_scalars ℝ, ?_⟩

Premises used: Real, InnerProductSpace.HarmonicAt, ContDiffAt.restrict_scalars, And.intro
-- Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℂ F
f : ℂ → F
x : ℂ
h : ContDiffAt ℂ 2 f x
refine : Laplacian.laplacian f =ᶠ[𝓝 x] 0
⊢ HarmonicAt f x

Tactic:
refine ⟨h.restrict_scalars ℝ, ?_⟩
-- Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℂ F
f : ℂ → F
x : ℂ
h : ContDiffAt ℂ 2 f x
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
⊢ Laplacian.laplacian f =ᶠ[𝓝 x] 0

Tactic:
filter_upwards [h.restrictScalars_iteratedFDeriv_eventuallyEq (𝕜 := ℝ)] with a ha

Premises used: ContDiffAt.restrictScalars_iteratedFDeriv_eventuallyEq
-- Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions
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)
⊢ (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]
-- Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions
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)
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)
⊢ Laplacian.laplacian f a = 0 a

Tactic:
simp_all [laplacian_eq_iteratedFDeriv_complexPlane f, ← ha,
    ContinuousMultilinearMap.coe_restrictScalars]

Premises used: InnerProductSpace.laplacian_eq_iteratedFDeriv_complexPlane, ContinuousMultilinearMap.coe_restrictScalars
-- Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℂ F
f : ℂ → F
x : ℂ
inst_2 : CompleteSpace F
h : AnalyticAt ℂ f x
⊢ HarmonicAt f x

Tactic:
h.contDiffAt.harmonicAt

Premises used: ContDiffAt.harmonicAt, AnalyticAt.contDiffAt
-- Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions
Goal:
x : ℂ
f : ℂ → ℂ
h : AnalyticAt ℂ f x
⊢ HarmonicAt (F := ℝ) (fun (z : ℂ) ↦ (f z).re) x

Tactic:
h.harmonicAt.comp_CLM reCLM

Premises used: Complex.reCLM, AnalyticAt.harmonicAt, InnerProductSpace.HarmonicAt.comp_CLM
-- Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions
Goal:
x : ℂ
f : ℂ → ℂ
h : AnalyticAt ℂ f x
⊢ HarmonicAt (F := ℝ) (fun (z : ℂ) ↦ (f z).im) x

Tactic:
h.harmonicAt.comp_CLM imCLM

Premises used: AnalyticAt.harmonicAt, InnerProductSpace.HarmonicAt.comp_CLM, Complex.imCLM
-- Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions
Goal:
x : ℂ
f : ℂ → ℂ
h : AnalyticAt ℂ f x
⊢ HarmonicAt (F := ℂ) ((starRingEnd (ℂ → ℂ) : (a : ℂ → ℂ) → ℂ → ℂ) f) x

Tactic:
(harmonicAt_comp_CLE_iff conjCLE).2 h.harmonicAt

Premises used: Iff.mpr, InnerProductSpace.harmonicAt_comp_CLE_iff, Complex.conjCLE, AnalyticAt.harmonicAt
-- Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions
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
rw₁ :
  Real.log ∘ (⇑normSq : (a : ℂ) → ℝ) ∘ g =ᶠ[𝓝 z] (⇑reCLM : (a : ℂ) → ℝ) ∘ ((⇑conjCLE : (a : ℂ) → ℂ) ∘ log ∘ g + log ∘ g)
⊢ HarmonicAt (Real.log ∘ (⇑normSq : (a : ℂ) → ℝ) ∘ g) z

Tactic:
rw [harmonicAt_congr_nhds (f₂ := reCLM ∘ (conjCLE ∘ log ∘ g + log ∘ g))]

Premises used: InnerProductSpace.harmonicAt_congr_nhds
-- Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions
Goal:
z : ℂ
g : ℂ → ℂ
h₁g : AnalyticAt ℂ g z
h₂g : g z ≠ 0
h₃g : g z ∈ slitPlane
⊢ HarmonicAt (F := ℝ) ((⇑reCLM : (a : ℂ) → ℝ) ∘ ((⇑conjCLE : (a : ℂ) → ℂ) ∘ log ∘ g + log ∘ g)) z

Tactic:
(((harmonicAt_comp_CLE_iff conjCLE).2 ((analyticAt_clog h₃g).comp h₁g).harmonicAt).add
      ((analyticAt_clog h₃g).comp h₁g).harmonicAt).comp_CLM reCLM

Premises used: Iff.mpr, InnerProductSpace.harmonicAt_comp_CLE_iff, Complex.conjCLE, Complex.reCLM, AnalyticAt.harmonicAt, analyticAt_clog, InnerProductSpace.HarmonicAt.comp_CLM, AnalyticAt.comp, InnerProductSpace.HarmonicAt.add
-- Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions
Goal:
z : ℂ
g : ℂ → ℂ
h₁g : AnalyticAt ℂ g z
h₂g : g z ≠ 0
h₃g : g z ∈ slitPlane
⊢ HarmonicAt (F := ℝ) ((⇑reCLM : (a : ℂ) → ℝ) ∘ ((⇑conjCLE : (a : ℂ) → ℂ) ∘ log ∘ g + log ∘ g)) z

Tactic:
exact (((harmonicAt_comp_CLE_iff conjCLE).2 ((analyticAt_clog h₃g).comp h₁g).harmonicAt).add
      ((analyticAt_clog h₃g).comp h₁g).harmonicAt).comp_CLM reCLM

Premises used: Iff.mpr, InnerProductSpace.harmonicAt_comp_CLE_iff, Complex.conjCLE, Complex.reCLM, AnalyticAt.harmonicAt, analyticAt_clog, InnerProductSpace.HarmonicAt.comp_CLM, AnalyticAt.comp, InnerProductSpace.HarmonicAt.add
-- Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions
Goal:
z : ℂ
g : ℂ → ℂ
h₁g : AnalyticAt ℂ g z
h₂g : g z ≠ 0
h₃g : g z ∈ slitPlane
⊢ 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⟩)