awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.InnerProductSpace.JointEigenspace
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
α : 𝕜
A B : E →ₗ[𝕜] E
inst_3 : FiniteDimensional 𝕜 E
hB : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) B
hAB : Commute A B
⊢ Eq.{u_2 + 1} (α := Submodule 𝕜 ↥(eigenspace A α))
    (⨆ (i : 𝕜), (genEigenspace (B.restrict ⋯) i : (a : ℕ∞) → Submodule 𝕜 ↥(eigenspace A α)) 1) ⊤

Tactic:
simpa only [genEigenspace_eq_eigenspace, Submodule.orthogonal_eq_bot_iff]
    using orthogonalComplement_iSup_eigenspaces_eq_bot <|
      hB.restrict_invariant <| mapsTo_genEigenspace_of_comm hAB α 1

Premises used: Submodule.orthogonal_eq_bot_iff, Module.End.mapsTo_genEigenspace_of_comm, LinearMap.IsSymmetric.restrict_invariant, LinearMap.IsSymmetric.orthogonalComplement_iSup_eigenspaces_eq_bot, Module.End.IsFinitelySemisimple.genEigenspace_eq_eigenspace, OfNat.ofNat
-- Module: Mathlib.Analysis.InnerProductSpace.JointEigenspace
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
A B : E →ₗ[𝕜] E
inst_3 : FiniteDimensional 𝕜 E
hA : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) A
hB : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) B
hAB : Commute A B
⊢ Eq.{u_2 + 1} (α := Submodule 𝕜 E) (⨆ (α : 𝕜), ⨆ (γ : 𝕜), eigenspace A α ⊓ eigenspace B γ) ⊤

Tactic:
simpa [iSup_eigenspace_inf_eigenspace_of_commute hB hAB] using
    Submodule.orthogonal_eq_bot_iff.mp <| hA.orthogonalComplement_iSup_eigenspaces_eq_bot

Premises used: Submodule.orthogonal_eq_bot_iff, LinearMap.IsSymmetric.orthogonalComplement_iSup_eigenspaces_eq_bot, Iff.mp, LinearMap.IsSymmetric.iSup_eigenspace_inf_eigenspace_of_commute
-- Module: Mathlib.Analysis.InnerProductSpace.JointEigenspace
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
A B : E →ₗ[𝕜] E
inst_3 : FiniteDimensional 𝕜 E
hA : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) A
hB : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) B
hAB : Commute A B
apply : Eq.{u_2 + 1} (α := Submodule 𝕜 E) (⨆ (i : 𝕜 × 𝕜), eigenspace A i.2 ⊓ eigenspace B i.1)ᗮ ⊥
⊢ DirectSum.IsInternal (S := Submodule 𝕜 E) fun (i : 𝕜 × 𝕜) ↦ eigenspace A i.2 ⊓ eigenspace B i.1

Tactic:
apply (orthogonalFamily_eigenspace_inf_eigenspace hA hB).isInternal_iff.mpr

Premises used: Iff.mpr, OrthogonalFamily.isInternal_iff, LinearMap.IsSymmetric.orthogonalFamily_eigenspace_inf_eigenspace
-- Module: Mathlib.Analysis.InnerProductSpace.JointEigenspace
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
A B : E →ₗ[𝕜] E
inst_3 : FiniteDimensional 𝕜 E
hA : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) A
hB : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) B
hAB : Commute A B
rw : Eq.{u_2 + 1} (α := Submodule 𝕜 E) (⨆ (j : 𝕜), ⨆ (i : 𝕜), eigenspace A (i, j).2 ⊓ eigenspace B (i, j).1) ⊤
⊢ Eq.{u_2 + 1} (α := Submodule 𝕜 E) (⨆ (i : 𝕜 × 𝕜), eigenspace A i.2 ⊓ eigenspace B i.1)ᗮ ⊥

Tactic:
rw [Submodule.orthogonal_eq_bot_iff, iSup_prod, iSup_comm]

