awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Deriv
Goal:
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F_1 : Type u_6
V : Type u_7
F : Type u_8
F₁ : Type u_9
F₂ : Type u_10
F₃ : Type u_11
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ F
inst_3 : NormedSpace ℝ E
inst_4 : RCLike 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
v w : E
f : 𝓢(E, F)
x : E
⊢ Eq.{u_8 + 1} (α := F) ((∂_{v + w} f : (a : E) → F) x : F) ((∂_{v} f + ∂_{w} f : (a : E) → F) x : F)

Tactic:
simp [lineDerivOp_apply_eq_fderiv]

Premises used: SchwartzMap.lineDerivOp_apply_eq_fderiv
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Deriv
Goal:
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F_1 : Type u_6
V : Type u_7
F : Type u_8
F₁ : Type u_9
F₂ : Type u_10
F₃ : Type u_11
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ F
inst_3 : NormedSpace ℝ E
inst_4 : RCLike 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
r : ℝ
y : E
f : 𝓢(E, F)
h : ∀ (x : E), Eq.{u_8 + 1} (α := F) ((∂_{r • y} f : (a : E) → F) x : F) ((r • ∂_{y} f : (a : E) → F) x : F)
⊢ ∂_{r • y} f = r • ∂_{y} f

Tactic:
ext x
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Deriv
Goal:
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F_1 : Type u_6
V : Type u_7
F : Type u_8
F₁ : Type u_9
F₂ : Type u_10
F₃ : Type u_11
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ F
inst_3 : NormedSpace ℝ E
inst_4 : RCLike 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
r : ℝ
y : E
f : 𝓢(E, F)
x : E
⊢ Eq.{u_8 + 1} (α := F) ((∂_{r • y} f : (a : E) → F) x : F) ((r • ∂_{y} f : (a : E) → F) x : F)

Tactic:
simp [lineDerivOp_apply_eq_fderiv]

Premises used: SchwartzMap.lineDerivOp_apply_eq_fderiv
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Deriv
Goal:
𝕜 : Type u_2
E : Type u_5
F : Type u_8
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ F
inst_3 : NormedSpace ℝ E
inst_4 : RCLike 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
m : E
⊢ Eq (α := 𝓢(E, F) →L[𝕜] 𝓢(E, F)) (lineDerivOpCLM 𝕜 𝓢(E, F) m) (SchwartzMap.evalCLM 𝕜 E F m ∘SL fderivCLM 𝕜 E F)

Tactic:
rfl

Premises used: ContinuousLinearMap.comp, LineDeriv.lineDerivOpCLM, rfl
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Deriv
Goal:
E : Type u_5
F : Type u_8
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ F
inst_3 : NormedSpace ℝ E
m : E
f : 𝓢(E, F)
x : E
⊢ Eq.{u_8 + 1} (α := F) ((∂_{m} f : (a : E) → F) x : F) (lineDeriv ℝ (⇑f : (a : E) → F) x m : F)

Tactic:
f.differentiableAt.lineDeriv_eq_fderiv.symm

Premises used: Eq.symm, SchwartzMap.differentiableAt, DifferentiableAt.lineDeriv_eq_fderiv
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Deriv
Goal:
E : Type u_5
F : Type u_8
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ F
inst_3 : NormedSpace ℝ E
f : 𝓢(E, F)
m : Fin 0 → E
x : E
⊢ Eq.{u_8 + 1} (α := F) ((∂^{m} f : (a : E) → F) x : F)
    ((iteratedFDeriv ℝ 0 (⇑f : (a : E) → F) x : (a : (i : Fin 0) → E) → F) m : F)

Tactic:
simp
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Deriv
Goal:
E : Type u_5
F : Type u_8
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ F
inst_3 : NormedSpace ℝ E
f : 𝓢(E, F)
n : ℕ
ih :
  ∀ {m : Fin n → E} {x : E},
    Eq.{u_8 + 1} (α := F) ((∂^{m} f : (a : E) → F) x : F)
      ((iteratedFDeriv ℝ n (⇑f : (a : E) → F) x : (a : (i : Fin n) → E) → F) m : F)
