awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
𝕜' : Type u_10
inst_4 : RCLike 𝕜'
inst_5 : NormedSpace 𝕜' F
g : E → ℝ
hg : Function.HasTemperateGrowth g
f : 𝓢(E, F)
x : E
⊢ Function.HasTemperateGrowth.{u_5, u_10} (F := 𝕜') fun (x : E) ↦ (↑(g x) : 𝕜')

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
𝕜' : Type u_10
inst_4 : RCLike 𝕜'
inst_5 : NormedSpace 𝕜' F
g : E → ℝ
hg : Function.HasTemperateGrowth g
f : 𝓢(E, F)
x : E
⊢ Function.HasTemperateGrowth g

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
𝕜' : Type u_10
inst_4 : RCLike 𝕜'
inst_5 : NormedSpace 𝕜' F
g : E → ℝ
hg : Function.HasTemperateGrowth g
f : 𝓢(E, F)
x : E
h :
  HSMul.hSMul.{u_10, u_6, u_6} (α := 𝕜') (β := F) (↑(g x) : 𝕜') ((f : (a : E) → F) x : F) =
    ((((smulLeftCLM F g : 𝓢(E, F) →L[ℝ] 𝓢(E, F)) : (a : 𝓢(E, F)) → 𝓢(E, F)) f : 𝓢(E, F)) : (a : E) → F) x
h₁ :
  HSMul.hSMul.{u_10, u_6, u_6} (α := 𝕜') (β := F) (↑(g x) : 𝕜') ((f : (a : E) → F) x : F) =
    HSMul.hSMul (β := F) (g x) ((f : (a : E) → F) x : F)
h₂ h₃ : HSMul.hSMul (β := F) (g x) ((f : (a : E) → F) x : F) = HSMul.hSMul (β := F) (g x) ((f : (a : E) → F) x : F)
⊢ Eq.{u_6 + 1} (α := F)
    (((((smulLeftCLM F fun (x : E) ↦ (↑(g x) : 𝕜') : 𝓢(E, F) →L[𝕜'] 𝓢(E, F)) : (a : 𝓢(E, F)) → 𝓢(E, F)) f : 𝓢(E, F)) :
          (a : E) → F)
        x :
      F)
    (((((smulLeftCLM F g : 𝓢(E, F) →L[ℝ] 𝓢(E, F)) : (a : 𝓢(E, F)) → 𝓢(E, F)) f : 𝓢(E, F)) : (a : E) → F) x : F)

Tactic:
rw [smulLeftCLM_apply_apply (by fun_prop), smulLeftCLM_apply_apply (by fun_prop),
    algebraMap_smul]

Premises used: algebraMap_smul, SchwartzMap.smulLeftCLM_apply_apply
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
𝕜' : Type u_10
inst_4 : RCLike 𝕜'
inst_5 : NormedSpace 𝕜' F
g : E → 𝕜'
hg : Function.HasTemperateGrowth g
c : ℝ
rw :
  smulLeftCLM F (HSMul.hSMul (α := 𝕜') (↑c : 𝕜') g) =
    HSMul.hSMul (β := 𝓢(E, F) →L[𝕜'] 𝓢(E, F)) c (smulLeftCLM F g : 𝓢(E, F) →L[𝕜'] 𝓢(E, F))
rw₁ :
  HSMul.hSMul (α := 𝕜') (β := 𝓢(E, F) →L[𝕜'] 𝓢(E, F)) (↑c : 𝕜') (smulLeftCLM F g : 𝓢(E, F) →L[𝕜'] 𝓢(E, F)) =
    HSMul.hSMul (β := 𝓢(E, F) →L[𝕜'] 𝓢(E, F)) c (smulLeftCLM F g : 𝓢(E, F) →L[𝕜'] 𝓢(E, F))