Premises used: Submodule.orthogonal_eq_bot_iff, iSup_comm, iSup_prod
-- Module: Mathlib.Analysis.InnerProductSpace.JointEigenspace
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
A B : E →ₗ[𝕜] E
inst_3 : FiniteDimensional 𝕜 E
hA : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) A
hB : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) B
hAB : Commute A B
⊢ Eq.{u_2 + 1} (α := Submodule 𝕜 E) (⨆ (j : 𝕜), ⨆ (i : 𝕜), eigenspace A (i, j).2 ⊓ eigenspace B (i, j).1) ⊤

Tactic:
iSup_iSup_eigenspace_inf_eigenspace_eq_top_of_commute hA hB hAB

Premises used: Set.Mem, setOf, LinearMap.IsSymmetric.iSup_iSup_eigenspace_inf_eigenspace_eq_top_of_commute
-- Module: Mathlib.Analysis.InnerProductSpace.JointEigenspace
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
A B : E →ₗ[𝕜] E
inst_3 : FiniteDimensional 𝕜 E
hA : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) A
hB : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) B
hAB : Commute A B
⊢ Eq.{u_2 + 1} (α := Submodule 𝕜 E) (⨆ (j : 𝕜), ⨆ (i : 𝕜), eigenspace A (i, j).2 ⊓ eigenspace B (i, j).1) ⊤

Tactic:
exact iSup_iSup_eigenspace_inf_eigenspace_eq_top_of_commute hA hB hAB

Premises used: LinearMap.IsSymmetric.iSup_iSup_eigenspace_inf_eigenspace_eq_top_of_commute
-- Module: Mathlib.Analysis.InnerProductSpace.JointEigenspace
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
ι : Type u_5
T : ι → E →ₗ[𝕜] E
hT : ∀ (i : ι), IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) (T i)
h : Pairwise (Commute on T)
x : ι
rw : Eq.{u_2 + 1} (α := Submodule 𝕜 E) (⨆ (μ : 𝕜), maxGenEigenspace (T x) μ)ᗮ ⊥
rw₁ : Eq.{u_2 + 1} (α := Submodule 𝕜 E) (⨆ (μ : 𝕜), eigenspace (T x) μ)ᗮ ⊥
rw₂ rw₃ : Eq.{u_2 + 1} (α := Submodule 𝕜 E) ⊥ ⊥
⊢ Eq.{u_2 + 1} (α := Submodule 𝕜 E) (⨆ (μ : 𝕜), maxGenEigenspace (T x) μ) ⊤

Tactic:
rw [← orthogonal_eq_bot_iff,
      congr(⨆ μ, $(maxGenEigenspace_eq_eigenspace (isFinitelySemisimple <| hT _) μ)),
      (hT _).orthogonalComplement_iSup_eigenspaces_eq_bot]

Premises used: Submodule.orthogonal_eq_bot_iff, LinearMap.IsSymmetric.orthogonalComplement_iSup_eigenspaces_eq_bot
-- Module: Mathlib.Analysis.InnerProductSpace.JointEigenspace
Goal:
𝕜 : Type u_1
E : Type u_2
n : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : n → Module.End 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
inst_4 : DecidableEq (n → 𝕜)
hT : ∀ (i : n), IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) (T i)
hC : Pairwise (Commute on T)
rw : Eq.{u_2 + 1} (α := Submodule 𝕜 E) (⨆ (α : n → 𝕜), ⨅ (j : n), (T j).eigenspace (α j))ᗮ ⊥
rw₁ :
  OrthogonalFamily 𝕜 (E := E) (fun (i : n → 𝕜) ↦ ↥(⨅ (j : n), (T j).eigenspace (i j))) fun (i : n → 𝕜) ↦
    subtypeₗᵢ (⨅ (j : n), (T j).eigenspace (i j))
⊢ DirectSum.IsInternal (S := Submodule 𝕜 E) fun (α : n → 𝕜) ↦ ⨅ (j : n), (T j).eigenspace (α j)

Tactic:
rw [OrthogonalFamily.isInternal_iff]