m : Fin (n + 1) → E
x : E
succ :
  Eq.{u_8 + 1} (α := F) ((∂_{m 0} (∂^{Fin.tail (α := fun (i : Fin (n + 1)) ↦ E) m} f) : (a : E) → F) x : F)
    ((fderiv ℝ
            (fun (y : E) ↦
              (iteratedFDeriv ℝ n (⇑f : (a : E) → F) y : (a : (i : Fin n) → E) → F)
                (Fin.tail (α := fun (i : Fin (n + 1)) ↦ E) m))
            x :
          (a : E) → F)
        (m 0) :
      F)
succ₁ :
  DifferentiableAt ℝ (F := ContinuousMultilinearMap.{0, 0, u_5, u_8} ℝ (fun (i : Fin n) ↦ E) F)
    (iteratedFDeriv ℝ n (⇑f : (a : E) → F)) x
⊢ Eq.{u_8 + 1} (α := F) ((∂^{m} f : (a : E) → F) x : F)
    ((iteratedFDeriv ℝ (n + 1) (⇑f : (a : E) → F) x : (a : (i : Fin (n + 1)) → E) → F) m : F)

Tactic:
rw [iteratedLineDerivOp_succ_left, iteratedFDeriv_succ_apply_left,
      ← fderiv_continuousMultilinear_apply_const_apply]

Premises used: LineDeriv.iteratedLineDerivOp_succ_left, fderiv_continuousMultilinear_apply_const_apply, iteratedFDeriv_succ_apply_left
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Deriv
Goal:
E : Type u_5
F : Type u_8
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ F
inst_3 : NormedSpace ℝ E
f : 𝓢(E, F)
n : ℕ
ih :
  ∀ {m : Fin n → E} {x : E},
    Eq.{u_8 + 1} (α := F) ((∂^{m} f : (a : E) → F) x : F)
      ((iteratedFDeriv ℝ n (⇑f : (a : E) → F) x : (a : (i : Fin n) → E) → F) m : F)
m : Fin (n + 1) → E
x : E
⊢ Eq.{u_8 + 1} (α := F) ((∂_{m 0} (∂^{Fin.tail (α := fun (i : Fin (n + 1)) ↦ E) m} f) : (a : E) → F) x : F)
    ((fderiv ℝ
            (fun (y : E) ↦
              (iteratedFDeriv ℝ n (⇑f : (a : E) → F) y : (a : (i : Fin n) → E) → F)
                (Fin.tail (α := fun (i : Fin (n + 1)) ↦ E) m))
            x :
          (a : E) → F)
        (m 0) :
      F)

Tactic:
simp only [lineDerivOp_apply_eq_fderiv, ← ih]

Premises used: SchwartzMap.lineDerivOp_apply_eq_fderiv
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Deriv
Goal:
E : Type u_5
F : Type u_8
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ F
inst_3 : NormedSpace ℝ E
f : 𝓢(E, F)
n : ℕ
ih :
  ∀ {m : Fin n → E} {x : E},
    Eq.{u_8 + 1} (α := F) ((∂^{m} f : (a : E) → F) x : F)
      ((iteratedFDeriv ℝ n (⇑f : (a : E) → F) x : (a : (i : Fin n) → E) → F) m : F)
m : Fin (n + 1) → E
x : E
⊢ DifferentiableAt ℝ (F := ContinuousMultilinearMap.{0, 0, u_5, u_8} ℝ (fun (i : Fin n) ↦ E) F)
    (iteratedFDeriv ℝ n (⇑f : (a : E) → F)) x

Tactic:
(f.smooth ⊤).differentiable_iteratedFDeriv (mod_cast ENat.coe_lt_top n) x

Premises used: ContDiff.differentiable_iteratedFDeriv, Top.top, SchwartzMap.smooth
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Deriv
Goal:
E : Type u_5
F : Type u_8
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ F
inst_3 : NormedSpace ℝ E
f : 𝓢(E, F)
n : ℕ
ih :
  ∀ {m : Fin n → E} {x : E},
    Eq.{u_8 + 1} (α := F) ((∂^{m} f : (a : E) → F) x : F)
      ((iteratedFDeriv ℝ n (⇑f : (a : E) → F) x : (a : (i : Fin n) → E) → F) m : F)
