awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : RCLike 𝕜
inst_5 : NormedAddCommGroup D
inst_6 : NormedSpace ℝ D
inst_7 : NormedSpace 𝕜 F
K : ℝ≥0
g : D → E
hg : Function.HasTemperateGrowth g
h'g : AntilipschitzWith K g
refine : ∀ (x : D), ‖x‖ ≤ (↑K : ℝ) * max 1 ‖g 0‖ * HPow.hPow (β := ℕ) (1 + ‖g x‖) 1
⊢ 𝓢(E, F) →L[𝕜] 𝓢(D, F)

Tactic:
refine compCLM 𝕜 hg ⟨1, K * max 1 ‖g 0‖, fun x ↦ ?_⟩

Premises used: Norm.norm, HMul.hMul, SchwartzMap.compCLM, Max.max, Exists.intro, OfNat.ofNat, NNReal.toReal
-- 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 : RCLike 𝕜
inst_5 : NormedAddCommGroup D
inst_6 : NormedSpace ℝ D
inst_7 : NormedSpace 𝕜 F
K : ℝ≥0
g : D → E
hg : Function.HasTemperateGrowth g
h'g : AntilipschitzWith K g
x : D
rw : dist x 0 ≤ (↑K : ℝ) * dist (g x) (g 0)
⊢ ‖x‖ ≤ (↑K : ℝ) * ‖g x - g 0‖

Tactic:
rw [← dist_zero_right, ← dist_eq_norm]

Premises used: dist_eq_norm, dist_zero_right
-- 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 : RCLike 𝕜
inst_5 : NormedAddCommGroup D
inst_6 : NormedSpace ℝ D
inst_7 : NormedSpace 𝕜 F
K : ℝ≥0
g : D → E
hg : Function.HasTemperateGrowth g
h'g : AntilipschitzWith K g
x : D
⊢ dist x 0 ≤ (↑K : ℝ) * dist (g x) (g 0)

Tactic:
apply h'g.le_mul_dist

Premises used: AntilipschitzWith.le_mul_dist
-- 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 : RCLike 𝕜
inst_5 : NormedAddCommGroup D
inst_6 : NormedSpace ℝ D
inst_7 : NormedSpace 𝕜 F
K : ℝ≥0
g : D → E
hg : Function.HasTemperateGrowth g
h'g : AntilipschitzWith K g
x : D
hbc : ‖g x - g 0‖ ≤ ‖g x‖ + ‖g 0‖
⊢ (↑K : ℝ) * ‖g x - g 0‖ ≤ (↑K : ℝ) * (‖g x‖ + ‖g 0‖)

Tactic:
gcongr
-- 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 : RCLike 𝕜
inst_5 : NormedAddCommGroup D
inst_6 : NormedSpace ℝ D
inst_7 : NormedSpace 𝕜 F
K : ℝ≥0
g : D → E
hg : Function.HasTemperateGrowth g
h'g : AntilipschitzWith K g
x : D
⊢ ‖g x - g 0‖ ≤ ‖g x‖ + ‖g 0‖

Tactic:
norm_sub_le _ _

Premises used: norm_sub_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
inst_4 : RCLike 𝕜
inst_5 : NormedAddCommGroup D
inst_6 : NormedSpace ℝ D
inst_7 : NormedSpace 𝕜 F
K : ℝ≥0
g : D → E
hg : Function.HasTemperateGrowth g
h'g : AntilipschitzWith K g
x : D
⊢ ‖g x - g 0‖ ≤ ‖g x‖ + ‖g 0‖

Tactic:
exact norm_sub_le _ _

Premises used: norm_sub_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
inst_4 : RCLike 𝕜
inst_5 : NormedAddCommGroup D
inst_6 : NormedSpace ℝ D
inst_7 : NormedSpace 𝕜 F
K : ℝ≥0
g : D → E
hg : Function.HasTemperateGrowth g
h'g : AntilipschitzWith K g
x : D
hbc : ‖g 0‖ ≤ max 1 ‖g 0‖
⊢ (↑K : ℝ) * (‖g x‖ + ‖g 0‖) ≤ (↑K : ℝ) * (‖g x‖ + max 1 ‖g 0‖)

