awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : NormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
m : ℕ × ℕ
k n : ℕ
hk : k ≤ m.1
hn : n ≤ m.2
f : 𝓢(E, F)
x : E
hk' : Finset.range (k + 1) ⊆ Finset.range (m.1 + 1)
i : ℕ
hi : i ∈ Finset.range (m.1 + 1)
h :
  ‖x‖ ^ i *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
        (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x) ≤
    ((Finset.Iic m).sup fun (m : ℕ × ℕ) ↦ SchwartzMap.seminorm 𝕜 m.1 m.2 : (a : 𝓢(E, F)) → ℝ) f
⊢ ‖x‖ ^ i *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
          (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x) *
      (↑(k.choose i) : ℝ) ≤
    HMul.hMul (α := ℝ) (β := ℝ)
      (((Finset.Iic m).sup fun (m : ℕ × ℕ) ↦ SchwartzMap.seminorm 𝕜 m.1 m.2 : (a : 𝓢(E, F)) → ℝ) f : ℝ)
      ((↑(m.1.choose i) : ℝ) : ℝ)

Tactic:
gcongr
-- 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 : NormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
m : ℕ × ℕ
k n : ℕ
hk : k ≤ m.1
hn : n ≤ m.2
f : 𝓢(E, F)
x : E
hk' : Finset.range (k + 1) ⊆ Finset.range (m.1 + 1)
i : ℕ
hi : i ∈ Finset.range (m.1 + 1)
h :
  LE.le (α := ℝ) ((SchwartzMap.seminorm 𝕜 i n : (a : 𝓢(E, F)) → ℝ) f : ℝ)
    (((Finset.Iic m).sup fun (m : ℕ × ℕ) ↦ SchwartzMap.seminorm 𝕜 m.1 m.2 : (a : 𝓢(E, F)) → ℝ) f : ℝ)
⊢ ‖x‖ ^ i *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
        (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x) ≤
    ((Finset.Iic m).sup fun (m : ℕ × ℕ) ↦ SchwartzMap.seminorm 𝕜 m.1 m.2 : (a : 𝓢(E, F)) → ℝ) f

Tactic:
grw [le_seminorm 𝕜 i n f x]

Premises used: SchwartzMap.le_seminorm
-- 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 : NormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
m : ℕ × ℕ
k n : ℕ
hk : k ≤ m.1
hn : n ≤ m.2
f : 𝓢(E, F)
x : E
hk' : Finset.range (k + 1) ⊆ Finset.range (m.1 + 1)
i : ℕ
hi : i ∈ Finset.range (m.1 + 1)
h :
  LE.le (α := Seminorm 𝕜 𝓢(E, F)) (SchwartzMap.seminorm 𝕜 i n)
    ((Finset.Iic m).sup fun (m : ℕ × ℕ) ↦ SchwartzMap.seminorm 𝕜 m.1 m.2)
⊢ LE.le (α := ℝ) ((SchwartzMap.seminorm 𝕜 i n : (a : 𝓢(E, F)) → ℝ) f : ℝ)
    (((Finset.Iic m).sup fun (m : ℕ × ℕ) ↦ SchwartzMap.seminorm 𝕜 m.1 m.2 : (a : 𝓢(E, F)) → ℝ) f : ℝ)

Tactic:
apply Seminorm.le_def.1

Premises used: Seminorm.le_def, Iff.mp
-- 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 : NormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
m : ℕ × ℕ
k n : ℕ
hk : k ≤ m.1
hn : n ≤ m.2
f : 𝓢(E, F)
x : E
hk' : Finset.range (k + 1) ⊆ Finset.range (m.1 + 1)
i : ℕ
hi : i ∈ Finset.range (m.1 + 1)
⊢ LE.le (α := Seminorm 𝕜 𝓢(E, F)) (SchwartzMap.seminorm 𝕜 i n)
    ((Finset.Iic m).sup fun (m : ℕ × ℕ) ↦ SchwartzMap.seminorm 𝕜 m.1 m.2)

Tactic:
Finset.le_sup_of_le (Finset.mem_Iic.2 <|
    Prod.mk_le_mk.2 ⟨Finset.mem_range_succ_iff.mp hi, hn⟩) le_rfl