m : Fin (n + 1) → E
x : E
⊢ DifferentiableAt ℝ (F := ContinuousMultilinearMap.{0, 0, u_5, u_8} ℝ (fun (i : Fin n) ↦ E) F)
    (iteratedFDeriv ℝ n (⇑f : (a : E) → F)) x

Tactic:
exact (f.smooth ⊤).differentiable_iteratedFDeriv (mod_cast ENat.coe_lt_top n) x

Premises used: ContDiff.differentiable_iteratedFDeriv, Top.top, SchwartzMap.smooth
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Deriv
Goal:
E : Type u_5
F : Type u_8
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ F
inst_3 : NormedSpace ℝ E
n : ℕ
m : Fin n → E
f : 𝓢(E, F)
x : E
zero :
  ∀ {m : Fin 0 → E} {x : E},
    Eq.{u_8 + 1} (α := F) ((∂^{m} f : (a : E) → F) x : F)
      ((iteratedFDeriv ℝ 0 (⇑f : (a : E) → F) x : (a : (i : Fin 0) → E) → F) m : F)
succ :
  ∀ (n : ℕ)
    (ih :
      ∀ {m : Fin n → E} {x : E},
        Eq.{u_8 + 1} (α := F) ((∂^{m} f : (a : E) → F) x : F)
          ((iteratedFDeriv ℝ n (⇑f : (a : E) → F) x : (a : (i : Fin n) → E) → F) m : F))
    {m : Fin (n + 1) → E} {x : E},
    Eq.{u_8 + 1} (α := F) ((∂^{m} f : (a : E) → F) x : F)
      ((iteratedFDeriv ℝ (n + 1) (⇑f : (a : E) → F) x : (a : (i : Fin (n + 1)) → E) → F) m : F)
⊢ Eq.{u_8 + 1} (α := F) ((∂^{m} f : (a : E) → F) x : F)
    ((iteratedFDeriv ℝ n (⇑f : (a : E) → F) x : (a : (i : Fin n) → E) → F) m : F)

Tactic:
induction n generalizing x with
  | zero => simp
  | succ n ih =>
    rw [iteratedLineDerivOp_succ_left, iteratedFDeriv_succ_apply_left,
      ← fderiv_continuousMultilinear_apply_const_apply]
    · simp only [lineDerivOp_apply_eq_fderiv, ← ih]
    · exact (f.smooth ⊤).differentiable_iteratedFDeriv (mod_cast ENat.coe_lt_top n) x

Premises used: ContDiff.differentiable_iteratedFDeriv, LineDeriv.iteratedLineDerivOp_succ_left, fderiv_continuousMultilinear_apply_const_apply, SchwartzMap.lineDerivOp_apply_eq_fderiv, Top.top, SchwartzMap.smooth, iteratedFDeriv_succ_apply_left
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Deriv
Goal:
𝕜 : Type u_2
D : Type u_4
E : Type u_5
F : Type u_8
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ F
inst_3 : NormedSpace ℝ E
inst_4 : RCLike 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : NormedAddCommGroup D
inst_7 : NormedSpace ℝ D
m : D
g : D ≃L[ℝ] E
f : 𝓢(E, F)
h :
  ∀ (x : D),
    Eq.{u_8 + 1} (α := F)
      ((lineDerivOp (E := 𝓢(D, F)) m ((compCLMOfContinuousLinearEquiv 𝕜 g : (a : 𝓢(E, F)) → 𝓢(D, F)) f : 𝓢(D, F)) :
            (a : D) → F)
          x :
        F)
      ((((compCLMOfContinuousLinearEquiv 𝕜 g : (a : 𝓢(E, F)) → 𝓢(D, F))
                (lineDerivOp (V := E) ((g : (a : D) → E) m : E) f) :
              𝓢(D, F)) :
            (a : D) → F)
          x :
        F)
