awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Distribution.TestFunction
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
Ω : Opens E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : NormedSpace 𝕜 F
n k : ℕ∞
inst_6 : Algebra ℝ 𝕜
inst_7 : IsScalarTower ℝ 𝕜 F
K : Compacts E
K_sub_Ω : (↑K : Set E) ⊆ (↑Ω : Set E)
f : 𝓓^{n}_{K}(E, F)
h :
  ∀ (a x : E),
    Eq.{u_4 + 1} (α := F)
      ((((((fderivCLM 𝕜 n k : 𝓓^{n}(Ω, F) →L[𝕜] 𝓓^{k}(Ω, E →L[ℝ] F)) : (a : 𝓓^{n}(Ω, F)) → 𝓓^{k}(Ω, E →L[ℝ] F))
                    (ofSupportedIn K_sub_Ω f) :
                  𝓓^{k}(Ω, E →L[ℝ] F)) :
                (a : E) → E →L[ℝ] F)
              a :
            (a : E) → F)
          x :
        F)
      (((ofSupportedIn K_sub_Ω
                  ((ContDiffMapSupportedIn.fderivCLM 𝕜 n k : (a : 𝓓^{n}_{K}(E, F)) → 𝓓^{k}_{K}(E, E →L[ℝ] F)) f) :
                (a : E) → E →L[ℝ] F)
              a :
            (a : E) → F)
          x :
        F)
⊢ Eq (α := 𝓓^{k}(Ω, E →L[ℝ] F))
    (((fderivCLM 𝕜 n k : 𝓓^{n}(Ω, F) →L[𝕜] 𝓓^{k}(Ω, E →L[ℝ] F)) : (a : 𝓓^{n}(Ω, F)) → 𝓓^{k}(Ω, E →L[ℝ] F))
        (ofSupportedIn K_sub_Ω f) :
      𝓓^{k}(Ω, E →L[ℝ] F))
    (ofSupportedIn K_sub_Ω
        ((ContDiffMapSupportedIn.fderivCLM 𝕜 n k : (a : 𝓓^{n}_{K}(E, F)) → 𝓓^{k}_{K}(E, E →L[ℝ] F)) f) :
      𝓓^{k}(Ω, E →L[ℝ] F))

Tactic:
ext
-- Module: Mathlib.Analysis.Distribution.TestFunction
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
Ω : Opens E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : NormedSpace 𝕜 F
n k : ℕ∞
inst_6 : Algebra ℝ 𝕜
inst_7 : IsScalarTower ℝ 𝕜 F
K : Compacts E
K_sub_Ω : (↑K : Set E) ⊆ (↑Ω : Set E)
f : 𝓓^{n}_{K}(E, F)
a x : E
⊢ Eq.{u_4 + 1} (α := F)
    ((((((fderivCLM 𝕜 n k : 𝓓^{n}(Ω, F) →L[𝕜] 𝓓^{k}(Ω, E →L[ℝ] F)) : (a : 𝓓^{n}(Ω, F)) → 𝓓^{k}(Ω, E →L[ℝ] F))
                  (ofSupportedIn K_sub_Ω f) :
                𝓓^{k}(Ω, E →L[ℝ] F)) :
              (a : E) → E →L[ℝ] F)
            a :
          (a : E) → F)
        x :
      F)
    (((ofSupportedIn K_sub_Ω
                ((ContDiffMapSupportedIn.fderivCLM 𝕜 n k : (a : 𝓓^{n}_{K}(E, F)) → 𝓓^{k}_{K}(E, E →L[ℝ] F)) f) :
              (a : E) → E →L[ℝ] F)
            a :
          (a : E) → F)
        x :
      F)