Premises used: OrthogonalFamily.isInternal_iff
-- Module: Mathlib.Analysis.InnerProductSpace.JointEigenspace
Goal:
𝕜 : Type u_1
E : Type u_2
n : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : n → Module.End 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
inst_4 : DecidableEq (n → 𝕜)
hT : ∀ (i : n), IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) (T i)
hC : Pairwise (Commute on T)
rw : Eq.{u_2 + 1} (α := Submodule 𝕜 E) ⊤ᗮ ⊥
rw₁ rw₂ : Eq.{u_2 + 1} (α := Submodule 𝕜 E) ⊥ ⊥
⊢ Eq.{u_2 + 1} (α := Submodule 𝕜 E) (⨆ (α : n → 𝕜), ⨅ (j : n), (T j).eigenspace (α j))ᗮ ⊥

Tactic:
rw [iSup_iInf_eq_top_of_commute hT hC, top_orthogonal_eq_bot]

Premises used: LinearMap.IsSymmetric.iSup_iInf_eq_top_of_commute, Submodule.top_orthogonal_eq_bot
-- Module: Mathlib.Analysis.InnerProductSpace.JointEigenspace
Goal:
𝕜 : Type u_1
E : Type u_2
n : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : n → Module.End 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
inst_4 : DecidableEq (n → 𝕜)
hT : ∀ (i : n), IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) (T i)
hC : Pairwise (Commute on T)
⊢ OrthogonalFamily 𝕜 (E := E) (fun (i : n → 𝕜) ↦ ↥(⨅ (j : n), (T j).eigenspace (i j))) fun (i : n → 𝕜) ↦
    subtypeₗᵢ (⨅ (j : n), (T j).eigenspace (i j))

Tactic:
orthogonalFamily_iInf_eigenspaces hT

Premises used: Set.Mem, LinearMap.IsSymmetric.orthogonalFamily_iInf_eigenspaces
-- Module: Mathlib.Analysis.InnerProductSpace.JointEigenspace
Goal:
𝕜 : Type u_1
E : Type u_2
n : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : n → Module.End 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
inst_4 : DecidableEq (n → 𝕜)
hT : ∀ (i : n), IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) (T i)
hC : Pairwise (Commute on T)
⊢ OrthogonalFamily 𝕜 (E := E) (fun (i : n → 𝕜) ↦ ↥(⨅ (j : n), (T j).eigenspace (i j))) fun (i : n → 𝕜) ↦
    subtypeₗᵢ (⨅ (j : n), (T j).eigenspace (i j))

Tactic:
exact orthogonalFamily_iInf_eigenspaces hT

Premises used: LinearMap.IsSymmetric.orthogonalFamily_iInf_eigenspaces
-- Module: Mathlib.Analysis.InnerProductSpace.Laplacian
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
e : E
s : Set E
f : E → F
hs : UniqueDiffOn 𝕜 s
he : e ∈ s
e₁ e₂ : E
⊢ Eq.{u_3 + 1} (α := F)
    ((((bilinearIteratedFDerivWithinTwo 𝕜 f s e : (a : E) → E →ₗ[𝕜] F) e₁ : E →ₗ[𝕜] F) : (a : E) → F) e₂ : F)
    ((iteratedFDerivWithin 𝕜 2 f s e : (a : (i : Fin 2) → E) → F) ![e₁, e₂] : F)

Tactic:
simp [iteratedFDerivWithin_two_apply f hs he ![e₁, e₂], bilinearIteratedFDerivWithinTwo]

Premises used: bilinearIteratedFDerivWithinTwo, Matrix.vecEmpty, iteratedFDerivWithin_two_apply, Matrix.vecCons
-- Module: Mathlib.Analysis.InnerProductSpace.Laplacian
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
e e₁ e₂ : E
⊢ Eq.{u_3 + 1} (α := F)
    ((((bilinearIteratedFDerivTwo 𝕜 f e : (a : E) → E →ₗ[𝕜] F) e₁ : E →ₗ[𝕜] F) : (a : E) → F) e₂ : F)
    ((iteratedFDeriv 𝕜 2 f e : (a : (i : Fin 2) → E) → F) ![e₁, e₂] : F)

