awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
H : Type u_8
V : Type u_9
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : 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
hbc :
  ∑ i ∈ Finset.range (n + 1),
      (↑(n.choose i) : ℝ) *
          norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_7} ℝ (fun (i : Fin i) ↦ E) (G →L[ℝ] ℝ))
            (iteratedFDeriv ℝ i (⇑L : (a : E) → G →L[ℝ] ℝ) x) *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin (n - i)) ↦ E) F)
          (iteratedFDeriv ℝ (n - i) (⇑f : (a : E) → F) x) ≤
    norm.{u_7} (E := G →L[ℝ] ℝ) ((L : (a : E) → G →L[ℝ] ℝ) x : G →L[ℝ] ℝ) *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
          (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x) +
      (↑n : ℝ) * ‖L‖ *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin (n - 1)) ↦ E) F)
          (iteratedFDeriv ℝ (n - 1) (⇑f : (a : E) → F) x)
⊢ ‖x‖ ^ k *
      ∑ i ∈ Finset.range (n + 1),
        (↑(n.choose i) : ℝ) *
            norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_7} ℝ (fun (i : Fin i) ↦ E) (G →L[ℝ] ℝ))
              (iteratedFDeriv ℝ i (⇑L : (a : E) → G →L[ℝ] ℝ) x) *
          norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin (n - i)) ↦ E) F)
            (iteratedFDeriv ℝ (n - i) (⇑f : (a : E) → F) x) ≤
    ‖x‖ ^ k *
      (norm.{u_7} (E := G →L[ℝ] ℝ) ((L : (a : E) → G →L[ℝ] ℝ) x : G →L[ℝ] ℝ) *
          norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
            (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x) +
        (↑n : ℝ) * ‖L‖ *
          norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin (n - 1)) ↦ E) F)
            (iteratedFDeriv ℝ (n - 1) (⇑f : (a : E) → F) x))

Tactic:
gcongr 1
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
H : Type u_8
V : Type u_9
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : 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
hbc :
  (↑(n.choose 0) : ℝ) *
          norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_7} ℝ (fun (i : Fin 0) ↦ E) (G →L[ℝ] ℝ))
            (iteratedFDeriv ℝ 0 (⇑L : (a : E) → G →L[ℝ] ℝ) x) *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin (n - 0)) ↦ E) F)
          (iteratedFDeriv ℝ (n - 0) (⇑f : (a : E) → F) x) +
      ∑ k ∈ Finset.range n,
        (↑(n.choose (k + 1)) : ℝ) *
            norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_7} ℝ (fun (i : Fin (k + 1)) ↦ E) (G →L[ℝ] ℝ))
              (iteratedFDeriv ℝ (k + 1) (⇑L : (a : E) → G →L[ℝ] ℝ) x) *
          norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin (n - (k + 1))) ↦ E) F)
            (iteratedFDeriv ℝ (n - (k + 1)) (⇑f : (a : E) → F) x) ≤
    norm.{u_7} (E := G →L[ℝ] ℝ) ((L : (a : E) → G →L[ℝ] ℝ) x : G →L[ℝ] ℝ) *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
          (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x) +
      (↑n : ℝ) * ‖L‖ *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin (n - 1)) ↦ E) F)
          (iteratedFDeriv ℝ (n - 1) (⇑f : (a : E) → F) x)
⊢ ∑ i ∈ Finset.range (n + 1),
      (↑(n.choose i) : ℝ) *
          norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_7} ℝ (fun (i : Fin i) ↦ E) (G →L[ℝ] ℝ))
            (iteratedFDeriv ℝ i (⇑L : (a : E) → G →L[ℝ] ℝ) x) *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin (n - i)) ↦ E) F)
          (iteratedFDeriv ℝ (n - i) (⇑f : (a : E) → F) x) ≤
    norm.{u_7} (E := G →L[ℝ] ℝ) ((L : (a : E) → G →L[ℝ] ℝ) x : G →L[ℝ] ℝ) *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
          (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x) +
      (↑n : ℝ) * ‖L‖ *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin (n - 1)) ↦ E) F)
          (iteratedFDeriv ℝ (n - 1) (⇑f : (a : E) → F) x)