Premises used: Iff.mpr, le_rfl, Finset.mem_range_succ_iff, Finset.mem_Iic, Finset.le_sup_of_le, And.intro, Iff.mp, Prod.mk_le_mk
-- 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 : NormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
m : ℕ × ℕ
k n : ℕ
hk : k ≤ m.1
hn : n ≤ m.2
f : 𝓢(E, F)
x : E
hk' : Finset.range (k + 1) ⊆ Finset.range (m.1 + 1)
i : ℕ
hi : i ∈ Finset.range (m.1 + 1)
⊢ LE.le (α := Seminorm 𝕜 𝓢(E, F)) (SchwartzMap.seminorm 𝕜 i n)
    ((Finset.Iic m).sup fun (m : ℕ × ℕ) ↦ SchwartzMap.seminorm 𝕜 m.1 m.2)

Tactic:
exact Finset.le_sup_of_le (Finset.mem_Iic.2 <|
    Prod.mk_le_mk.2 ⟨Finset.mem_range_succ_iff.mp hi, hn⟩) le_rfl

Premises used: Iff.mpr, le_rfl, Finset.mem_range_succ_iff, Finset.mem_Iic, Finset.le_sup_of_le, And.intro, Iff.mp, Prod.mk_le_mk
-- 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 : NormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
⊢ WithSeminorms (E := 𝓢(E, F)) (schwartzSeminormFamily ℝ E F)

Tactic:
have A : WithSeminorms (schwartzSeminormFamily ℝ E F) := ⟨rfl⟩
-- 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 : NormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
A : WithSeminorms (E := 𝓢(E, F)) (schwartzSeminormFamily ℝ E F)
rw :
  ∀
    (A :
      Eq (α := Filter 𝓢(E, F)) (nhds 0)
        (⨅ (i : ℕ × ℕ), Filter.comap (β := ℝ) (⇑(schwartzSeminormFamily ℝ E F i) : (a : 𝓢(E, F)) → ℝ) (nhds 0))),
    Eq (α := Filter 𝓢(E, F)) (nhds 0)
      (⨅ (i : ℕ × ℕ), Filter.comap (β := ℝ) (⇑(schwartzSeminormFamily 𝕜 E F i) : (a : 𝓢(E, F)) → ℝ) (nhds 0))
⊢ WithSeminorms (E := 𝓢(E, F)) (schwartzSeminormFamily 𝕜 E F)

Tactic:
rw [SeminormFamily.withSeminorms_iff_nhds_eq_iInf] at A ⊢

Premises used: SeminormFamily.withSeminorms_iff_nhds_eq_iInf
-- 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 : NormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
A :
  Eq (α := Filter 𝓢(E, F)) (nhds 0)
    (⨅ (i : ℕ × ℕ), Filter.comap (β := ℝ) (⇑(schwartzSeminormFamily ℝ E F i) : (a : 𝓢(E, F)) → ℝ) (nhds 0))
rw :
  Eq (α := Filter 𝓢(E, F))
    (⨅ (i : ℕ × ℕ), Filter.comap (β := ℝ) (⇑(schwartzSeminormFamily ℝ E F i) : (a : 𝓢(E, F)) → ℝ) (nhds 0))
    (⨅ (i : ℕ × ℕ), Filter.comap (β := ℝ) (⇑(schwartzSeminormFamily 𝕜 E F i) : (a : 𝓢(E, F)) → ℝ) (nhds 0))
⊢ Eq (α := Filter 𝓢(E, F)) (nhds 0)
    (⨅ (i : ℕ × ℕ), Filter.comap (β := ℝ) (⇑(schwartzSeminormFamily 𝕜 E F i) : (a : 𝓢(E, F)) → ℝ) (nhds 0))

Tactic:
rw [A]
-- 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 : NormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
A :
  Eq (α := Filter 𝓢(E, F)) (nhds 0)
    (⨅ (i : ℕ × ℕ), Filter.comap (β := ℝ) (⇑(schwartzSeminormFamily ℝ E F i) : (a : 𝓢(E, F)) → ℝ) (nhds 0))
⊢ Eq (α := Filter 𝓢(E, F))
    (⨅ (i : ℕ × ℕ), Filter.comap (β := ℝ) (⇑(schwartzSeminormFamily ℝ E F i) : (a : 𝓢(E, F)) → ℝ) (nhds 0))
    (⨅ (i : ℕ × ℕ), Filter.comap (β := ℝ) (⇑(schwartzSeminormFamily 𝕜 E F i) : (a : 𝓢(E, F)) → ℝ) (nhds 0))