Tactic:
simp [iteratedFDeriv_two_apply f e ![e₁, e₂], bilinearIteratedFDerivTwo]

Premises used: bilinearIteratedFDerivTwo, Matrix.vecEmpty, iteratedFDeriv_two_apply, Matrix.vecCons
-- Module: Mathlib.Analysis.InnerProductSpace.Laplacian
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
e : E
s : Set E
f : E → F
hs : UniqueDiffOn 𝕜 s
he : e ∈ s
e₁ e₂ : E
rw :
  Eq.{u_3 + 1} (α := F) ((tensorIteratedFDerivWithinTwo 𝕜 f s e : (a : E ⊗[𝕜] E) → F) (e₁ ⊗ₜ[𝕜] e₂) : F)
    ((((bilinearIteratedFDerivWithinTwo 𝕜 f s e : (a : E) → E →ₗ[𝕜] F) e₁ : E →ₗ[𝕜] F) : (a : E) → F) e₂ : F)
rw₁ :
  Eq.{u_3 + 1} (α := F) ((lift (bilinearIteratedFDerivWithinTwo 𝕜 f s e) : (a : E ⊗[𝕜] E) → F) (e₁ ⊗ₜ[𝕜] e₂) : F)
    ((((bilinearIteratedFDerivWithinTwo 𝕜 f s e : (a : E) → E →ₗ[𝕜] F) e₁ : E →ₗ[𝕜] F) : (a : E) → F) e₂ : F)
rw₂ rw₃ :
  Eq.{u_3 + 1} (α := F)
    ((((bilinearIteratedFDerivWithinTwo 𝕜 f s e : (a : E) → E →ₗ[𝕜] F) e₁ : E →ₗ[𝕜] F) : (a : E) → F) e₂ : F)
    ((((bilinearIteratedFDerivWithinTwo 𝕜 f s e : (a : E) → E →ₗ[𝕜] F) e₁ : E →ₗ[𝕜] F) : (a : E) → F) e₂ : F)
⊢ Eq.{u_3 + 1} (α := F) ((tensorIteratedFDerivWithinTwo 𝕜 f s e : (a : E ⊗[𝕜] E) → F) (e₁ ⊗ₜ[𝕜] e₂) : F)
    ((iteratedFDerivWithin 𝕜 2 f s e : (a : (i : Fin 2) → E) → F) ![e₁, e₂] : F)

Tactic:
rw [← bilinearIteratedFDerivWithinTwo_eq_iteratedFDeriv f hs he, tensorIteratedFDerivWithinTwo,
    lift.tmul]

Premises used: tensorIteratedFDerivWithinTwo, TensorProduct.lift.tmul, bilinearIteratedFDerivWithinTwo_eq_iteratedFDeriv
-- Module: Mathlib.Analysis.InnerProductSpace.Laplacian
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
e e₁ e₂ : E
rw :
  Eq.{u_3 + 1} (α := F) ((tensorIteratedFDerivTwo 𝕜 f e : (a : E ⊗[𝕜] E) → F) (e₁ ⊗ₜ[𝕜] e₂) : F)
    ((((bilinearIteratedFDerivTwo 𝕜 f e : (a : E) → E →ₗ[𝕜] F) e₁ : E →ₗ[𝕜] F) : (a : E) → F) e₂ : F)
rw₁ :
  Eq.{u_3 + 1} (α := F) ((lift (bilinearIteratedFDerivTwo 𝕜 f e) : (a : E ⊗[𝕜] E) → F) (e₁ ⊗ₜ[𝕜] e₂) : F)
    ((((bilinearIteratedFDerivTwo 𝕜 f e : (a : E) → E →ₗ[𝕜] F) e₁ : E →ₗ[𝕜] F) : (a : E) → F) e₂ : F)
rw₂ rw₃ :
  Eq.{u_3 + 1} (α := F)
    ((((bilinearIteratedFDerivTwo 𝕜 f e : (a : E) → E →ₗ[𝕜] F) e₁ : E →ₗ[𝕜] F) : (a : E) → F) e₂ : F)
    ((((bilinearIteratedFDerivTwo 𝕜 f e : (a : E) → E →ₗ[𝕜] F) e₁ : E →ₗ[𝕜] F) : (a : E) → F) e₂ : F)