Tactic:
gcongr
-- 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 : RCLike 𝕜
inst_5 : NormedAddCommGroup D
inst_6 : NormedSpace ℝ D
inst_7 : NormedSpace 𝕜 F
K : ℝ≥0
g : D → E
hg : Function.HasTemperateGrowth g
h'g : AntilipschitzWith K g
x : D
⊢ ‖g 0‖ ≤ max 1 ‖g 0‖

Tactic:
le_max_right _ _

Premises used: le_max_right
-- 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 : RCLike 𝕜
inst_5 : NormedAddCommGroup D
inst_6 : NormedSpace ℝ D
inst_7 : NormedSpace 𝕜 F
K : ℝ≥0
g : D → E
hg : Function.HasTemperateGrowth g
h'g : AntilipschitzWith K g
x : D
⊢ ‖g 0‖ ≤ max 1 ‖g 0‖

Tactic:
exact le_max_right _ _

Premises used: le_max_right
-- 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 : RCLike 𝕜
inst_5 : NormedAddCommGroup D
inst_6 : NormedSpace ℝ D
inst_7 : NormedSpace 𝕜 F
K : ℝ≥0
g : D → E
hg : Function.HasTemperateGrowth g
h'g : AntilipschitzWith K g
x : D
simp : (↑K : ℝ) * ‖g x‖ ≤ (↑K : ℝ) * max 1 ‖g 0‖ * ‖g x‖
⊢ (↑K : ℝ) * (‖g x‖ + max 1 ‖g 0‖) ≤ (↑K : ℝ) * max 1 ‖g 0‖ * HPow.hPow (β := ℕ) (1 + ‖g x‖) 1

Tactic:
simp only [mul_add, add_comm (K * ‖g x‖), pow_one, mul_one, add_le_add_iff_left]

Premises used: Norm.norm, HMul.hMul, add_le_add_iff_left, add_comm, pow_one, mul_add, mul_one, NNReal.toReal
-- 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 : RCLike 𝕜
inst_5 : NormedAddCommGroup D
inst_6 : NormedSpace ℝ D
inst_7 : NormedSpace 𝕜 F
K : ℝ≥0
g : D → E
hg : Function.HasTemperateGrowth g
h'g : AntilipschitzWith K g
x : D
hbc : (↑K : ℝ) ≤ (↑K : ℝ) * max 1 ‖g 0‖
⊢ (↑K : ℝ) * ‖g x‖ ≤ (↑K : ℝ) * max 1 ‖g 0‖ * ‖g x‖

Tactic:
gcongr
-- 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 : RCLike 𝕜
inst_5 : NormedAddCommGroup D
inst_6 : NormedSpace ℝ D
inst_7 : NormedSpace 𝕜 F
K : ℝ≥0
g : D → E
hg : Function.HasTemperateGrowth g
h'g : AntilipschitzWith K g
x : D
⊢ 0 ≤ (↑K : ℝ)

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 : RCLike 𝕜
inst_5 : NormedAddCommGroup D
inst_6 : NormedSpace ℝ D
inst_7 : NormedSpace 𝕜 F
K : ℝ≥0
g : D → E
hg : Function.HasTemperateGrowth g
h'g : AntilipschitzWith K g
x : D
⊢ (↑K : ℝ) ≤ (↑K : ℝ) * max 1 ‖g 0‖

Tactic:
exact le_mul_of_one_le_right (by positivity) (le_max_left _ _)

