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 : RCLike 𝕜
inst_5 : NormedAddCommGroup D
inst_6 : NormedSpace ℝ D
inst_7 : NormedSpace 𝕜 F
K : ℝ≥0
g : D → E
hg : Function.HasTemperateGrowth g
h'g : AntilipschitzWith K g
x : D
⊢ (↑K : ℝ) * ‖g x - g 0‖ ≤ (↑K : ℝ) * (‖g x‖ + ‖g 0‖)
have hbc : ‖g x - g 0‖ ≤ ‖g x‖ + ‖g 0‖
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
K : ℝ≥0
g : D → E
hg : Function.HasTemperateGrowth g
h'g : AntilipschitzWith K g
x : D
⊢ (↑K : ℝ) * (‖g x‖ + ‖g 0‖) ≤ (↑K : ℝ) * (‖g x‖ + max 1 ‖g 0‖)
have hbc : ‖g 0‖ ≤ max 1 ‖g 0‖
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
K : ℝ≥0
g : D → E
hg : Function.HasTemperateGrowth g
h'g : AntilipschitzWith K g
x : D
⊢ (↑K : ℝ) * (‖g x‖ + max 1 ‖g 0‖) ≤ (↑K : ℝ) * max 1 ‖g 0‖ * HPow.hPow (β := ℕ) (1 + ‖g x‖) 1
have simp : (↑K : ℝ) * ‖g x‖ ≤ (↑K : ℝ) * max 1 ‖g 0‖ * ‖g x‖
Tactic: simp only [mul_add, add_comm (K * ‖g x‖), pow_one, mul_one, add_le_add_iff_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
inst_4 : RCLike 𝕜
inst_5 : NormedAddCommGroup D
inst_6 : NormedSpace ℝ D
inst_7 : NormedSpace 𝕜 F
K : ℝ≥0
g : D → E
hg : Function.HasTemperateGrowth g
h'g : AntilipschitzWith K g
x : D
⊢ (↑K : ℝ) * ‖g x‖ ≤ (↑K : ℝ) * max 1 ‖g 0‖ * ‖g x‖
have hbc : (↑K : ℝ) ≤ (↑K : ℝ) * max 1 ‖g 0‖
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
K : ℝ≥0
g : D → E
hg : Function.HasTemperateGrowth g
h'g : AntilipschitzWith K g
x : D
⊢ ‖x‖ ≤ (↑K : ℝ) * max 1 ‖g 0‖ * HPow.hPow (β := ℕ) (1 + ‖g x‖) 1
have K₁ : ‖x‖ ≤ (↑K : ℝ) * ‖g x - g 0‖
Tactic: calc
  ‖x‖ ≤ K * ‖g x - g 0‖ := by
    rw [← dist_zero_right, ← dist_eq_norm]
    apply h'g.le_mul_dist
  _ ≤ K * (‖g x‖ + ‖g 0‖) := by
    gcongr
    exact norm_sub_le _ _
  _ ≤ K * (‖g x‖ + max 1 ‖g 0‖) := by
    gcongr
    exact le_max_right _ _
  _ ≤ (K * max 1 ‖g 0‖ : ℝ) * (1 + ‖g x‖) ^ 1 := by
    simp only [mul_add, add_comm (K * ‖g x‖), pow_one, mul_one, add_le_add_iff_left]
    gcongr
    exact le_mul_of_one_le_right (by positivity) (le_max_left _ _)
-- 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
K : ℝ≥0
g : D → E
hg : Function.HasTemperateGrowth g
h'g : AntilipschitzWith K g
x : D
K₁ : ‖x‖ ≤ (↑K : ℝ) * ‖g x - g 0‖
⊢ ‖x‖ ≤ (↑K : ℝ) * max 1 ‖g 0‖ * HPow.hPow (β := ℕ) (1 + ‖g x‖) 1
have K₂ : (↑K : ℝ) * ‖g x - g 0‖ ≤ (↑K : ℝ) * (‖g x‖ + ‖g 0‖)
Tactic: calc
  ‖x‖ ≤ K * ‖g x - g 0‖ := by
    rw [← dist_zero_right, ← dist_eq_norm]
    apply h'g.le_mul_dist
  _ ≤ K * (‖g x‖ + ‖g 0‖) := by
    gcongr
    exact norm_sub_le _ _
  _ ≤ K * (‖g x‖ + max 1 ‖g 0‖) := by
    gcongr
    exact le_max_right _ _
  _ ≤ (K * max 1 ‖g 0‖ : ℝ) * (1 + ‖g x‖) ^ 1 := by
    simp only [mul_add, add_comm (K * ‖g x‖), pow_one, mul_one, add_le_add_iff_left]
    gcongr
    exact le_mul_of_one_le_right (by positivity) (le_max_left _ _)
-- 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
K : ℝ≥0
g : D → E
hg : Function.HasTemperateGrowth g
h'g : AntilipschitzWith K g
x : D
K₁ : ‖x‖ ≤ (↑K : ℝ) * ‖g x - g 0‖
K₂ : (↑K : ℝ) * ‖g x - g 0‖ ≤ (↑K : ℝ) * (‖g x‖ + ‖g 0‖)
⊢ ‖x‖ ≤ (↑K : ℝ) * max 1 ‖g 0‖ * HPow.hPow (β := ℕ) (1 + ‖g x‖) 1
have K₃ : (↑K : ℝ) * (‖g x‖ + ‖g 0‖) ≤ (↑K : ℝ) * (‖g x‖ + max 1 ‖g 0‖)
Tactic: calc
  ‖x‖ ≤ K * ‖g x - g 0‖ := by
    rw [← dist_zero_right, ← dist_eq_norm]
    apply h'g.le_mul_dist
  _ ≤ K * (‖g x‖ + ‖g 0‖) := by
    gcongr
    exact norm_sub_le _ _
  _ ≤ K * (‖g x‖ + max 1 ‖g 0‖) := by
    gcongr
    exact le_max_right _ _
  _ ≤ (K * max 1 ‖g 0‖ : ℝ) * (1 + ‖g x‖) ^ 1 := by
    simp only [mul_add, add_comm (K * ‖g x‖), pow_one, mul_one, add_le_add_iff_left]
    gcongr
    exact le_mul_of_one_le_right (by positivity) (le_max_left _ _)
-- 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
K : ℝ≥0
g : D → E
hg : Function.HasTemperateGrowth g
h'g : AntilipschitzWith K g
x : D
K₁ : ‖x‖ ≤ (↑K : ℝ) * ‖g x - g 0‖
K₂ : (↑K : ℝ) * ‖g x - g 0‖ ≤ (↑K : ℝ) * (‖g x‖ + ‖g 0‖)
K₃ : (↑K : ℝ) * (‖g x‖ + ‖g 0‖) ≤ (↑K : ℝ) * (‖g x‖ + max 1 ‖g 0‖)
⊢ ‖x‖ ≤ (↑K : ℝ) * max 1 ‖g 0‖ * HPow.hPow (β := ℕ) (1 + ‖g x‖) 1
have K₄ : (↑K : ℝ) * (‖g x‖ + max 1 ‖g 0‖) ≤ (↑K : ℝ) * max 1 ‖g 0‖ * HPow.hPow (β := ℕ) (1 + ‖g x‖) 1
Tactic: calc
  ‖x‖ ≤ K * ‖g x - g 0‖ := by
    rw [← dist_zero_right, ← dist_eq_norm]
    apply h'g.le_mul_dist
  _ ≤ K * (‖g x‖ + ‖g 0‖) := by
    gcongr
    exact norm_sub_le _ _
  _ ≤ K * (‖g x‖ + max 1 ‖g 0‖) := by
    gcongr
    exact le_max_right _ _
  _ ≤ (K * max 1 ‖g 0‖ : ℝ) * (1 + ‖g x‖) ^ 1 := by
    simp only [mul_add, add_comm (K * ‖g x‖), pow_one, mul_one, add_le_add_iff_left]
    gcongr
    exact le_mul_of_one_le_right (by positivity) (le_max_left _ _)
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Basic (goal)
Goal:
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : RCLike 𝕜
inst_5 : NormedAddCommGroup D
inst_6 : NormedSpace ℝ D
inst_7 : NormedSpace 𝕜 F
inst_8 : NontriviallyNormedField 𝕜'
inst_9 : NormedAlgebra ℝ 𝕜'
inst_10 : NormedSpace 𝕜' F
u : D → 𝕜'
hu : Function.HasTemperateGrowth u
g : D ≃L[ℝ] E
f : 𝓢(E, F)
⊢ Eq (α := 𝓢(D, F))
    (((smulLeftCLM F u : 𝓢(D, F) →L[𝕜'] 𝓢(D, F)) : (a : 𝓢(D, F)) → 𝓢(D, F))
        ((compCLMOfContinuousLinearEquiv 𝕜 g : (a : 𝓢(E, F)) → 𝓢(D, F)) f) :
      𝓢(D, F))
    ((compCLMOfContinuousLinearEquiv 𝕜 g : (a : 𝓢(E, F)) → 𝓢(D, F))
        (((smulLeftCLM F (u ∘ (⇑g.symm : (a : E) → D)) : 𝓢(E, F) →L[𝕜'] 𝓢(E, F)) : (a : 𝓢(E, F)) → 𝓢(E, F)) f) :
      𝓢(D, F))
have h : ∀ (x : D),
  Eq.{u_6 + 1} (α := F)
    (((((smulLeftCLM F u : 𝓢(D, F) →L[𝕜'] 𝓢(D, F)) : (a : 𝓢(D, F)) → 𝓢(D, F))
              ((compCLMOfContinuousLinearEquiv 𝕜 g : (a : 𝓢(E, F)) → 𝓢(D, F)) f) :
            𝓢(D, F)) :
          (a : D) → F)
        x :
      F)
    ((((compCLMOfContinuousLinearEquiv 𝕜 g : (a : 𝓢(E, F)) → 𝓢(D, F))
              (((smulLeftCLM F (u ∘ (⇑g.symm : (a : E) → D)) : 𝓢(E, F) →L[𝕜'] 𝓢(E, F)) : (a : 𝓢(E, F)) → 𝓢(E, F)) f) :
            𝓢(D, F)) :
          (a : D) → F)
        x :
      F)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Basic (hypothesis)
Goal:
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : RCLike 𝕜
inst_5 : NormedAddCommGroup D
inst_6 : NormedSpace ℝ D
inst_7 : NormedSpace 𝕜 F
inst_8 : NontriviallyNormedField 𝕜'
inst_9 : NormedAlgebra ℝ 𝕜'
inst_10 : NormedSpace 𝕜' F
u : D → 𝕜'
hu : Function.HasTemperateGrowth u
g : D ≃L[ℝ] E
f : 𝓢(E, F)
x : D
⊢ Eq.{u_6 + 1} (α := F)
    (((((smulLeftCLM F u : 𝓢(D, F) →L[𝕜'] 𝓢(D, F)) : (a : 𝓢(D, F)) → 𝓢(D, F))
              ((compCLMOfContinuousLinearEquiv 𝕜 g : (a : 𝓢(E, F)) → 𝓢(D, F)) f) :
            𝓢(D, F)) :
          (a : D) → F)
        x :
      F)
    ((((compCLMOfContinuousLinearEquiv 𝕜 g : (a : 𝓢(E, F)) → 𝓢(D, F))
              (((smulLeftCLM F (u ∘ (⇑g.symm : (a : E) → D)) : 𝓢(E, F) →L[𝕜'] 𝓢(E, F)) : (a : 𝓢(E, F)) → 𝓢(E, F)) f) :
            𝓢(D, F)) :
          (a : D) → F)
        x :
      F)
have hu' : Function.HasTemperateGrowth.{u_5, u_3} (E := E) (u ∘ (⇑g.symm : (a : E) → D))
Tactic: have hu' : (u ∘ g.symm).HasTemperateGrowth := by fun_prop
-- 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 : NormedSpace 𝕜 F
inst_6 : NormedAddCommGroup G
inst_7 : NormedSpace ℝ G
inst_8 : NormedSpace 𝕜 G
inst_9 : NormedAddCommGroup H
inst_10 : NormedSpace ℝ H
inst_11 : NormedSpace 𝕜 H
L : F →L[𝕜] G
k n : ℕ
⊢ ∃ (s : Finset (ℕ × ℕ)) (C : ℝ),
    0 ≤ C ∧
      ∀ (f : 𝓢(E, F)) (x : E),
        ‖x‖ ^ (k, n).1 *
            norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_7} ℝ (fun (i : Fin (k, n).2) ↦ E) G)
              (iteratedFDeriv ℝ (k, n).2
                ((fun (f : 𝓢(E, F)) ↦
                    (Function.comp.{u_5 + 1, u_6 + 1, u_7 + 1} (β := F) (⇑L : (a : F) → G) (⇑f : (a : E) → F) : E → G))
                  f)
                x) ≤
          HMul.hMul (β := ℝ) C ((s.sup (schwartzSeminormFamily 𝕜 E F) : (a : 𝓢(E, F)) → ℝ) f : ℝ)
have right : ∀ (f : 𝓢(E, F)) (x : E),
  ‖x‖ ^ (k, n).1 *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_7} ℝ (fun (i : Fin (k, n).2) ↦ E) G)
        (iteratedFDeriv ℝ (k, n).2
          ((fun (f : 𝓢(E, F)) ↦
              (Function.comp.{u_5 + 1, u_6 + 1, u_7 + 1} (β := F) (⇑L : (a : F) → G) (⇑f : (a : E) → F) : E → G))
            f)
          x) ≤
    HMul.hMul (β := ℝ) ‖L‖ ((Finset.sup {(k, n)} (schwartzSeminormFamily 𝕜 E F) : (a : 𝓢(E, F)) → ℝ) f : ℝ)
Tactic: use {⟨k, n⟩}, ‖L‖, 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 : NormedSpace 𝕜 F
inst_6 : NormedAddCommGroup G
inst_7 : NormedSpace ℝ G
inst_8 : NormedSpace 𝕜 G
inst_9 : NormedAddCommGroup H
inst_10 : NormedSpace ℝ H
inst_11 : NormedSpace 𝕜 H
L : F →L[𝕜] G
k n : ℕ
f : 𝓢(E, F)
x : E
⊢ ‖x‖ ^ (k, n).1 *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_7} ℝ (fun (i : Fin (k, n).2) ↦ E) G)
        (iteratedFDeriv ℝ (k, n).2
          ((fun (f : 𝓢(E, F)) ↦
              (Function.comp.{u_5 + 1, u_6 + 1, u_7 + 1} (β := F) (⇑L : (a : F) → G) (⇑f : (a : E) → F) : E → G))
            f)
          x) ≤
    HMul.hMul (β := ℝ) ‖L‖ ((Finset.sup {(k, n)} (schwartzSeminormFamily 𝕜 E F) : (a : 𝓢(E, F)) → ℝ) f : ℝ)
have right : ‖x‖ ^ k *
    norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_7} ℝ (fun (i : Fin n) ↦ E) G)
      (iteratedFDeriv ℝ n (Function.comp.{u_5 + 1, u_6 + 1, u_7 + 1} (β := F) (⇑L : (a : F) → G) (⇑f : (a : E) → F))
        x) ≤
  HMul.hMul (β := ℝ) ‖L‖ ((SchwartzMap.seminorm 𝕜 k n : (a : 𝓢(E, F)) → ℝ) f : ℝ)
Tactic: simp only [Finset.sup_singleton, schwartzSeminormFamily_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 : NormedSpace 𝕜 F
inst_6 : NormedAddCommGroup G
inst_7 : NormedSpace ℝ G
inst_8 : NormedSpace 𝕜 G
inst_9 : NormedAddCommGroup H
inst_10 : NormedSpace ℝ H
inst_11 : NormedSpace 𝕜 H
L : F →L[𝕜] G
k n : ℕ
f : 𝓢(E, F)
x : E
⊢ ‖x‖ ^ k *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_7} ℝ (fun (i : Fin n) ↦ E) G)
        (iteratedFDeriv ℝ n (Function.comp.{u_5 + 1, u_6 + 1, u_7 + 1} (β := F) (⇑L : (a : F) → G) (⇑f : (a : E) → F))
          x) =
    ‖x‖ ^ k *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_7} ℝ (fun (i : Fin n) ↦ E) G)
        (ContinuousLinearMap.compContinuousMultilinearMap (M₁ := fun (i : Fin n) ↦ E)
          (ContinuousLinearMap.restrictScalars ℝ L) (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x))
have e_a : Eq (α := ContinuousMultilinearMap.{0, 0, u_5, u_7} ℝ (fun (i : Fin n) ↦ E) G)
  (iteratedFDeriv ℝ n (Function.comp.{u_5 + 1, u_6 + 1, u_7 + 1} (β := F) (⇑L : (a : F) → G) (⇑f : (a : E) → F)) x)
  (ContinuousLinearMap.compContinuousMultilinearMap (M₁ := fun (i : Fin n) ↦ E)
    (ContinuousLinearMap.restrictScalars ℝ L) (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x))
Tactic: congr
-- 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 : NormedSpace 𝕜 F
inst_6 : NormedAddCommGroup G
inst_7 : NormedSpace ℝ G
inst_8 : NormedSpace 𝕜 G
inst_9 : NormedAddCommGroup H
inst_10 : NormedSpace ℝ H
inst_11 : NormedSpace 𝕜 H
L : F →L[𝕜] G
k n : ℕ
f : 𝓢(E, F)
x : E
⊢ ‖x‖ ^ k *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_7} ℝ (fun (i : Fin n) ↦ E) G)
        (ContinuousLinearMap.compContinuousMultilinearMap (M₁ := fun (i : Fin n) ↦ E)
          (ContinuousLinearMap.restrictScalars ℝ L) (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x)) ≤
    ‖x‖ ^ k *
      (‖L‖ *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
          (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x))
have hbc : norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_7} ℝ (fun (i : Fin n) ↦ E) G)
    (ContinuousLinearMap.compContinuousMultilinearMap (M₁ := fun (i : Fin n) ↦ E)
      (ContinuousLinearMap.restrictScalars ℝ L) (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x)) ≤
  ‖L‖ *
    norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
      (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x)
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 : NormedSpace 𝕜 F
inst_6 : NormedAddCommGroup G
inst_7 : NormedSpace ℝ G
inst_8 : NormedSpace 𝕜 G
inst_9 : NormedAddCommGroup H
inst_10 : NormedSpace ℝ H
inst_11 : NormedSpace 𝕜 H
L : F →L[𝕜] G
k n : ℕ
f : 𝓢(E, F)
x : E
⊢ ‖L‖ *
      (‖x‖ ^ k *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
          (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x)) ≤
    HMul.hMul (β := ℝ) ‖L‖ ((SchwartzMap.seminorm 𝕜 k n : (a : 𝓢(E, F)) → ℝ) f : ℝ)
have h₁ : 0 ≤ ‖L‖
Tactic: grw [le_seminorm 𝕜 k n 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 : RCLike 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : NormedAddCommGroup G
inst_7 : NormedSpace ℝ G
inst_8 : NormedSpace 𝕜 G
inst_9 : NormedAddCommGroup H
inst_10 : NormedSpace ℝ H
inst_11 : NormedSpace 𝕜 H
L : F →L[𝕜] G
k n : ℕ
f : 𝓢(E, F)
x : E
h₁ : 0 ≤ ‖L‖
⊢ ‖L‖ *
      (‖x‖ ^ k *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
          (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x)) ≤
    HMul.hMul (β := ℝ) ‖L‖ ((SchwartzMap.seminorm 𝕜 k n : (a : 𝓢(E, F)) → ℝ) f : ℝ)
have grw : HMul.hMul (β := ℝ) ‖L‖ ((SchwartzMap.seminorm 𝕜 k n : (a : 𝓢(E, F)) → ℝ) f : ℝ) ≤
  HMul.hMul (β := ℝ) ‖L‖ ((SchwartzMap.seminorm 𝕜 k n : (a : 𝓢(E, F)) → ℝ) f : ℝ)
Tactic: grw [le_seminorm 𝕜 k n 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 : RCLike 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : NormedAddCommGroup G
inst_7 : NormedSpace ℝ G
inst_8 : NormedSpace 𝕜 G
inst_9 : NormedAddCommGroup H
inst_10 : NormedSpace ℝ H
inst_11 : NormedSpace 𝕜 H
L : F →L[𝕜] G
k n : ℕ
f : 𝓢(E, F)
x : E
⊢ ‖x‖ ^ k *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_7} ℝ (fun (i : Fin n) ↦ E) G)
        (iteratedFDeriv ℝ n (Function.comp.{u_5 + 1, u_6 + 1, u_7 + 1} (β := F) (⇑L : (a : F) → G) (⇑f : (a : E) → F))
          x) ≤
    HMul.hMul (β := ℝ) ‖L‖ ((SchwartzMap.seminorm 𝕜 k n : (a : 𝓢(E, F)) → ℝ) f : ℝ)
have _ : ‖x‖ ^ k *
    norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_7} ℝ (fun (i : Fin n) ↦ E) G)
      (iteratedFDeriv ℝ n (Function.comp.{u_5 + 1, u_6 + 1, u_7 + 1} (β := F) (⇑L : (a : F) → G) (⇑f : (a : E) → F))
        x) =
  ‖x‖ ^ k *
    norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_7} ℝ (fun (i : Fin n) ↦ E) G)
      (ContinuousLinearMap.compContinuousMultilinearMap (M₁ := fun (i : Fin n) ↦ E)
        (ContinuousLinearMap.restrictScalars ℝ L) (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x))
Tactic: calc
    _ = ‖x‖ ^ k * ‖(L.restrictScalars ℝ).compContinuousMultilinearMap
        (iteratedFDeriv ℝ n f x)‖ := by
      congr
      exact (L.restrictScalars ℝ).iteratedFDeriv_comp_left f.smooth'.contDiffAt (mod_cast le_top)
    _ ≤ ‖x‖ ^ k * (‖L‖ * ‖iteratedFDeriv ℝ n f x‖) := by
      gcongr
      apply (L.restrictScalars ℝ).norm_compContinuousMultilinearMap_le
    _ = ‖L‖ * (‖x‖ ^ k * ‖iteratedFDeriv ℝ n f x‖) := by ring
    _ ≤ ‖L‖ * (SchwartzMap.seminorm 𝕜 k n) f := by
      grw [le_seminorm 𝕜 k n 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 : RCLike 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : NormedAddCommGroup G
inst_7 : NormedSpace ℝ G
inst_8 : NormedSpace 𝕜 G
inst_9 : NormedAddCommGroup H
inst_10 : NormedSpace ℝ H
inst_11 : NormedSpace 𝕜 H
L : F →L[𝕜] G
k n : ℕ
f : 𝓢(E, F)
x : E
_ :
  ‖x‖ ^ k *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_7} ℝ (fun (i : Fin n) ↦ E) G)
        (iteratedFDeriv ℝ n (Function.comp.{u_5 + 1, u_6 + 1, u_7 + 1} (β := F) (⇑L : (a : F) → G) (⇑f : (a : E) → F))
          x) =
    ‖x‖ ^ k *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_7} ℝ (fun (i : Fin n) ↦ E) G)
        (ContinuousLinearMap.compContinuousMultilinearMap (M₁ := fun (i : Fin n) ↦ E)
          (ContinuousLinearMap.restrictScalars ℝ L) (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x))