⊢ Eq.{u_3 + 1} (α := F) ((tensorIteratedFDerivTwo 𝕜 f e : (a : E ⊗[𝕜] E) → F) (e₁ ⊗ₜ[𝕜] e₂) : F)
    ((iteratedFDeriv 𝕜 2 f e : (a : (i : Fin 2) → E) → F) ![e₁, e₂] : F)

Tactic:
rw [← bilinearIteratedFDerivTwo_eq_iteratedFDeriv, tensorIteratedFDerivTwo, lift.tmul]

Premises used: bilinearIteratedFDerivTwo_eq_iteratedFDeriv, tensorIteratedFDerivTwo, TensorProduct.lift.tmul
-- Module: Mathlib.Analysis.InnerProductSpace.Laplacian
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
f : E → F
h : ∀ (x : E), (Δ[Set.univ] f) x = Δ f x
⊢ Δ[Set.univ] f = Δ f

Tactic:
ext x
-- Module: Mathlib.Analysis.InnerProductSpace.Laplacian
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
f : E → F
x : E
⊢ (Δ[Set.univ] f) x = Δ f x

Tactic:
simp [laplacian, tensorIteratedFDerivTwo, bilinearIteratedFDerivTwo,
    laplacianWithin, tensorIteratedFDerivWithinTwo, bilinearIteratedFDerivWithinTwo]

Premises used: Laplacian.laplacian, bilinearIteratedFDerivWithinTwo, tensorIteratedFDerivTwo, tensorIteratedFDerivWithinTwo, bilinearIteratedFDerivTwo, InnerProductSpace.laplacianWithin
-- Module: Mathlib.Analysis.InnerProductSpace.Laplacian
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
f : E → F
s : Set E
ι : Type u_5
inst_5 : Fintype ι
e : E
hs : UniqueDiffOn ℝ s
he : e ∈ s
v : OrthonormalBasis ι ℝ E
⊢ (Δ[s] f) e =
    ∑ i : ι,
      (iteratedFDerivWithin ℝ 2 f s e : (a : (i : Fin 2) → E) → F)
        (![(v : (a : ι) → E) i, (v : (a : ι) → E) i] : Fin (Nat.succ 1) → E)

Tactic:
simp [InnerProductSpace.laplacianWithin, canonicalCovariantTensor_eq_sum E v,
    tensorIteratedFDerivWithinTwo_eq_iteratedFDerivWithin f hs he]

Premises used: InnerProductSpace.canonicalCovariantTensor_eq_sum, tensorIteratedFDerivWithinTwo_eq_iteratedFDerivWithin, InnerProductSpace.laplacianWithin
-- Module: Mathlib.Analysis.InnerProductSpace.Laplacian
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
f : E → F
ι : Type u_5
inst_5 : Fintype ι
v : OrthonormalBasis ι ℝ E
h :
  ∀ (x : E),
    Δ f x =
      ∑ i : ι,
        (iteratedFDeriv ℝ 2 f x : (a : (i : Fin 2) → E) → F)
          (![(v : (a : ι) → E) i, (v : (a : ι) → E) i] : Fin (Nat.succ 1) → E)
⊢ Δ f = fun (x : E) ↦
    ∑ i : ι,
      (iteratedFDeriv ℝ 2 f x : (a : (i : Fin 2) → E) → F)
        (![(v : (a : ι) → E) i, (v : (a : ι) → E) i] : Fin (Nat.succ 1) → E)

Tactic:
ext x
-- Module: Mathlib.Analysis.InnerProductSpace.Laplacian
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
f : E → F
ι : Type u_5
inst_5 : Fintype ι
v : OrthonormalBasis ι ℝ E
x : E
⊢ Δ f x =
    ∑ i : ι,
      (iteratedFDeriv ℝ 2 f x : (a : (i : Fin 2) → E) → F)
        (![(v : (a : ι) → E) i, (v : (a : ι) → E) i] : Fin (Nat.succ 1) → E)