rw₂ rw₃ :
  HSMul.hSMul (β := 𝓢(E, F) →L[𝕜'] 𝓢(E, F)) c (smulLeftCLM F g : 𝓢(E, F) →L[𝕜'] 𝓢(E, F)) =
    HSMul.hSMul (β := 𝓢(E, F) →L[𝕜'] 𝓢(E, F)) c (smulLeftCLM F g : 𝓢(E, F) →L[𝕜'] 𝓢(E, F))
⊢ smulLeftCLM F (c • g) = HSMul.hSMul (β := 𝓢(E, F) →L[𝕜'] 𝓢(E, F)) c (smulLeftCLM F g : 𝓢(E, F) →L[𝕜'] 𝓢(E, F))

Tactic:
rw [RCLike.real_smul_eq_coe_smul (K := 𝕜') c, smulLeftCLM_smul hg,
    ← RCLike.real_smul_eq_coe_smul c]

Premises used: RCLike.real_smul_eq_coe_smul, SchwartzMap.smulLeftCLM_smul
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
𝕜 : Type u_2
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedAlgebra ℝ 𝕜
inst_6 : NormedSpace 𝕜 F
g : E → 𝕜
f : 𝓢(E, F)
pos :
  ∀ (hg : Function.HasTemperateGrowth g),
    tsupport.{u_5, u_6} (α := F)
        (⇑(((smulLeftCLM F g : 𝓢(E, F) →L[𝕜] 𝓢(E, F)) : (a : 𝓢(E, F)) → 𝓢(E, F)) f : 𝓢(E, F)) : (a : E) → F) ⊆
      tsupport.{u_5, u_6} (α := F) (⇑f : (a : E) → F) ∩ tsupport g
neg :
  ∀ (hg : ¬Function.HasTemperateGrowth g),
    tsupport.{u_5, u_6} (α := F)
        (⇑(((smulLeftCLM F g : 𝓢(E, F) →L[𝕜] 𝓢(E, F)) : (a : 𝓢(E, F)) → 𝓢(E, F)) f : 𝓢(E, F)) : (a : E) → F) ⊆
      tsupport.{u_5, u_6} (α := F) (⇑f : (a : E) → F) ∩ tsupport g
⊢ tsupport.{u_5, u_6} (α := F)
      (⇑(((smulLeftCLM F g : 𝓢(E, F) →L[𝕜] 𝓢(E, F)) : (a : 𝓢(E, F)) → 𝓢(E, F)) f : 𝓢(E, F)) : (a : E) → F) ⊆
    tsupport.{u_5, u_6} (α := F) (⇑f : (a : E) → F) ∩ tsupport g

Tactic:
by_cases hg : g.HasTemperateGrowth

Premises used: Function.HasTemperateGrowth
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
𝕜 : Type u_2
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedAlgebra ℝ 𝕜
inst_6 : NormedSpace 𝕜 F
g : E → 𝕜
f : 𝓢(E, F)
hg : Function.HasTemperateGrowth g
⊢ tsupport.{u_5, u_6} (α := F)
      (⇑(((smulLeftCLM F g : 𝓢(E, F) →L[𝕜] 𝓢(E, F)) : (a : 𝓢(E, F)) → 𝓢(E, F)) f : 𝓢(E, F)) : (a : E) → F) ⊆
    tsupport.{u_5, u_6} (α := F) (⇑f : (a : E) → F) ∩ tsupport g

Tactic:
simpa [smulLeftCLM_apply hg] using
      ⟨tsupport_smul_subset_right g f, tsupport_smul_subset_left g f⟩

Premises used: SchwartzMap.smulLeftCLM_apply
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
𝕜 : Type u_2
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedAlgebra ℝ 𝕜
inst_6 : NormedSpace 𝕜 F
g : E → 𝕜
f : 𝓢(E, F)
hg : ¬Function.HasTemperateGrowth g
⊢ tsupport.{u_5, u_6} (α := F)
      (⇑(((smulLeftCLM F g : 𝓢(E, F) →L[𝕜] 𝓢(E, F)) : (a : 𝓢(E, F)) → 𝓢(E, F)) f : 𝓢(E, F)) : (a : E) → F) ⊆
    tsupport.{u_5, u_6} (α := F) (⇑f : (a : E) → F) ∩ tsupport g

Tactic:
simp [smulLeftCLM, hg]

Premises used: SchwartzMap.smulLeftCLM
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
H : Type u_8
V : Type u_9
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedAlgebra ℝ 𝕜
inst_6 : NormedAddCommGroup D
inst_7 : NormedSpace ℝ D
inst_8 : NormedAddCommGroup G
inst_9 : NormedSpace ℝ G
inst_10 : NormedSpace 𝕜 F
inst_11 : NormedSpace 𝕜 E
inst_12 : NormedSpace 𝕜 G
B : E →L[𝕜] F →L[𝕜] G
x x_1 : 𝓢(D, E)
h :
  ∀ (x_2 : 𝓢(D, F)) (x_3 : D),
    Eq.{u_7 + 1} (α := G)
      (((((bilinLeftCLM B.flip ⋯ : 𝓢(D, F) →L[𝕜] 𝓢(D, G)) : (a : 𝓢(D, F)) → 𝓢(D, G)) x_2 : 𝓢(D, G)) : (a : D) → G) x_3 :
        G)
      ((((HAdd.hAdd (α := 𝓢(D, F) →L[𝕜] 𝓢(D, G)) (β := 𝓢(D, F) →L[𝕜] 𝓢(D, G))
                    (bilinLeftCLM B.flip ⋯ : 𝓢(D, F) →L[𝕜] 𝓢(D, G)) (bilinLeftCLM B.flip ⋯ : 𝓢(D, F) →L[𝕜] 𝓢(D, G)) :
                  (a : 𝓢(D, F)) → 𝓢(D, G))
                x_2 :
              𝓢(D, G)) :
            (a : D) → G)
          x_3 :
        G)
⊢ bilinLeftCLM B.flip ⋯ =
    HAdd.hAdd (α := 𝓢(D, F) →L[𝕜] 𝓢(D, G)) (β := 𝓢(D, F) →L[𝕜] 𝓢(D, G)) (bilinLeftCLM B.flip ⋯ : 𝓢(D, F) →L[𝕜] 𝓢(D, G))
      (bilinLeftCLM B.flip ⋯ : 𝓢(D, F) →L[𝕜] 𝓢(D, G))

Tactic:
ext
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
H : Type u_8
V : Type u_9
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedAlgebra ℝ 𝕜
inst_6 : NormedAddCommGroup D
inst_7 : NormedSpace ℝ D
inst_8 : NormedAddCommGroup G
inst_9 : NormedSpace ℝ G
inst_10 : NormedSpace 𝕜 F
inst_11 : NormedSpace 𝕜 E
inst_12 : NormedSpace 𝕜 G
B : E →L[𝕜] F →L[𝕜] G
x x_1 : 𝓢(D, E)
x_2 : 𝓢(D, F)
x_3 : D
⊢ Eq.{u_7 + 1} (α := G)
    (((((bilinLeftCLM B.flip ⋯ : 𝓢(D, F) →L[𝕜] 𝓢(D, G)) : (a : 𝓢(D, F)) → 𝓢(D, G)) x_2 : 𝓢(D, G)) : (a : D) → G) x_3 :
      G)
    ((((HAdd.hAdd (α := 𝓢(D, F) →L[𝕜] 𝓢(D, G)) (β := 𝓢(D, F) →L[𝕜] 𝓢(D, G))
                  (bilinLeftCLM B.flip ⋯ : 𝓢(D, F) →L[𝕜] 𝓢(D, G)) (bilinLeftCLM B.flip ⋯ : 𝓢(D, F) →L[𝕜] 𝓢(D, G)) :
                (a : 𝓢(D, F)) → 𝓢(D, G))
              x_2 :
            𝓢(D, G)) :
          (a : D) → G)
        x_3 :
      G)

Tactic:
simp
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
H : Type u_8
V : Type u_9
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedAlgebra ℝ 𝕜
inst_6 : NormedAddCommGroup D
inst_7 : NormedSpace ℝ D
inst_8 : NormedAddCommGroup G
inst_9 : NormedSpace ℝ G
inst_10 : NormedSpace 𝕜 F
inst_11 : NormedSpace 𝕜 E
inst_12 : NormedSpace 𝕜 G
B : E →L[𝕜] F →L[𝕜] G
x : 𝕜
x_1 : 𝓢(D, E)
h :
  ∀ (x_2 : 𝓢(D, F)) (x_3 : D),
    Eq.{u_7 + 1} (α := G)
      (((((bilinLeftCLM B.flip ⋯ : 𝓢(D, F) →L[𝕜] 𝓢(D, G)) : (a : 𝓢(D, F)) → 𝓢(D, G)) x_2 : 𝓢(D, G)) : (a : D) → G) x_3 :
        G)
      ((((HSMul.hSMul (α := 𝕜) (β := 𝓢(D, F) →L[𝕜] 𝓢(D, G)) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜)
                    (bilinLeftCLM B.flip ⋯ : 𝓢(D, F) →L[𝕜] 𝓢(D, G)) :
                  (a : 𝓢(D, F)) → 𝓢(D, G))
                x_2 :
              𝓢(D, G)) :
            (a : D) → G)
          x_3 :
        G)
