awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Laplacian (goal)
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
⊢ Δ 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)
have 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)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Laplacian (goal)
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 = iteratedDerivWithin 2 f s e
have 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)
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]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Laplacian (goal)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
e : ℝ
s : Set ℝ
f : ℝ → F
hs : UniqueDiffOn ℝ s
he : e ∈ s
⊢ 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)
have h : ∀ (i : Fin (Nat.succ 1)), Eq (α := ℝ) (![1, 1] i) 1
Tactic: congr with i
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Laplacian (goal)
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)
⊢ Eq (α := ℝ) (![1, 1] i) 1
have h : Eq (α := ℝ) (![1, 1] ((fun (i : Fin (Nat.succ 1)) ↦ i) ⟨0, sorry⟩)) 1
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Laplacian (goal)
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
⊢ Eq (α := ℝ) (![1, 1] i) 1
have h₁ : Eq (α := ℝ) (![1, 1] ((fun (i : Fin (Nat.succ 1)) ↦ i) ⟨1, sorry⟩)) 1
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Laplacian (goal)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
e : ℝ
f : ℝ → F
⊢ Δ f e = iteratedDeriv 2 f e
have rw : (Δ[Set.univ] f) e = iteratedDeriv 2 f e
Tactic: rw [← laplacianWithin_univ, ← iteratedDerivWithin_univ,
    laplacianWithin_eq_iteratedDerivWithin_real _ (by simp) (by simp)]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Laplacian (goal)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
e : ℝ
f : ℝ → F
rw : (Δ[Set.univ] f) e = iteratedDeriv 2 f e
⊢ Δ f e = iteratedDeriv 2 f e
have rw₁ : (Δ[Set.univ] f) e = iteratedDerivWithin 2 f Set.univ e
Tactic: rw [← laplacianWithin_univ, ← iteratedDerivWithin_univ,
    laplacianWithin_eq_iteratedDerivWithin_real _ (by simp) (by simp)]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Laplacian (goal)
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
⊢ Δ f e = iteratedDeriv 2 f e
have rw₂ : iteratedDerivWithin 2 f Set.univ e = iteratedDerivWithin 2 f Set.univ e
Tactic: rw [← laplacianWithin_univ, ← iteratedDerivWithin_univ,
    laplacianWithin_eq_iteratedDerivWithin_real _ (by simp) (by simp)]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Laplacian (goal)
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
⊢ Δ[s] f₁ =ᶠ[𝓝[s] x] Δ[s] f₂
have 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
Tactic: filter_upwards [EventuallyEq.iteratedFDerivWithin (𝕜 := ℝ) h 2,
    eventually_mem_nhdsWithin] with x h₁x h₂x
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Laplacian (goal)
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₂
⊢ Δ f₁ =ᶠ[𝓝 x] Δ f₂
have 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
Tactic: filter_upwards [EventuallyEq.iteratedFDeriv ℝ h 2] with x hx
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Laplacian (goal)
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₂ =ᶠ[𝓝[s] x] (Δ[s] f₁) + Δ[s] f₂
have nth_rw : Δ[s] f₁ + f₂ =ᶠ[𝓝[insert x s] x] (Δ[s] f₁) + Δ[s] f₂
Tactic: nth_rw 1 [← s.insert_eq_of_mem hx]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Laplacian (goal)
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₂ =ᶠ[𝓝[insert x s] x] (Δ[s] f₁) + Δ[s] f₂
have 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
Tactic: filter_upwards [h₁.eventually (by simp), h₂.eventually (by simp),
    eventually_mem_nhdsWithin] with y h₁y h₂y h₃y
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Laplacian (hypothesis)
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
⊢ (Δ[s] f₁ + f₂) y = ((Δ[s] f₁) + Δ[s] f₂) y
have h₃y₁ : y ∈ s
Tactic: rw [s.insert_eq_of_mem hx] at h₃y
Cleared hypotheses: h₃y
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Laplacian (goal)
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₁ + Δ f₂
have h : ∀ (x : E) (h₁x : ContDiffAt ℝ 2 f₁ x) (h₂x : ContDiffAt ℝ 2 f₂ x), Δ (f₁ + f₂) x = (Δ f₁ + Δ f₂) x
Tactic: filter_upwards [h₁.eventually (by simp), h₂.eventually (by simp)] with x h₁x h₂x
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Laplacian (goal)
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
⊢ (Δ[s] -f) x = -(Δ[s] f) x
have 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))
Tactic: simp only [laplacianWithin_eq_iteratedFDerivWithin_stdOrthonormalBasis _ hs hx]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Laplacian (goal)
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))
have 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))
Tactic: rw [iteratedFDerivWithin_neg_apply hs hx]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Laplacian (goal)
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) = -Δ f
have 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))
Tactic: simp only [laplacian_eq_iteratedFDeriv_stdOrthonormalBasis, iteratedFDeriv_neg]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Laplacian (goal)
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₂ =ᶠ[𝓝[s] x] (Δ[s] f₁) - Δ[s] f₂
have nth_rw : Δ[s] f₁ - f₂ =ᶠ[𝓝[insert x s] x] (Δ[s] f₁) - Δ[s] f₂
Tactic: nth_rw 1 [← s.insert_eq_of_mem hx]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Laplacian (goal)
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₂ =ᶠ[𝓝[insert x s] x] (Δ[s] f₁) - Δ[s] f₂
have 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
Tactic: filter_upwards [h₁.eventually (by simp), h₂.eventually (by simp),
    eventually_mem_nhdsWithin] with y h₁y h₂y h₃y
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Laplacian (hypothesis)
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
⊢ (Δ[s] f₁ - f₂) y = ((Δ[s] f₁) - Δ[s] f₂) y
have h₃y₁ : y ∈ s
Tactic: rw [s.insert_eq_of_mem hx] at h₃y
Cleared hypotheses: h₃y
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Laplacian (goal)
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₁ - Δ f₂
have h : ∀ (x : E) (h₁x : ContDiffAt ℝ 2 f₁ x) (h₂x : ContDiffAt ℝ 2 f₂ x), Δ (f₁ - f₂) x = (Δ f₁ - Δ f₂) x
Tactic: filter_upwards [h₁.eventually (by simp), h₂.eventually (by simp)] with x h₁x h₂x
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Laplacian (goal)
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
⊢ Δ[s] v • f =ᶠ[𝓝[s] x] v • Δ[s] f
have 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
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
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Laplacian (goal)
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
⊢ Δ[s] v • f =ᶠ[𝓝[s] x] v • Δ[s] f
have h₁ : ∀ (a : E), ContDiffWithinAt ℝ 2 f s a → a ∈ s → (Δ[s] v • f) a = (v • Δ[s] f) a
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
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Laplacian (goal)
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
⊢ Δ (v • f) =ᶠ[𝓝 x] v • Δ f
have h₁ : ∀ (a : E) (ha : ContDiffAt ℝ 2 f a), Δ (v • f) a = (v • Δ f) a
Tactic: filter_upwards [h.eventually (by simp)] with a ha
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Laplacian (goal)
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
⊢ EventuallyEq.{u_2, u_4} (β := G) (𝓝[s] x) (Δ[s] (⇑l : (a : F) → G) ∘ f) ((⇑l : (a : F) → G) ∘ Δ[s] f)
have 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) ↦
                      Eq.{u_4 + 1} (α := G) ((Δ[s] (⇑l : (a : F) → G) ∘ f) x) (((⇑l : (a : F) → G) ∘ Δ[s] f) x))
                    x}
                x}
          x}
    a