⊢ lineDerivOp (E := 𝓢(D, F)) m ((compCLMOfContinuousLinearEquiv 𝕜 g : (a : 𝓢(E, F)) → 𝓢(D, F)) f : 𝓢(D, F)) =
    (compCLMOfContinuousLinearEquiv 𝕜 g : (a : 𝓢(E, F)) → 𝓢(D, F)) (lineDerivOp (V := E) ((g : (a : D) → E) m : E) f)

Tactic:
ext x
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Deriv
Goal:
𝕜 : Type u_2
D : Type u_4
E : Type u_5
F : Type u_8
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ F
inst_3 : NormedSpace ℝ E
inst_4 : RCLike 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : NormedAddCommGroup D
inst_7 : NormedSpace ℝ D
m : D
g : D ≃L[ℝ] E
f : 𝓢(E, F)
x : D
⊢ Eq.{u_8 + 1} (α := F)
    ((lineDerivOp (E := 𝓢(D, F)) m ((compCLMOfContinuousLinearEquiv 𝕜 g : (a : 𝓢(E, F)) → 𝓢(D, F)) f : 𝓢(D, F)) :
          (a : D) → F)
        x :
      F)
    ((((compCLMOfContinuousLinearEquiv 𝕜 g : (a : 𝓢(E, F)) → 𝓢(D, F))
              (lineDerivOp (V := E) ((g : (a : D) → E) m : E) f) :
            𝓢(D, F)) :
          (a : D) → F)
        x :
      F)

Tactic:
simp [lineDerivOp_apply_eq_fderiv, ContinuousLinearEquiv.comp_right_fderiv]

Premises used: ContinuousLinearEquiv.comp_right_fderiv, SchwartzMap.lineDerivOp_apply_eq_fderiv
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Deriv
Goal:
𝕜 : Type u_2
F : Type u_8
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : RCLike 𝕜
inst_3 : NormedSpace 𝕜 F
f : 𝓢(ℝ, F)
change :
  Subset (α := Set ℝ) (tsupport.{0, u_8} (α := F) fun (x : ℝ) ↦ deriv (⇑f : (a : ℝ) → F) x)
    (tsupport (α := F) (⇑f : (a : ℝ) → F))
⊢ Subset (α := Set ℝ) (tsupport (α := F) (⇑((derivCLM 𝕜 F : (a : 𝓢(ℝ, F)) → 𝓢(ℝ, F)) f : 𝓢(ℝ, F)) : (a : ℝ) → F))
    (tsupport (α := F) (⇑f : (a : ℝ) → F))

Tactic:
change tsupport (deriv f ·) ⊆ _

Premises used: deriv, tsupport, DFunLike.coe
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Deriv
Goal:
𝕜 : Type u_2
F : Type u_8
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : RCLike 𝕜
inst_3 : NormedSpace 𝕜 F
f : 𝓢(ℝ, F)
simp_rw :
  Subset (α := Set ℝ) (tsupport.{0, u_8} (α := F) fun (x : ℝ) ↦ (fderiv ℝ (⇑f : (a : ℝ) → F) x : (a : ℝ) → F) 1)
    (tsupport (α := F) (⇑f : (a : ℝ) → F))
⊢ Subset (α := Set ℝ) (tsupport.{0, u_8} (α := F) fun (x : ℝ) ↦ deriv (⇑f : (a : ℝ) → F) x)
    (tsupport (α := F) (⇑f : (a : ℝ) → F))

Tactic:
simp_rw [← fderiv_apply_one_eq_deriv]

Premises used: fderiv_apply_one_eq_deriv
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Deriv
Goal:
𝕜 : Type u_2
F : Type u_8
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : RCLike 𝕜
inst_3 : NormedSpace 𝕜 F
f : 𝓢(ℝ, F)
⊢ Subset (α := Set ℝ) (tsupport.{0, u_8} (α := F) fun (x : ℝ) ↦ (fderiv ℝ (⇑f : (a : ℝ) → F) x : (a : ℝ) → F) 1)
    (tsupport (α := F) (⇑f : (a : ℝ) → F))

Tactic:
tsupport_fderiv_apply_subset ℝ 1