⊢ bilinLeftCLM B.flip ⋯ =
    HSMul.hSMul (α := 𝕜) (β := 𝓢(D, F) →L[𝕜] 𝓢(D, G)) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜)
      (bilinLeftCLM B.flip ⋯ : 𝓢(D, F) →L[𝕜] 𝓢(D, G))

Tactic:
ext
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
H : Type u_8
V : Type u_9
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedAlgebra ℝ 𝕜
inst_6 : NormedAddCommGroup D
inst_7 : NormedSpace ℝ D
inst_8 : NormedAddCommGroup G
inst_9 : NormedSpace ℝ G
inst_10 : NormedSpace 𝕜 F
inst_11 : NormedSpace 𝕜 E
inst_12 : NormedSpace 𝕜 G
B : E →L[𝕜] F →L[𝕜] G
x : 𝕜
x_1 : 𝓢(D, E)
x_2 : 𝓢(D, F)
x_3 : D
⊢ Eq.{u_7 + 1} (α := G)
    (((((bilinLeftCLM B.flip ⋯ : 𝓢(D, F) →L[𝕜] 𝓢(D, G)) : (a : 𝓢(D, F)) → 𝓢(D, G)) x_2 : 𝓢(D, G)) : (a : D) → G) x_3 :
      G)
    ((((HSMul.hSMul (α := 𝕜) (β := 𝓢(D, F) →L[𝕜] 𝓢(D, G)) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜)
                  (bilinLeftCLM B.flip ⋯ : 𝓢(D, F) →L[𝕜] 𝓢(D, G)) :
                (a : 𝓢(D, F)) → 𝓢(D, G))
              x_2 :
            𝓢(D, G)) :
          (a : D) → G)
        x_3 :
      G)

