awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : NontriviallyNormedField 𝕜
inst_5 : NormedAlgebra ℝ 𝕜
inst_6 : NormedAddCommGroup D
inst_7 : NormedSpace ℝ D
inst_8 : NormedAddCommGroup G
inst_9 : NormedSpace ℝ G
inst_10 : NormedSpace 𝕜 F
inst_11 : NormedSpace 𝕜 E
inst_12 : NormedSpace 𝕜 G
B : E →L[𝕜] F →L[𝕜] G
g : D → F
hg : Function.HasTemperateGrowth g
k n l : ℕ
C : ℝ
hC : 0 ≤ C
f : 𝓢(D, E)
x : D
hxk : 0 ≤ ‖x‖ ^ k
hnorm_mul :
  norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_7} ℝ (fun (i : Fin n) ↦ D) G)
      (iteratedFDeriv ℝ n
        (fun (y : D) ↦
          (((ContinuousLinearMap.bilinearRestrictScalars ℝ B : (a : E) → F →L[ℝ] G) ((f : (a : D) → E) y) : F →L[ℝ] G) :
              (a : F) → G)
            (g y))
        x) ≤
    norm (E := E →L[ℝ] F →L[ℝ] G) (ContinuousLinearMap.bilinearRestrictScalars ℝ B) *
      ∑ i ∈ Finset.range (n + 1),
        (↑(n.choose i) : ℝ) *
            norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin i) ↦ D) E)
              (iteratedFDeriv ℝ i (⇑f : (a : D) → E) x) *
          norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_6} ℝ (fun (i : Fin (n - i)) ↦ D) F)
            (iteratedFDeriv ℝ (n - i) g x)
this : ∑ _x ∈ Finset.range (n + 1), 1 = HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
i : ℕ
hgrowth :
  norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_6} ℝ (fun (i : Fin (n - i)) ↦ D) F) (iteratedFDeriv ℝ (n - i) g x) ≤
    C * (1 + ‖x‖) ^ l
hi : i ≤ (l + k, n).2
⊢ ‖x‖ ^ k *
        norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin i) ↦ D) E)
          (iteratedFDeriv ℝ i (⇑f : (a : D) → E) x) *
      (1 + ‖x‖) ^ l ≤
    HMul.hMul (β := ℝ) (HPow.hPow (α := ℝ) 2 (l + k))
      (((Finset.Iic (l + k, n)).sup (schwartzSeminormFamily 𝕜 D E) : (a : 𝓢(D, E)) → ℝ) f : ℝ)
have right : ‖x‖ ^ k *
      norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin i) ↦ D) E)
        (iteratedFDeriv ℝ i (⇑f : (a : D) → E) x) *
    (1 + ‖x‖) ^ l ≤
  (1 + ‖x‖) ^ (l + k, n).1 *
    norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin i) ↦ D) E)
      (iteratedFDeriv ℝ i (⇑f : (a : D) → E) x)
Tactic: refine le_trans ?_ (one_add_le_sup_seminorm_apply le_rfl hi f x)
-- 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 : NontriviallyNormedField 𝕜
inst_5 : NormedAlgebra ℝ 𝕜
inst_6 : NormedAddCommGroup D
inst_7 : NormedSpace ℝ D
inst_8 : NormedAddCommGroup G
inst_9 : NormedSpace ℝ G
inst_10 : NormedSpace 𝕜 F
inst_11 : NormedSpace 𝕜 E
inst_12 : NormedSpace 𝕜 G
B : E →L[𝕜] F →L[𝕜] G
g : D → F
hg : Function.HasTemperateGrowth g
k n l : ℕ
C : ℝ
hC : 0 ≤ C
f : 𝓢(D, E)
x : D
hxk : 0 ≤ ‖x‖ ^ k
hnorm_mul :
  norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_7} ℝ (fun (i : Fin n) ↦ D) G)
      (iteratedFDeriv ℝ n
        (fun (y : D) ↦
          (((ContinuousLinearMap.bilinearRestrictScalars ℝ B : (a : E) → F →L[ℝ] G) ((f : (a : D) → E) y) : F →L[ℝ] G) :
              (a : F) → G)
            (g y))
        x) ≤
    norm (E := E →L[ℝ] F →L[ℝ] G) (ContinuousLinearMap.bilinearRestrictScalars ℝ B) *
      ∑ i ∈ Finset.range (n + 1),
        (↑(n.choose i) : ℝ) *
            norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin i) ↦ D) E)
              (iteratedFDeriv ℝ i (⇑f : (a : D) → E) x) *
          norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_6} ℝ (fun (i : Fin (n - i)) ↦ D) F)
            (iteratedFDeriv ℝ (n - i) g x)
