awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
h : f₁ =ᶠ[𝓝 x_1] f₂
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

Tactic:
simp [laplacian_eq_iteratedFDeriv_stdOrthonormalBasis, hx]

Premises used: InnerProductSpace.laplacian_eq_iteratedFDeriv_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
s : Set E
h₁ : ContDiffWithinAt ℝ 2 f₁ s x
h₂ : ContDiffWithinAt ℝ 2 f₂ s x
hs : UniqueDiffOn ℝ s
hx : x ∈ s
⊢ (Δ[s] f₁ + f₂) x = (Δ[s] f₁) x + (Δ[s] f₂) x

Tactic:
simp [laplacianWithin_eq_iteratedFDerivWithin_stdOrthonormalBasis _ hs hx,
    ← Finset.sum_add_distrib, iteratedFDerivWithin_add_apply h₁ h₂ hs hx]

Premises used: Finset.sum_add_distrib, iteratedFDerivWithin_add_apply, 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₁ : ContDiffAt ℝ 2 f₁ x
h₂ : ContDiffAt ℝ 2 f₂ x
⊢ Δ (f₁ + f₂) x = Δ f₁ x + Δ f₂ x

Tactic:
simp [laplacian_eq_iteratedFDeriv_stdOrthonormalBasis,
    ← Finset.sum_add_distrib, iteratedFDeriv_add_apply h₁ h₂]

Premises used: Finset.sum_add_distrib, iteratedFDeriv_add_apply, InnerProductSpace.laplacian_eq_iteratedFDeriv_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
s : Set E
h₁ : ContDiffWithinAt ℝ 2 f₁ s x
h₂ : ContDiffWithinAt ℝ 2 f₂ s x
hs : UniqueDiffOn ℝ s
hx : x ∈ s
nth_rw : Δ[s] f₁ + f₂ =ᶠ[𝓝[insert x s] x] (Δ[s] f₁) + Δ[s] f₂
⊢ Δ[s] f₁ + f₂ =ᶠ[𝓝[s] x] (Δ[s] f₁) + Δ[s] f₂

Tactic:
nth_rw 1 [← s.insert_eq_of_mem hx]

Premises used: Set.insert_eq_of_mem
-- 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₁ : ContDiffWithinAt ℝ 2 f₁ s x
h₂ : ContDiffWithinAt ℝ 2 f₂ s x
hs : UniqueDiffOn ℝ s
hx : x ∈ s
⊢ Ne (α := WithTop ℕ∞) 2 (↑⊤ : WithTop ℕ∞)

Tactic:
simp
-- 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₁ : ContDiffWithinAt ℝ 2 f₁ s x
h₂ : ContDiffWithinAt ℝ 2 f₂ s x
hs : UniqueDiffOn ℝ s
hx : x ∈ s
h :
  ∀ (y : E) (h₁y : ContDiffWithinAt ℝ 2 f₁ s y) (h₂y : ContDiffWithinAt ℝ 2 f₂ s y) (h₃y : y ∈ insert x s),
    (Δ[s] f₁ + f₂) y = ((Δ[s] f₁) + Δ[s] f₂) y
⊢ Δ[s] f₁ + f₂ =ᶠ[𝓝[insert x s] x] (Δ[s] f₁) + Δ[s] f₂

Tactic:
filter_upwards [h₁.eventually (by simp), h₂.eventually (by simp),
    eventually_mem_nhdsWithin] with y h₁y h₂y h₃y

Premises used: ContDiffWithinAt.eventually, eventually_mem_nhdsWithin
-- 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₁ : ContDiffWithinAt ℝ 2 f₁ s x
h₂ : ContDiffWithinAt ℝ 2 f₂ s x
hs : UniqueDiffOn ℝ s
hx : x ∈ s
y : E
h₁y : ContDiffWithinAt ℝ 2 f₁ s y
h₂y : ContDiffWithinAt ℝ 2 f₂ s y
h₃y : y ∈ insert x s
⊢ y ∈ s

Tactic:
rw [s.insert_eq_of_mem hx] at h₃y