⊢ ‖x‖ ^ k *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_7} ℝ (fun (i : Fin n) ↦ E) G)
        (iteratedFDeriv ℝ n (Function.comp.{u_5 + 1, u_6 + 1, u_7 + 1} (β := F) (⇑L : (a : F) → G) (⇑f : (a : E) → F))
          x) ≤
    HMul.hMul (β := ℝ) ‖L‖ ((SchwartzMap.seminorm 𝕜 k n : (a : 𝓢(E, F)) → ℝ) f : ℝ)
have _₁ : ‖x‖ ^ k *
    norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_7} ℝ (fun (i : Fin n) ↦ E) G)
      (ContinuousLinearMap.compContinuousMultilinearMap (M₁ := fun (i : Fin n) ↦ E)
        (ContinuousLinearMap.restrictScalars ℝ L) (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x)) ≤
  ‖x‖ ^ k *
    (‖L‖ *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
        (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x))
Tactic: calc
    _ = ‖x‖ ^ k * ‖(L.restrictScalars ℝ).compContinuousMultilinearMap
        (iteratedFDeriv ℝ n f x)‖ := by
      congr
      exact (L.restrictScalars ℝ).iteratedFDeriv_comp_left f.smooth'.contDiffAt (mod_cast le_top)
    _ ≤ ‖x‖ ^ k * (‖L‖ * ‖iteratedFDeriv ℝ n f x‖) := by
      gcongr
      apply (L.restrictScalars ℝ).norm_compContinuousMultilinearMap_le
    _ = ‖L‖ * (‖x‖ ^ k * ‖iteratedFDeriv ℝ n f x‖) := by ring
    _ ≤ ‖L‖ * (SchwartzMap.seminorm 𝕜 k n) f := by
      grw [le_seminorm 𝕜 k n f x]