Tactic: filter_upwards [(h.eventually (by simp)).filter_mono (nhdsWithin_mono _ (Set.subset_insert ..)),
    eventually_mem_nhdsWithin] with a h₁a using h₁a.laplacianWithin_CLM_comp_left hs
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Laplacian (goal)
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
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) ↦
                        Eq.{u_4 + 1} (α := G) ((Δ[s] (⇑l : (a : F) → G) ∘ f) x) (((⇑l : (a : F) → G) ∘ Δ[s] f) x))
                      x}
                  x}
            x}
      a
⊢ EventuallyEq.{u_2, u_4} (β := G) (𝓝[s] x) (Δ[s] (⇑l : (a : F) → G) ∘ f) ((⇑l : (a : F) → G) ∘ Δ[s] f)
have h₂ : ∀ (a : E),
  ContDiffWithinAt ℝ 2 f s a →
    a ∈ s → Eq.{u_4 + 1} (α := G) ((Δ[s] (⇑l : (a : F) → G) ∘ f) a) (((⇑l : (a : F) → G) ∘ Δ[s] f) a)
Tactic: filter_upwards [(h.eventually (by simp)).filter_mono (nhdsWithin_mono _ (Set.subset_insert ..)),
    eventually_mem_nhdsWithin] with a h₁a using h₁a.laplacianWithin_CLM_comp_left hs
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Laplacian (goal)
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
have h₁ : ∀ (a : E) (ha : ContDiffAt ℝ 2 f a), Δ (E := E → G) ((⇑l : (a : F) → G) ∘ f) a = ((⇑l : (a : F) → G) ∘ Δ f) a
Tactic: filter_upwards [h.eventually (by simp)] with a ha
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Laplacian (goal)
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
a : E
ha : ContDiffAt ℝ 2 f a
⊢ Δ (E := E → G) ((⇑l : (a : F) → G) ∘ f) a = ((⇑l : (a : F) → G) ∘ Δ f) a
have h₁ : Eq.{u_4 + 1} (α := G) (((⇑l : (a : F) → G) ∘ Δ f) a) (((⇑l : (a : F) → G) ∘ Δ f) a)
Tactic: rw [ha.laplacian_CLM_comp_left]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Laplacian (goal)
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
l : F ≃L[ℝ] G
⊢ Δ (E := E → G) ((⇑l : (a : F) → G) ∘ f) = (⇑l : (a : F) → G) ∘ Δ f
have h : ∀ (x : E), Δ (E := E → G) ((⇑l : (a : F) → G) ∘ f) x = ((⇑l : (a : F) → G) ∘ Δ f) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.LaxMilgram (goal)
Goal:
V : Type u
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
coercive : IsCoercive B
⊢ ∃ (C : ℝ), 0 < C ∧ ∀ (v : V), C * ‖v‖ ≤ norm (E := V) ((continuousLinearMapOfBilin B : (a : V) → V) v : V)
have rcases : ∀ (C : ℝ) (C_ge_0 : 0 < C)
  (coercivity : ∀ (u : V), C * ‖u‖ * ‖u‖ ≤ (((B : (a : V) → V →L[ℝ] ℝ) u : V →L[ℝ] ℝ) : (a : V) → ℝ) u),
  ∃ (C : ℝ), 0 < C ∧ ∀ (v : V), C * ‖v‖ ≤ norm (E := V) ((continuousLinearMapOfBilin B : (a : V) → V) v : V)