Tactic:
simp
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
𝕜 : Type u_2
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedAlgebra ℝ 𝕜
inst_6 : NormedAddCommGroup D
inst_7 : NormedSpace ℝ D
inst_8 : NormedAddCommGroup G
inst_9 : NormedSpace ℝ G
inst_10 : NormedSpace 𝕜 F
inst_11 : NormedSpace 𝕜 E
inst_12 : NormedSpace 𝕜 G
B : E →L[𝕜] F →L[𝕜] G
f : 𝓢(D, E)
g : 𝓢(D, F)
⊢ Eq (α := (a : D) → G)
    (⇑(((((pairing B : 𝓢(D, E) →ₗ[𝕜] 𝓢(D, F) →L[𝕜] 𝓢(D, G)) : (a : 𝓢(D, E)) → 𝓢(D, F) →L[𝕜] 𝓢(D, G)) f :
                𝓢(D, F) →L[𝕜] 𝓢(D, G)) :
              (a : 𝓢(D, F)) → 𝓢(D, G))
            g :
          𝓢(D, G)) :
      (a : D) → G)
    fun (x : D) ↦
    (((B : (a : E) → F →L[𝕜] G) ((f : (a : D) → E) x) : F →L[𝕜] G) : (a : F) → G) ((g : (a : D) → F) x : F)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