Premises used: le_mul_of_one_le_right, le_max_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
inst_4 : RCLike 𝕜
inst_5 : NormedAddCommGroup D
inst_6 : NormedSpace ℝ D
inst_7 : NormedSpace 𝕜 F
K : ℝ≥0
g : D → E
hg : Function.HasTemperateGrowth g
h'g : AntilipschitzWith K g
x : D
K₁ : ‖x‖ ≤ (↑K : ℝ) * ‖g x - g 0‖
K₂ : (↑K : ℝ) * ‖g x - g 0‖ ≤ (↑K : ℝ) * (‖g x‖ + ‖g 0‖)
K₃ : (↑K : ℝ) * (‖g x‖ + ‖g 0‖) ≤ (↑K : ℝ) * (‖g x‖ + max 1 ‖g 0‖)
K₄ : (↑K : ℝ) * (‖g x‖ + max 1 ‖g 0‖) ≤ (↑K : ℝ) * max 1 ‖g 0‖ * HPow.hPow (β := ℕ) (1 + ‖g x‖) 1
⊢ ‖x‖ ≤ (↑K : ℝ) * max 1 ‖g 0‖ * HPow.hPow (β := ℕ) (1 + ‖g x‖) 1

Tactic:
calc
  ‖x‖ ≤ K * ‖g x - g 0‖ := by
    rw [← dist_zero_right, ← dist_eq_norm]
    apply h'g.le_mul_dist
  _ ≤ K * (‖g x‖ + ‖g 0‖) := by
    gcongr
    exact norm_sub_le _ _
  _ ≤ K * (‖g x‖ + max 1 ‖g 0‖) := by
    gcongr
    exact le_max_right _ _
  _ ≤ (K * max 1 ‖g 0‖ : ℝ) * (1 + ‖g x‖) ^ 1 := by
    simp only [mul_add, add_comm (K * ‖g x‖), pow_one, mul_one, add_le_add_iff_left]
    gcongr
    exact le_mul_of_one_le_right (by positivity) (le_max_left _ _)