Tactic:
simp [laplacian, canonicalCovariantTensor_eq_sum E v, tensorIteratedFDerivTwo_eq_iteratedFDeriv]

Premises used: InnerProductSpace.canonicalCovariantTensor_eq_sum, Laplacian.laplacian, tensorIteratedFDerivTwo_eq_iteratedFDeriv
-- Module: Mathlib.Analysis.InnerProductSpace.Laplacian
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
f : E → F
s : Set E
e : E
hs : UniqueDiffOn ℝ s
he : e ∈ s
⊢ (Δ[s] f) e =
    ∑ i : Fin (Module.finrank ℝ E),
      (iteratedFDerivWithin ℝ 2 f s e : (a : (i : Fin 2) → E) → F)
        (![(stdOrthonormalBasis ℝ E : (a : Fin (Module.finrank ℝ E)) → E) i,
            (stdOrthonormalBasis ℝ E : (a : Fin (Module.finrank ℝ E)) → E) i] :
          Fin (Nat.succ 1) → E)

Tactic:
apply laplacianWithin_eq_iteratedFDerivWithin_orthonormalBasis f hs he (stdOrthonormalBasis ℝ E)

Premises used: Real, InnerProductSpace.laplacianWithin_eq_iteratedFDerivWithin_orthonormalBasis, stdOrthonormalBasis
-- Module: Mathlib.Analysis.InnerProductSpace.Laplacian
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
f : E → F
⊢ Δ f = fun (x : E) ↦
    ∑ i : Fin (Module.finrank ℝ E),
      (iteratedFDeriv ℝ 2 f x : (a : (i : Fin 2) → E) → F)
        (![(stdOrthonormalBasis ℝ E : (a : Fin (Module.finrank ℝ E)) → E) i,
            (stdOrthonormalBasis ℝ E : (a : Fin (Module.finrank ℝ E)) → E) i] :
          Fin (Nat.succ 1) → E)

Tactic:
laplacian_eq_iteratedFDeriv_orthonormalBasis f (stdOrthonormalBasis ℝ E)

Premises used: Real, InnerProductSpace.laplacian_eq_iteratedFDeriv_orthonormalBasis, stdOrthonormalBasis
-- Module: Mathlib.Analysis.InnerProductSpace.Laplacian
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
e : ℝ
s : Set ℝ
f : ℝ → F
hs : UniqueDiffOn ℝ s
he : e ∈ s
simp :
  Eq (α := F) ((iteratedFDerivWithin ℝ 2 f s e : (a : (i : Fin 2) → ℝ) → F) ![1, 1] : F)
    ((iteratedFDerivWithin ℝ 2 f s e : (a : (i : Fin 2) → ℝ) → F) fun (x : Fin 2) ↦ 1 : F)
⊢ (Δ[s] f) e = iteratedDerivWithin 2 f s e

Tactic:
simp only [laplacianWithin_eq_iteratedFDerivWithin_orthonormalBasis f hs he
        (OrthonormalBasis.singleton (Fin 1) ℝ),
    Finset.univ_unique, Fin.default_eq_zero, Fin.isValue, OrthonormalBasis.singleton_apply,
    Finset.sum_const, Finset.card_singleton, one_smul, iteratedDerivWithin_eq_iteratedFDerivWithin]

Premises used: Real, iteratedDerivWithin_eq_iteratedFDerivWithin, OrthonormalBasis.singleton_apply, Finset.univ_unique, OrthonormalBasis.singleton, InnerProductSpace.laplacianWithin_eq_iteratedFDerivWithin_orthonormalBasis, one_smul, Fin.isValue, Fin.default_eq_zero, OfNat.ofNat, Fin, Finset.sum_const, Finset.card_singleton
-- Module: Mathlib.Analysis.InnerProductSpace.Laplacian
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
e : ℝ
s : Set ℝ
f : ℝ → F
hs : UniqueDiffOn ℝ s
he : e ∈ s
h : ∀ (i : Fin (Nat.succ 1)), Eq (α := ℝ) (![1, 1] i) 1
⊢ Eq (α := F) ((iteratedFDerivWithin ℝ 2 f s e : (a : (i : Fin 2) → ℝ) → F) ![1, 1] : F)
    ((iteratedFDerivWithin ℝ 2 f s e : (a : (i : Fin 2) → ℝ) → F) fun (x : Fin 2) ↦ 1 : F)

