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
L : ContinuousLinearMap.{0, 0, u_5, u_7} (RingHom.id ℝ) E (G →L[ℝ] ℝ)
k n : ℕ
f : 𝓢(E, F)
x : E
⊢ HMul.hMul (β := ℝ) (‖L‖ * 1) ((SchwartzMap.seminorm 𝕜 (k + 1) n : (a : 𝓢(E, F)) → ℝ) f : ℝ) +
      HMul.hMul (β := ℝ) (‖L‖ * (↑n : ℝ)) ((SchwartzMap.seminorm 𝕜 k (n - 1) : (a : 𝓢(E, F)) → ℝ) f : ℝ) ≤
    HMul.hMul (β := ℝ) (‖L‖ * (↑(max 1 n) : ℝ))
        (max ((SchwartzMap.seminorm 𝕜 (k + 1) n : (a : 𝓢(E, F)) → ℝ) f)
            ((SchwartzMap.seminorm 𝕜 k (n - 1) : (a : 𝓢(E, F)) → ℝ) f) :
          ℝ) +
      HMul.hMul (β := ℝ) (‖L‖ * (↑(max 1 n) : ℝ))
        (max ((SchwartzMap.seminorm 𝕜 (k + 1) n : (a : 𝓢(E, F)) → ℝ) f)
            ((SchwartzMap.seminorm 𝕜 k (n - 1) : (a : 𝓢(E, F)) → ℝ) f) :
          ℝ)
have h₁ : LE.le (α := ℝ) 1 (↑(max 1 n) : ℝ)
Tactic: gcongr
-- 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
L : ContinuousLinearMap.{0, 0, u_5, u_7} (RingHom.id ℝ) E (G →L[ℝ] ℝ)
k n : ℕ
f : 𝓢(E, F)
x : E
h₁ : LE.le (α := ℝ) 1 (↑(max 1 n) : ℝ)
⊢ HMul.hMul (β := ℝ) (‖L‖ * 1) ((SchwartzMap.seminorm 𝕜 (k + 1) n : (a : 𝓢(E, F)) → ℝ) f : ℝ) +
      HMul.hMul (β := ℝ) (‖L‖ * (↑n : ℝ)) ((SchwartzMap.seminorm 𝕜 k (n - 1) : (a : 𝓢(E, F)) → ℝ) f : ℝ) ≤
    HMul.hMul (β := ℝ) (‖L‖ * (↑(max 1 n) : ℝ))
        (max ((SchwartzMap.seminorm 𝕜 (k + 1) n : (a : 𝓢(E, F)) → ℝ) f)
            ((SchwartzMap.seminorm 𝕜 k (n - 1) : (a : 𝓢(E, F)) → ℝ) f) :
          ℝ) +
      HMul.hMul (β := ℝ) (‖L‖ * (↑(max 1 n) : ℝ))
        (max ((SchwartzMap.seminorm 𝕜 (k + 1) n : (a : 𝓢(E, F)) → ℝ) f)
            ((SchwartzMap.seminorm 𝕜 k (n - 1) : (a : 𝓢(E, F)) → ℝ) f) :
          ℝ)
have h₂ : LE.le (α := ℝ) ((SchwartzMap.seminorm 𝕜 (k + 1) n : (a : 𝓢(E, F)) → ℝ) f : ℝ)
  (max ((SchwartzMap.seminorm 𝕜 (k + 1) n : (a : 𝓢(E, F)) → ℝ) f)
      ((SchwartzMap.seminorm 𝕜 k (n - 1) : (a : 𝓢(E, F)) → ℝ) f) :
    ℝ)