Tactic:
rfl
-- 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 : NormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
rw : ContinuousSMul 𝕜 𝓢(E, F)
⊢ ContinuousSMul 𝕜 𝓢(E, F)

Tactic:
rw [(schwartz_withSeminorms 𝕜 E F).withSeminorms_eq]

Premises used: schwartz_withSeminorms, WithSeminorms.withSeminorms_eq
-- 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 : NormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
⊢ ContinuousSMul 𝕜 𝓢(E, F)

Tactic:
(schwartzSeminormFamily 𝕜 E F).moduleFilterBasis.continuousSMul

Premises used: SeminormFamily.moduleFilterBasis, schwartzSeminormFamily, ModuleFilterBasis.continuousSMul
-- 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 : NormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
⊢ ContinuousSMul 𝕜 𝓢(E, F)

Tactic:
exact (schwartzSeminormFamily 𝕜 E F).moduleFilterBasis.continuousSMul

Premises used: SeminormFamily.moduleFilterBasis, schwartzSeminormFamily, ModuleFilterBasis.continuousSMul
-- 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 : NormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
⊢ IsTopologicalAddGroup 𝓢(E, F)

Tactic:
(schwartzSeminormFamily ℝ E F).addGroupFilterBasis.isTopologicalAddGroup

Premises used: Real, AddGroupFilterBasis.isTopologicalAddGroup, schwartzSeminormFamily, SeminormFamily.addGroupFilterBasis
-- 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 : NormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
⊢ IsUniformAddGroup 𝓢(E, F)

Tactic:
(schwartzSeminormFamily ℝ E F).addGroupFilterBasis.isUniformAddGroup

Premises used: Real, schwartzSeminormFamily, SeminormFamily.addGroupFilterBasis, AddGroupFilterBasis.isUniformAddGroup
-- 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 : NormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
⊢ LocallyConvexSpace ℝ 𝓢(E, F)

Tactic:
(schwartz_withSeminorms ℝ E F).toLocallyConvexSpace

Premises used: schwartz_withSeminorms, WithSeminorms.toLocallyConvexSpace, Real
-- 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 : NormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
⊢ FirstCountableTopology 𝓢(E, F)

Tactic:
(schwartz_withSeminorms ℝ E F).firstCountableTopology

Premises used: schwartz_withSeminorms, Real, WithSeminorms.firstCountableTopology
-- 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
f : 𝓢(E, F)
⊢ Function.HasTemperateGrowth.{u_5, u_6} (E := E) (F := F) (⇑f : (a : E) → F)

Tactic:
⟨smooth f ⊤, fun n => ?_⟩

Premises used: Function.HasTemperateGrowth, And.intro, Top.top, SchwartzMap.smooth
-- 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
f : 𝓢(E, F)
refine :
  ∀ (n : ℕ),
    ∃ (k : ℕ) (C : ℝ),
      ∀ (x : E),
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
            (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x) ≤
          C * (1 + ‖x‖) ^ k
⊢ Function.HasTemperateGrowth.{u_5, u_6} (E := E) (F := F) (⇑f : (a : E) → F)

Tactic:
refine ⟨smooth f ⊤, fun n => ?_⟩
-- 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
f : 𝓢(E, F)
n : ℕ
rcases :
  ∀ (C : ℝ) (Cpos : 0 < C)
    (hC :
      ∀ (x : E),
        HPow.hPow (β := ℕ) ‖x‖ 0 *
            norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
              (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x) ≤
          C),
    ∃ (k : ℕ) (C : ℝ),
      ∀ (x : E),
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
            (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x) ≤
          C * (1 + ‖x‖) ^ k
⊢ ∃ (k : ℕ) (C : ℝ),
    ∀ (x : E),
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
          (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x) ≤
        C * (1 + ‖x‖) ^ k

Tactic:
rcases f.decay 0 n with ⟨C, Cpos, hC⟩

Premises used: SchwartzMap.decay, OfNat.ofNat
-- 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
f : 𝓢(E, F)
n : ℕ
C : ℝ
Cpos : 0 < C
hC :
  ∀ (x : E),
    HPow.hPow (β := ℕ) ‖x‖ 0 *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
          (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x) ≤
      C
⊢ ∀ (x : E),
    norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
        (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x) ≤
      C * HPow.hPow (β := ℕ) (1 + ‖x‖) 0