Tactic:
congr with i
-- Module: Mathlib.Analysis.InnerProductSpace.Laplacian
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
e : ℝ
s : Set ℝ
f : ℝ → F
hs : UniqueDiffOn ℝ s
he : e ∈ s
i : Fin (Nat.succ 1)
h : Eq (α := ℝ) (![1, 1] ((fun (i : Fin (Nat.succ 1)) ↦ i) ⟨0, ⋯⟩)) 1
h₁ : Eq (α := ℝ) (![1, 1] ((fun (i : Fin (Nat.succ 1)) ↦ i) ⟨1, ⋯⟩)) 1
⊢ Eq (α := ℝ) (![1, 1] i) 1

Tactic:
fin_cases i
-- Module: Mathlib.Analysis.InnerProductSpace.Laplacian
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
e : ℝ
s : Set ℝ
f : ℝ → F
hs : UniqueDiffOn ℝ s
he : e ∈ s
⊢ Eq (α := ℝ) (![1, 1] ((fun (i : Fin (Nat.succ 1)) ↦ i) ⟨0, ⋯⟩)) 1

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.Laplacian
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
e : ℝ
s : Set ℝ
f : ℝ → F
hs : UniqueDiffOn ℝ s
he : e ∈ s
⊢ Eq (α := ℝ) (![1, 1] ((fun (i : Fin (Nat.succ 1)) ↦ i) ⟨1, ⋯⟩)) 1

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.Laplacian
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
e : ℝ
f : ℝ → F
⊢ UniqueDiffOn ℝ (E := ℝ) Set.univ

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.Laplacian
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
e : ℝ
f : ℝ → F
⊢ Membership.mem (γ := Set ℝ) Set.univ e

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.Laplacian
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
e : ℝ
f : ℝ → F
rw : (Δ[Set.univ] f) e = iteratedDeriv 2 f e
rw₁ : (Δ[Set.univ] f) e = iteratedDerivWithin 2 f Set.univ e
rw₂ rw₃ : iteratedDerivWithin 2 f Set.univ e = iteratedDerivWithin 2 f Set.univ e
⊢ Δ f e = iteratedDeriv 2 f e

Tactic:
rw [← laplacianWithin_univ, ← iteratedDerivWithin_univ,
    laplacianWithin_eq_iteratedDerivWithin_real _ (by simp) (by simp)]

Premises used: InnerProductSpace.laplacianWithin_eq_iteratedDerivWithin_real, InnerProductSpace.laplacianWithin_univ, iteratedDerivWithin_univ
-- Module: Mathlib.Analysis.InnerProductSpace.Laplacian
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
e : ℂ
s : Set ℂ
f : ℂ → F
hs : UniqueDiffOn ℝ s
he : e ∈ s
⊢ (Δ[s] f) e =
    HAdd.hAdd (α := F) (β := F) ((iteratedFDerivWithin ℝ 2 f s e : (a : (i : Fin 2) → ℂ) → F) ![1, 1] : F)
      ((iteratedFDerivWithin ℝ 2 f s e : (a : (i : Fin 2) → ℂ) → F) ![Complex.I, Complex.I] : F)

Tactic:
simp [laplacianWithin_eq_iteratedFDerivWithin_orthonormalBasis f hs he
    Complex.orthonormalBasisOneI]

Premises used: Complex.orthonormalBasisOneI, InnerProductSpace.laplacianWithin_eq_iteratedFDerivWithin_orthonormalBasis
-- Module: Mathlib.Analysis.InnerProductSpace.Laplacian
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℂ → F
⊢ Δ f = fun (x : ℂ) ↦
    HAdd.hAdd (α := F) (β := F) ((iteratedFDeriv ℝ 2 f x : (a : (i : Fin 2) → ℂ) → F) ![1, 1] : F)
      ((iteratedFDeriv ℝ 2 f x : (a : (i : Fin 2) → ℂ) → F) ![Complex.I, Complex.I] : F)