Tactic:
simp
-- Module: Mathlib.Analysis.Distribution.TestFunction
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
Ω : Opens E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : NormedSpace 𝕜 F
n k : ℕ∞
inst_6 : Algebra ℝ 𝕜
inst_7 : IsScalarTower ℝ 𝕜 F
𝕜' : Type u_6
inst_8 : NontriviallyNormedField 𝕜'
inst_9 : NormedSpace 𝕜' F
inst_10 : Algebra ℝ 𝕜'
inst_11 : IsScalarTower ℝ 𝕜' F
⊢ Eq (α := (a : 𝓓^{n}(Ω, F)) → 𝓓^{k}(Ω, E →L[ℝ] F))
    (⇑(fderivCLM 𝕜 n k : 𝓓^{n}(Ω, F) →L[𝕜] 𝓓^{k}(Ω, E →L[ℝ] F)) : (a : 𝓓^{n}(Ω, F)) → 𝓓^{k}(Ω, E →L[ℝ] F))
    (⇑(fderivCLM 𝕜' n k : 𝓓^{n}(Ω, F) →L[𝕜'] 𝓓^{k}(Ω, E →L[ℝ] F)) : (a : 𝓓^{n}(Ω, F)) → 𝓓^{k}(Ω, E →L[ℝ] F))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Distribution.TestFunction
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
Ω : Opens E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : NormedSpace 𝕜 F
n k : ℕ∞
inst_6 : Algebra ℝ 𝕜
inst_7 : IsScalarTower ℝ 𝕜 F
f : 𝓓^{n}(Ω, F)
v x : E
⊢ ((((lineDerivCLM 𝕜 v : 𝓓^{n}(Ω, F) →L[𝕜] 𝓓^{k}(Ω, F)) : (a : 𝓓^{n}(Ω, F)) → 𝓓^{k}(Ω, F)) f : 𝓓^{k}(Ω, F)) :
        (a : E) → F)
      x =
    (((((fderivCLM 𝕜 n k : 𝓓^{n}(Ω, F) →L[𝕜] 𝓓^{k}(Ω, E →L[ℝ] F)) : (a : 𝓓^{n}(Ω, F)) → 𝓓^{k}(Ω, E →L[ℝ] F)) f :
              𝓓^{k}(Ω, E →L[ℝ] F)) :
            (a : E) → E →L[ℝ] F)
          x :
        (a : E) → F)
      v

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Distribution.TestFunction
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
Ω : Opens E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : NormedSpace 𝕜 F
n k : ℕ∞
inst_6 : Algebra ℝ 𝕜
inst_7 : IsScalarTower ℝ 𝕜 F
f : 𝓓^{n}(Ω, F)
v x : E
rw :
  (((if k + 1 ≤ n then fderiv ℝ (⇑f : (a : E) → F) else 0) x : E →L[ℝ] F) : (a : E) → F) v =
    if k + 1 ≤ n then lineDeriv ℝ (⇑f : (a : E) → F) x v else 0
⊢ ((((lineDerivCLM 𝕜 v : 𝓓^{n}(Ω, F) →L[𝕜] 𝓓^{k}(Ω, F)) : (a : 𝓓^{n}(Ω, F)) → 𝓓^{k}(Ω, F)) f : 𝓓^{k}(Ω, F)) :
        (a : E) → F)
      x =
    if k + 1 ≤ n then lineDeriv ℝ (⇑f : (a : E) → F) x v else 0

Tactic:
rw [lineDerivCLM_eq_fderivCLM, fderivCLM_apply]

Premises used: TestFunction.lineDerivCLM_eq_fderivCLM, TestFunction.fderivCLM_apply
-- Module: Mathlib.Analysis.Distribution.TestFunction
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
Ω : Opens E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : NormedSpace 𝕜 F
n k : ℕ∞
inst_6 : Algebra ℝ 𝕜
inst_7 : IsScalarTower ℝ 𝕜 F
f : 𝓓^{n}(Ω, F)
v x : E
pos : ∀ (hk : k + 1 ≤ n), (fderiv ℝ (⇑f : (a : E) → F) x : (a : E) → F) v = lineDeriv ℝ (⇑f : (a : E) → F) x v
neg : ∀ (hk : ¬k + 1 ≤ n), Eq.{u_4 + 1} (α := F) ((0 x : (a : E) → F) v : F) (0 : F)
⊢ (((if k + 1 ≤ n then fderiv ℝ (⇑f : (a : E) → F) else 0) x : E →L[ℝ] F) : (a : E) → F) v =
    if k + 1 ≤ n then lineDeriv ℝ (⇑f : (a : E) → F) x v else 0