Premises used: Set.insert_eq_of_mem
-- 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₁ : ContDiffWithinAt ℝ 2 f₁ s x
h₂ : ContDiffWithinAt ℝ 2 f₂ s x
hs : UniqueDiffOn ℝ s
hx : x ∈ s
y : E
h₁y : ContDiffWithinAt ℝ 2 f₁ s y
h₂y : ContDiffWithinAt ℝ 2 f₂ s y
h₃y : y ∈ s
⊢ (Δ[s] f₁ + f₂) y = ((Δ[s] f₁) + Δ[s] f₂) y

Tactic:
simp [h₁y.laplacianWithin_add h₂y hs h₃y]

Premises used: ContDiffWithinAt.laplacianWithin_add
-- 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₁ : ContDiffAt ℝ 2 f₁ x
h₂ : ContDiffAt ℝ 2 f₂ x
⊢ Ne (α := WithTop ℕ∞) 2 (↑⊤ : WithTop ℕ∞)

Tactic:
simp
-- 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₁ : ContDiffAt ℝ 2 f₁ x
h₂ : ContDiffAt ℝ 2 f₂ x
h : ∀ (x : E) (h₁x : ContDiffAt ℝ 2 f₁ x) (h₂x : ContDiffAt ℝ 2 f₂ x), Δ (f₁ + f₂) x = (Δ f₁ + Δ f₂) x
⊢ Δ (f₁ + f₂) =ᶠ[𝓝 x] Δ f₁ + Δ f₂

Tactic:
filter_upwards [h₁.eventually (by simp), h₂.eventually (by simp)] with x h₁x h₂x

Premises used: ContDiffAt.eventually
-- 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
h₁ : ContDiffAt ℝ 2 f₁ x_1
h₂ : ContDiffAt ℝ 2 f₂ x_1
x : E
h₁x : ContDiffAt ℝ 2 f₁ x
h₂x : ContDiffAt ℝ 2 f₂ x
⊢ Δ (f₁ + f₂) x = (Δ f₁ + Δ f₂) x

Tactic:
h₁x.laplacian_add h₂x

Premises used: ContDiffAt.laplacian_add
-- 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
h₁ : ContDiffAt ℝ 2 f₁ x_1
h₂ : ContDiffAt ℝ 2 f₂ x_1
x : E
h₁x : ContDiffAt ℝ 2 f₁ x
h₂x : ContDiffAt ℝ 2 f₂ x
⊢ Δ (f₁ + f₂) x = (Δ f₁ + Δ f₂) x

Tactic:
exact h₁x.laplacian_add h₂x

Premises used: ContDiffAt.laplacian_add
-- 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
s : Set E
hs : UniqueDiffOn ℝ s
hx : x ∈ s
simp :
  Eq.{u_3 + 1} (α := F)
    (∑ i : Fin (Module.finrank ℝ E),
      (iteratedFDerivWithin ℝ 2 (-f) s 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))
    (-∑ i : Fin (Module.finrank ℝ E),
        (iteratedFDerivWithin ℝ 2 f s 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))
⊢ (Δ[s] -f) x = -(Δ[s] f) x

Tactic:
simp only [laplacianWithin_eq_iteratedFDerivWithin_stdOrthonormalBasis _ hs hx]

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 : E → F
x : E
s : Set E
hs : UniqueDiffOn ℝ s
hx : x ∈ s
rw :
  Eq.{u_3 + 1} (α := F)
    (∑ i : Fin (Module.finrank ℝ E),
      (-iteratedFDerivWithin ℝ 2 f s 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))
    (-∑ i : Fin (Module.finrank ℝ E),
        (iteratedFDerivWithin ℝ 2 f s 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))