this : ∑ _x ∈ Finset.range (n + 1), 1 = HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
i : ℕ
hgrowth :
  norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_6} ℝ (fun (i : Fin (n - i)) ↦ D) F) (iteratedFDeriv ℝ (n - i) g x) ≤
    C * (1 + ‖x‖) ^ l
hi : i ≤ (l + k, n).2
⊢ ‖x‖ ^ k *
        norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin i) ↦ D) E)
          (iteratedFDeriv ℝ i (⇑f : (a : D) → E) x) *
      (1 + ‖x‖) ^ l ≤
    (1 + ‖x‖) ^ (l + k, n).1 *
      norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin i) ↦ D) E)
        (iteratedFDeriv ℝ i (⇑f : (a : D) → E) x)
have right : ‖x‖ ^ k *
      norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin i) ↦ D) E)
        (iteratedFDeriv ℝ i (⇑f : (a : D) → E) x) *
    (1 + ‖x‖) ^ l ≤
  (1 + ‖x‖) ^ l * (1 + ‖x‖) ^ k *
    norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin i) ↦ D) E)
      (iteratedFDeriv ℝ i (⇑f : (a : D) → E) x)
Tactic: rw [pow_add]
-- 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 : NontriviallyNormedField 𝕜
inst_5 : NormedAlgebra ℝ 𝕜
inst_6 : NormedAddCommGroup D
inst_7 : NormedSpace ℝ D
inst_8 : NormedAddCommGroup G
inst_9 : NormedSpace ℝ G
inst_10 : NormedSpace 𝕜 F
inst_11 : NormedSpace 𝕜 E
inst_12 : NormedSpace 𝕜 G
B : E →L[𝕜] F →L[𝕜] G
g : D → F
hg : Function.HasTemperateGrowth g
k n l : ℕ
C : ℝ
hC : 0 ≤ C
f : 𝓢(D, E)
x : D
hxk : 0 ≤ ‖x‖ ^ k
hnorm_mul :
  norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_7} ℝ (fun (i : Fin n) ↦ D) G)
      (iteratedFDeriv ℝ n
        (fun (y : D) ↦
          (((ContinuousLinearMap.bilinearRestrictScalars ℝ B : (a : E) → F →L[ℝ] G) ((f : (a : D) → E) y) : F →L[ℝ] G) :
              (a : F) → G)
            (g y))
        x) ≤
    norm (E := E →L[ℝ] F →L[ℝ] G) (ContinuousLinearMap.bilinearRestrictScalars ℝ B) *
      ∑ i ∈ Finset.range (n + 1),
        (↑(n.choose i) : ℝ) *
            norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin i) ↦ D) E)
              (iteratedFDeriv ℝ i (⇑f : (a : D) → E) x) *
          norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_6} ℝ (fun (i : Fin (n - i)) ↦ D) F)
            (iteratedFDeriv ℝ (n - i) g x)
this : ∑ _x ∈ Finset.range (n + 1), 1 = HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
i : ℕ
hgrowth :
  norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_6} ℝ (fun (i : Fin (n - i)) ↦ D) F) (iteratedFDeriv ℝ (n - i) g x) ≤
    C * (1 + ‖x‖) ^ l
hi : i ≤ (l + k, n).2
⊢ ‖x‖ ^ k *
        norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin i) ↦ D) E)
          (iteratedFDeriv ℝ i (⇑f : (a : D) → E) x) *
      (1 + ‖x‖) ^ l ≤
    (1 + ‖x‖) ^ l * (1 + ‖x‖) ^ k *
      norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin i) ↦ D) E)
        (iteratedFDeriv ℝ i (⇑f : (a : D) → E) x)