Tactic:
simpa using hC
-- 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
f : 𝓢(E, F)
n : ℕ
C : ℝ
Cpos : 0 < C
hC :
  ∀ (x : E),
    HPow.hPow (β := ℕ) ‖x‖ 0 *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
          (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x) ≤
      C
⊢ ∃ (k : ℕ) (C : ℝ),
    ∀ (x : E),
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
          (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x) ≤
        C * (1 + ‖x‖) ^ k

Tactic:
exact ⟨0, C, by simpa using hC⟩
-- 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
f : E → F
h₁ : HasCompactSupport f
h₂ : ContDiff ℝ ∞ f
k n : ℕ
g : (x : E) → ℝ :=
  fun (x : E) ↦
    ‖x‖ ^ k * norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F) (iteratedFDeriv ℝ n f x)
⊢ Continuous (Y := ℝ) fun (x : E) ↦ ‖x‖ ^ k

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
f : E → F
h₁ : HasCompactSupport f
h₂ : ContDiff ℝ ∞ f
k n : ℕ
g : (x : E) → ℝ :=
  fun (x : E) ↦
    ‖x‖ ^ k * norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F) (iteratedFDeriv ℝ n f x)
apply :
  Continuous (Y := ℝ) fun (x : E) ↦
    norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F) (iteratedFDeriv ℝ n f x)
⊢ Continuous g

Tactic:
apply Continuous.mul (by fun_prop)

Premises used: Continuous.mul
-- 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
f : E → F
h₁ : HasCompactSupport f
h₂ : ContDiff ℝ ∞ f
k n : ℕ
g : (x : E) → ℝ :=
  fun (x : E) ↦
    ‖x‖ ^ k * norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F) (iteratedFDeriv ℝ n f x)
⊢ Continuous (Y := ℝ) fun (x : E) ↦
    norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F) (iteratedFDeriv ℝ n f x)

Tactic:
(h₂.of_le (mod_cast le_top)).continuous_iteratedFDeriv'.norm

Premises used: Continuous.norm, ContDiff.continuous_iteratedFDeriv', ContDiff.of_le
-- 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
f : E → F
h₁ : HasCompactSupport f
h₂ : ContDiff ℝ ∞ f
k n : ℕ
g : (x : E) → ℝ :=
  fun (x : E) ↦
    ‖x‖ ^ k * norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F) (iteratedFDeriv ℝ n f x)
⊢ Continuous g

Tactic:
have hg₁ : Continuous g := by
      apply Continuous.mul (by fun_prop)
      exact (h₂.of_le (mod_cast le_top)).continuous_iteratedFDeriv'.norm
-- 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
f : E → F
h₁ : HasCompactSupport f
h₂ : ContDiff ℝ ∞ f
k n : ℕ
g : (x : E) → ℝ :=
  fun (x : E) ↦
    ‖x‖ ^ k * norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F) (iteratedFDeriv ℝ n f x)
hg₁ : Continuous g
⊢ HasCompactSupport g

Tactic:
have hg₂ : HasCompactSupport g := (h₁.iteratedFDeriv _).norm.mul_left
-- 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
f : E → F
h₁ : HasCompactSupport f
h₂ : ContDiff ℝ ∞ f
k n : ℕ
g : (x : E) → ℝ :=
  fun (x : E) ↦
    ‖x‖ ^ k * norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F) (iteratedFDeriv ℝ n f x)
hg₁ : Continuous g
hg₂ : HasCompactSupport g
obtain :
  ∀ (x₀ : E) (hx₀ : ∀ (y : E), g y ≤ g x₀),
    ∃ (C : ℝ),
      ∀ (x : E),
        ‖x‖ ^ k *
            norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F) (iteratedFDeriv ℝ n f x) ≤
          C
⊢ ∃ (C : ℝ),
    ∀ (x : E),
      ‖x‖ ^ k *
          norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F) (iteratedFDeriv ℝ n f x) ≤
        C

Tactic:
obtain ⟨x₀, hx₀⟩ := hg₁.exists_forall_ge_of_hasCompactSupport hg₂

Premises used: Continuous.exists_forall_ge_of_hasCompactSupport
-- 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
f : E → F
h₁ : HasCompactSupport f
h₂ : ContDiff ℝ ∞ f
k n : ℕ
g : (x : E) → ℝ :=
  fun (x : E) ↦
    ‖x‖ ^ k * norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F) (iteratedFDeriv ℝ n f x)