𝕜 : Type u_2
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedAlgebra ℝ 𝕜
inst_6 : NormedAddCommGroup D
inst_7 : NormedSpace ℝ D
inst_8 : NormedAddCommGroup G
inst_9 : NormedSpace ℝ G
inst_10 : NormedSpace 𝕜 F
inst_11 : NormedSpace 𝕜 E
inst_12 : NormedSpace 𝕜 G
B : E →L[𝕜] F →L[𝕜] G
f : 𝓢(D, E)
g : 𝓢(D, F)
x : D
⊢ Eq.{u_7 + 1} (α := G)
    (((((((pairing B : 𝓢(D, E) →ₗ[𝕜] 𝓢(D, F) →L[𝕜] 𝓢(D, G)) : (a : 𝓢(D, E)) → 𝓢(D, F) →L[𝕜] 𝓢(D, G)) f :
                  𝓢(D, F) →L[𝕜] 𝓢(D, G)) :
                (a : 𝓢(D, F)) → 𝓢(D, G))
              g :
            𝓢(D, G)) :
          (a : D) → G)
        x :
      G)
    ((((B : (a : E) → F →L[𝕜] G) ((f : (a : D) → E) x) : F →L[𝕜] G) : (a : F) → G) ((g : (a : D) → F) x : F) : G)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
𝕜 : Type u_2
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedAlgebra ℝ 𝕜
inst_6 : NormedAddCommGroup D
inst_7 : NormedSpace ℝ D
inst_8 : NormedAddCommGroup G
inst_9 : NormedSpace ℝ G
inst_10 : NormedSpace 𝕜 F
inst_11 : NormedSpace 𝕜 E
inst_12 : NormedSpace 𝕜 G
B : E →L[𝕜] F →L[𝕜] G
g : 𝓢(D, F)
⊢ Continuous (Y := 𝓢(D, G)) fun (x : 𝓢(D, E)) ↦
    ((((pairing B : 𝓢(D, E) →ₗ[𝕜] 𝓢(D, F) →L[𝕜] 𝓢(D, G)) : (a : 𝓢(D, E)) → 𝓢(D, F) →L[𝕜] 𝓢(D, G)) x :
          𝓢(D, F) →L[𝕜] 𝓢(D, G)) :
        (a : 𝓢(D, F)) → 𝓢(D, G))
      g

Tactic:
(pairing B.flip g).continuous