Tactic:
rw [Finset.sum_range_succ', add_comm]

Premises used: add_comm, Finset.sum_range_succ'
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
H : Type u_8
V : Type u_9
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : 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 : ℕ
f : 𝓢(E, F)
x : E
⊢ (↑(Nat.choose 0 0) : ℝ) *
          norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_7} ℝ (fun (i : Fin 0) ↦ E) (G →L[ℝ] ℝ))
            (iteratedFDeriv ℝ 0 (⇑L : (a : E) → G →L[ℝ] ℝ) x) *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin (HSub.hSub (α := ℕ) 0 0)) ↦ E) F)
          (iteratedFDeriv ℝ (HSub.hSub (α := ℕ) 0 0) (⇑f : (a : E) → F) x) +
      ∑ k ∈ Finset.range 0,
        (↑(Nat.choose 0 (k + 1)) : ℝ) *
            norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_7} ℝ (fun (i : Fin (k + 1)) ↦ E) (G →L[ℝ] ℝ))
              (iteratedFDeriv ℝ (k + 1) (⇑L : (a : E) → G →L[ℝ] ℝ) x) *
          norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin (0 - (k + 1))) ↦ E) F)
            (iteratedFDeriv ℝ (0 - (k + 1)) (⇑f : (a : E) → F) x) ≤
    norm.{u_7} (E := G →L[ℝ] ℝ) ((L : (a : E) → G →L[ℝ] ℝ) x : G →L[ℝ] ℝ) *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin 0) ↦ E) F)
          (iteratedFDeriv ℝ 0 (⇑f : (a : E) → F) x) +
      (↑0 : ℝ) * ‖L‖ *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin (HSub.hSub (α := ℕ) 0 1)) ↦ E) F)
          (iteratedFDeriv ℝ (HSub.hSub (α := ℕ) 0 1) (⇑f : (a : E) → F) x)

Tactic:
simp
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
H : Type u_8
V : Type u_9
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : 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 : ℕ
f : 𝓢(E, F)
x : E
n : ℕ
h :
  ∀ x_1 ∈ Finset.range n,
    (↑((n + 1).choose (x_1 + 1 + 1)) : ℝ) *
          norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_7} ℝ (fun (i : Fin (x_1 + 1 + 1)) ↦ E) (G →L[ℝ] ℝ))
            (iteratedFDeriv ℝ (x_1 + 1 + 1) (⇑L : (a : E) → G →L[ℝ] ℝ) x) *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin (n + 1 - (x_1 + 1 + 1))) ↦ E) F)
          (iteratedFDeriv ℝ (n + 1 - (x_1 + 1 + 1)) (⇑f : (a : E) → F) x) =
      0
⊢ Eq (α := ℝ)
    (∑ k ∈ Finset.range n,
      (↑((n + 1).choose (k + 1 + 1)) : ℝ) *
          norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_7} ℝ (fun (i : Fin (k + 1 + 1)) ↦ E) (G →L[ℝ] ℝ))
            (iteratedFDeriv ℝ (k + 1 + 1) (⇑L : (a : E) → G →L[ℝ] ℝ) x) *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin (n + 1 - (k + 1 + 1))) ↦ E) F)
          (iteratedFDeriv ℝ (n + 1 - (k + 1 + 1)) (⇑f : (a : E) → F) x))
    0

Tactic:
apply Finset.sum_eq_zero

Premises used: Finset.sum_eq_zero
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
H : Type u_8
V : Type u_9
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : 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 : ℕ
f : 𝓢(E, F)
x : E
n : ℕ
⊢ Eq (α := ℝ)
    (∑ k ∈ Finset.range n,
      (↑((n + 1).choose (k + 1 + 1)) : ℝ) *
          norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_7} ℝ (fun (i : Fin (k + 1 + 1)) ↦ E) (G →L[ℝ] ℝ))
            (iteratedFDeriv ℝ (k + 1 + 1) (⇑L : (a : E) → G →L[ℝ] ℝ) x) *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin (n + 1 - (k + 1 + 1))) ↦ E) F)
          (iteratedFDeriv ℝ (n + 1 - (k + 1 + 1)) (⇑f : (a : E) → F) x))
    0