Tactic: rcases coercive with ⟨C, C_ge_0, coercivity⟩
Cleared hypotheses: coercive
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.LaxMilgram (goal)
Goal:
V : Type u
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
C : ℝ
C_ge_0 : 0 < C
coercivity : ∀ (u : V), C * ‖u‖ * ‖u‖ ≤ (((B : (a : V) → V →L[ℝ] ℝ) u : V →L[ℝ] ℝ) : (a : V) → ℝ) u
⊢ ∃ (C : ℝ), 0 < C ∧ ∀ (v : V), C * ‖v‖ ≤ norm (E := V) ((continuousLinearMapOfBilin B : (a : V) → V) v : V)
have refine : ∀ (v : V), C * ‖v‖ ≤ norm (E := V) ((continuousLinearMapOfBilin B : (a : V) → V) v : V)
Tactic: refine ⟨C, C_ge_0, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.LaxMilgram (goal)
Goal:
V : Type u
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
C : ℝ
C_ge_0 : 0 < C
coercivity : ∀ (u : V), C * ‖u‖ * ‖u‖ ≤ (((B : (a : V) → V →L[ℝ] ℝ) u : V →L[ℝ] ℝ) : (a : V) → ℝ) u
v : V
⊢ C * ‖v‖ ≤ norm (E := V) ((continuousLinearMapOfBilin B : (a : V) → V) v : V)
have pos : ∀ (h : 0 < ‖v‖), C * ‖v‖ ≤ norm (E := V) ((continuousLinearMapOfBilin B : (a : V) → V) v : V)
Tactic: by_cases h : 0 < ‖v‖
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.LaxMilgram (goal)
Goal:
V : Type u
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
C : ℝ
C_ge_0 : 0 < C
coercivity : ∀ (u : V), C * ‖u‖ * ‖u‖ ≤ (((B : (a : V) → V →L[ℝ] ℝ) u : V →L[ℝ] ℝ) : (a : V) → ℝ) u
v : V
pos : ∀ (h : 0 < ‖v‖), C * ‖v‖ ≤ norm (E := V) ((continuousLinearMapOfBilin B : (a : V) → V) v : V)
⊢ C * ‖v‖ ≤ norm (E := V) ((continuousLinearMapOfBilin B : (a : V) → V) v : V)
have neg : ∀ (h : ¬0 < ‖v‖), C * ‖v‖ ≤ norm (E := V) ((continuousLinearMapOfBilin B : (a : V) → V) v : V)
Tactic: by_cases h : 0 < ‖v‖
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.LaxMilgram (goal)
Goal:
V : Type u
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
C : ℝ
C_ge_0 : 0 < C
coercivity : ∀ (u : V), C * ‖u‖ * ‖u‖ ≤ (((B : (a : V) → V →L[ℝ] ℝ) u : V →L[ℝ] ℝ) : (a : V) → ℝ) u
v : V
h : 0 < ‖v‖
⊢ C * ‖v‖ ≤ norm (E := V) ((continuousLinearMapOfBilin B : (a : V) → V) v : V)
have pos : C * ‖v‖ * ‖v‖ ≤ norm (E := V) ((continuousLinearMapOfBilin B : (a : V) → V) v : V) * ‖v‖
Tactic: refine (mul_le_mul_iff_left₀ h).mp ?_