Premises used: Real, tsupport_fderiv_apply_subset, OfNat.ofNat
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Deriv
Goal:
𝕜 : Type u_2
F : Type u_8
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : RCLike 𝕜
inst_3 : NormedSpace 𝕜 F
f : 𝓢(ℝ, F)
⊢ Subset (α := Set ℝ) (tsupport.{0, u_8} (α := F) fun (x : ℝ) ↦ (fderiv ℝ (⇑f : (a : ℝ) → F) x : (a : ℝ) → F) 1)
    (tsupport (α := F) (⇑f : (a : ℝ) → F))

Tactic:
exact tsupport_fderiv_apply_subset ℝ 1

Premises used: Real, tsupport_fderiv_apply_subset, OfNat.ofNat
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Deriv
Goal:
𝕜 : Type u_2
E : Type u_5
F : Type u_8
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ F
inst_3 : RCLike 𝕜
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedSpace ℝ E
inst_6 : SMulCommClass ℝ 𝕜 F
f : 𝓢(E, F)
⊢ Subset.{u_5} (α := Set E)
    (tsupport (α := E →L[ℝ] F)
      (⇑((fderivCLM 𝕜 E F : (a : 𝓢(E, F)) → 𝓢(E, E →L[ℝ] F)) f : 𝓢(E, E →L[ℝ] F)) : (a : E) → E →L[ℝ] F))
    (tsupport.{u_5, u_8} (α := F) (⇑f : (a : E) → F))

Tactic:
tsupport_fderiv_subset ℝ

Premises used: Real, tsupport_fderiv_subset
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Deriv
Goal:
E : Type u_5
F : Type u_8
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ F
inst_3 : NormedSpace ℝ E
m : E
f : 𝓢(E, F)
⊢ Subset.{u_5} (α := Set E) (tsupport.{u_5, u_8} (α := F) (⇑(∂_{m} f) : (a : E) → F))
    (tsupport.{u_5, u_8} (α := F) (⇑f : (a : E) → F))

Tactic:
tsupport_fderiv_apply_subset ℝ m

Premises used: Real, tsupport_fderiv_apply_subset
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Deriv
Goal:
E : Type u_5
F : Type u_8
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ F
inst_3 : NormedSpace ℝ E
f : 𝓢(E, F)
m : Fin 0 → E
⊢ Subset.{u_5} (α := Set E) (tsupport.{u_5, u_8} (α := F) (⇑(∂^{m} f) : (a : E) → F))
    (tsupport.{u_5, u_8} (α := F) (⇑f : (a : E) → F))

Tactic:
simp
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Deriv
Goal:
E : Type u_5
F : Type u_8
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ F
inst_3 : NormedSpace ℝ E
f : 𝓢(E, F)
n : ℕ
IH :
  ∀ (m : Fin n → E),
    Subset.{u_5} (α := Set E) (tsupport.{u_5, u_8} (α := F) (⇑(∂^{m} f) : (a : E) → F))
      (tsupport.{u_5, u_8} (α := F) (⇑f : (a : E) → F))
m : Fin (n + 1) → E
succ :
  Subset.{u_5} (α := Set E)
    (tsupport.{u_5, u_8} (α := F) (⇑(∂_{m 0} (∂^{Fin.tail (α := fun (i : Fin (n + 1)) ↦ E) m} f)) : (a : E) → F))
    (tsupport.{u_5, u_8} (α := F) (⇑f : (a : E) → F))
⊢ Subset.{u_5} (α := Set E) (tsupport.{u_5, u_8} (α := F) (⇑(∂^{m} f) : (a : E) → F))
    (tsupport.{u_5, u_8} (α := F) (⇑f : (a : E) → F))

Tactic:
rw [iteratedLineDerivOp_succ_left]

Premises used: LineDeriv.iteratedLineDerivOp_succ_left
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Deriv
Goal:
E : Type u_5
F : Type u_8
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ F
inst_3 : NormedSpace ℝ E
f : 𝓢(E, F)
n : ℕ
IH :
  ∀ (m : Fin n → E),
    Subset.{u_5} (α := Set E) (tsupport.{u_5, u_8} (α := F) (⇑(∂^{m} f) : (a : E) → F))
      (tsupport.{u_5, u_8} (α := F) (⇑f : (a : E) → F))