Tactic:
have : ∑ k ∈ Finset.range n,
                (((n + 1).choose (k + 1 + 1)) : ℝ) * ‖iteratedFDeriv ℝ (k + 1 + 1) L x‖ *
                ‖iteratedFDeriv ℝ (n + 1 - (k + 1 + 1)) f x‖ = 0 := by
              apply Finset.sum_eq_zero
              simp [iteratedFDeriv_succ_eq_comp_right, iteratedFDeriv_succ_const]
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
H : Type u_8
V : Type u_9
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : 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 : ℕ
f : 𝓢(E, F)
x : E
n : ℕ
this :
  Eq (α := ℝ)
    (∑ k ∈ Finset.range n,
      (↑((n + 1).choose (k + 1 + 1)) : ℝ) *
          norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_7} ℝ (fun (i : Fin (k + 1 + 1)) ↦ E) (G →L[ℝ] ℝ))
            (iteratedFDeriv ℝ (k + 1 + 1) (⇑L : (a : E) → G →L[ℝ] ℝ) x) *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin (n + 1 - (k + 1 + 1))) ↦ E) F)
          (iteratedFDeriv ℝ (n + 1 - (k + 1 + 1)) (⇑f : (a : E) → F) x))
    0
⊢ (↑((n + 1).choose 0) : ℝ) *
          norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_7} ℝ (fun (i : Fin 0) ↦ E) (G →L[ℝ] ℝ))
            (iteratedFDeriv ℝ 0 (⇑L : (a : E) → G →L[ℝ] ℝ) x) *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin (n + 1 - 0)) ↦ E) F)
          (iteratedFDeriv ℝ (n + 1 - 0) (⇑f : (a : E) → F) x) +
      ∑ k ∈ Finset.range (n + 1),
        (↑((n + 1).choose (k + 1)) : ℝ) *
            norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_7} ℝ (fun (i : Fin (k + 1)) ↦ E) (G →L[ℝ] ℝ))
              (iteratedFDeriv ℝ (k + 1) (⇑L : (a : E) → G →L[ℝ] ℝ) x) *
          norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin (n + 1 - (k + 1))) ↦ E) F)
            (iteratedFDeriv ℝ (n + 1 - (k + 1)) (⇑f : (a : E) → F) x) ≤
    norm.{u_7} (E := G →L[ℝ] ℝ) ((L : (a : E) → G →L[ℝ] ℝ) x : G →L[ℝ] ℝ) *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin (n + 1)) ↦ E) F)
          (iteratedFDeriv ℝ (n + 1) (⇑f : (a : E) → F) x) +
      (↑(n + 1) : ℝ) * ‖L‖ *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin (n + 1 - 1)) ↦ E) F)
          (iteratedFDeriv ℝ (n + 1 - 1) (⇑f : (a : E) → F) x)

Tactic:
simp [Finset.sum_range_succ', this]

Premises used: Finset.sum_range_succ'
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
H : Type u_8
V : Type u_9
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : 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
⊢ ‖x‖ ^ k *
      (norm.{u_7} (E := G →L[ℝ] ℝ) ((L : (a : E) → G →L[ℝ] ℝ) x : G →L[ℝ] ℝ) *
          norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
            (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x) +
        (↑n : ℝ) * ‖L‖ *
          norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin (n - 1)) ↦ E) F)
            (iteratedFDeriv ℝ (n - 1) (⇑f : (a : E) → F) x)) =
    ‖x‖ ^ k * norm.{u_7} (E := G →L[ℝ] ℝ) ((L : (a : E) → G →L[ℝ] ℝ) x : G →L[ℝ] ℝ) *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
          (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x) +
      ‖x‖ ^ k * (↑n : ℝ) * ‖L‖ *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin (n - 1)) ↦ E) F)
          (iteratedFDeriv ℝ (n - 1) (⇑f : (a : E) → F) x)