Tactic:
split_ifs with hk
-- Module: Mathlib.Analysis.Distribution.TestFunction
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
Ω : Opens E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : NormedSpace 𝕜 F
n k : ℕ∞
inst_6 : Algebra ℝ 𝕜
inst_7 : IsScalarTower ℝ 𝕜 F
f : 𝓓^{n}(Ω, F)
v x : E
hk : k + 1 ≤ n
⊢ 0 < (↑n : ℕ∞ω)

Tactic:
have hk' : 0 < (n : ℕ∞ω) := mod_cast (ENat.add_one_pos.trans_le hk)
-- Module: Mathlib.Analysis.Distribution.TestFunction
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
Ω : Opens E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : NormedSpace 𝕜 F
n k : ℕ∞
inst_6 : Algebra ℝ 𝕜
inst_7 : IsScalarTower ℝ 𝕜 F
f : 𝓓^{n}(Ω, F)
v x : E
hk : k + 1 ≤ n
hk' : 0 < (↑n : ℕ∞ω)
pos pos₁ :
  Eq.{u_4 + 1} (α := F) ((fderiv ℝ (⇑f : (a : E) → F) x : (a : E) → F) v : F)
    ((fderiv ℝ (⇑f : (a : E) → F) x : (a : E) → F) v : F)
⊢ (fderiv ℝ (⇑f : (a : E) → F) x : (a : E) → F) v = lineDeriv ℝ (⇑f : (a : E) → F) x v

Tactic:
rw [(f.contDiff.differentiable hk'.ne').differentiableAt.lineDeriv_eq_fderiv]

Premises used: Differentiable.differentiableAt, TestFunction.contDiff, LT.lt.ne', ContDiff.differentiable, DifferentiableAt.lineDeriv_eq_fderiv
-- Module: Mathlib.Analysis.Distribution.TestFunction
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
Ω : Opens E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : NormedSpace 𝕜 F
n k : ℕ∞
inst_6 : Algebra ℝ 𝕜
inst_7 : IsScalarTower ℝ 𝕜 F
f : 𝓓^{n}(Ω, F)
v x : E
hk : ¬k + 1 ≤ n
⊢ Eq.{u_4 + 1} (α := F) ((0 x : (a : E) → F) v : F) (0 : F)

Tactic:
rfl
-- Module: Mathlib.Analysis.Distribution.TestFunction
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
Ω : Opens E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : NormedSpace 𝕜 F
n k : ℕ∞
inst_6 : Algebra ℝ 𝕜
inst_7 : IsScalarTower ℝ 𝕜 F
f : 𝓓^{n}(Ω, F)
v x : E
hk : k + 1 ≤ n
⊢ ((((lineDerivCLM 𝕜 v : 𝓓^{n}(Ω, F) →L[𝕜] 𝓓^{k}(Ω, F)) : (a : 𝓓^{n}(Ω, F)) → 𝓓^{k}(Ω, F)) f : 𝓓^{k}(Ω, F)) :
        (a : E) → F)
      x =
    lineDeriv ℝ (⇑f : (a : E) → F) x v

Tactic:
simp [hk]
-- Module: Mathlib.Analysis.Distribution.TestFunction
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
Ω : Opens E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : NormedSpace 𝕜 F
n k : ℕ∞
inst_6 : Algebra ℝ 𝕜
inst_7 : IsScalarTower ℝ 𝕜 F
v : E
hk : n < k + 1
h :
  ∀ (x : 𝓓^{n}(Ω, F)) (a : E),
    ((((lineDerivCLM 𝕜 v : 𝓓^{n}(Ω, F) →L[𝕜] 𝓓^{k}(Ω, F)) : (a : 𝓓^{n}(Ω, F)) → 𝓓^{k}(Ω, F)) x : 𝓓^{k}(Ω, F)) :
          (a : E) → F)
        a =
      (((0 : (a : 𝓓^{n}(Ω, F)) → 𝓓^{k}(Ω, F)) x : 𝓓^{k}(Ω, F)) : (a : E) → F) a
⊢ Eq (α := 𝓓^{n}(Ω, F) →L[𝕜] 𝓓^{k}(Ω, F)) (lineDerivCLM 𝕜 v : 𝓓^{n}(Ω, F) →L[𝕜] 𝓓^{k}(Ω, F))
    (0 : 𝓓^{n}(Ω, F) →L[𝕜] 𝓓^{k}(Ω, F))