m : Fin (n + 1) → E
⊢ Subset.{u_5} (α := Set E)
    (tsupport.{u_5, u_8} (α := F) (⇑(∂_{m 0} (∂^{Fin.tail (α := fun (i : Fin (n + 1)) ↦ E) m} f)) : (a : E) → F))
    (tsupport.{u_5, u_8} (α := F) (⇑f : (a : E) → F))

Tactic:
(tsupport_lineDerivOp_subset (m 0) _).trans (IH <| Fin.tail m)

Premises used: HasSubset.Subset.trans, SchwartzMap.tsupport_lineDerivOp_subset, OfNat.ofNat, Fin.tail
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Deriv
Goal:
E : Type u_5
F : Type u_8
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ F
inst_3 : NormedSpace ℝ E
f : 𝓢(E, F)
n : ℕ
IH :
  ∀ (m : Fin n → E),
    Subset.{u_5} (α := Set E) (tsupport.{u_5, u_8} (α := F) (⇑(∂^{m} f) : (a : E) → F))
      (tsupport.{u_5, u_8} (α := F) (⇑f : (a : E) → F))
m : Fin (n + 1) → E
⊢ Subset.{u_5} (α := Set E)
    (tsupport.{u_5, u_8} (α := F) (⇑(∂_{m 0} (∂^{Fin.tail (α := fun (i : Fin (n + 1)) ↦ E) m} f)) : (a : E) → F))
    (tsupport.{u_5, u_8} (α := F) (⇑f : (a : E) → F))

Tactic:
exact (tsupport_lineDerivOp_subset (m 0) _).trans (IH <| Fin.tail m)

Premises used: HasSubset.Subset.trans, SchwartzMap.tsupport_lineDerivOp_subset, OfNat.ofNat, Fin.tail
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Deriv
Goal:
E : Type u_5
F : Type u_8
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ F
inst_3 : NormedSpace ℝ E
n : ℕ
m : Fin n → E
f : 𝓢(E, F)
zero :
  ∀ (m : Fin 0 → E),
    Subset.{u_5} (α := Set E) (tsupport.{u_5, u_8} (α := F) (⇑(∂^{m} f) : (a : E) → F))
      (tsupport.{u_5, u_8} (α := F) (⇑f : (a : E) → F))
succ :
  ∀ (n : ℕ)
    (IH :
      ∀ (m : Fin n → E),
        Subset.{u_5} (α := Set E) (tsupport.{u_5, u_8} (α := F) (⇑(∂^{m} f) : (a : E) → F))
          (tsupport.{u_5, u_8} (α := F) (⇑f : (a : E) → F)))
    (m : Fin (n + 1) → E),
    Subset.{u_5} (α := Set E) (tsupport.{u_5, u_8} (α := F) (⇑(∂^{m} f) : (a : E) → F))
      (tsupport.{u_5, u_8} (α := F) (⇑f : (a : E) → F))
⊢ Subset.{u_5} (α := Set E) (tsupport.{u_5, u_8} (α := F) (⇑(∂^{m} f) : (a : E) → F))
    (tsupport.{u_5, u_8} (α := F) (⇑f : (a : E) → F))

Tactic:
induction n with
  | zero => simp
  | succ n IH =>
    rw [iteratedLineDerivOp_succ_left]
    exact (tsupport_lineDerivOp_subset (m 0) _).trans (IH <| Fin.tail m)

Premises used: LineDeriv.iteratedLineDerivOp_succ_left
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Deriv
Goal:
E : Type u_5
F : Type u_8
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ F
inst_3 : InnerProductSpace ℝ E
inst_4 : FiniteDimensional ℝ E
f : 𝓢(E, F)
⊢ (laplacianCLM ℝ E 𝓢(E, F) : (a : 𝓢(E, F)) → 𝓢(E, F)) f = Δ f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Deriv
Goal:
ι : Type u_1
E : Type u_5
F : Type u_8
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ F
inst_3 : InnerProductSpace ℝ E
inst_4 : FiniteDimensional ℝ E
inst_5 : Fintype ι
b : OrthonormalBasis ι ℝ E
f : 𝓢(E, F)
⊢ Δ f = ∑ i : ι, lineDerivOp (V := E) ((b : (a : ι) → E) i : E) (lineDerivOp (V := E) ((b : (a : ι) → E) i : E) f)

