awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Basic (goal)
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 (α := ℝ) ((SchwartzMap.seminorm 𝕜 i n : (a : 𝓢(E, F)) → ℝ) f : ℝ)
    (((Finset.Iic m).sup fun (m : ℕ × ℕ) ↦ SchwartzMap.seminorm 𝕜 m.1 m.2 : (a : 𝓢(E, F)) → ℝ) f : ℝ)
have h : LE.le (α := Seminorm 𝕜 𝓢(E, F)) (SchwartzMap.seminorm 𝕜 i n)
  ((Finset.Iic m).sup fun (m : ℕ × ℕ) ↦ SchwartzMap.seminorm 𝕜 m.1 m.2)
Tactic: apply Seminorm.le_def.1
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Basic (hypothesis)
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)
have A : WithSeminorms (E := 𝓢(E, F)) (schwartzSeminormFamily ℝ E F)
Tactic: have A : WithSeminorms (schwartzSeminormFamily ℝ E F) := ⟨rfl⟩
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Basic (goal)
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)
⊢ WithSeminorms (E := 𝓢(E, F)) (schwartzSeminormFamily 𝕜 E F)
have 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))
Tactic: rw [SeminormFamily.withSeminorms_iff_nhds_eq_iInf] at A ⊢
Cleared hypotheses: A
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Basic (goal)
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)) (nhds 0)
    (⨅ (i : ℕ × ℕ), Filter.comap (β := ℝ) (⇑(schwartzSeminormFamily 𝕜 E F i) : (a : 𝓢(E, F)) → ℝ) (nhds 0))
have 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))
Tactic: rw [A]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Basic (goal)
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)
have rw : ContinuousSMul 𝕜 𝓢(E, F)
Tactic: rw [(schwartz_withSeminorms 𝕜 E F).withSeminorms_eq]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Basic (goal)
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)
have 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
Tactic: refine ⟨smooth f ⊤, fun n => ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Basic (goal)
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 : ℕ
⊢ ∃ (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
have 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
Tactic: rcases f.decay 0 n with ⟨C, Cpos, hC⟩
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Basic (goal)
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
have 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)
Tactic: apply Continuous.mul (by fun_prop)
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Basic (hypothesis)
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)
⊢ ∃ (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
have hg₁ : 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
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Basic (hypothesis)
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
⊢ ∃ (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
have hg₂ : HasCompactSupport g
Tactic: have hg₂ : HasCompactSupport g := (h₁.iteratedFDeriv _).norm.mul_left
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Basic (goal)
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
⊢ ∃ (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
have 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
Tactic: obtain ⟨x₀, hx₀⟩ := hg₁.exists_forall_ge_of_hasCompactSupport hg₂
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Basic (goal)
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 : ℕ
⊢ ∃ (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
have 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
Tactic: rcases hbound ⟨k, n⟩ with ⟨s, C, _, h⟩
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Basic (goal)
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))
have 𝕜₁ : ∀ (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))
Tactic: refine
      WithSeminorms.continuous_of_isBounded (schwartz_withSeminorms 𝕜 D E)
        (schwartz_withSeminorms 𝕜' F G) _ fun n => ?_
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Basic (goal)
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))
have 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))
Tactic: rcases hbound n with ⟨s, C, hC, h⟩
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Basic (goal)
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))
have 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)
Tactic: refine ⟨s, ⟨C, hC⟩, fun f => ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Basic (goal)
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 }
⊢ Continuous f.toFun
have change : Continuous (X := 𝓢(D, E)) (Y := G)
  (⇑{ toFun := fun (x : 𝓢(D, E)) ↦ A x, map_add' := hadd, map_smul' := hsmul } : (a : 𝓢(D, E)) → G)
Tactic: change Continuous (LinearMap.mk _ _)
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Basic (goal)
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 }
⊢ Continuous (X := 𝓢(D, E)) (Y := G)
    (⇑{ toFun := fun (x : 𝓢(D, E)) ↦ A x, map_add' := hadd, map_smul' := hsmul } : (a : 𝓢(D, E)) → G)
have 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))
Tactic: apply WithSeminorms.continuous_normedSpace_rng G (schwartz_withSeminorms 𝕜 D E)
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Basic (goal)
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 }
⊢ ∃ (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))
have 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))
Tactic: rcases hbound with ⟨s, C, hC, h⟩
Cleared hypotheses: hbound
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Basic (goal)
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 : NormedAddCommGroup G
inst_6 : NormedSpace ℝ G
inst_7 : NormedSpace 𝕜 G
inst_8 : SMulCommClass ℝ 𝕜 G
m : F
k n : ℕ
⊢ ∃ (s : Finset (ℕ × ℕ)) (C : ℝ),
    0 ≤ C ∧
      ∀ (f : 𝓢(E, F →L[ℝ] G)) (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 →L[ℝ] G)) (x : E) ↦ ((((f : (a : E) → F →L[ℝ] G) x : F →L[ℝ] G) : (a : F) → G) m : G))
                  f)
                x) ≤
          HMul.hMul (β := ℝ) C ((s.sup (schwartzSeminormFamily 𝕜 E (F →L[ℝ] G)) : (a : 𝓢(E, F →L[ℝ] G)) → ℝ) f : ℝ)
have right : ∀ (f : 𝓢(E, F →L[ℝ] G)) (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 →L[ℝ] G)) (x : E) ↦ ((((f : (a : E) → F →L[ℝ] G) x : F →L[ℝ] G) : (a : F) → G) m : G)) f)
          x) ≤
    HMul.hMul (β := ℝ) ‖m‖
      ((Finset.sup {(k, n)} (schwartzSeminormFamily 𝕜 E (F →L[ℝ] G)) : (a : 𝓢(E, F →L[ℝ] G)) → ℝ) f : ℝ)
Tactic: use {(k, n)}, ‖m‖, norm_nonneg _
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Basic (goal)
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 : NormedAddCommGroup G
inst_6 : NormedSpace ℝ G
inst_7 : NormedSpace 𝕜 G
inst_8 : SMulCommClass ℝ 𝕜 G
m : F
k n : ℕ
f : 𝓢(E, F →L[ℝ] G)
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 →L[ℝ] G)) (x : E) ↦ ((((f : (a : E) → F →L[ℝ] G) x : F →L[ℝ] G) : (a : F) → G) m : G)) f)
          x) ≤
    HMul.hMul (β := ℝ) ‖m‖
      ((Finset.sup {(k, n)} (schwartzSeminormFamily 𝕜 E (F →L[ℝ] G)) : (a : 𝓢(E, F →L[ℝ] G)) → ℝ) f : ℝ)
have right : ‖x‖ ^ k *
    norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_7} ℝ (fun (i : Fin n) ↦ E) G)
      (iteratedFDeriv ℝ n (fun (x : E) ↦ (((f : (a : E) → F →L[ℝ] G) x : F →L[ℝ] G) : (a : F) → G) m) x) ≤
  HMul.hMul (β := ℝ) ‖m‖ ((SchwartzMap.seminorm 𝕜 k n : (a : 𝓢(E, F →L[ℝ] G)) → ℝ) f : ℝ)
Tactic: simp only [Finset.sup_singleton, schwartzSeminormFamily_apply]