Tactic:
ext
-- Module: Mathlib.Analysis.Distribution.TestFunction
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
Ω : Opens E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : NormedSpace 𝕜 F
n k : ℕ∞
inst_6 : Algebra ℝ 𝕜
inst_7 : IsScalarTower ℝ 𝕜 F
v : E
hk : n < k + 1
x : 𝓓^{n}(Ω, F)
a : E
⊢ ((((lineDerivCLM 𝕜 v : 𝓓^{n}(Ω, F) →L[𝕜] 𝓓^{k}(Ω, F)) : (a : 𝓓^{n}(Ω, F)) → 𝓓^{k}(Ω, F)) x : 𝓓^{k}(Ω, F)) :
        (a : E) → F)
      a =
    (((0 : (a : 𝓓^{n}(Ω, F)) → 𝓓^{k}(Ω, F)) x : 𝓓^{k}(Ω, F)) : (a : E) → F) a

Tactic:
simp [not_le_of_gt hk]

Premises used: not_le_of_gt
-- Module: Mathlib.Analysis.Distribution.TestFunction
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
Ω : Opens E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : NormedSpace 𝕜 F
n k : ℕ∞
inst_6 : Algebra ℝ 𝕜
inst_7 : IsScalarTower ℝ 𝕜 F
𝕜' : Type u_6
inst_8 : NontriviallyNormedField 𝕜'
inst_9 : NormedSpace 𝕜' F
inst_10 : Algebra ℝ 𝕜'
inst_11 : IsScalarTower ℝ 𝕜' F
v : E
⊢ Eq (α := (a : 𝓓^{n}(Ω, F)) → 𝓓^{k}(Ω, F))
    (⇑(lineDerivCLM 𝕜 v : 𝓓^{n}(Ω, F) →L[𝕜] 𝓓^{k}(Ω, F)) : (a : 𝓓^{n}(Ω, F)) → 𝓓^{k}(Ω, F))
    (⇑(lineDerivCLM 𝕜' v : 𝓓^{n}(Ω, F) →L[𝕜'] 𝓓^{k}(Ω, F)) : (a : 𝓓^{n}(Ω, F)) → 𝓓^{k}(Ω, F))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Distribution.TestFunction
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
Ω : Opens E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : NormedSpace 𝕜 F
n k : ℕ∞
inst_6 : Algebra ℝ 𝕜
inst_7 : IsScalarTower ℝ 𝕜 F
v₁ v₂ : E
h :
  ∀ (x : 𝓓^{n}(Ω, F)) (a : E),
    ((((lineDerivCLM 𝕜 (v₁ + v₂) : 𝓓^{n}(Ω, F) →L[𝕜] 𝓓^{k}(Ω, F)) : (a : 𝓓^{n}(Ω, F)) → 𝓓^{k}(Ω, F)) x : 𝓓^{k}(Ω, F)) :
          (a : E) → F)
        a =
      (((HAdd.hAdd (α := 𝓓^{n}(Ω, F) →L[𝕜] 𝓓^{k}(Ω, F)) (β := 𝓓^{n}(Ω, F) →L[𝕜] 𝓓^{k}(Ω, F))
                  (lineDerivCLM 𝕜 v₁ : 𝓓^{n}(Ω, F) →L[𝕜] 𝓓^{k}(Ω, F))
                  (lineDerivCLM 𝕜 v₂ : 𝓓^{n}(Ω, F) →L[𝕜] 𝓓^{k}(Ω, F)) :
                (a : 𝓓^{n}(Ω, F)) → 𝓓^{k}(Ω, F))
              x :
            𝓓^{k}(Ω, F)) :
          (a : E) → F)
        a
⊢ lineDerivCLM 𝕜 (v₁ + v₂) =
    HAdd.hAdd (α := 𝓓^{n}(Ω, F) →L[𝕜] 𝓓^{k}(Ω, F)) (β := 𝓓^{n}(Ω, F) →L[𝕜] 𝓓^{k}(Ω, F))
      (lineDerivCLM 𝕜 v₁ : 𝓓^{n}(Ω, F) →L[𝕜] 𝓓^{k}(Ω, F)) (lineDerivCLM 𝕜 v₂ : 𝓓^{n}(Ω, F) →L[𝕜] 𝓓^{k}(Ω, F))