Tactic:
ring
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
H : Type u_8
V : Type u_9
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : 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
grw :
  ‖x‖ ^ k * (‖L‖ * ‖x‖) *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
          (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x) +
      ‖x‖ ^ k * (↑n : ℝ) * ‖L‖ *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin (n - 1)) ↦ E) F)
          (iteratedFDeriv ℝ (n - 1) (⇑f : (a : E) → F) x) ≤
    ‖L‖ * 1 *
        (‖x‖ ^ (k + 1) *
          norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
            (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x)) +
      ‖L‖ * (↑n : ℝ) *
        (‖x‖ ^ k *
          norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin (n - 1)) ↦ E) F)
            (iteratedFDeriv ℝ (n - 1) (⇑f : (a : E) → F) x))
⊢ ‖x‖ ^ k * norm.{u_7} (E := G →L[ℝ] ℝ) ((L : (a : E) → G →L[ℝ] ℝ) x : G →L[ℝ] ℝ) *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
          (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x) +
      ‖x‖ ^ k * (↑n : ℝ) * ‖L‖ *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin (n - 1)) ↦ E) F)
          (iteratedFDeriv ℝ (n - 1) (⇑f : (a : E) → F) x) ≤
    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 : ℝ)

Tactic:
grw [le_opNorm, ← le_seminorm 𝕜 (k + 1) n f x, ← le_seminorm 𝕜 k (n - 1) f x]

Premises used: ContinuousLinearMap.le_opNorm, HSub.hSub, SchwartzMap.le_seminorm, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
H : Type u_8
V : Type u_9
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : 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
hab :
  ‖x‖ ^ k * (‖L‖ * ‖x‖) *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
          (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x) +
      ‖x‖ ^ k * (↑n : ℝ) * ‖L‖ *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin (n - 1)) ↦ E) F)
          (iteratedFDeriv ℝ (n - 1) (⇑f : (a : E) → F) x) =
    ‖L‖ * 1 *
        (‖x‖ ^ (k + 1) *
          norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
            (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x)) +
      ‖L‖ * (↑n : ℝ) *
        (‖x‖ ^ k *
          norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin (n - 1)) ↦ E) F)
            (iteratedFDeriv ℝ (n - 1) (⇑f : (a : E) → F) x))
⊢ ‖x‖ ^ k * (‖L‖ * ‖x‖) *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
          (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x) +
      ‖x‖ ^ k * (↑n : ℝ) * ‖L‖ *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin (n - 1)) ↦ E) F)
          (iteratedFDeriv ℝ (n - 1) (⇑f : (a : E) → F) x) ≤
    ‖L‖ * 1 *
        (‖x‖ ^ (k + 1) *
          norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
            (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x)) +
      ‖L‖ * (↑n : ℝ) *
        (‖x‖ ^ k *
          norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin (n - 1)) ↦ E) F)
            (iteratedFDeriv ℝ (n - 1) (⇑f : (a : E) → F) x))

Tactic:
apply le_of_eq

Premises used: le_of_eq
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
H : Type u_8
V : Type u_9
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : 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
⊢ ‖x‖ ^ k * (‖L‖ * ‖x‖) *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
          (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x) +
      ‖x‖ ^ k * (↑n : ℝ) * ‖L‖ *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin (n - 1)) ↦ E) F)
          (iteratedFDeriv ℝ (n - 1) (⇑f : (a : E) → F) x) =
    ‖L‖ * 1 *
        (‖x‖ ^ (k + 1) *
          norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
            (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x)) +
      ‖L‖ * (↑n : ℝ) *
        (‖x‖ ^ k *
          norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin (n - 1)) ↦ E) F)
            (iteratedFDeriv ℝ (n - 1) (⇑f : (a : E) → F) x))

Tactic:
ring
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
H : Type u_8
V : Type u_9
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : 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
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) :
      ℝ)
⊢ 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) :
          ℝ)

Tactic:
gcongr
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
H : Type u_8
V : Type u_9
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : 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
⊢ LE.le (α := ℝ) 1 (↑(max 1 n) : ℝ)

Tactic:
simp
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
H : Type u_8
V : Type u_9
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : 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
⊢ 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:
simp
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
H : Type u_8
V : Type u_9
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : 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
⊢ n ≤ max 1 n

Tactic:
simp
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
H : Type u_8
V : Type u_9
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : 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
⊢ 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:
simp