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 : 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 : ℕ
s : Finset (ℕ × ℕ)
C : ℝ
left : 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

Tactic:
⟨C * (s.sup (schwartzSeminormFamily 𝕜 D E)) f, h f⟩

Premises used: HMul.hMul, schwartzSeminormFamily, Exists.intro, Finset.sup, 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 : 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 : ℕ
s : Finset (ℕ × ℕ)
C : ℝ
left : 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

Tactic:
exact ⟨C * (s.sup (schwartzSeminormFamily 𝕜 D E)) f, h f⟩
-- 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
σ : 𝕜 →+* 𝕜'
inst_14 : RingHomIsometric σ
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 : ℝ)
⊢ Continuous (X := 𝓢(D, E)) (Y := 𝓢(F, G)) (⇑(mkLM A hadd hsmul hsmooth hbound) : (a : 𝓢(D, E)) → 𝓢(F, G))

Tactic:
WithSeminorms.continuous_of_isBounded (schwartz_withSeminorms 𝕜 D E)
        (schwartz_withSeminorms 𝕜' F G) _ fun n => ?_

Premises used: schwartz_withSeminorms, WithSeminorms.continuous_of_isBounded
-- 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
σ : 𝕜 →+* 𝕜'
inst_14 : RingHomIsometric σ
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 : ℝ)
𝕜₁ :
  ∀ (n : ℕ × ℕ),
    ∃ (s : Finset (ℕ × ℕ)) (C : ℝ≥0),
      Seminorm.comp (schwartzSeminormFamily 𝕜' F G n) (mkLM A hadd hsmul hsmooth hbound) ≤
        HSMul.hSMul (β := Seminorm 𝕜 𝓢(D, E)) C (s.sup (schwartzSeminormFamily 𝕜 D E))
⊢ Continuous (X := 𝓢(D, E)) (Y := 𝓢(F, G)) (⇑(mkLM A hadd hsmul hsmooth hbound) : (a : 𝓢(D, E)) → 𝓢(F, G))

Tactic:
refine
      WithSeminorms.continuous_of_isBounded (schwartz_withSeminorms 𝕜 D E)
        (schwartz_withSeminorms 𝕜' F G) _ fun n => ?_

Premises used: schwartz_withSeminorms, WithSeminorms.continuous_of_isBounded
-- 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
σ : 𝕜 →+* 𝕜'
inst_14 : RingHomIsometric σ
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 : ℝ)
n : ℕ × ℕ
rcases :
  ∀ (s : Finset (ℕ × ℕ)) (C : ℝ) (hC : 0 ≤ C)
    (h :
      ∀ (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 : ℝ)),
    ∃ (s : Finset (ℕ × ℕ)) (C : ℝ≥0),
      Seminorm.comp (schwartzSeminormFamily 𝕜' F G n) (mkLM A hadd hsmul hsmooth hbound) ≤
        HSMul.hSMul (β := Seminorm 𝕜 𝓢(D, E)) C (s.sup (schwartzSeminormFamily 𝕜 D E))
⊢ ∃ (s : Finset (ℕ × ℕ)) (C : ℝ≥0),
    Seminorm.comp (schwartzSeminormFamily 𝕜' F G n) (mkLM A hadd hsmul hsmooth hbound) ≤
      HSMul.hSMul (β := Seminorm 𝕜 𝓢(D, E)) C (s.sup (schwartzSeminormFamily 𝕜 D E))

Tactic:
rcases hbound n with ⟨s, C, hC, h⟩
-- 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
σ : 𝕜 →+* 𝕜'
inst_14 : RingHomIsometric σ
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 : ℝ)
n : ℕ × ℕ
s : Finset (ℕ × ℕ)
C : ℝ
hC : 0 ≤ C
h :
  ∀ (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 : ℝ)
⊢ ∃ (s : Finset (ℕ × ℕ)) (C : ℝ≥0),
    Seminorm.comp (schwartzSeminormFamily 𝕜' F G n) (mkLM A hadd hsmul hsmooth hbound) ≤
      HSMul.hSMul (β := Seminorm 𝕜 𝓢(D, E)) C (s.sup (schwartzSeminormFamily 𝕜 D E))

Tactic:
⟨s, ⟨C, hC⟩, fun f => ?_⟩

Premises used: Subtype.mk, 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
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
σ : 𝕜 →+* 𝕜'
inst_14 : RingHomIsometric σ
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 : ℝ)
n : ℕ × ℕ
s : Finset (ℕ × ℕ)
C : ℝ
hC : 0 ≤ C
h :
  ∀ (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 : ℝ)
refine :
  ∀ (f : 𝓢(D, E)),
    LE.le (α := (fun (a : 𝓢(D, E)) ↦ ℝ) f)
      ((fun (f : Seminorm 𝕜 𝓢(D, E)) ↦ ((⇑f : (a : 𝓢(D, E)) → ℝ) : (a : 𝓢(D, E)) → ℝ))
        (Seminorm.comp (schwartzSeminormFamily 𝕜' F G n) (mkLM A hadd hsmul hsmooth hbound)) f)
      ((fun (f : Seminorm 𝕜 𝓢(D, E)) ↦ ((⇑f : (a : 𝓢(D, E)) → ℝ) : (a : 𝓢(D, E)) → ℝ))
        (HSMul.hSMul (β := Seminorm 𝕜 𝓢(D, E)) (Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) C hC)
          (s.sup (schwartzSeminormFamily 𝕜 D E)))
        f)
⊢ ∃ (s : Finset (ℕ × ℕ)) (C : ℝ≥0),
    Seminorm.comp (schwartzSeminormFamily 𝕜' F G n) (mkLM A hadd hsmul hsmooth hbound) ≤
      HSMul.hSMul (β := Seminorm 𝕜 𝓢(D, E)) C (s.sup (schwartzSeminormFamily 𝕜 D E))

Tactic:
refine ⟨s, ⟨C, hC⟩, fun f => ?_⟩
-- 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
σ : 𝕜 →+* 𝕜'
inst_14 : RingHomIsometric σ
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 : ℝ)
n : ℕ × ℕ
s : Finset (ℕ × ℕ)
C : ℝ
hC : 0 ≤ C
h :
  ∀ (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)
⊢ LE.le (α := ℝ) 0
    ((fun (f : Seminorm 𝕜 𝓢(D, E)) ↦ ((⇑f : (a : 𝓢(D, E)) → ℝ) : (a : 𝓢(D, E)) → ℝ))
      (HSMul.hSMul (β := Seminorm 𝕜 𝓢(D, E)) (Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) C hC)
        (s.sup (schwartzSeminormFamily 𝕜 D E)))
      f)

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 : 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
σ : 𝕜 →+* 𝕜'
inst_14 : RingHomIsometric σ
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 : ℝ)
n : ℕ × ℕ
s : Finset (ℕ × ℕ)
C : ℝ
hC : 0 ≤ C
h :
  ∀ (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)
⊢ LE.le (α := (fun (a : 𝓢(D, E)) ↦ ℝ) f)
    ((fun (f : Seminorm 𝕜 𝓢(D, E)) ↦ ((⇑f : (a : 𝓢(D, E)) → ℝ) : (a : 𝓢(D, E)) → ℝ))
      (Seminorm.comp (schwartzSeminormFamily 𝕜' F G n) (mkLM A hadd hsmul hsmooth hbound)) f)
    ((fun (f : Seminorm 𝕜 𝓢(D, E)) ↦ ((⇑f : (a : 𝓢(D, E)) → ℝ) : (a : 𝓢(D, E)) → ℝ))
      (HSMul.hSMul (β := Seminorm 𝕜 𝓢(D, E)) (Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) C hC)
        (s.sup (schwartzSeminormFamily 𝕜 D E)))
      f)

Tactic:
exact (mkLM A hadd hsmul hsmooth hbound f).seminorm_le_bound 𝕜' n.1 n.2 (by positivity) (h f)

Premises used: SchwartzMap.seminorm_le_bound, Prod.fst, SchwartzMap.mkLM, Prod.snd, 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 : 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
σ : 𝕜 →+* 𝕜'
inst_14 : RingHomIsometric σ
A : 𝓢(D, E) → G
hadd : ∀ (f g : 𝓢(D, E)), A (f + g) = A f + A g
hsmul : ∀ (a : 𝕜) (f : 𝓢(D, E)), A (a • f) = HSMul.hSMul.{u_3, u_7, u_7} (α := 𝕜') ((σ : (a : 𝕜) → 𝕜') a : 𝕜') (A f)
hbound :
  ∃ (s : Finset (ℕ × ℕ)) (C : ℝ),
    0 ≤ C ∧
      ∀ (f : 𝓢(D, E)), ‖A f‖ ≤ HMul.hMul (β := ℝ) C ((s.sup (schwartzSeminormFamily 𝕜 D E) : (a : 𝓢(D, E)) → ℝ) f : ℝ)
f : 𝓢(D, E) →ₛₗ[σ] G := { toFun := fun (x : 𝓢(D, E)) ↦ A x, map_add' := hadd, map_smul' := hsmul }
change :
  Continuous (X := 𝓢(D, E)) (Y := G)
    (⇑{ toFun := fun (x : 𝓢(D, E)) ↦ A x, map_add' := hadd, map_smul' := hsmul } : (a : 𝓢(D, E)) → G)
⊢ Continuous f.toFun

Tactic:
change Continuous (LinearMap.mk _ _)

Premises used: Continuous, LinearMap.mk, 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 : 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
σ : 𝕜 →+* 𝕜'
inst_14 : RingHomIsometric σ
A : 𝓢(D, E) → G
hadd : ∀ (f g : 𝓢(D, E)), A (f + g) = A f + A g
hsmul : ∀ (a : 𝕜) (f : 𝓢(D, E)), A (a • f) = HSMul.hSMul.{u_3, u_7, u_7} (α := 𝕜') ((σ : (a : 𝕜) → 𝕜') a : 𝕜') (A f)
hbound :
  ∃ (s : Finset (ℕ × ℕ)) (C : ℝ),
    0 ≤ C ∧
      ∀ (f : 𝓢(D, E)), ‖A f‖ ≤ HMul.hMul (β := ℝ) C ((s.sup (schwartzSeminormFamily 𝕜 D E) : (a : 𝓢(D, E)) → ℝ) f : ℝ)
f : 𝓢(D, E) →ₛₗ[σ] G := { toFun := fun (x : 𝓢(D, E)) ↦ A x, map_add' := hadd, map_smul' := hsmul }
hf :
  ∃ (s : Finset (ℕ × ℕ)) (C : ℝ≥0),
    Seminorm.comp (σ₁₂ := σ) (normSeminorm 𝕜' G)
        { toFun := fun (x : 𝓢(D, E)) ↦ A x, map_add' := hadd, map_smul' := hsmul } ≤
      HSMul.hSMul (β := Seminorm 𝕜 𝓢(D, E)) C (s.sup (schwartzSeminormFamily 𝕜 D E))
⊢ Continuous (X := 𝓢(D, E)) (Y := G)
    (⇑{ toFun := fun (x : 𝓢(D, E)) ↦ A x, map_add' := hadd, map_smul' := hsmul } : (a : 𝓢(D, E)) → G)

Tactic:
apply WithSeminorms.continuous_normedSpace_rng G (schwartz_withSeminorms 𝕜 D E)

Premises used: schwartz_withSeminorms, WithSeminorms.continuous_normedSpace_rng
-- 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
σ : 𝕜 →+* 𝕜'
inst_14 : RingHomIsometric σ
A : 𝓢(D, E) → G
hadd : ∀ (f g : 𝓢(D, E)), A (f + g) = A f + A g
hsmul : ∀ (a : 𝕜) (f : 𝓢(D, E)), A (a • f) = HSMul.hSMul.{u_3, u_7, u_7} (α := 𝕜') ((σ : (a : 𝕜) → 𝕜') a : 𝕜') (A f)
hbound :
  ∃ (s : Finset (ℕ × ℕ)) (C : ℝ),
    0 ≤ C ∧
      ∀ (f : 𝓢(D, E)), ‖A f‖ ≤ HMul.hMul (β := ℝ) C ((s.sup (schwartzSeminormFamily 𝕜 D E) : (a : 𝓢(D, E)) → ℝ) f : ℝ)
f : 𝓢(D, E) →ₛₗ[σ] G := { toFun := fun (x : 𝓢(D, E)) ↦ A x, map_add' := hadd, map_smul' := hsmul }
hf :
  ∀ (s : Finset (ℕ × ℕ)) (C : ℝ) (hC : 0 ≤ C)
    (h :
      ∀ (f : 𝓢(D, E)), ‖A f‖ ≤ HMul.hMul (β := ℝ) C ((s.sup (schwartzSeminormFamily 𝕜 D E) : (a : 𝓢(D, E)) → ℝ) f : ℝ)),
    ∃ (s : Finset (ℕ × ℕ)) (C : ℝ≥0),
      Seminorm.comp (σ₁₂ := σ) (normSeminorm 𝕜' G)
          { toFun := fun (x : 𝓢(D, E)) ↦ A x, map_add' := hadd, map_smul' := hsmul } ≤
        HSMul.hSMul (β := Seminorm 𝕜 𝓢(D, E)) C (s.sup (schwartzSeminormFamily 𝕜 D E))
⊢ ∃ (s : Finset (ℕ × ℕ)) (C : ℝ≥0),
    Seminorm.comp (σ₁₂ := σ) (normSeminorm 𝕜' G)
        { toFun := fun (x : 𝓢(D, E)) ↦ A x, map_add' := hadd, map_smul' := hsmul } ≤
      HSMul.hSMul (β := Seminorm 𝕜 𝓢(D, E)) C (s.sup (schwartzSeminormFamily 𝕜 D E))

Tactic:
rcases hbound with ⟨s, C, hC, h⟩
-- 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
σ : 𝕜 →+* 𝕜'
inst_14 : RingHomIsometric σ
A : 𝓢(D, E) → G
hadd : ∀ (f g : 𝓢(D, E)), A (f + g) = A f + A g
hsmul : ∀ (a : 𝕜) (f : 𝓢(D, E)), A (a • f) = HSMul.hSMul.{u_3, u_7, u_7} (α := 𝕜') ((σ : (a : 𝕜) → 𝕜') a : 𝕜') (A f)
f : 𝓢(D, E) →ₛₗ[σ] G := { toFun := fun (x : 𝓢(D, E)) ↦ A x, map_add' := hadd, map_smul' := hsmul }
s : Finset (ℕ × ℕ)
C : ℝ
hC : 0 ≤ C
h : ∀ (f : 𝓢(D, E)), ‖A f‖ ≤ HMul.hMul (β := ℝ) C ((s.sup (schwartzSeminormFamily 𝕜 D E) : (a : 𝓢(D, E)) → ℝ) f : ℝ)
⊢ ∃ (s : Finset (ℕ × ℕ)) (C : ℝ≥0),
    Seminorm.comp (σ₁₂ := σ) (normSeminorm 𝕜' G)
        { toFun := fun (x : 𝓢(D, E)) ↦ A x, map_add' := hadd, map_smul' := hsmul } ≤
      HSMul.hSMul (β := Seminorm 𝕜 𝓢(D, E)) C (s.sup (schwartzSeminormFamily 𝕜 D E))

Tactic:
⟨s, ⟨C, hC⟩, h⟩

Premises used: Subtype.mk, Exists.intro