Tactic: gcongr
-- 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
L : ContinuousLinearMap.{0, 0, u_5, u_7} (RingHom.id ℝ) E (G →L[ℝ] ℝ)
k n : ℕ
f : 𝓢(E, F)
x : E
h₁ : LE.le (α := ℝ) 1 (↑(max 1 n) : ℝ)
h₂ :
  LE.le (α := ℝ) ((SchwartzMap.seminorm 𝕜 (k + 1) n : (a : 𝓢(E, F)) → ℝ) f : ℝ)
    (max ((SchwartzMap.seminorm 𝕜 (k + 1) n : (a : 𝓢(E, F)) → ℝ) f)
        ((SchwartzMap.seminorm 𝕜 k (n - 1) : (a : 𝓢(E, F)) → ℝ) f) :
      ℝ)
⊢ HMul.hMul (β := ℝ) (‖L‖ * 1) ((SchwartzMap.seminorm 𝕜 (k + 1) n : (a : 𝓢(E, F)) → ℝ) f : ℝ) +
      HMul.hMul (β := ℝ) (‖L‖ * (↑n : ℝ)) ((SchwartzMap.seminorm 𝕜 k (n - 1) : (a : 𝓢(E, F)) → ℝ) f : ℝ) ≤
    HMul.hMul (β := ℝ) (‖L‖ * (↑(max 1 n) : ℝ))
        (max ((SchwartzMap.seminorm 𝕜 (k + 1) n : (a : 𝓢(E, F)) → ℝ) f)
            ((SchwartzMap.seminorm 𝕜 k (n - 1) : (a : 𝓢(E, F)) → ℝ) f) :
          ℝ) +
      HMul.hMul (β := ℝ) (‖L‖ * (↑(max 1 n) : ℝ))
        (max ((SchwartzMap.seminorm 𝕜 (k + 1) n : (a : 𝓢(E, F)) → ℝ) f)
            ((SchwartzMap.seminorm 𝕜 k (n - 1) : (a : 𝓢(E, F)) → ℝ) f) :
          ℝ)
have h₃ : n ≤ max 1 n
Tactic: gcongr
-- 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
L : ContinuousLinearMap.{0, 0, u_5, u_7} (RingHom.id ℝ) E (G →L[ℝ] ℝ)
k n : ℕ
f : 𝓢(E, F)
x : E
h₁ : LE.le (α := ℝ) 1 (↑(max 1 n) : ℝ)
h₂ :
  LE.le (α := ℝ) ((SchwartzMap.seminorm 𝕜 (k + 1) n : (a : 𝓢(E, F)) → ℝ) f : ℝ)
    (max ((SchwartzMap.seminorm 𝕜 (k + 1) n : (a : 𝓢(E, F)) → ℝ) f)
        ((SchwartzMap.seminorm 𝕜 k (n - 1) : (a : 𝓢(E, F)) → ℝ) f) :
      ℝ)
h₃ : n ≤ max 1 n
⊢ HMul.hMul (β := ℝ) (‖L‖ * 1) ((SchwartzMap.seminorm 𝕜 (k + 1) n : (a : 𝓢(E, F)) → ℝ) f : ℝ) +
      HMul.hMul (β := ℝ) (‖L‖ * (↑n : ℝ)) ((SchwartzMap.seminorm 𝕜 k (n - 1) : (a : 𝓢(E, F)) → ℝ) f : ℝ) ≤
    HMul.hMul (β := ℝ) (‖L‖ * (↑(max 1 n) : ℝ))
        (max ((SchwartzMap.seminorm 𝕜 (k + 1) n : (a : 𝓢(E, F)) → ℝ) f)
            ((SchwartzMap.seminorm 𝕜 k (n - 1) : (a : 𝓢(E, F)) → ℝ) f) :
          ℝ) +
      HMul.hMul (β := ℝ) (‖L‖ * (↑(max 1 n) : ℝ))
        (max ((SchwartzMap.seminorm 𝕜 (k + 1) n : (a : 𝓢(E, F)) → ℝ) f)
            ((SchwartzMap.seminorm 𝕜 k (n - 1) : (a : 𝓢(E, F)) → ℝ) f) :
          ℝ)