Tactic:
simp [laplacian_eq_iteratedFDeriv_orthonormalBasis f Complex.orthonormalBasisOneI]

Premises used: Complex.orthonormalBasisOneI, InnerProductSpace.laplacian_eq_iteratedFDeriv_orthonormalBasis
-- Module: Mathlib.Analysis.InnerProductSpace.Laplacian
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
c : F
⊢ (Δ (E := E → F) fun (x : E) ↦ c) = 0

Tactic:
simp [laplacian_eq_iteratedFDeriv_stdOrthonormalBasis, iteratedFDeriv_const_of_ne two_ne_zero,
    Pi.zero_def]

Premises used: Pi.zero_def, two_ne_zero, InnerProductSpace.laplacian_eq_iteratedFDeriv_stdOrthonormalBasis, iteratedFDeriv_const_of_ne
-- Module: Mathlib.Analysis.InnerProductSpace.Laplacian
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
f₁ f₂ : E → F
x : E
s : Set E
h : f₁ =ᶠ[𝓝[s] x] f₂
hs : UniqueDiffOn ℝ s
h₁ :
  ∀ (x : E)
    (h₁x :
      Eq (α := ContinuousMultilinearMap.{0, 0, u_2, u_3} ℝ (fun (i : Fin 2) ↦ E) F) (iteratedFDerivWithin ℝ 2 f₁ s x)
        (iteratedFDerivWithin ℝ 2 f₂ s x))
    (h₂x : x ∈ s), (Δ[s] f₁) x = (Δ[s] f₂) x
⊢ Δ[s] f₁ =ᶠ[𝓝[s] x] Δ[s] f₂

Tactic:
filter_upwards [EventuallyEq.iteratedFDerivWithin (𝕜 := ℝ) h 2,
    eventually_mem_nhdsWithin] with x h₁x h₂x

Premises used: Real, eventually_mem_nhdsWithin, Filter.EventuallyEq.iteratedFDerivWithin, OfNat.ofNat
-- Module: Mathlib.Analysis.InnerProductSpace.Laplacian
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
f₁ f₂ : E → F
x_1 : E
s : Set E
h : f₁ =ᶠ[𝓝[s] x_1] f₂
hs : UniqueDiffOn ℝ s
x : E
h₁x :
  Eq (α := ContinuousMultilinearMap.{0, 0, u_2, u_3} ℝ (fun (i : Fin 2) ↦ E) F) (iteratedFDerivWithin ℝ 2 f₁ s x)
    (iteratedFDerivWithin ℝ 2 f₂ s x)
h₂x : x ∈ s
⊢ (Δ[s] f₁) x = (Δ[s] f₂) x

Tactic:
simp [laplacianWithin_eq_iteratedFDerivWithin_stdOrthonormalBasis _ hs h₂x, h₁x]

Premises used: InnerProductSpace.laplacianWithin_eq_iteratedFDerivWithin_stdOrthonormalBasis
-- Module: Mathlib.Analysis.InnerProductSpace.Laplacian
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
f₁ f₂ : E → F
x : E
h : f₁ =ᶠ[𝓝 x] f₂
h₁ :
  ∀ (x : E)
    (hx :
      Eq (α := ContinuousMultilinearMap.{0, 0, u_2, u_3} ℝ (fun (i : Fin 2) ↦ E) F) (iteratedFDeriv ℝ 2 f₁ x)
        (iteratedFDeriv ℝ 2 f₂ x)),
    Δ f₁ x = Δ f₂ x
⊢ Δ f₁ =ᶠ[𝓝 x] Δ f₂

Tactic:
filter_upwards [EventuallyEq.iteratedFDeriv ℝ h 2] with x hx

Premises used: Real, Filter.EventuallyEq.iteratedFDeriv, OfNat.ofNat