have right : ‖x‖ ^ k *
      norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin i) ↦ D) E)
        (iteratedFDeriv ℝ i (⇑f : (a : D) → E) x) *
    (1 + ‖x‖) ^ l ≤
  (1 + ‖x‖) ^ k *
      norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin i) ↦ D) E)
        (iteratedFDeriv ℝ i (⇑f : (a : D) → E) x) *
    (1 + ‖x‖) ^ l
Tactic: move_mul [(1 + ‖x‖) ^ l]
-- 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 : NontriviallyNormedField 𝕜
inst_5 : NormedAlgebra ℝ 𝕜
inst_6 : NormedAddCommGroup D
inst_7 : NormedSpace ℝ D
inst_8 : NormedAddCommGroup G
inst_9 : NormedSpace ℝ G
inst_10 : NormedSpace 𝕜 F
inst_11 : NormedSpace 𝕜 E
inst_12 : NormedSpace 𝕜 G
B : E →L[𝕜] F →L[𝕜] G
g : D → F
hg : Function.HasTemperateGrowth g
k n l : ℕ
C : ℝ
hC : 0 ≤ C
f : 𝓢(D, E)
x : D
hxk : 0 ≤ ‖x‖ ^ k
hnorm_mul :
  norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_7} ℝ (fun (i : Fin n) ↦ D) G)
      (iteratedFDeriv ℝ n
        (fun (y : D) ↦
          (((ContinuousLinearMap.bilinearRestrictScalars ℝ B : (a : E) → F →L[ℝ] G) ((f : (a : D) → E) y) : F →L[ℝ] G) :
              (a : F) → G)
            (g y))
        x) ≤
    norm (E := E →L[ℝ] F →L[ℝ] G) (ContinuousLinearMap.bilinearRestrictScalars ℝ B) *
      ∑ i ∈ Finset.range (n + 1),
        (↑(n.choose i) : ℝ) *
            norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin i) ↦ D) E)
              (iteratedFDeriv ℝ i (⇑f : (a : D) → E) x) *
          norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_6} ℝ (fun (i : Fin (n - i)) ↦ D) F)
            (iteratedFDeriv ℝ (n - i) g x)
this : ∑ _x ∈ Finset.range (n + 1), 1 = HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
i : ℕ
hgrowth :
  norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_6} ℝ (fun (i : Fin (n - i)) ↦ D) F) (iteratedFDeriv ℝ (n - i) g x) ≤
    C * (1 + ‖x‖) ^ l
hi : i ≤ (l + k, n).2
⊢ ‖x‖ ^ k *
        norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin i) ↦ D) E)
          (iteratedFDeriv ℝ i (⇑f : (a : D) → E) x) *
      (1 + ‖x‖) ^ l ≤
    (1 + ‖x‖) ^ k *
        norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin i) ↦ D) E)
          (iteratedFDeriv ℝ i (⇑f : (a : D) → E) x) *
      (1 + ‖x‖) ^ l
have right : ‖x‖ ≤ 1 + ‖x‖
Tactic: gcongr
-- 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 : NontriviallyNormedField 𝕜
inst_5 : NormedAlgebra ℝ 𝕜
inst_6 : NormedSpace 𝕜 F
c : 𝕜
⊢ (smulLeftCLM F fun (x : E) ↦ c) = HSMul.hSMul (β := 𝓢(E, F) →L[𝕜] 𝓢(E, F)) c (ContinuousLinearMap.id 𝕜 𝓢(E, F))
have h : ∀ (f : 𝓢(E, F)) (x : E),
  Eq.{u_6 + 1} (α := F)
    (((((smulLeftCLM F fun (x : E) ↦ c : 𝓢(E, F) →L[𝕜] 𝓢(E, F)) : (a : 𝓢(E, F)) → 𝓢(E, F)) f : 𝓢(E, F)) : (a : E) → F)
        x :
      F)
    ((((HSMul.hSMul (β := 𝓢(E, F) →L[𝕜] 𝓢(E, F)) c (ContinuousLinearMap.id 𝕜 𝓢(E, F)) : (a : 𝓢(E, F)) → 𝓢(E, F)) f :
            𝓢(E, F)) :
          (a : E) → F)
        x :
      F)