have h₄ : LE.le (α := ℝ) ((SchwartzMap.seminorm 𝕜 k (n - 1) : (a : 𝓢(E, F)) → ℝ) f : ℝ)
  (max ((SchwartzMap.seminorm 𝕜 (k + 1) n : (a : 𝓢(E, F)) → ℝ) f)
      ((SchwartzMap.seminorm 𝕜 k (n - 1) : (a : 𝓢(E, F)) → ℝ) f) :
    ℝ)
Tactic: gcongr
-- 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
L : ContinuousLinearMap.{0, 0, u_5, u_7} (RingHom.id ℝ) E (G →L[ℝ] ℝ)
k n : ℕ
f : 𝓢(E, F)
x : E
⊢ HMul.hMul (β := ℝ) (‖L‖ * (↑(max 1 n) : ℝ))
        (max ((SchwartzMap.seminorm 𝕜 (k + 1) n : (a : 𝓢(E, F)) → ℝ) f)
            ((SchwartzMap.seminorm 𝕜 k (n - 1) : (a : 𝓢(E, F)) → ℝ) f) :
          ℝ) +
      HMul.hMul (β := ℝ) (‖L‖ * (↑(max 1 n) : ℝ))
        (max ((SchwartzMap.seminorm 𝕜 (k + 1) n : (a : 𝓢(E, F)) → ℝ) f)
            ((SchwartzMap.seminorm 𝕜 k (n - 1) : (a : 𝓢(E, F)) → ℝ) f) :
          ℝ) =
    HMul.hMul (β := ℝ) (2 * ‖L‖ * (↑(max 1 n) : ℝ))
      ((Finset.sup {(k + 1, n), (k, n - 1)} (schwartzSeminormFamily 𝕜 E F) : (a : 𝓢(E, F)) → ℝ) f : ℝ)
have simp : HMul.hMul (β := ℝ) (‖L‖ * (↑(max 1 n) : ℝ))
      (max ((SchwartzMap.seminorm 𝕜 (k + 1) n : (a : 𝓢(E, F)) → ℝ) f)
          ((SchwartzMap.seminorm 𝕜 k (n - 1) : (a : 𝓢(E, F)) → ℝ) f) :
        ℝ) +
    HMul.hMul (β := ℝ) (‖L‖ * (↑(max 1 n) : ℝ))
      (max ((SchwartzMap.seminorm 𝕜 (k + 1) n : (a : 𝓢(E, F)) → ℝ) f)
          ((SchwartzMap.seminorm 𝕜 k (n - 1) : (a : 𝓢(E, F)) → ℝ) f) :
        ℝ) =
  HMul.hMul (β := ℝ) (2 * ‖L‖ * (↑(max 1 n) : ℝ))
    (max ((SchwartzMap.seminorm 𝕜 (k + 1) n : (a : 𝓢(E, F)) → ℝ) f)
        ((SchwartzMap.seminorm 𝕜 k (n - 1) : (a : 𝓢(E, F)) → ℝ) f) :
      ℝ)
Tactic: simp only [Finset.sup_insert, schwartzSeminormFamily_apply, Finset.sup_singleton,
            Seminorm.coe_sup, Pi.sup_apply]
-- 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 : RCLike 𝕜
inst_5 : NormedAddCommGroup D
inst_6 : NormedSpace ℝ D
inst_7 : NormedSpace 𝕜 F
g : D → E
hg : Function.HasTemperateGrowth g
hg_upper : ∃ (k : ℕ) (C : ℝ), ∀ (x : D), ‖x‖ ≤ C * (1 + ‖g x‖) ^ k
k n : ℕ
⊢ ∃ (s : Finset (ℕ × ℕ)) (C : ℝ),
    0 ≤ C ∧
      ∀ (f : 𝓢(E, F)) (x : D),
        ‖x‖ ^ (k, n).1 *
            norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_6} ℝ (fun (i : Fin (k, n).2) ↦ D) F)
              (iteratedFDeriv ℝ (k, n).2 ((fun (f : 𝓢(E, F)) ↦ ((⇑f : (a : E) → F) ∘ g : D → F)) f) x) ≤
          HMul.hMul (β := ℝ) C ((s.sup (schwartzSeminormFamily 𝕜 E F) : (a : 𝓢(E, F)) → ℝ) f : ℝ)