Premises used: ContinuousLinearMap.continuous, SchwartzMap.pairing, ContinuousLinearMap.flip, DFunLike.coe
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
H : Type u_8
V : Type u_9
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedAlgebra ℝ 𝕜
inst_6 : NormedAddCommGroup D
inst_7 : NormedSpace ℝ D
inst_8 : NormedAddCommGroup G
inst_9 : NormedSpace ℝ G
inst_10 : NormedSpace 𝕜 F
L : ContinuousLinearMap.{0, 0, u_5, u_7} (RingHom.id ℝ) E (G →L[ℝ] ℝ)
f g : 𝓢(E, F)
x : E
h :
  ∀ (x_1 : G),
    Eq.{u_6 + 1} (α := F)
      (((fun (f : 𝓢(E, F)) (x : E) ↦
                (smulRight (S := ℝ) ((L : (a : E) → G →L[ℝ] ℝ) x) ((f : (a : E) → F) x) : G →L[ℝ] F))
              (f + g) x :
            (a : G) → F)
          x_1 :
        F)
      ((HAdd.hAdd (α := G →L[ℝ] F)
              ((fun (f : 𝓢(E, F)) (x : E) ↦
                  (smulRight (S := ℝ) ((L : (a : E) → G →L[ℝ] ℝ) x) ((f : (a : E) → F) x) : G →L[ℝ] F))
                f x)
              ((fun (f : 𝓢(E, F)) (x : E) ↦
                  (smulRight (S := ℝ) ((L : (a : E) → G →L[ℝ] ℝ) x) ((f : (a : E) → F) x) : G →L[ℝ] F))
                g x) :
            (a : G) → F)
          x_1 :
        F)
⊢ (fun (f : 𝓢(E, F)) (x : E) ↦ (smulRight (S := ℝ) ((L : (a : E) → G →L[ℝ] ℝ) x) ((f : (a : E) → F) x) : G →L[ℝ] F))
      (f + g) x =
    HAdd.hAdd (α := G →L[ℝ] F)
      ((fun (f : 𝓢(E, F)) (x : E) ↦
          (smulRight (S := ℝ) ((L : (a : E) → G →L[ℝ] ℝ) x) ((f : (a : E) → F) x) : G →L[ℝ] F))
        f x)
      ((fun (f : 𝓢(E, F)) (x : E) ↦
          (smulRight (S := ℝ) ((L : (a : E) → G →L[ℝ] ℝ) x) ((f : (a : E) → F) x) : G →L[ℝ] F))
        g x)

Tactic:
ext
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
H : Type u_8
V : Type u_9
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedAlgebra ℝ 𝕜
inst_6 : NormedAddCommGroup D
inst_7 : NormedSpace ℝ D
inst_8 : NormedAddCommGroup G
inst_9 : NormedSpace ℝ G
inst_10 : NormedSpace 𝕜 F
L : ContinuousLinearMap.{0, 0, u_5, u_7} (RingHom.id ℝ) E (G →L[ℝ] ℝ)
f g : 𝓢(E, F)
x : E
x_1 : G
⊢ Eq.{u_6 + 1} (α := F)
    (((fun (f : 𝓢(E, F)) (x : E) ↦ (smulRight (S := ℝ) ((L : (a : E) → G →L[ℝ] ℝ) x) ((f : (a : E) → F) x) : G →L[ℝ] F))
            (f + g) x :
          (a : G) → F)
        x_1 :
      F)
    ((HAdd.hAdd (α := G →L[ℝ] F)
            ((fun (f : 𝓢(E, F)) (x : E) ↦
                (smulRight (S := ℝ) ((L : (a : E) → G →L[ℝ] ℝ) x) ((f : (a : E) → F) x) : G →L[ℝ] F))
              f x)
            ((fun (f : 𝓢(E, F)) (x : E) ↦
                (smulRight (S := ℝ) ((L : (a : E) → G →L[ℝ] ℝ) x) ((f : (a : E) → F) x) : G →L[ℝ] F))
              g x) :
          (a : G) → F)
        x_1 :
      F)