Tactic:
ext
-- Module: Mathlib.Analysis.Distribution.TestFunction
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
Ω : Opens E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : NormedSpace 𝕜 F
n k : ℕ∞
inst_6 : Algebra ℝ 𝕜
inst_7 : IsScalarTower ℝ 𝕜 F
v₁ v₂ : E
x : 𝓓^{n}(Ω, F)
a : E
⊢ ((((lineDerivCLM 𝕜 (v₁ + v₂) : 𝓓^{n}(Ω, F) →L[𝕜] 𝓓^{k}(Ω, F)) : (a : 𝓓^{n}(Ω, F)) → 𝓓^{k}(Ω, F)) x : 𝓓^{k}(Ω, F)) :
        (a : E) → F)
      a =
    (((HAdd.hAdd (α := 𝓓^{n}(Ω, F) →L[𝕜] 𝓓^{k}(Ω, F)) (β := 𝓓^{n}(Ω, F) →L[𝕜] 𝓓^{k}(Ω, F))
                (lineDerivCLM 𝕜 v₁ : 𝓓^{n}(Ω, F) →L[𝕜] 𝓓^{k}(Ω, F))
                (lineDerivCLM 𝕜 v₂ : 𝓓^{n}(Ω, F) →L[𝕜] 𝓓^{k}(Ω, F)) :
              (a : 𝓓^{n}(Ω, F)) → 𝓓^{k}(Ω, F))
            x :
          𝓓^{k}(Ω, F)) :
        (a : E) → F)
      a

Tactic:
simp [-lineDerivCLM_apply, lineDerivCLM_eq_fderivCLM]

Premises used: TestFunction.lineDerivCLM_eq_fderivCLM, TestFunction.lineDerivCLM_apply
-- Module: Mathlib.Analysis.Distribution.TestFunction
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
Ω : Opens E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : NormedSpace 𝕜 F
n k : ℕ∞
inst_6 : Algebra ℝ 𝕜
inst_7 : IsScalarTower ℝ 𝕜 F
c : ℝ
v : E
h :
  ∀ (x : 𝓓^{n}(Ω, F)) (a : E),
    ((((lineDerivCLM 𝕜 (c • v) : 𝓓^{n}(Ω, F) →L[𝕜] 𝓓^{k}(Ω, F)) : (a : 𝓓^{n}(Ω, F)) → 𝓓^{k}(Ω, F)) x : 𝓓^{k}(Ω, F)) :
          (a : E) → F)
        a =
      (((HSMul.hSMul (β := 𝓓^{n}(Ω, F) →L[𝕜] 𝓓^{k}(Ω, F)) c (lineDerivCLM 𝕜 v : 𝓓^{n}(Ω, F) →L[𝕜] 𝓓^{k}(Ω, F)) :
                (a : 𝓓^{n}(Ω, F)) → 𝓓^{k}(Ω, F))
              x :
            𝓓^{k}(Ω, F)) :
          (a : E) → F)
        a
⊢ lineDerivCLM 𝕜 (c • v) =
    HSMul.hSMul (β := 𝓓^{n}(Ω, F) →L[𝕜] 𝓓^{k}(Ω, F)) c (lineDerivCLM 𝕜 v : 𝓓^{n}(Ω, F) →L[𝕜] 𝓓^{k}(Ω, F))

Tactic:
ext
-- Module: Mathlib.Analysis.Distribution.TestFunction
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
Ω : Opens E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : NormedSpace 𝕜 F
n k : ℕ∞
inst_6 : Algebra ℝ 𝕜
inst_7 : IsScalarTower ℝ 𝕜 F
c : ℝ
v : E
x : 𝓓^{n}(Ω, F)
a : E
⊢ ((((lineDerivCLM 𝕜 (c • v) : 𝓓^{n}(Ω, F) →L[𝕜] 𝓓^{k}(Ω, F)) : (a : 𝓓^{n}(Ω, F)) → 𝓓^{k}(Ω, F)) x : 𝓓^{k}(Ω, F)) :
        (a : E) → F)
      a =
    (((HSMul.hSMul (β := 𝓓^{n}(Ω, F) →L[𝕜] 𝓓^{k}(Ω, F)) c (lineDerivCLM 𝕜 v : 𝓓^{n}(Ω, F) →L[𝕜] 𝓓^{k}(Ω, F)) :
              (a : 𝓓^{n}(Ω, F)) → 𝓓^{k}(Ω, F))
            x :
          𝓓^{k}(Ω, F)) :
        (a : E) → F)
      a