have rcases : ∀ (l : ℕ) (C : ℝ) (hC : 0 ≤ C)
  (hgrowth :
    ∀ N ≤ n,
      ∀ (x : D),
        norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin N) ↦ D) E) (iteratedFDeriv ℝ N g x) ≤
          C * (1 + ‖x‖) ^ l),
  ∃ (s : Finset (ℕ × ℕ)) (C : ℝ),
    0 ≤ C ∧
      ∀ (f : 𝓢(E, F)) (x : D),
        ‖x‖ ^ (k, n).1 *
            norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_6} ℝ (fun (i : Fin (k, n).2) ↦ D) F)
              (iteratedFDeriv ℝ (k, n).2 ((fun (f : 𝓢(E, F)) ↦ ((⇑f : (a : E) → F) ∘ g : D → F)) f) x) ≤
          HMul.hMul (β := ℝ) C ((s.sup (schwartzSeminormFamily 𝕜 E F) : (a : 𝓢(E, F)) → ℝ) f : ℝ)
Tactic: rcases hg.norm_iteratedFDeriv_le_uniform n with ⟨l, C, hC, hgrowth⟩
-- 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 : RCLike 𝕜
inst_5 : NormedAddCommGroup D
inst_6 : NormedSpace ℝ D
inst_7 : NormedSpace 𝕜 F
g : D → E
hg : Function.HasTemperateGrowth g
hg_upper : ∃ (k : ℕ) (C : ℝ), ∀ (x : D), ‖x‖ ≤ C * (1 + ‖g x‖) ^ k
k n l : ℕ
C : ℝ
hC : 0 ≤ C
hgrowth :
  ∀ N ≤ n,
    ∀ (x : D),
      norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin N) ↦ D) E) (iteratedFDeriv ℝ N g x) ≤
        C * (1 + ‖x‖) ^ l
⊢ ∃ (s : Finset (ℕ × ℕ)) (C : ℝ),
    0 ≤ C ∧
      ∀ (f : 𝓢(E, F)) (x : D),
        ‖x‖ ^ (k, n).1 *
            norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_6} ℝ (fun (i : Fin (k, n).2) ↦ D) F)
              (iteratedFDeriv ℝ (k, n).2 ((fun (f : 𝓢(E, F)) ↦ ((⇑f : (a : E) → F) ∘ g : D → F)) f) x) ≤
          HMul.hMul (β := ℝ) C ((s.sup (schwartzSeminormFamily 𝕜 E F) : (a : 𝓢(E, F)) → ℝ) f : ℝ)
have rcases : ∀ (kg : ℕ) (Cg : ℝ) (hg_upper' : ∀ (x : D), ‖x‖ ≤ Cg * (1 + ‖g x‖) ^ kg),
  ∃ (s : Finset (ℕ × ℕ)) (C : ℝ),
    0 ≤ C ∧
      ∀ (f : 𝓢(E, F)) (x : D),
        ‖x‖ ^ (k, n).1 *
            norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_6} ℝ (fun (i : Fin (k, n).2) ↦ D) F)
              (iteratedFDeriv ℝ (k, n).2 ((fun (f : 𝓢(E, F)) ↦ ((⇑f : (a : E) → F) ∘ g : D → F)) f) x) ≤
          HMul.hMul (β := ℝ) C ((s.sup (schwartzSeminormFamily 𝕜 E F) : (a : 𝓢(E, F)) → ℝ) f : ℝ)
Tactic: rcases hg_upper with ⟨kg, Cg, hg_upper'⟩
Cleared hypotheses: hg_upper
-- 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 : RCLike 𝕜
inst_5 : NormedAddCommGroup D
inst_6 : NormedSpace ℝ D
inst_7 : NormedSpace 𝕜 F
g : D → E
hg : Function.HasTemperateGrowth g
k n l : ℕ
C : ℝ
hC : 0 ≤ C
hgrowth :
  ∀ N ≤ n,
    ∀ (x : D),
      norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin N) ↦ D) E) (iteratedFDeriv ℝ N g x) ≤
        C * (1 + ‖x‖) ^ l