Tactic:
simp
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
H : Type u_8
V : Type u_9
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedAlgebra ℝ 𝕜
inst_6 : NormedAddCommGroup D
inst_7 : NormedSpace ℝ D
inst_8 : NormedAddCommGroup G
inst_9 : NormedSpace ℝ G
inst_10 : NormedSpace 𝕜 F
L : ContinuousLinearMap.{0, 0, u_5, u_7} (RingHom.id ℝ) E (G →L[ℝ] ℝ)
c : 𝕜
g : 𝓢(E, F)
x : E
v : G
⊢ Eq.{u_6 + 1} (α := F)
    (((fun (f : 𝓢(E, F)) (x : E) ↦ (smulRight (S := ℝ) ((L : (a : E) → G →L[ℝ] ℝ) x) ((f : (a : E) → F) x) : G →L[ℝ] F))
            (c • g) x :
          (a : G) → F)
        v :
      F)
    ((HSMul.hSMul (α := 𝕜) (β := G →L[ℝ] F) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜)
            ((fun (f : 𝓢(E, F)) (x : E) ↦
                (smulRight (S := ℝ) ((L : (a : E) → G →L[ℝ] ℝ) x) ((f : (a : E) → F) x) : G →L[ℝ] F))
              g x) :
          (a : G) → F)
        v :
      F)

Tactic:
simpa using smul_comm (L x v) c (g x)

Premises used: SMulCommClass.smul_comm, DFunLike.coe
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
H : Type u_8
V : Type u_9
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedAlgebra ℝ 𝕜
inst_6 : NormedAddCommGroup D
inst_7 : NormedSpace ℝ D
inst_8 : NormedAddCommGroup G
inst_9 : NormedSpace ℝ G
inst_10 : NormedSpace 𝕜 F
L : ContinuousLinearMap.{0, 0, u_5, u_7} (RingHom.id ℝ) E (G →L[ℝ] ℝ)
⊢ ∀ (f : 𝓢(E, F)),
    ContDiff ℝ (E := E) (F := G →L[ℝ] F) ∞
      ((fun (f : 𝓢(E, F)) (x : E) ↦
          (smulRight (S := ℝ) ((L : (a : E) → G →L[ℝ] ℝ) x) ((f : (a : E) → F) x) : G →L[ℝ] F))
        f)

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
H : Type u_8
V : Type u_9
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedAlgebra ℝ 𝕜
inst_6 : NormedAddCommGroup D
inst_7 : NormedSpace ℝ D
inst_8 : NormedAddCommGroup G
inst_9 : NormedSpace ℝ G
inst_10 : NormedSpace 𝕜 F
L : ContinuousLinearMap.{0, 0, u_5, u_7} (RingHom.id ℝ) E (G →L[ℝ] ℝ)
k n : ℕ
⊢ 0 ≤ 2 * ‖L‖ * (↑(max 1 n) : ℝ)

Tactic:
positivity
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
H : Type u_8
V : Type u_9
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedAlgebra ℝ 𝕜
inst_6 : NormedAddCommGroup D
inst_7 : NormedSpace ℝ D
inst_8 : NormedAddCommGroup G
inst_9 : NormedSpace ℝ G
inst_10 : NormedSpace 𝕜 F
L : ContinuousLinearMap.{0, 0, u_5, u_7} (RingHom.id ℝ) E (G →L[ℝ] ℝ)
k n : ℕ
right :
  ∀ (f : 𝓢(E, F)) (x : E),
    ‖x‖ ^ (k, n).1 *
        norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin (k, n).2) ↦ E) (G →L[ℝ] F))
          (iteratedFDeriv ℝ (k, n).2
            ((fun (f : 𝓢(E, F)) (x : E) ↦
                (smulRight (S := ℝ) ((L : (a : E) → G →L[ℝ] ℝ) x) ((f : (a : E) → F) x) : G →L[ℝ] F))
              f)
            x) ≤
      HMul.hMul (β := ℝ) (2 * ‖L‖ * (↑(max 1 n) : ℝ))
        ((Finset.sup {(k + 1, n), (k, n - 1)} (schwartzSeminormFamily 𝕜 E F) : (a : 𝓢(E, F)) → ℝ) f : ℝ)