Tactic:
LineDeriv.laplacianCLM_eq_sum b f

Premises used: LineDeriv.laplacianCLM_eq_sum
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Deriv
Goal:
𝕜 : Type u_2
E : Type u_5
F : Type u_8
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ F
inst_3 : InnerProductSpace ℝ E
inst_4 : FiniteDimensional ℝ E
inst_5 : RCLike 𝕜
inst_6 : NormedSpace 𝕜 F
f : 𝓢(E, F)
⊢ (laplacianCLM 𝕜 E 𝓢(E, F) : (a : 𝓢(E, F)) → 𝓢(E, F)) f = Δ f

Tactic:
simp [laplacianCLM, laplacian_eq_sum (stdOrthonormalBasis ℝ E)]

Premises used: Real, LineDeriv.laplacianCLM, SchwartzMap.laplacian_eq_sum, stdOrthonormalBasis
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Deriv
Goal:
E : Type u_5
F : Type u_8
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ F
inst_3 : InnerProductSpace ℝ E
inst_4 : FiniteDimensional ℝ E
f : 𝓢(E, F)
x : E
rw :
  (∑ i : Fin (Module.finrank ℝ E),
          lineDerivOp (V := E) ((stdOrthonormalBasis ℝ E : (a : Fin (Module.finrank ℝ E)) → E) i : E)
            (lineDerivOp (V := E) ((stdOrthonormalBasis ℝ E : (a : Fin (Module.finrank ℝ E)) → E) i : E) f) :
        (a : E) → F)
      x =
    Δ (E := (a : E) → F) (⇑f : (a : E) → F) x
⊢ (Δ f : (a : E) → F) x = Δ (E := (a : E) → F) (⇑f : (a : E) → F) x

Tactic:
rw [laplacian_eq_sum (stdOrthonormalBasis ℝ E)]

Premises used: Real, SchwartzMap.laplacian_eq_sum, stdOrthonormalBasis
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Deriv
Goal:
E : Type u_5
F : Type u_8
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ F
inst_3 : InnerProductSpace ℝ E
inst_4 : FiniteDimensional ℝ E
f : 𝓢(E, F)
x : E
⊢ (∑ i : Fin (Module.finrank ℝ E),
          lineDerivOp (V := E) ((stdOrthonormalBasis ℝ E : (a : Fin (Module.finrank ℝ E)) → E) i : E)
            (lineDerivOp (V := E) ((stdOrthonormalBasis ℝ E : (a : Fin (Module.finrank ℝ E)) → E) i : E) f) :
        (a : E) → F)
      x =
    Δ (E := (a : E) → F) (⇑f : (a : E) → F) x

Tactic:
simp [InnerProductSpace.laplacian_eq_iteratedFDeriv_orthonormalBasis f (stdOrthonormalBasis ℝ E),
    sum_apply, ← iteratedLineDerivOp_eq_iteratedFDeriv, iteratedLineDerivOp_succ_left]

Premises used: Real, LineDeriv.iteratedLineDerivOp_succ_left, SchwartzMap.iteratedLineDerivOp_eq_iteratedFDeriv, SchwartzMap.sum_apply, InnerProductSpace.laplacian_eq_iteratedFDeriv_orthonormalBasis, DFunLike.coe, stdOrthonormalBasis
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Deriv
Goal:
E : Type u_5
V : Type u_7
F : Type u_8
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ F
inst_3 : NormedSpace ℝ E
inst_4 : NormedAddCommGroup V
inst_5 : NormedSpace ℝ V
f : 𝓢(ℝ, E)
g : 𝓢(ℝ, F)
L : E →L[ℝ] F →L[ℝ] V
⊢ Eq.{u_7 + 1} (α := V)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦
      (((L : (a : E) → F →L[ℝ] V) ((f : (a : ℝ) → E) x) : F →L[ℝ] V) : (a : F) → V) (deriv (⇑g : (a : ℝ) → F) x))
    (-@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦
        (((L : (a : E) → F →L[ℝ] V) (deriv (⇑f : (a : ℝ) → E) x) : F →L[ℝ] V) : (a : F) → V) ((g : (a : ℝ) → F) x : F))