kg : ℕ
Cg : ℝ
hg_upper' : ∀ (x : D), ‖x‖ ≤ Cg * (1 + ‖g x‖) ^ kg
⊢ 1 ≤ 1 + Cg
have refine : 0 ≤ Cg
Tactic: refine le_add_of_nonneg_right ?_
-- 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
inst_4 : RCLike 𝕜
inst_5 : NormedAddCommGroup D
inst_6 : NormedSpace ℝ D
inst_7 : NormedSpace 𝕜 F
g : D → E
hg : Function.HasTemperateGrowth g
k n l : ℕ
C : ℝ
hC : 0 ≤ C
hgrowth :
  ∀ N ≤ n,
    ∀ (x : D),
      norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin N) ↦ D) E) (iteratedFDeriv ℝ N g x) ≤
        C * (1 + ‖x‖) ^ l
kg : ℕ
Cg : ℝ
hg_upper' : ∀ (x : D), ‖x‖ ≤ Cg * (1 + ‖g x‖) ^ kg
⊢ 0 ≤ Cg
have hg_upper'₁ : norm.{u_4} (E := D) 0 ≤ Cg * (1 + ‖g 0‖) ^ kg
Tactic: specialize hg_upper' 0
Cleared hypotheses: hg_upper'
-- 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
inst_4 : RCLike 𝕜
inst_5 : NormedAddCommGroup D
inst_6 : NormedSpace ℝ D
inst_7 : NormedSpace 𝕜 F
g : D → E
hg : Function.HasTemperateGrowth g
k n l : ℕ
C : ℝ
hC : 0 ≤ C
hgrowth :
  ∀ N ≤ n,
    ∀ (x : D),
      norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin N) ↦ D) E) (iteratedFDeriv ℝ N g x) ≤
        C * (1 + ‖x‖) ^ l
kg : ℕ
Cg : ℝ
hg_upper' : norm.{u_4} (E := D) 0 ≤ Cg * (1 + ‖g 0‖) ^ kg
⊢ 0 ≤ Cg
have hg_upper'₁ : 0 ≤ Cg * (1 + ‖g 0‖) ^ kg
Tactic: rw [norm_zero] at hg_upper'
Cleared hypotheses: hg_upper'
-- 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
inst_4 : RCLike 𝕜
inst_5 : NormedAddCommGroup D
inst_6 : NormedSpace ℝ D
inst_7 : NormedSpace 𝕜 F
g : D → E
hg : Function.HasTemperateGrowth g
k n l : ℕ
C : ℝ
hC : 0 ≤ C
hgrowth :
  ∀ N ≤ n,
    ∀ (x : D),
      norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin N) ↦ D) E) (iteratedFDeriv ℝ N g x) ≤
        C * (1 + ‖x‖) ^ l
kg : ℕ
Cg : ℝ
hg_upper' : ∀ (x : D), ‖x‖ ≤ Cg * (1 + ‖g x‖) ^ kg
⊢ ∃ (s : Finset (ℕ × ℕ)) (C : ℝ),
    0 ≤ C ∧
      ∀ (f : 𝓢(E, F)) (x : D),
        ‖x‖ ^ (k, n).1 *
            norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_6} ℝ (fun (i : Fin (k, n).2) ↦ D) F)
              (iteratedFDeriv ℝ (k, n).2 ((fun (f : 𝓢(E, F)) ↦ ((⇑f : (a : E) → F) ∘ g : D → F)) f) x) ≤
          HMul.hMul (β := ℝ) C ((s.sup (schwartzSeminormFamily 𝕜 E F) : (a : 𝓢(E, F)) → ℝ) f : ℝ)