⊢ ∃ (s : Finset (ℕ × ℕ)) (C : ℝ),
    0 ≤ C ∧
      ∀ (f : 𝓢(E, F)) (x : E),
        ‖x‖ ^ (k, n).1 *
            norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin (k, n).2) ↦ E) (G →L[ℝ] F))
              (iteratedFDeriv ℝ (k, n).2
                ((fun (f : 𝓢(E, F)) (x : E) ↦
                    (smulRight (S := ℝ) ((L : (a : E) → G →L[ℝ] ℝ) x) ((f : (a : E) → F) x) : G →L[ℝ] F))
                  f)
                x) ≤
          HMul.hMul (β := ℝ) C ((s.sup (schwartzSeminormFamily 𝕜 E F) : (a : 𝓢(E, F)) → ℝ) f : ℝ)

Tactic:
use {(k + 1, n), (k, n - 1)}, 2 * ‖L‖ * (max 1 n), by positivity

Premises used: HSub.hSub, Prod.mk, HAdd.hAdd, Max.max, OfNat.ofNat
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
H : Type u_8
V : Type u_9
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedAlgebra ℝ 𝕜
inst_6 : NormedAddCommGroup D
inst_7 : NormedSpace ℝ D
inst_8 : NormedAddCommGroup G
inst_9 : NormedSpace ℝ G
inst_10 : NormedSpace 𝕜 F
L : ContinuousLinearMap.{0, 0, u_5, u_7} (RingHom.id ℝ) E (G →L[ℝ] ℝ)
k n : ℕ
f : 𝓢(E, F)
x : E
hbc :
  norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin (k, n).2) ↦ E) (G →L[ℝ] F))
      (iteratedFDeriv ℝ (k, n).2
        ((fun (f : 𝓢(E, F)) (x : E) ↦
            (smulRight (S := ℝ) ((L : (a : E) → G →L[ℝ] ℝ) x) ((f : (a : E) → F) x) : G →L[ℝ] F))
          f)
        x) ≤
    ∑ i ∈ Finset.range (n + 1),
      (↑(n.choose i) : ℝ) *
          norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_7} ℝ (fun (i : Fin i) ↦ E) (G →L[ℝ] ℝ))
            (iteratedFDeriv ℝ i (⇑L : (a : E) → G →L[ℝ] ℝ) x) *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin (n - i)) ↦ E) F)
          (iteratedFDeriv ℝ (n - i) (⇑f : (a : E) → F) x)
⊢ ‖x‖ ^ (k, n).1 *
      norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin (k, n).2) ↦ E) (G →L[ℝ] F))
        (iteratedFDeriv ℝ (k, n).2
          ((fun (f : 𝓢(E, F)) (x : E) ↦
              (smulRight (S := ℝ) ((L : (a : E) → G →L[ℝ] ℝ) x) ((f : (a : E) → F) x) : G →L[ℝ] F))
            f)
          x) ≤
    ‖x‖ ^ k *
      ∑ i ∈ Finset.range (n + 1),
        (↑(n.choose i) : ℝ) *
            norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_7} ℝ (fun (i : Fin i) ↦ E) (G →L[ℝ] ℝ))
              (iteratedFDeriv ℝ i (⇑L : (a : E) → G →L[ℝ] ℝ) x) *
          norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin (n - i)) ↦ E) F)
            (iteratedFDeriv ℝ (n - i) (⇑f : (a : E) → F) x)

Tactic:
gcongr 1
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
H : Type u_8
V : Type u_9
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedAlgebra ℝ 𝕜
inst_6 : NormedAddCommGroup D
inst_7 : NormedSpace ℝ D
inst_8 : NormedAddCommGroup G
inst_9 : NormedSpace ℝ G
inst_10 : NormedSpace 𝕜 F
L : ContinuousLinearMap.{0, 0, u_5, u_7} (RingHom.id ℝ) E (G →L[ℝ] ℝ)
k n : ℕ
f : 𝓢(E, F)
x : E
⊢ ContDiff.{0, u_5, u_7} ℝ (E := E) (F := StrongDual ℝ G) ∞ (⇑L : (a : E) → G →L[ℝ] ℝ)

Tactic:
fun_prop