Tactic:
simp [-lineDerivCLM_apply, lineDerivCLM_eq_fderivCLM]

Premises used: TestFunction.lineDerivCLM_eq_fderivCLM, TestFunction.lineDerivCLM_apply
-- Module: Mathlib.Analysis.Distribution.TestFunction
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
Ω : Opens E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : NormedSpace 𝕜 F
inst_6 : Algebra ℝ 𝕜
inst_7 : IsScalarTower ℝ 𝕜 F
v : E
f : 𝓓(Ω, F)
⊢ ∂_{v} f = ((lineDerivCLM 𝕜 v : 𝓓(Ω, F) →L[𝕜] 𝓓(Ω, F)) : (a : 𝓓(Ω, F)) → 𝓓(Ω, F)) f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Distribution.TestFunction
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
Ω : Opens E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : NormedSpace 𝕜 F
inst_6 : Algebra ℝ 𝕜
inst_7 : IsScalarTower ℝ 𝕜 F
v : E
⊢ Eq (α := 𝓓(Ω, F) →L[𝕜] 𝓓(Ω, F)) (lineDerivOpCLM 𝕜 𝓓(Ω, F) v : 𝓓(Ω, F) →L[𝕜] 𝓓(Ω, F))
    (lineDerivCLM 𝕜 v : 𝓓(Ω, F) →L[𝕜] 𝓓(Ω, F))

Tactic:
rfl

Premises used: ContinuousLinearMap.comp, LineDeriv.lineDerivOpCLM, TestFunction.lineDerivCLM, rfl
-- Module: Mathlib.Analysis.Distribution.TestFunction
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
Ω : Opens E
F : Type u_4
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
n : ℕ∞
m : MeasurableSpace E
inst_4 : OpensMeasurableSpace E
f : 𝓓^{n}(Ω, F)
⊢ StronglyMeasurable (⇑f : (a : E) → F)

Tactic:
f.continuous.stronglyMeasurable_of_hasCompactSupport f.hasCompactSupport

Premises used: Continuous.stronglyMeasurable_of_hasCompactSupport, TestFunction.continuous, TestFunction.hasCompactSupport
-- Module: Mathlib.Analysis.Distribution.TestFunction
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
Ω : Opens E
F : Type u_4
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
n : ℕ∞
m : MeasurableSpace E
inst_4 : OpensMeasurableSpace E
f : 𝓓^{n}(Ω, F)
⊢ StronglyMeasurable (⇑f : (a : E) → F)

Tactic:
exact f.continuous.stronglyMeasurable_of_hasCompactSupport f.hasCompactSupport

Premises used: Continuous.stronglyMeasurable_of_hasCompactSupport, TestFunction.continuous, TestFunction.hasCompactSupport
-- Module: Mathlib.Analysis.Distribution.TestFunction
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
Ω : Opens E
F : Type u_4
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
n : ℕ∞
m : MeasurableSpace E
inst_4 : OpensMeasurableSpace E
μ : Measure E
f : 𝓓^{n}(Ω, F)
⊢ AEStronglyMeasurable (⇑f : (a : E) → F) μ

Tactic:
f.stronglyMeasurable.aestronglyMeasurable

Premises used: MeasureTheory.StronglyMeasurable.aestronglyMeasurable, TestFunction.stronglyMeasurable
-- Module: Mathlib.Analysis.Distribution.TestFunction
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
Ω : Opens E
F : Type u_4
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
n : ℕ∞
m : MeasurableSpace E
inst_4 : OpensMeasurableSpace E
μ : Measure E
f : 𝓓^{n}(Ω, F)
⊢ MemLp (⇑f : (a : E) → F) ⊤ μ

Tactic:
f.continuous.memLp_top_of_hasCompactSupport f.hasCompactSupport μ