Tactic: ext f x
-- 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 : NontriviallyNormedField 𝕜
inst_5 : NormedAlgebra ℝ 𝕜
inst_6 : NormedSpace 𝕜 F
c : 𝕜
f : 𝓢(E, F)
x : E
⊢ Eq.{u_6 + 1} (α := F)
    (((((smulLeftCLM F fun (x : E) ↦ c : 𝓢(E, F) →L[𝕜] 𝓢(E, F)) : (a : 𝓢(E, F)) → 𝓢(E, F)) f : 𝓢(E, F)) : (a : E) → F)
        x :
      F)
    ((((HSMul.hSMul (β := 𝓢(E, F) →L[𝕜] 𝓢(E, F)) c (ContinuousLinearMap.id 𝕜 𝓢(E, F)) : (a : 𝓢(E, F)) → 𝓢(E, F)) f :
            𝓢(E, F)) :
          (a : E) → F)
        x :
      F)
have this : Function.HasTemperateGrowth.{u_5, u_2} (F := 𝕜) fun (x : E) ↦ c
Tactic: have : (fun (_ : E) ↦ c).HasTemperateGrowth := by fun_prop
-- 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 : NontriviallyNormedField 𝕜
inst_5 : NormedAlgebra ℝ 𝕜
inst_6 : NormedSpace 𝕜 F
g₁ g₂ : E → 𝕜
hg₁ : Function.HasTemperateGrowth g₁
hg₂ : Function.HasTemperateGrowth g₂
f : 𝓢(E, F)
⊢ Eq (α := 𝓢(E, F))
    (((smulLeftCLM F g₁ : 𝓢(E, F) →L[𝕜] 𝓢(E, F)) : (a : 𝓢(E, F)) → 𝓢(E, F))
        (((smulLeftCLM F g₂ : 𝓢(E, F) →L[𝕜] 𝓢(E, F)) : (a : 𝓢(E, F)) → 𝓢(E, F)) f) :
      𝓢(E, F))
    (((smulLeftCLM F (g₁ * g₂) : 𝓢(E, F) →L[𝕜] 𝓢(E, F)) : (a : 𝓢(E, F)) → 𝓢(E, F)) f : 𝓢(E, F))
have h : ∀ (x : E),
  Eq.{u_6 + 1} (α := F)
    (((((smulLeftCLM F g₁ : 𝓢(E, F) →L[𝕜] 𝓢(E, F)) : (a : 𝓢(E, F)) → 𝓢(E, F))
              (((smulLeftCLM F g₂ : 𝓢(E, F) →L[𝕜] 𝓢(E, F)) : (a : 𝓢(E, F)) → 𝓢(E, F)) f) :
            𝓢(E, F)) :
          (a : E) → F)
        x :
      F)
    (((((smulLeftCLM F (g₁ * g₂) : 𝓢(E, F) →L[𝕜] 𝓢(E, F)) : (a : 𝓢(E, F)) → 𝓢(E, F)) f : 𝓢(E, F)) : (a : E) → F) x : F)
Tactic: ext x
-- 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 : NontriviallyNormedField 𝕜
inst_5 : NormedAlgebra ℝ 𝕜
inst_6 : NormedSpace 𝕜 F
g₁ g₂ : E → 𝕜
hg₁ : Function.HasTemperateGrowth g₁
hg₂ : Function.HasTemperateGrowth g₂
⊢ Eq (α := 𝓢(E, F) →L[𝕜] 𝓢(E, F))
    ((smulLeftCLM F g₁ : 𝓢(E, F) →L[𝕜] 𝓢(E, F)) ∘SL (smulLeftCLM F g₂ : 𝓢(E, F) →L[𝕜] 𝓢(E, F)) : 𝓢(E, F) →L[𝕜] 𝓢(E, F))
    (smulLeftCLM F (g₁ * g₂) : 𝓢(E, F) →L[𝕜] 𝓢(E, F))