Tactic:
MeasureTheory.integral_bilinear_hasDerivAt_right_eq_neg_left_of_integrable
    (fun x _ ↦ f.hasDerivAt x) (fun x _ ↦ g.hasDerivAt x) (pairing L f (derivCLM ℝ F g)).integrable
    (pairing L (derivCLM ℝ E f) g).integrable (pairing L f g).integrable

Premises used: Real, SchwartzMap.hasDerivAt, SchwartzMap.pairing, SchwartzMap.integrable, DFunLike.coe, SchwartzMap.derivCLM, MeasureTheory.integral_bilinear_hasDerivAt_right_eq_neg_left_of_integrable
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Deriv
Goal:
𝕜 : Type u_2
inst : NormedRing 𝕜
inst_1 : NormedSpace ℝ 𝕜
inst_2 : IsScalarTower ℝ 𝕜 𝕜
inst_3 : SMulCommClass ℝ 𝕜 𝕜
f g : 𝓢(ℝ, 𝕜)
⊢ Eq.{u_2 + 1} (α := 𝕜)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦
      HMul.hMul (α := 𝕜) (β := 𝕜) ((f : (a : ℝ) → 𝕜) x : 𝕜) (deriv (⇑g : (a : ℝ) → 𝕜) x : 𝕜))
    (-@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦
        HMul.hMul (α := 𝕜) (β := 𝕜) (deriv (⇑f : (a : ℝ) → 𝕜) x : 𝕜) ((g : (a : ℝ) → 𝕜) x : 𝕜))

Tactic:
integral_bilinear_deriv_right_eq_neg_left f g (ContinuousLinearMap.mul ℝ 𝕜)

Premises used: Real, SchwartzMap.integral_bilinear_deriv_right_eq_neg_left, ContinuousLinearMap.mul
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Deriv
Goal:
𝕜 : Type u_2
F : Type u_8
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : RCLike 𝕜
inst_3 : NormedSpace 𝕜 F
f : 𝓢(ℝ, 𝕜)
g : 𝓢(ℝ, F)
⊢ Eq.{u_8 + 1} (α := F)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦
      HSMul.hSMul (α := 𝕜) (β := F) ((f : (a : ℝ) → 𝕜) x : 𝕜) (deriv (⇑g : (a : ℝ) → F) x))
    (-@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦
        HSMul.hSMul (α := 𝕜) (β := F) (deriv (⇑f : (a : ℝ) → 𝕜) x) ((g : (a : ℝ) → F) x : F))

Tactic:
integral_bilinear_deriv_right_eq_neg_left f g (ContinuousLinearMap.lsmul ℝ 𝕜)

Premises used: Real, SchwartzMap.integral_bilinear_deriv_right_eq_neg_left, ContinuousLinearMap.lsmul
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Deriv
Goal:
𝕜 : Type u_2
V : Type u_7
F : Type u_8
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : NormedAddCommGroup V
inst_3 : NormedSpace ℝ V
inst_4 : RCLike 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : NormedSpace 𝕜 V
f : 𝓢(ℝ, F →L[𝕜] V)
g : 𝓢(ℝ, F)
⊢ Eq.{u_7 + 1} (α := V)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦
      (((f : (a : ℝ) → F →L[𝕜] V) x : F →L[𝕜] V) : (a : F) → V) (deriv (⇑g : (a : ℝ) → F) x))
    (-@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦
        (deriv (⇑f : (a : ℝ) → F →L[𝕜] V) x : (a : F) → V) ((g : (a : ℝ) → F) x : F))

Tactic:
integral_bilinear_deriv_right_eq_neg_left f g
    ((ContinuousLinearMap.id 𝕜 (F →L[𝕜] V)).bilinearRestrictScalars ℝ)

Premises used: Real, SchwartzMap.integral_bilinear_deriv_right_eq_neg_left, ContinuousLinearMap.id, ContinuousLinearMap, ContinuousLinearMap.bilinearRestrictScalars, RingHom.id