Premises used: Norm.norm, HMul.hMul, HAdd.hAdd, Max.max, OfNat.ofNat, NNReal.toReal
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
𝕜 : Type u_2
D : Type u_4
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 : RCLike 𝕜
inst_5 : NormedAddCommGroup D
inst_6 : NormedSpace ℝ D
inst_7 : NormedSpace 𝕜 F
K : ℝ≥0
g : D → E
hg : Function.HasTemperateGrowth g
h'g : AntilipschitzWith K g
f : 𝓢(E, F)
⊢ Eq (α := (a : D) → F) (⇑((compCLMOfAntilipschitz 𝕜 hg h'g : (a : 𝓢(E, F)) → 𝓢(D, F)) f : 𝓢(D, F)) : (a : D) → F)
    ((⇑f : (a : E) → 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
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : RCLike 𝕜
inst_5 : NormedAddCommGroup D
inst_6 : NormedSpace ℝ D
inst_7 : NormedSpace 𝕜 F
g : D ≃L[ℝ] E
f : 𝓢(E, F)
⊢ Eq (α := (a : D) → F) (⇑((compCLMOfContinuousLinearEquiv 𝕜 g : (a : 𝓢(E, F)) → 𝓢(D, F)) f : 𝓢(D, F)) : (a : D) → F)
    (Function.comp.{u_4 + 1, u_5 + 1, u_6 + 1} (β := E) (⇑f : (a : E) → F) (⇑g : (a : D) → E))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
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 : RCLike 𝕜
inst_5 : NormedAddCommGroup D
inst_6 : NormedSpace ℝ D
inst_7 : NormedSpace 𝕜 F
inst_8 : NontriviallyNormedField 𝕜'
inst_9 : NormedAlgebra ℝ 𝕜'
inst_10 : NormedSpace 𝕜' F
u : D → 𝕜'
hu : Function.HasTemperateGrowth u
g : D ≃L[ℝ] E
f : 𝓢(E, F)
h :
  ∀ (x : D),
    Eq.{u_6 + 1} (α := F)
      (((((smulLeftCLM F u : 𝓢(D, F) →L[𝕜'] 𝓢(D, F)) : (a : 𝓢(D, F)) → 𝓢(D, F))
                ((compCLMOfContinuousLinearEquiv 𝕜 g : (a : 𝓢(E, F)) → 𝓢(D, F)) f) :
              𝓢(D, F)) :
            (a : D) → F)
          x :
        F)
      ((((compCLMOfContinuousLinearEquiv 𝕜 g : (a : 𝓢(E, F)) → 𝓢(D, F))
                (((smulLeftCLM F (u ∘ (⇑g.symm : (a : E) → D)) : 𝓢(E, F) →L[𝕜'] 𝓢(E, F)) : (a : 𝓢(E, F)) → 𝓢(E, F)) f) :
              𝓢(D, F)) :
            (a : D) → F)
          x :
        F)
⊢ Eq (α := 𝓢(D, F))
    (((smulLeftCLM F u : 𝓢(D, F) →L[𝕜'] 𝓢(D, F)) : (a : 𝓢(D, F)) → 𝓢(D, F))
        ((compCLMOfContinuousLinearEquiv 𝕜 g : (a : 𝓢(E, F)) → 𝓢(D, F)) f) :
      𝓢(D, F))
    ((compCLMOfContinuousLinearEquiv 𝕜 g : (a : 𝓢(E, F)) → 𝓢(D, F))
        (((smulLeftCLM F (u ∘ (⇑g.symm : (a : E) → D)) : 𝓢(E, F) →L[𝕜'] 𝓢(E, F)) : (a : 𝓢(E, F)) → 𝓢(E, F)) f) :
      𝓢(D, F))

Tactic:
ext x
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
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 : RCLike 𝕜
inst_5 : NormedAddCommGroup D
inst_6 : NormedSpace ℝ D
inst_7 : NormedSpace 𝕜 F
inst_8 : NontriviallyNormedField 𝕜'
inst_9 : NormedAlgebra ℝ 𝕜'
inst_10 : NormedSpace 𝕜' F
u : D → 𝕜'
hu : Function.HasTemperateGrowth u
g : D ≃L[ℝ] E
f : 𝓢(E, F)
x : D
⊢ Function.HasTemperateGrowth.{u_5, u_3} (E := E) (u ∘ (⇑g.symm : (a : E) → D))

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
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 : RCLike 𝕜
inst_5 : NormedAddCommGroup D
inst_6 : NormedSpace ℝ D
inst_7 : NormedSpace 𝕜 F
inst_8 : NontriviallyNormedField 𝕜'
inst_9 : NormedAlgebra ℝ 𝕜'
inst_10 : NormedSpace 𝕜' F
u : D → 𝕜'
hu : Function.HasTemperateGrowth u
g : D ≃L[ℝ] E
f : 𝓢(E, F)
x : D
⊢ Function.HasTemperateGrowth.{u_5, u_3} (E := E) (u ∘ (⇑g.symm : (a : E) → D))

Tactic:
have hu' : (u ∘ g.symm).HasTemperateGrowth := by fun_prop
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
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 : RCLike 𝕜
inst_5 : NormedAddCommGroup D
inst_6 : NormedSpace ℝ D
inst_7 : NormedSpace 𝕜 F
inst_8 : NontriviallyNormedField 𝕜'
inst_9 : NormedAlgebra ℝ 𝕜'
inst_10 : NormedSpace 𝕜' F
u : D → 𝕜'
hu : Function.HasTemperateGrowth u
g : D ≃L[ℝ] E
f : 𝓢(E, F)
x : D
hu' : Function.HasTemperateGrowth.{u_5, u_3} (E := E) (u ∘ (⇑g.symm : (a : E) → D))
⊢ Eq.{u_6 + 1} (α := F)
    (((((smulLeftCLM F u : 𝓢(D, F) →L[𝕜'] 𝓢(D, F)) : (a : 𝓢(D, F)) → 𝓢(D, F))
              ((compCLMOfContinuousLinearEquiv 𝕜 g : (a : 𝓢(E, F)) → 𝓢(D, F)) f) :
            𝓢(D, F)) :
          (a : D) → F)
        x :
      F)
    ((((compCLMOfContinuousLinearEquiv 𝕜 g : (a : 𝓢(E, F)) → 𝓢(D, F))
              (((smulLeftCLM F (u ∘ (⇑g.symm : (a : E) → D)) : 𝓢(E, F) →L[𝕜'] 𝓢(E, F)) : (a : 𝓢(E, F)) → 𝓢(E, F)) f) :
            𝓢(D, F)) :
          (a : D) → F)
        x :
      F)

Tactic:
simp [smulLeftCLM_apply_apply hu, smulLeftCLM_apply_apply hu']

Premises used: SchwartzMap.smulLeftCLM_apply_apply
-- 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 : RCLike 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : NormedAddCommGroup G
inst_7 : NormedSpace ℝ G
inst_8 : NormedSpace 𝕜 G
inst_9 : NormedAddCommGroup H
inst_10 : NormedSpace ℝ H
inst_11 : NormedSpace 𝕜 H
L : F →L[𝕜] G
x x_1 : 𝓢(E, F)
x_2 : E
⊢ (fun (f : 𝓢(E, F)) ↦
        (Function.comp.{u_5 + 1, u_6 + 1, u_7 + 1} (β := F) (⇑L : (a : F) → G) (⇑f : (a : E) → F) : E → G))
      (x + x_1) x_2 =
    HAdd.hAdd (α := G)
      ((fun (f : 𝓢(E, F)) ↦
          (Function.comp.{u_5 + 1, u_6 + 1, u_7 + 1} (β := F) (⇑L : (a : F) → G) (⇑f : (a : E) → F) : E → G))
        x x_2)
      ((fun (f : 𝓢(E, F)) ↦
          (Function.comp.{u_5 + 1, u_6 + 1, u_7 + 1} (β := F) (⇑L : (a : F) → G) (⇑f : (a : E) → F) : E → G))
        x_1 x_2)

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 : RCLike 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : NormedAddCommGroup G
inst_7 : NormedSpace ℝ G
inst_8 : NormedSpace 𝕜 G
inst_9 : NormedAddCommGroup H
inst_10 : NormedSpace ℝ H
inst_11 : NormedSpace 𝕜 H
L : F →L[𝕜] G
x : 𝕜
x_1 : 𝓢(E, F)
x_2 : E
⊢ (fun (f : 𝓢(E, F)) ↦
        (Function.comp.{u_5 + 1, u_6 + 1, u_7 + 1} (β := F) (⇑L : (a : F) → G) (⇑f : (a : E) → F) : E → G))
      (x • x_1) x_2 =
    HSMul.hSMul (α := 𝕜) (β := G) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜)
      ((fun (f : 𝓢(E, F)) ↦
          (Function.comp.{u_5 + 1, u_6 + 1, u_7 + 1} (β := F) (⇑L : (a : F) → G) (⇑f : (a : E) → F) : E → G))
        x_1 x_2)

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 : RCLike 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : NormedAddCommGroup G
inst_7 : NormedSpace ℝ G
inst_8 : NormedSpace 𝕜 G
inst_9 : NormedAddCommGroup H
inst_10 : NormedSpace ℝ H
inst_11 : NormedSpace 𝕜 H
L : F →L[𝕜] G
k n : ℕ
⊢ 0 ≤ ‖L‖

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 : RCLike 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : NormedAddCommGroup G
inst_7 : NormedSpace ℝ G
inst_8 : NormedSpace 𝕜 G
inst_9 : NormedAddCommGroup H
inst_10 : NormedSpace ℝ H
inst_11 : NormedSpace 𝕜 H
L : F →L[𝕜] G
k n : ℕ
right :
  ∀ (f : 𝓢(E, F)) (x : E),
    ‖x‖ ^ (k, n).1 *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_7} ℝ (fun (i : Fin (k, n).2) ↦ E) G)
          (iteratedFDeriv ℝ (k, n).2
            ((fun (f : 𝓢(E, F)) ↦
                (Function.comp.{u_5 + 1, u_6 + 1, u_7 + 1} (β := F) (⇑L : (a : F) → G) (⇑f : (a : E) → F) : E → G))
              f)
            x) ≤
      HMul.hMul (β := ℝ) ‖L‖ ((Finset.sup {(k, n)} (schwartzSeminormFamily 𝕜 E F) : (a : 𝓢(E, F)) → ℝ) f : ℝ)
⊢ ∃ (s : Finset (ℕ × ℕ)) (C : ℝ),
    0 ≤ C ∧
      ∀ (f : 𝓢(E, F)) (x : E),
        ‖x‖ ^ (k, n).1 *
            norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_7} ℝ (fun (i : Fin (k, n).2) ↦ E) G)
              (iteratedFDeriv ℝ (k, n).2
                ((fun (f : 𝓢(E, F)) ↦
                    (Function.comp.{u_5 + 1, u_6 + 1, u_7 + 1} (β := F) (⇑L : (a : F) → G) (⇑f : (a : E) → F) : E → G))
                  f)
                x) ≤
          HMul.hMul (β := ℝ) C ((s.sup (schwartzSeminormFamily 𝕜 E F) : (a : 𝓢(E, F)) → ℝ) f : ℝ)

Tactic:
use {⟨k, n⟩}, ‖L‖, by 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 : RCLike 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : NormedAddCommGroup G
inst_7 : NormedSpace ℝ G
inst_8 : NormedSpace 𝕜 G
inst_9 : NormedAddCommGroup H
inst_10 : NormedSpace ℝ H
inst_11 : NormedSpace 𝕜 H
L : F →L[𝕜] G
k n : ℕ
f : 𝓢(E, F)
x : E
right :
  ‖x‖ ^ k *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_7} ℝ (fun (i : Fin n) ↦ E) G)
        (iteratedFDeriv ℝ n (Function.comp.{u_5 + 1, u_6 + 1, u_7 + 1} (β := F) (⇑L : (a : F) → G) (⇑f : (a : E) → F))
          x) ≤
    HMul.hMul (β := ℝ) ‖L‖ ((SchwartzMap.seminorm 𝕜 k n : (a : 𝓢(E, F)) → ℝ) f : ℝ)
⊢ ‖x‖ ^ (k, n).1 *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_7} ℝ (fun (i : Fin (k, n).2) ↦ E) G)
        (iteratedFDeriv ℝ (k, n).2
          ((fun (f : 𝓢(E, F)) ↦
              (Function.comp.{u_5 + 1, u_6 + 1, u_7 + 1} (β := F) (⇑L : (a : F) → G) (⇑f : (a : E) → F) : E → G))
            f)
          x) ≤
    HMul.hMul (β := ℝ) ‖L‖ ((Finset.sup {(k, n)} (schwartzSeminormFamily 𝕜 E F) : (a : 𝓢(E, F)) → ℝ) f : ℝ)

Tactic:
simp only [Finset.sup_singleton, schwartzSeminormFamily_apply]

Premises used: Finset.sup_singleton, SchwartzMap.schwartzSeminormFamily_apply
-- 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 : RCLike 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : NormedAddCommGroup G
inst_7 : NormedSpace ℝ G
inst_8 : NormedSpace 𝕜 G
inst_9 : NormedAddCommGroup H
inst_10 : NormedSpace ℝ H
inst_11 : NormedSpace 𝕜 H
L : F →L[𝕜] G
k n : ℕ
f : 𝓢(E, F)
x : E
e_a :
  Eq (α := ContinuousMultilinearMap.{0, 0, u_5, u_7} ℝ (fun (i : Fin n) ↦ E) G)
    (iteratedFDeriv ℝ n (Function.comp.{u_5 + 1, u_6 + 1, u_7 + 1} (β := F) (⇑L : (a : F) → G) (⇑f : (a : E) → F)) x)
    (ContinuousLinearMap.compContinuousMultilinearMap (M₁ := fun (i : Fin n) ↦ E)
      (ContinuousLinearMap.restrictScalars ℝ L) (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x))
⊢ ‖x‖ ^ k *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_7} ℝ (fun (i : Fin n) ↦ E) G)
        (iteratedFDeriv ℝ n (Function.comp.{u_5 + 1, u_6 + 1, u_7 + 1} (β := F) (⇑L : (a : F) → G) (⇑f : (a : E) → F))
          x) =
    ‖x‖ ^ k *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_7} ℝ (fun (i : Fin n) ↦ E) G)
        (ContinuousLinearMap.compContinuousMultilinearMap (M₁ := fun (i : Fin n) ↦ E)
          (ContinuousLinearMap.restrictScalars ℝ L) (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x))

Tactic:
congr
-- 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 : RCLike 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : NormedAddCommGroup G
inst_7 : NormedSpace ℝ G
inst_8 : NormedSpace 𝕜 G
inst_9 : NormedAddCommGroup H
inst_10 : NormedSpace ℝ H
inst_11 : NormedSpace 𝕜 H
L : F →L[𝕜] G
k n : ℕ
f : 𝓢(E, F)
x : E
⊢ Eq (α := ContinuousMultilinearMap.{0, 0, u_5, u_7} ℝ (fun (i : Fin n) ↦ E) G)
    (iteratedFDeriv ℝ n (Function.comp.{u_5 + 1, u_6 + 1, u_7 + 1} (β := F) (⇑L : (a : F) → G) (⇑f : (a : E) → F)) x)
    (ContinuousLinearMap.compContinuousMultilinearMap (M₁ := fun (i : Fin n) ↦ E)
      (ContinuousLinearMap.restrictScalars ℝ L) (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x))

Tactic:
(L.restrictScalars ℝ).iteratedFDeriv_comp_left f.smooth'.contDiffAt (mod_cast le_top)

Premises used: Real, ContinuousLinearMap.restrictScalars, WithTop.coe_le_coe._simp_1, cast, le_top, SchwartzMap.smooth', Eq.symm, ContinuousLinearMap.iteratedFDeriv_comp_left, ContDiff.contDiffAt
-- 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 : RCLike 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : NormedAddCommGroup G
inst_7 : NormedSpace ℝ G
inst_8 : NormedSpace 𝕜 G
inst_9 : NormedAddCommGroup H
inst_10 : NormedSpace ℝ H
inst_11 : NormedSpace 𝕜 H
L : F →L[𝕜] G
k n : ℕ
f : 𝓢(E, F)
x : E
⊢ Eq (α := ContinuousMultilinearMap.{0, 0, u_5, u_7} ℝ (fun (i : Fin n) ↦ E) G)
    (iteratedFDeriv ℝ n (Function.comp.{u_5 + 1, u_6 + 1, u_7 + 1} (β := F) (⇑L : (a : F) → G) (⇑f : (a : E) → F)) x)
    (ContinuousLinearMap.compContinuousMultilinearMap (M₁ := fun (i : Fin n) ↦ E)
      (ContinuousLinearMap.restrictScalars ℝ L) (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x))

Tactic:
exact (L.restrictScalars ℝ).iteratedFDeriv_comp_left f.smooth'.contDiffAt (mod_cast le_top)

Premises used: Real, ContinuousLinearMap.restrictScalars, SchwartzMap.smooth', ContinuousLinearMap.iteratedFDeriv_comp_left, ContDiff.contDiffAt