have h : ∀ (f : 𝓢(E, F)),
  Eq (α := 𝓢(E, F))
    ((((smulLeftCLM F g₁ : 𝓢(E, F) →L[𝕜] 𝓢(E, F)) ∘SL (smulLeftCLM F g₂ : 𝓢(E, F) →L[𝕜] 𝓢(E, F)) :
            𝓢(E, F) →L[𝕜] 𝓢(E, F)) :
          (a : 𝓢(E, F)) → 𝓢(E, F))
        f :
      𝓢(E, F))
    (((smulLeftCLM F (g₁ * g₂) : 𝓢(E, F) →L[𝕜] 𝓢(E, F)) : (a : 𝓢(E, F)) → 𝓢(E, F)) f : 𝓢(E, F))
Tactic: ext1 f
-- 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 : NontriviallyNormedField 𝕜
inst_5 : NormedAlgebra ℝ 𝕜
inst_6 : NormedSpace 𝕜 F
g : E → 𝕜
hg : Function.HasTemperateGrowth g
c : 𝕜
⊢ smulLeftCLM F (c • g) = HSMul.hSMul (β := 𝓢(E, F) →L[𝕜] 𝓢(E, F)) c (smulLeftCLM F g : 𝓢(E, F) →L[𝕜] 𝓢(E, F))
have this : Function.HasTemperateGrowth.{u_5, u_2} (F := 𝕜) fun (x : E) ↦ c
Tactic: have : (fun (_ : E) ↦ c).HasTemperateGrowth := by fun_prop
-- 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 : NontriviallyNormedField 𝕜
inst_5 : NormedAlgebra ℝ 𝕜
inst_6 : NormedSpace 𝕜 F
g : E → 𝕜
hg : Function.HasTemperateGrowth g
c : 𝕜
this : Function.HasTemperateGrowth.{u_5, u_2} (F := 𝕜) fun (x : E) ↦ c
⊢ smulLeftCLM F (c • g) = HSMul.hSMul (β := 𝓢(E, F) →L[𝕜] 𝓢(E, F)) c (smulLeftCLM F g : 𝓢(E, F) →L[𝕜] 𝓢(E, F))
have h : HSMul.hSMul (β := 𝓢(E, F) →L[𝕜] 𝓢(E, F)) c (smulLeftCLM F g : 𝓢(E, F) →L[𝕜] 𝓢(E, F)) =
  (smulLeftCLM F fun (x : E) ↦ c : 𝓢(E, F) →L[𝕜] 𝓢(E, F)) ∘SL (smulLeftCLM F g : 𝓢(E, F) →L[𝕜] 𝓢(E, F))
Tactic: convert! (smulLeftCLM_compL_smulLeftCLM this hg).symm using 1
-- 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 : NontriviallyNormedField 𝕜
inst_5 : NormedAlgebra ℝ 𝕜
inst_6 : NormedSpace 𝕜 F
g₁ g₂ : E → 𝕜
hg₁ : Function.HasTemperateGrowth g₁
hg₂ : Function.HasTemperateGrowth g₂
⊢ smulLeftCLM F (g₁ + g₂) =
    HAdd.hAdd (α := 𝓢(E, F) →L[𝕜] 𝓢(E, F)) (β := 𝓢(E, F) →L[𝕜] 𝓢(E, F)) (smulLeftCLM F g₁ : 𝓢(E, F) →L[𝕜] 𝓢(E, F))
      (smulLeftCLM F g₂ : 𝓢(E, F) →L[𝕜] 𝓢(E, F))
have h : ∀ (f : 𝓢(E, F)) (x : E),
  Eq.{u_6 + 1} (α := F)
    (((((smulLeftCLM F (g₁ + g₂) : 𝓢(E, F) →L[𝕜] 𝓢(E, F)) : (a : 𝓢(E, F)) → 𝓢(E, F)) f : 𝓢(E, F)) : (a : E) → F) x : F)
    ((((HAdd.hAdd (α := 𝓢(E, F) →L[𝕜] 𝓢(E, F)) (β := 𝓢(E, F) →L[𝕜] 𝓢(E, F)) (smulLeftCLM F g₁ : 𝓢(E, F) →L[𝕜] 𝓢(E, F))
                  (smulLeftCLM F g₂ : 𝓢(E, F) →L[𝕜] 𝓢(E, F)) :
                (a : 𝓢(E, F)) → 𝓢(E, F))
              f :
            𝓢(E, F)) :
          (a : E) → F)
        x :
      F)