have hCg : 1 ≤ 1 + Cg
Tactic: have hCg : 1 ≤ 1 + Cg := by
    refine le_add_of_nonneg_right ?_
    specialize hg_upper' 0
    rw [norm_zero] at hg_upper'
    exact nonneg_of_mul_nonneg_left hg_upper' (by positivity)
-- 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 : RCLike 𝕜
inst_5 : NormedAddCommGroup D
inst_6 : NormedSpace ℝ D
inst_7 : NormedSpace 𝕜 F
g : D → E
hg : Function.HasTemperateGrowth g
k n l : ℕ
C : ℝ
hC : 0 ≤ C
hgrowth :
  ∀ N ≤ n,
    ∀ (x : D),
      norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin N) ↦ D) E) (iteratedFDeriv ℝ N g x) ≤
        C * (1 + ‖x‖) ^ l
kg : ℕ
Cg : ℝ
hg_upper' : ∀ (x : D), ‖x‖ ≤ Cg * (1 + ‖g x‖) ^ kg
hCg : 1 ≤ 1 + Cg
k' : ℕ := kg * (k + l * n)
⊢ ∃ (s : Finset (ℕ × ℕ)) (C : ℝ),
    0 ≤ C ∧
      ∀ (f : 𝓢(E, F)) (x : D),
        ‖x‖ ^ (k, n).1 *
            norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_6} ℝ (fun (i : Fin (k, n).2) ↦ D) F)
              (iteratedFDeriv ℝ (k, n).2 ((fun (f : 𝓢(E, F)) ↦ ((⇑f : (a : E) → F) ∘ g : D → F)) f) x) ≤
          HMul.hMul (β := ℝ) C ((s.sup (schwartzSeminormFamily 𝕜 E F) : (a : 𝓢(E, F)) → ℝ) f : ℝ)