⊢ Eq.{u_3 + 1} (α := F)
    (∑ i : Fin (Module.finrank ℝ E),
      (iteratedFDerivWithin ℝ 2 (-f) s 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))
    (-∑ i : Fin (Module.finrank ℝ E),
        (iteratedFDerivWithin ℝ 2 f s 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:
rw [iteratedFDerivWithin_neg_apply hs hx]

Premises used: iteratedFDerivWithin_neg_apply
-- 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
s : Set E
hs : UniqueDiffOn ℝ s
hx : x ∈ s
⊢ Eq.{u_3 + 1} (α := F)
    (∑ i : Fin (Module.finrank ℝ E),
      (-iteratedFDerivWithin ℝ 2 f s 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))
    (-∑ i : Fin (Module.finrank ℝ E),
        (iteratedFDerivWithin ℝ 2 f s 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:
aesop
-- 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
simp :
  Eq (α := E → F)
    (fun (x : E) ↦
      ∑ x_1 : Fin (Module.finrank ℝ E),
        (((-iteratedFDeriv ℝ 2 f) x : ContinuousMultilinearMap.{0, 0, u_2, u_3} ℝ (fun (i : Fin 2) ↦ E) F) :
            (a : (i : Fin 2) → E) → F)
          (![(stdOrthonormalBasis ℝ E : (a : Fin (Module.finrank ℝ E)) → E) x_1,
              (stdOrthonormalBasis ℝ E : (a : Fin (Module.finrank ℝ E)) → E) x_1] :
            Fin (Nat.succ 1) → E))
    (-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))
⊢ Δ (-f) = -Δ f

Tactic:
simp only [laplacian_eq_iteratedFDeriv_stdOrthonormalBasis, iteratedFDeriv_neg]

Premises used: InnerProductSpace.laplacian_eq_iteratedFDeriv_stdOrthonormalBasis, iteratedFDeriv_neg
-- 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
⊢ Eq (α := E → F)
    (fun (x : E) ↦
      ∑ x_1 : Fin (Module.finrank ℝ E),
        (((-iteratedFDeriv ℝ 2 f) x : ContinuousMultilinearMap.{0, 0, u_2, u_3} ℝ (fun (i : Fin 2) ↦ E) F) :
            (a : (i : Fin 2) → E) → F)
          (![(stdOrthonormalBasis ℝ E : (a : Fin (Module.finrank ℝ E)) → E) x_1,
              (stdOrthonormalBasis ℝ E : (a : Fin (Module.finrank ℝ E)) → E) x_1] :
            Fin (Nat.succ 1) → E))
    (-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:
aesop
-- 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₁ : ContDiffWithinAt ℝ 2 f₁ s x
h₂ : ContDiffWithinAt ℝ 2 f₂ s x
hs : UniqueDiffOn ℝ s
hx : x ∈ s
⊢ (Δ[s] f₁ - f₂) x = (Δ[s] f₁) x - (Δ[s] f₂) x

Tactic:
simp [laplacianWithin_eq_iteratedFDerivWithin_stdOrthonormalBasis _ hs hx,
    ← Finset.sum_sub_distrib, iteratedFDerivWithin_sub_apply h₁ h₂ hs hx]

Premises used: InnerProductSpace.laplacianWithin_eq_iteratedFDerivWithin_stdOrthonormalBasis, Finset.sum_sub_distrib, iteratedFDerivWithin_sub_apply
-- 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₁ : ContDiffAt ℝ 2 f₁ x
h₂ : ContDiffAt ℝ 2 f₂ x
⊢ Δ (f₁ - f₂) x = Δ f₁ x - Δ f₂ x

Tactic:
simp [laplacian_eq_iteratedFDeriv_stdOrthonormalBasis,
    ← Finset.sum_sub_distrib, iteratedFDeriv_sub_apply h₁ h₂]

Premises used: Finset.sum_sub_distrib, InnerProductSpace.laplacian_eq_iteratedFDeriv_stdOrthonormalBasis, iteratedFDeriv_sub_apply
-- 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₁ : ContDiffWithinAt ℝ 2 f₁ s x
h₂ : ContDiffWithinAt ℝ 2 f₂ s x
hs : UniqueDiffOn ℝ s
hx : x ∈ s
nth_rw : Δ[s] f₁ - f₂ =ᶠ[𝓝[insert x s] x] (Δ[s] f₁) - Δ[s] f₂
⊢ Δ[s] f₁ - f₂ =ᶠ[𝓝[s] x] (Δ[s] f₁) - Δ[s] f₂

Tactic:
nth_rw 1 [← s.insert_eq_of_mem hx]

Premises used: Set.insert_eq_of_mem
-- 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₁ : ContDiffWithinAt ℝ 2 f₁ s x
h₂ : ContDiffWithinAt ℝ 2 f₂ s x
hs : UniqueDiffOn ℝ s
hx : x ∈ s
h :
  ∀ (y : E) (h₁y : ContDiffWithinAt ℝ 2 f₁ s y) (h₂y : ContDiffWithinAt ℝ 2 f₂ s y) (h₃y : y ∈ insert x s),
    (Δ[s] f₁ - f₂) y = ((Δ[s] f₁) - Δ[s] f₂) y
⊢ Δ[s] f₁ - f₂ =ᶠ[𝓝[insert x s] x] (Δ[s] f₁) - Δ[s] f₂

Tactic:
filter_upwards [h₁.eventually (by simp), h₂.eventually (by simp),
    eventually_mem_nhdsWithin] with y h₁y h₂y h₃y

Premises used: ContDiffWithinAt.eventually, eventually_mem_nhdsWithin
-- 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₁ : ContDiffWithinAt ℝ 2 f₁ s x
h₂ : ContDiffWithinAt ℝ 2 f₂ s x
hs : UniqueDiffOn ℝ s
hx : x ∈ s
y : E
h₁y : ContDiffWithinAt ℝ 2 f₁ s y
h₂y : ContDiffWithinAt ℝ 2 f₂ s y
h₃y : y ∈ s
⊢ (Δ[s] f₁ - f₂) y = ((Δ[s] f₁) - Δ[s] f₂) y

Tactic:
simp [h₁y.laplacianWithin_sub h₂y hs h₃y]

Premises used: ContDiffWithinAt.laplacianWithin_sub
-- 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₁ : ContDiffAt ℝ 2 f₁ x
h₂ : ContDiffAt ℝ 2 f₂ x
h : ∀ (x : E) (h₁x : ContDiffAt ℝ 2 f₁ x) (h₂x : ContDiffAt ℝ 2 f₂ x), Δ (f₁ - f₂) x = (Δ f₁ - Δ f₂) x
⊢ Δ (f₁ - f₂) =ᶠ[𝓝 x] Δ f₁ - Δ f₂

Tactic:
filter_upwards [h₁.eventually (by simp), h₂.eventually (by simp)] with x h₁x h₂x

Premises used: ContDiffAt.eventually
-- 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
h₁ : ContDiffAt ℝ 2 f₁ x_1
h₂ : ContDiffAt ℝ 2 f₂ x_1
x : E
h₁x : ContDiffAt ℝ 2 f₁ x
h₂x : ContDiffAt ℝ 2 f₂ x
⊢ Δ (f₁ - f₂) x = (Δ f₁ - Δ f₂) x

Tactic:
h₁x.laplacian_sub h₂x

Premises used: ContDiffAt.laplacian_sub
-- 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
h₁ : ContDiffAt ℝ 2 f₁ x_1
h₂ : ContDiffAt ℝ 2 f₂ x_1
x : E
h₁x : ContDiffAt ℝ 2 f₁ x
h₂x : ContDiffAt ℝ 2 f₂ x
⊢ Δ (f₁ - f₂) x = (Δ f₁ - Δ f₂) x

Tactic:
exact h₁x.laplacian_sub h₂x

Premises used: ContDiffAt.laplacian_sub
-- Module: Mathlib.Analysis.InnerProductSpace.Laplacian
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAlgebra ℝ 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : InnerProductSpace ℝ E
inst_4 : FiniteDimensional ℝ E
F : Type u_3
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace ℝ F
inst_7 : NormedSpace 𝕜 F
inst_8 : IsScalarTower ℝ 𝕜 F
f : E → F
x : E
s : Set E
v : 𝕜
hf : ContDiffWithinAt ℝ 2 f s x
hs : UniqueDiffOn ℝ s
hx : x ∈ s
⊢ (Δ[s] v • f) x = v • (Δ[s] f) x

Tactic:
simp [laplacianWithin_eq_iteratedFDerivWithin_stdOrthonormalBasis _ hs hx,
    iteratedFDerivWithin_const_smul_apply hf hs hx,
    Finset.smul_sum]

Premises used: iteratedFDerivWithin_const_smul_apply, InnerProductSpace.laplacianWithin_eq_iteratedFDerivWithin_stdOrthonormalBasis, Finset.smul_sum
-- Module: Mathlib.Analysis.InnerProductSpace.Laplacian
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAlgebra ℝ 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : InnerProductSpace ℝ E
inst_4 : FiniteDimensional ℝ E
F : Type u_3
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace ℝ F
inst_7 : NormedSpace 𝕜 F
inst_8 : IsScalarTower ℝ 𝕜 F
f : E → F
x : E
v : 𝕜
hf : ContDiffAt ℝ 2 f x
⊢ Δ (v • f) x = v • Δ f x

Tactic:
simp [laplacian_eq_iteratedFDeriv_stdOrthonormalBasis, iteratedFDeriv_const_smul_apply hf,
    Finset.smul_sum]

Premises used: iteratedFDeriv_const_smul_apply, InnerProductSpace.laplacian_eq_iteratedFDeriv_stdOrthonormalBasis, Finset.smul_sum
-- Module: Mathlib.Analysis.InnerProductSpace.Laplacian
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAlgebra ℝ 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : InnerProductSpace ℝ E
inst_4 : FiniteDimensional ℝ E
F : Type u_3
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace ℝ F
inst_7 : NormedSpace 𝕜 F
inst_8 : IsScalarTower ℝ 𝕜 F
f : E → F
x : E
s : Set E
v : 𝕜
hf : ContDiffWithinAt ℝ 2 f s x
hs : UniqueDiffOn ℝ s
⊢ Ne (α := WithTop ℕ∞) 2 (↑⊤ : WithTop ℕ∞)

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.Laplacian
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAlgebra ℝ 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : InnerProductSpace ℝ E
inst_4 : FiniteDimensional ℝ E
F : Type u_3
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace ℝ F
inst_7 : NormedSpace 𝕜 F
inst_8 : IsScalarTower ℝ 𝕜 F
f : E → F
x : E
s : Set E
v : 𝕜
hf : ContDiffWithinAt ℝ 2 f s x
hs : UniqueDiffOn ℝ s
a : E
h₁a : ContDiffWithinAt ℝ 2 f s a
⊢ a ∈ s → (Δ[s] v • f) a = (v • Δ[s] f) a

Tactic:
laplacianWithin_smul v h₁a hs

Premises used: InnerProductSpace.laplacianWithin_smul
-- Module: Mathlib.Analysis.InnerProductSpace.Laplacian
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAlgebra ℝ 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : InnerProductSpace ℝ E
inst_4 : FiniteDimensional ℝ E
F : Type u_3
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace ℝ F
inst_7 : NormedSpace 𝕜 F
inst_8 : IsScalarTower ℝ 𝕜 F
f : E → F
x : E
s : Set E
v : 𝕜
hf : ContDiffWithinAt ℝ 2 f s x
hs : UniqueDiffOn ℝ s
h :
  ∀ (a : E),
    Membership.mem (γ := Set E)
      {x : E |
        Membership.mem (γ := Set E) {x : E | (fun (x : E) ↦ ContDiffWithinAt ℝ 2 f s x) x} x →
          Membership.mem (γ := Set E)
            {x : E |
              Membership.mem (γ := Set E) {x : E | (fun (x : E) ↦ x ∈ s) x} x →
                Membership.mem (γ := Set E) {x : E | (fun (x : E) ↦ (Δ[s] v • f) x = (v • Δ[s] f) x) x} x}
            x}
      a
h₁ h₂ : ∀ (a : E) (h₁a : ContDiffWithinAt ℝ 2 f s a), a ∈ s → (Δ[s] v • f) a = (v • Δ[s] f) a
⊢ Δ[s] v • f =ᶠ[𝓝[s] x] v • Δ[s] f

Tactic:
filter_upwards [(hf.eventually (by simp)).filter_mono (nhdsWithin_mono _ (Set.subset_insert ..)),
    eventually_mem_nhdsWithin] with a h₁a using laplacianWithin_smul v h₁a hs

Premises used: Filter.Eventually.filter_mono, ContDiffWithinAt.eventually, eventually_mem_nhdsWithin, Set.subset_insert, nhdsWithin_mono
-- Module: Mathlib.Analysis.InnerProductSpace.Laplacian
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAlgebra ℝ 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : InnerProductSpace ℝ E
inst_4 : FiniteDimensional ℝ E
F : Type u_3
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace ℝ F
inst_7 : NormedSpace 𝕜 F
inst_8 : IsScalarTower ℝ 𝕜 F
f : E → F
x : E
v : 𝕜
h : ContDiffAt ℝ 2 f x
⊢ Ne (α := WithTop ℕ∞) 2 (↑⊤ : WithTop ℕ∞)

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.Laplacian
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAlgebra ℝ 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : InnerProductSpace ℝ E
inst_4 : FiniteDimensional ℝ E
F : Type u_3
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace ℝ F
inst_7 : NormedSpace 𝕜 F
inst_8 : IsScalarTower ℝ 𝕜 F
f : E → F
x : E
v : 𝕜
h : ContDiffAt ℝ 2 f x
h₁ : ∀ (a : E) (ha : ContDiffAt ℝ 2 f a), Δ (v • f) a = (v • Δ f) a
⊢ Δ (v • f) =ᶠ[𝓝 x] v • Δ f

Tactic:
filter_upwards [h.eventually (by simp)] with a ha

Premises used: ContDiffAt.eventually
-- Module: Mathlib.Analysis.InnerProductSpace.Laplacian
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAlgebra ℝ 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : InnerProductSpace ℝ E
inst_4 : FiniteDimensional ℝ E
F : Type u_3
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace ℝ F
inst_7 : NormedSpace 𝕜 F
inst_8 : IsScalarTower ℝ 𝕜 F
f : E → F
x : E
v : 𝕜
h : ContDiffAt ℝ 2 f x
a : E
ha : ContDiffAt ℝ 2 f a
⊢ Δ (v • f) a = (v • Δ f) a

Tactic:
simp [laplacian_smul v ha]

Premises used: InnerProductSpace.laplacian_smul
-- 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
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace ℝ G
f : E → F
x : E
s : Set E
l : F →L[ℝ] G
h : ContDiffWithinAt ℝ 2 f s x
hs : UniqueDiffOn ℝ s
hx : x ∈ s
⊢ Eq.{u_4 + 1} (α := G) ((Δ[s] (⇑l : (a : F) → G) ∘ f) x) (((⇑l : (a : F) → G) ∘ Δ[s] f) x)

Tactic:
simp [laplacianWithin_eq_iteratedFDerivWithin_stdOrthonormalBasis _ hs hx,
    l.iteratedFDerivWithin_comp_left h hs hx]

Premises used: ContinuousLinearMap.iteratedFDerivWithin_comp_left, 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
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace ℝ G
f : E → F
x : E
l : F →L[ℝ] G
h : ContDiffAt ℝ 2 f x
⊢ Δ (E := E → G) ((⇑l : (a : F) → G) ∘ f) x = ((⇑l : (a : F) → G) ∘ Δ f) x

Tactic:
simp [laplacian_eq_iteratedFDeriv_stdOrthonormalBasis, l.iteratedFDeriv_comp_left h]

Premises used: InnerProductSpace.laplacian_eq_iteratedFDeriv_stdOrthonormalBasis, ContinuousLinearMap.iteratedFDeriv_comp_left