Tactic: ext f x
-- 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 : NontriviallyNormedField 𝕜
inst_5 : NormedAlgebra ℝ 𝕜
inst_6 : NormedSpace 𝕜 F
g₁ g₂ : E → 𝕜
hg₁ : Function.HasTemperateGrowth g₁
hg₂ : Function.HasTemperateGrowth g₂
⊢ smulLeftCLM F (g₁ - g₂) =
    HSub.hSub (α := 𝓢(E, F) →L[𝕜] 𝓢(E, F)) (β := 𝓢(E, F) →L[𝕜] 𝓢(E, F)) (smulLeftCLM F g₁ : 𝓢(E, F) →L[𝕜] 𝓢(E, F))
      (smulLeftCLM F g₂ : 𝓢(E, F) →L[𝕜] 𝓢(E, F))
have h : ∀ (f : 𝓢(E, F)) (x : E),
  Eq.{u_6 + 1} (α := F)
    (((((smulLeftCLM F (g₁ - g₂) : 𝓢(E, F) →L[𝕜] 𝓢(E, F)) : (a : 𝓢(E, F)) → 𝓢(E, F)) f : 𝓢(E, F)) : (a : E) → F) x : F)
    ((((HSub.hSub (α := 𝓢(E, F) →L[𝕜] 𝓢(E, F)) (β := 𝓢(E, F) →L[𝕜] 𝓢(E, F)) (smulLeftCLM F g₁ : 𝓢(E, F) →L[𝕜] 𝓢(E, F))
                  (smulLeftCLM F g₂ : 𝓢(E, F) →L[𝕜] 𝓢(E, F)) :
                (a : 𝓢(E, F)) → 𝓢(E, F))
              f :
            𝓢(E, F)) :
          (a : E) → F)
        x :
      F)
Tactic: ext f x
-- 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 : NontriviallyNormedField 𝕜
inst_5 : NormedAlgebra ℝ 𝕜
inst_6 : NormedSpace 𝕜 F
g : E → 𝕜
hg : Function.HasTemperateGrowth g
⊢ Eq (α := 𝓢(E, F) →L[𝕜] 𝓢(E, F)) (smulLeftCLM F (-g) : 𝓢(E, F) →L[𝕜] 𝓢(E, F))
    (-smulLeftCLM F g : 𝓢(E, F) →L[𝕜] 𝓢(E, F))
have h : ∀ (f : 𝓢(E, F)) (x : E),
  Eq.{u_6 + 1} (α := F)
    (((((smulLeftCLM F (-g) : 𝓢(E, F) →L[𝕜] 𝓢(E, F)) : (a : 𝓢(E, F)) → 𝓢(E, F)) f : 𝓢(E, F)) : (a : E) → F) x : F)
    (((((-smulLeftCLM F g : 𝓢(E, F) →L[𝕜] 𝓢(E, F)) : (a : 𝓢(E, F)) → 𝓢(E, F)) f : 𝓢(E, F)) : (a : E) → F) x : F)