have right : ∀ (f : 𝓢(E, F)) (x : D),
  ‖x‖ ^ (k, n).1 *
      norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_6} ℝ (fun (i : Fin (k, n).2) ↦ D) F)
        (iteratedFDeriv ℝ (k, n).2 ((fun (f : 𝓢(E, F)) ↦ ((⇑f : (a : E) → F) ∘ g : D → F)) f) x) ≤
    HMul.hMul (β := ℝ) ((1 + Cg) ^ (k + l * n) * ((C + 1) ^ n * (↑n ! : ℝ) * HPow.hPow (α := ℝ) 2 k'))
      (((Finset.Iic (k', n)).sup (schwartzSeminormFamily 𝕜 E F) : (a : 𝓢(E, F)) → ℝ) f : ℝ)
Tactic: use Finset.Iic (k', n), (1 + Cg) ^ (k + l * n) * ((C + 1) ^ n * n ! * 2 ^ k'), by positivity
-- 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 : RCLike 𝕜
inst_5 : NormedAddCommGroup D
inst_6 : NormedSpace ℝ D
inst_7 : NormedSpace 𝕜 F
g : D → E
hg : Function.HasTemperateGrowth g
k n l : ℕ
C : ℝ
hC : 0 ≤ C
hgrowth :
  ∀ N ≤ n,
    ∀ (x : D),
      norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin N) ↦ D) E) (iteratedFDeriv ℝ N g x) ≤
        C * (1 + ‖x‖) ^ l
kg : ℕ
Cg : ℝ
hg_upper' : ∀ (x : D), ‖x‖ ≤ Cg * (1 + ‖g x‖) ^ kg
hCg : 1 ≤ 1 + Cg
k' : ℕ := kg * (k + l * n)
f : 𝓢(E, F)
x : D
seminorm_f : ℝ := ((Finset.Iic (k', n)).sup (schwartzSeminormFamily 𝕜 E F) : (a : 𝓢(E, F)) → ℝ) f
⊢ (1 + ‖x‖) ^ (k + l * n) ≤ (1 + Cg) ^ (k + l * n) * (1 + ‖g x‖) ^ k'
have rw : (1 + ‖x‖) ^ (k + l * n) ≤ ((1 + Cg) * (1 + ‖g x‖) ^ kg) ^ (k + l * n)
Tactic: rw [pow_mul, ← mul_pow]
-- 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 : RCLike 𝕜
inst_5 : NormedAddCommGroup D
inst_6 : NormedSpace ℝ D
inst_7 : NormedSpace 𝕜 F
g : D → E
hg : Function.HasTemperateGrowth g
k n l : ℕ
C : ℝ
hC : 0 ≤ C
hgrowth :
  ∀ N ≤ n,
    ∀ (x : D),
      norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin N) ↦ D) E) (iteratedFDeriv ℝ N g x) ≤
        C * (1 + ‖x‖) ^ l
kg : ℕ
Cg : ℝ
hg_upper' : ∀ (x : D), ‖x‖ ≤ Cg * (1 + ‖g x‖) ^ kg
hCg : 1 ≤ 1 + Cg
k' : ℕ := kg * (k + l * n)
f : 𝓢(E, F)
x : D
seminorm_f : ℝ := ((Finset.Iic (k', n)).sup (schwartzSeminormFamily 𝕜 E F) : (a : 𝓢(E, F)) → ℝ) f
⊢ (1 + ‖x‖) ^ (k + l * n) ≤ ((1 + Cg) * (1 + ‖g x‖) ^ kg) ^ (k + l * n)
have hab : 1 + ‖x‖ ≤ (1 + Cg) * (1 + ‖g x‖) ^ kg
Tactic: gcongr
-- 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 : RCLike 𝕜
inst_5 : NormedAddCommGroup D
inst_6 : NormedSpace ℝ D
inst_7 : NormedSpace 𝕜 F
g : D → E
hg : Function.HasTemperateGrowth g
k n l : ℕ
C : ℝ
hC : 0 ≤ C
hgrowth :
  ∀ N ≤ n,
    ∀ (x : D),
      norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin N) ↦ D) E) (iteratedFDeriv ℝ N g x) ≤
        C * (1 + ‖x‖) ^ l
kg : ℕ
Cg : ℝ
hg_upper' : ∀ (x : D), ‖x‖ ≤ Cg * (1 + ‖g x‖) ^ kg
hCg : 1 ≤ 1 + Cg
k' : ℕ := kg * (k + l * n)
f : 𝓢(E, F)
x : D
seminorm_f : ℝ := ((Finset.Iic (k', n)).sup (schwartzSeminormFamily 𝕜 E F) : (a : 𝓢(E, F)) → ℝ) f
⊢ 1 + ‖x‖ ≤ (1 + Cg) * (1 + ‖g x‖) ^ kg
have hab : 1 + ‖x‖ ≤ 1 * (1 + ‖g x‖) ^ kg + Cg * (1 + ‖g x‖) ^ kg
Tactic: rw [add_mul]
-- 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 : RCLike 𝕜
inst_5 : NormedAddCommGroup D
inst_6 : NormedSpace ℝ D
inst_7 : NormedSpace 𝕜 F
g : D → E
hg : Function.HasTemperateGrowth g
k n l : ℕ
C : ℝ
hC : 0 ≤ C
hgrowth :
  ∀ N ≤ n,
    ∀ (x : D),
      norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin N) ↦ D) E) (iteratedFDeriv ℝ N g x) ≤
        C * (1 + ‖x‖) ^ l
kg : ℕ
Cg : ℝ
hg_upper' : ∀ (x : D), ‖x‖ ≤ Cg * (1 + ‖g x‖) ^ kg
hCg : 1 ≤ 1 + Cg
k' : ℕ := kg * (k + l * n)
f : 𝓢(E, F)
x : D
seminorm_f : ℝ := ((Finset.Iic (k', n)).sup (schwartzSeminormFamily 𝕜 E F) : (a : 𝓢(E, F)) → ℝ) f
⊢ 1 + ‖x‖ ≤ 1 * (1 + ‖g x‖) ^ kg + Cg * (1 + ‖g x‖) ^ kg
have hab : 1 ≤ 1 * (1 + ‖g x‖) ^ kg
Tactic: refine add_le_add ?_ (hg_upper' 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 : RCLike 𝕜
inst_5 : NormedAddCommGroup D
inst_6 : NormedSpace ℝ D
inst_7 : NormedSpace 𝕜 F
g : D → E
hg : Function.HasTemperateGrowth g
k n l : ℕ
C : ℝ
hC : 0 ≤ C
hgrowth :
  ∀ N ≤ n,
    ∀ (x : D),
      norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin N) ↦ D) E) (iteratedFDeriv ℝ N g x) ≤
        C * (1 + ‖x‖) ^ l
kg : ℕ
Cg : ℝ
hg_upper' : ∀ (x : D), ‖x‖ ≤ Cg * (1 + ‖g x‖) ^ kg
hCg : 1 ≤ 1 + Cg
k' : ℕ := kg * (k + l * n)
f : 𝓢(E, F)
x : D
seminorm_f : ℝ := ((Finset.Iic (k', n)).sup (schwartzSeminormFamily 𝕜 E F) : (a : 𝓢(E, F)) → ℝ) f
⊢ 1 ≤ 1 * (1 + ‖g x‖) ^ kg
have hab : HMul.hMul (α := ℝ) 1 1 ≤ 1 * (1 + ‖g x‖) ^ kg
Tactic: nth_rw 1 [← one_mul (1 : ℝ)]
-- 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 : RCLike 𝕜
inst_5 : NormedAddCommGroup D
inst_6 : NormedSpace ℝ D
inst_7 : NormedSpace 𝕜 F
g : D → E
hg : Function.HasTemperateGrowth g
k n l : ℕ
C : ℝ
hC : 0 ≤ C
hgrowth :
  ∀ N ≤ n,
    ∀ (x : D),
      norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin N) ↦ D) E) (iteratedFDeriv ℝ N g x) ≤
        C * (1 + ‖x‖) ^ l
kg : ℕ
Cg : ℝ
hg_upper' : ∀ (x : D), ‖x‖ ≤ Cg * (1 + ‖g x‖) ^ kg
hCg : 1 ≤ 1 + Cg
k' : ℕ := kg * (k + l * n)
f : 𝓢(E, F)
x : D
seminorm_f : ℝ := ((Finset.Iic (k', n)).sup (schwartzSeminormFamily 𝕜 E F) : (a : 𝓢(E, F)) → ℝ) f
⊢ HMul.hMul (α := ℝ) 1 1 ≤ 1 * (1 + ‖g x‖) ^ kg
have hab : 1 ≤ (1 + ‖g x‖) ^ kg
Tactic: gcongr
-- 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 : RCLike 𝕜
inst_5 : NormedAddCommGroup D
inst_6 : NormedSpace ℝ D
inst_7 : NormedSpace 𝕜 F
g : D → E
hg : Function.HasTemperateGrowth g
k n l : ℕ
C : ℝ
hC : 0 ≤ C
hgrowth :
  ∀ N ≤ n,
    ∀ (x : D),
      norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin N) ↦ D) E) (iteratedFDeriv ℝ N g x) ≤
        C * (1 + ‖x‖) ^ l
kg : ℕ
Cg : ℝ
hg_upper' : ∀ (x : D), ‖x‖ ≤ Cg * (1 + ‖g x‖) ^ kg
hCg : 1 ≤ 1 + Cg
k' : ℕ := kg * (k + l * n)
f : 𝓢(E, F)
x : D
seminorm_f : ℝ := ((Finset.Iic (k', n)).sup (schwartzSeminormFamily 𝕜 E F) : (a : 𝓢(E, F)) → ℝ) f
⊢ 1 ≤ (1 + ‖g x‖) ^ kg
have hab : 1 ≤ 1 + ‖g x‖
Tactic: apply one_le_pow₀