Premises used: TestFunction.continuous, Continuous.memLp_top_of_hasCompactSupport, TestFunction.hasCompactSupport
-- Module: Mathlib.Analysis.Distribution.TestFunction
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
Ω : Opens E
n : ℕ∞
m : MeasurableSpace E
inst_3 : OpensMeasurableSpace E
F₁ : Type u_6
F₂ : Type u_7
F₃ : Type u_8
inst_4 : NormedAddCommGroup F₁
inst_5 : NormedSpace 𝕜 F₁
inst_6 : NormedSpace ℝ F₁
inst_7 : NormedAddCommGroup F₂
inst_8 : NormedSpace 𝕜 F₂
inst_9 : NormedAddCommGroup F₃
inst_10 : NormedSpace 𝕜 F₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
μ : Measure E
φ : E → F₂
hφ : LocallyIntegrableOn φ (↑Ω : Set E) μ
f : 𝓓^{n}(Ω, F₁)
this :
  IntegrableOn.{u_3, u_8} (ε := F₃)
    (fun (x : E) ↦ (((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x))
    (tsupport (⇑f : (a : E) → F₁)) μ
rwa :
  (support.{u_3, u_8} (M := F₃) fun (x : E) ↦
      (((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x)) ⊆
    tsupport (⇑f : (a : E) → F₁)
⊢ Integrable.{u_8, u_3} (ε := F₃)
    (fun (x : E) ↦ (((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x)) μ

Tactic:
rwa [integrableOn_iff_integrable_of_support_subset] at this

Premises used: MeasureTheory.integrableOn_iff_integrable_of_support_subset
-- Module: Mathlib.Analysis.Distribution.TestFunction
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
Ω : Opens E
n : ℕ∞
m : MeasurableSpace E
inst_3 : OpensMeasurableSpace E
F₁ : Type u_6
F₂ : Type u_7
F₃ : Type u_8
inst_4 : NormedAddCommGroup F₁
inst_5 : NormedSpace 𝕜 F₁
inst_6 : NormedSpace ℝ F₁
inst_7 : NormedAddCommGroup F₂
inst_8 : NormedSpace 𝕜 F₂
inst_9 : NormedAddCommGroup F₃
inst_10 : NormedSpace 𝕜 F₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
μ : Measure E
φ : E → F₂
hφ : LocallyIntegrableOn φ (↑Ω : Set E) μ
f : 𝓓^{n}(Ω, F₁)
this :
  IntegrableOn.{u_3, u_8} (ε := F₃)
    (fun (x : E) ↦ (((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x))
    (tsupport (⇑f : (a : E) → F₁)) μ
⊢ (support.{u_3, u_8} (M := F₃) fun (x : E) ↦
      (((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x)) ⊆
    tsupport (⇑f : (a : E) → F₁)

Tactic:
subset_trans ?_ (subset_tsupport f)

Premises used: subset_tsupport, subset_trans, DFunLike.coe
-- Module: Mathlib.Analysis.Distribution.TestFunction
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
Ω : Opens E
n : ℕ∞
m : MeasurableSpace E
inst_3 : OpensMeasurableSpace E
F₁ : Type u_6
F₂ : Type u_7
F₃ : Type u_8
inst_4 : NormedAddCommGroup F₁
inst_5 : NormedSpace 𝕜 F₁
inst_6 : NormedSpace ℝ F₁
inst_7 : NormedAddCommGroup F₂
inst_8 : NormedSpace 𝕜 F₂
inst_9 : NormedAddCommGroup F₃
inst_10 : NormedSpace 𝕜 F₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
μ : Measure E
φ : E → F₂
hφ : LocallyIntegrableOn φ (↑Ω : Set E) μ
f : 𝓓^{n}(Ω, F₁)
this :
  IntegrableOn.{u_3, u_8} (ε := F₃)
    (fun (x : E) ↦ (((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x))
    (tsupport (⇑f : (a : E) → F₁)) μ
refine :
  (support.{u_3, u_8} (M := F₃) fun (x : E) ↦
      (((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x)) ⊆
    support (⇑f : (a : E) → F₁)
⊢ (support.{u_3, u_8} (M := F₃) fun (x : E) ↦
      (((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x)) ⊆
    tsupport (⇑f : (a : E) → F₁)

Tactic:
refine subset_trans ?_ (subset_tsupport f)

Premises used: subset_tsupport, subset_trans, DFunLike.coe
-- Module: Mathlib.Analysis.Distribution.TestFunction
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
Ω : Opens E
n : ℕ∞
m : MeasurableSpace E
inst_3 : OpensMeasurableSpace E
F₁ : Type u_6
F₂ : Type u_7
F₃ : Type u_8
inst_4 : NormedAddCommGroup F₁
inst_5 : NormedSpace 𝕜 F₁
inst_6 : NormedSpace ℝ F₁
inst_7 : NormedAddCommGroup F₂
inst_8 : NormedSpace 𝕜 F₂
inst_9 : NormedAddCommGroup F₃
inst_10 : NormedSpace 𝕜 F₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
μ : Measure E
φ : E → F₂
hφ : LocallyIntegrableOn φ (↑Ω : Set E) μ
f : 𝓓^{n}(Ω, F₁)
this :
  IntegrableOn.{u_3, u_8} (ε := F₃)
    (fun (x : E) ↦ (((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x))
    (tsupport (⇑f : (a : E) → F₁)) μ
x : E
hx :
  Membership.mem (γ := Set E)
    (support.{u_3, u_8} (M := F₃) fun (x : E) ↦
      (((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x))
    x
hfx : (f : (a : E) → F₁) x = 0
⊢ Eq.{u_8 + 1} (α := F₃)
    ((fun (x : E) ↦ ((((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x) : F₃))
      x)
    0

Tactic:
simp [hfx]
-- Module: Mathlib.Analysis.Distribution.TestFunction
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
Ω : Opens E
n : ℕ∞
m : MeasurableSpace E
inst_3 : OpensMeasurableSpace E
F₁ : Type u_6
F₂ : Type u_7
F₃ : Type u_8
inst_4 : NormedAddCommGroup F₁
inst_5 : NormedSpace 𝕜 F₁
inst_6 : NormedSpace ℝ F₁
inst_7 : NormedAddCommGroup F₂
inst_8 : NormedSpace 𝕜 F₂
inst_9 : NormedAddCommGroup F₃
inst_10 : NormedSpace 𝕜 F₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
μ : Measure E
φ : E → F₂
hφ : LocallyIntegrableOn φ (↑Ω : Set E) μ
f : 𝓓^{n}(Ω, F₁)
this :
  IntegrableOn.{u_3, u_8} (ε := F₃)
    (fun (x : E) ↦ (((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x))
    (tsupport (⇑f : (a : E) → F₁)) μ
⊢ (support.{u_3, u_8} (M := F₃) fun (x : E) ↦
      (((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x)) ⊆
    support (⇑f : (a : E) → F₁)

Tactic:
exact fun x hx hfx ↦ hx (by simp [hfx])
-- Module: Mathlib.Analysis.Distribution.TestFunction
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
Ω : Opens E
n : ℕ∞
m : MeasurableSpace E
inst_3 : OpensMeasurableSpace E
F₁ : Type u_6
F₂ : Type u_7
F₃ : Type u_8
inst_4 : NormedAddCommGroup F₁
inst_5 : NormedSpace 𝕜 F₁
inst_6 : NormedSpace ℝ F₁
inst_7 : NormedAddCommGroup F₂
inst_8 : NormedSpace 𝕜 F₂
inst_9 : NormedAddCommGroup F₃
inst_10 : NormedSpace 𝕜 F₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
μ : Measure E
φ : E → F₂
hφ : LocallyIntegrableOn φ (↑Ω : Set E) μ
f : 𝓓^{n}(Ω, F₁)
suffices :
  IntegrableOn.{u_3, u_8} (ε := F₃)
    (fun (x : E) ↦ (((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x))
    (tsupport (⇑f : (a : E) → F₁)) μ
⊢ Integrable.{u_8, u_3} (ε := F₃)
    (fun (x : E) ↦ (((B : (a : F₁) → F₂ →L[𝕜] F₃) ((f : (a : E) → F₁) x) : F₂ →L[𝕜] F₃) : (a : F₂) → F₃) (φ x)) μ

Tactic:
suffices IntegrableOn (fun x ↦ B (f x) (φ x)) (tsupport f) μ by
    rwa [integrableOn_iff_integrable_of_support_subset] at this
    refine subset_trans ?_ (subset_tsupport f)
    exact fun x hx hfx ↦ hx (by simp [hfx])