Tactic: ext f x
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Basic (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedAlgebra ℝ 𝕜
inst_6 : NormedSpace 𝕜 F
g : ι → E → 𝕜
s : Finset ι
hg : ∀ i ∈ s, Function.HasTemperateGrowth (g i)
⊢ Eq (α := 𝓢(E, F) →L[𝕜] 𝓢(E, F)) (smulLeftCLM F fun (x : E) ↦ ∑ i ∈ s, g i x : 𝓢(E, F) →L[𝕜] 𝓢(E, F))
    (∑ i ∈ s, smulLeftCLM F (g i) : 𝓢(E, F) →L[𝕜] 𝓢(E, F))
have h : ∀ (f : 𝓢(E, F)) (x : E),
  Eq.{u_6 + 1} (α := F)
    (((((smulLeftCLM F fun (x : E) ↦ ∑ i ∈ s, g i x : 𝓢(E, F) →L[𝕜] 𝓢(E, F)) : (a : 𝓢(E, F)) → 𝓢(E, F)) f : 𝓢(E, F)) :
          (a : E) → F)
        x :
      F)
    ((((∑ i ∈ s, smulLeftCLM F (g i) : (a : 𝓢(E, F)) → 𝓢(E, F)) f : 𝓢(E, F)) : (a : E) → F) x : F)
Tactic: ext f x
-- 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
𝕜' : Type u_10
inst_4 : RCLike 𝕜'
inst_5 : NormedSpace 𝕜' F
g : E → ℝ
hg : Function.HasTemperateGrowth g
f : 𝓢(E, F)
x : E
⊢ Eq.{u_6 + 1} (α := F)
    (((((smulLeftCLM F fun (x : E) ↦ (↑(g x) : 𝕜') : 𝓢(E, F) →L[𝕜'] 𝓢(E, F)) : (a : 𝓢(E, F)) → 𝓢(E, F)) f : 𝓢(E, F)) :
          (a : E) → F)
        x :
      F)
    (((((smulLeftCLM F g : 𝓢(E, F) →L[ℝ] 𝓢(E, F)) : (a : 𝓢(E, F)) → 𝓢(E, F)) f : 𝓢(E, F)) : (a : E) → F) x : F)
have h : HSMul.hSMul.{u_10, u_6, u_6} (α := 𝕜') (β := F) (↑(g x) : 𝕜') ((f : (a : E) → F) x : F) =
  ((((smulLeftCLM F g : 𝓢(E, F) →L[ℝ] 𝓢(E, F)) : (a : 𝓢(E, F)) → 𝓢(E, F)) f : 𝓢(E, F)) : (a : E) → F) x
Tactic: rw [smulLeftCLM_apply_apply (by fun_prop), smulLeftCLM_apply_apply (by fun_prop),
    algebraMap_smul]
-- 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
𝕜' : Type u_10
inst_4 : RCLike 𝕜'
inst_5 : NormedSpace 𝕜' F
g : E → ℝ
hg : Function.HasTemperateGrowth g
f : 𝓢(E, F)
x : E
h :
  HSMul.hSMul.{u_10, u_6, u_6} (α := 𝕜') (β := F) (↑(g x) : 𝕜') ((f : (a : E) → F) x : F) =
    ((((smulLeftCLM F g : 𝓢(E, F) →L[ℝ] 𝓢(E, F)) : (a : 𝓢(E, F)) → 𝓢(E, F)) f : 𝓢(E, F)) : (a : E) → F) x
⊢ Eq.{u_6 + 1} (α := F)
    (((((smulLeftCLM F fun (x : E) ↦ (↑(g x) : 𝕜') : 𝓢(E, F) →L[𝕜'] 𝓢(E, F)) : (a : 𝓢(E, F)) → 𝓢(E, F)) f : 𝓢(E, F)) :
          (a : E) → F)
        x :
      F)
    (((((smulLeftCLM F g : 𝓢(E, F) →L[ℝ] 𝓢(E, F)) : (a : 𝓢(E, F)) → 𝓢(E, F)) f : 𝓢(E, F)) : (a : E) → F) x : F)
have h₁ : HSMul.hSMul.{u_10, u_6, u_6} (α := 𝕜') (β := F) (↑(g x) : 𝕜') ((f : (a : E) → F) x : F) =
  HSMul.hSMul (β := F) (g x) ((f : (a : E) → F) x : F)
Tactic: rw [smulLeftCLM_apply_apply (by fun_prop), smulLeftCLM_apply_apply (by fun_prop),
    algebraMap_smul]
-- 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
𝕜' : Type u_10
inst_4 : RCLike 𝕜'
inst_5 : NormedSpace 𝕜' F
g : E → ℝ
hg : Function.HasTemperateGrowth g
f : 𝓢(E, F)
x : E
h :
  HSMul.hSMul.{u_10, u_6, u_6} (α := 𝕜') (β := F) (↑(g x) : 𝕜') ((f : (a : E) → F) x : F) =
    ((((smulLeftCLM F g : 𝓢(E, F) →L[ℝ] 𝓢(E, F)) : (a : 𝓢(E, F)) → 𝓢(E, F)) f : 𝓢(E, F)) : (a : E) → F) x
h₁ :
  HSMul.hSMul.{u_10, u_6, u_6} (α := 𝕜') (β := F) (↑(g x) : 𝕜') ((f : (a : E) → F) x : F) =
    HSMul.hSMul (β := F) (g x) ((f : (a : E) → F) x : F)
⊢ Eq.{u_6 + 1} (α := F)
    (((((smulLeftCLM F fun (x : E) ↦ (↑(g x) : 𝕜') : 𝓢(E, F) →L[𝕜'] 𝓢(E, F)) : (a : 𝓢(E, F)) → 𝓢(E, F)) f : 𝓢(E, F)) :
          (a : E) → F)
        x :
      F)
    (((((smulLeftCLM F g : 𝓢(E, F) →L[ℝ] 𝓢(E, F)) : (a : 𝓢(E, F)) → 𝓢(E, F)) f : 𝓢(E, F)) : (a : E) → F) x : F)
have h₂ : HSMul.hSMul (β := F) (g x) ((f : (a : E) → F) x : F) = HSMul.hSMul (β := F) (g x) ((f : (a : E) → F) x : F)
Tactic: rw [smulLeftCLM_apply_apply (by fun_prop), smulLeftCLM_apply_apply (by fun_prop),
    algebraMap_smul]
-- 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
𝕜' : Type u_10
inst_4 : RCLike 𝕜'
inst_5 : NormedSpace 𝕜' F
g : E → 𝕜'
hg : Function.HasTemperateGrowth g
c : ℝ
⊢ smulLeftCLM F (c • g) = HSMul.hSMul (β := 𝓢(E, F) →L[𝕜'] 𝓢(E, F)) c (smulLeftCLM F g : 𝓢(E, F) →L[𝕜'] 𝓢(E, F))
have rw : smulLeftCLM F (HSMul.hSMul (α := 𝕜') (↑c : 𝕜') g) =
  HSMul.hSMul (β := 𝓢(E, F) →L[𝕜'] 𝓢(E, F)) c (smulLeftCLM F g : 𝓢(E, F) →L[𝕜'] 𝓢(E, F))
Tactic: rw [RCLike.real_smul_eq_coe_smul (K := 𝕜') c, smulLeftCLM_smul hg,
    ← RCLike.real_smul_eq_coe_smul c]
-- 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
𝕜' : Type u_10
inst_4 : RCLike 𝕜'
inst_5 : NormedSpace 𝕜' F
g : E → 𝕜'
hg : Function.HasTemperateGrowth g
c : ℝ
rw :
  smulLeftCLM F (HSMul.hSMul (α := 𝕜') (↑c : 𝕜') g) =
    HSMul.hSMul (β := 𝓢(E, F) →L[𝕜'] 𝓢(E, F)) c (smulLeftCLM F g : 𝓢(E, F) →L[𝕜'] 𝓢(E, F))
⊢ smulLeftCLM F (c • g) = HSMul.hSMul (β := 𝓢(E, F) →L[𝕜'] 𝓢(E, F)) c (smulLeftCLM F g : 𝓢(E, F) →L[𝕜'] 𝓢(E, F))
have rw₁ : HSMul.hSMul (α := 𝕜') (β := 𝓢(E, F) →L[𝕜'] 𝓢(E, F)) (↑c : 𝕜') (smulLeftCLM F g : 𝓢(E, F) →L[𝕜'] 𝓢(E, F)) =
  HSMul.hSMul (β := 𝓢(E, F) →L[𝕜'] 𝓢(E, F)) c (smulLeftCLM F g : 𝓢(E, F) →L[𝕜'] 𝓢(E, F))
Tactic: rw [RCLike.real_smul_eq_coe_smul (K := 𝕜') c, smulLeftCLM_smul hg,
    ← RCLike.real_smul_eq_coe_smul c]