hg₁ : Continuous g
hg₂ : HasCompactSupport g
x₀ : E
hx₀ : ∀ (y : E), g y ≤ g x₀
⊢ ∃ (C : ℝ),
    ∀ (x : E),
      ‖x‖ ^ k *
          norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F) (iteratedFDeriv ℝ n f x) ≤
        C

Tactic:
⟨g x₀, hx₀⟩

Premises used: Exists.intro
-- 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
f : E → F
h₁ : HasCompactSupport f
h₂ : ContDiff ℝ ∞ f
k n : ℕ
g : (x : E) → ℝ :=
  fun (x : E) ↦
    ‖x‖ ^ k * norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F) (iteratedFDeriv ℝ n f x)
hg₁ : Continuous g
hg₂ : HasCompactSupport g
x₀ : E
hx₀ : ∀ (y : E), g y ≤ g x₀
⊢ ∃ (C : ℝ),
    ∀ (x : E),
      ‖x‖ ^ k *
          norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F) (iteratedFDeriv ℝ n f x) ≤
        C

Tactic:
exact ⟨g x₀, hx₀⟩
-- 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 : NormedField 𝕜
inst_5 : NormedField 𝕜'
inst_6 : NormedAddCommGroup D
inst_7 : NormedSpace ℝ D
inst_8 : NormedSpace 𝕜 E
inst_9 : SMulCommClass ℝ 𝕜 E
inst_10 : NormedAddCommGroup G
inst_11 : NormedSpace ℝ G
inst_12 : NormedSpace 𝕜' G
inst_13 : SMulCommClass ℝ 𝕜' G
σ : 𝕜 →+* 𝕜'
A : 𝓢(D, E) → F → G
hadd : ∀ (f g : 𝓢(D, E)) (x : F), A (f + g) x = A f x + A g x
hsmul :
  ∀ (a : 𝕜) (f : 𝓢(D, E)) (x : F),
    A (a • f) x = HSMul.hSMul.{u_3, u_7, u_7} (α := 𝕜') ((σ : (a : 𝕜) → 𝕜') a : 𝕜') (A f x)
hsmooth : ∀ (f : 𝓢(D, E)), ContDiff ℝ ∞ (A f)
hbound :
  ∀ (n : ℕ × ℕ),
    ∃ (s : Finset (ℕ × ℕ)) (C : ℝ),
      0 ≤ C ∧
        ∀ (f : 𝓢(D, E)) (x : F),
          ‖x‖ ^ n.1 *
              norm (E := ContinuousMultilinearMap.{0, 0, u_6, u_7} ℝ (fun (i : Fin n.2) ↦ F) G)
                (iteratedFDeriv ℝ n.2 (A f) x) ≤
            HMul.hMul (β := ℝ) C ((s.sup (schwartzSeminormFamily 𝕜 D E) : (a : 𝓢(D, E)) → ℝ) f : ℝ)
f : 𝓢(D, E)
k n : ℕ
rcases :
  ∀ (s : Finset (ℕ × ℕ)) (C : ℝ),
    0 ≤ C →
      ∀
        (h :
          ∀ (f : 𝓢(D, E)) (x : F),
            ‖x‖ ^ (k, n).1 *
                norm (E := ContinuousMultilinearMap.{0, 0, u_6, u_7} ℝ (fun (i : Fin (k, n).2) ↦ F) G)
                  (iteratedFDeriv ℝ (k, n).2 (A f) x) ≤
              HMul.hMul (β := ℝ) C ((s.sup (schwartzSeminormFamily 𝕜 D E) : (a : 𝓢(D, E)) → ℝ) f : ℝ)),
        ∃ (C : ℝ),
          ∀ (x : F),
            ‖x‖ ^ k *
                norm (E := ContinuousMultilinearMap.{0, 0, u_6, u_7} ℝ (fun (i : Fin n) ↦ F) G)
                  (iteratedFDeriv ℝ n (A f) x) ≤
              C
⊢ ∃ (C : ℝ),
    ∀ (x : F),
      ‖x‖ ^ k *
          norm (E := ContinuousMultilinearMap.{0, 0, u_6, u_7} ℝ (fun (i : Fin n) ↦ F) G) (iteratedFDeriv ℝ n (A f) x) ≤
        C

Tactic:
rcases hbound ⟨k, n⟩ with ⟨s, C, _, h⟩

Premises used: Prod.mk