-- 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
⊢ ‖x‖ ^ (k, n).1 *
      norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin (k, n).2) ↦ E) (G →L[ℝ] F))
        (iteratedFDeriv ℝ (k, n).2
          ((fun (f : 𝓢(E, F)) (x : E) ↦
              (smulRight (S := ℝ) ((L : (a : E) → G →L[ℝ] ℝ) x) ((f : (a : E) → F) x) : G →L[ℝ] F))
            f)
          x) ≤
    HMul.hMul (β := ℝ) (2 * ‖L‖ * (↑(max 1 n) : ℝ))
      ((Finset.sup {(k + 1, n), (k, n - 1)} (schwartzSeminormFamily 𝕜 E F) : (a : 𝓢(E, F)) → ℝ) f : ℝ)
have _ : ‖x‖ ^ (k, n).1 *
    norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin (k, n).2) ↦ E) (G →L[ℝ] F))
      (iteratedFDeriv ℝ (k, n).2
        ((fun (f : 𝓢(E, F)) (x : E) ↦
            (smulRight (S := ℝ) ((L : (a : E) → G →L[ℝ] ℝ) x) ((f : (a : E) → F) x) : G →L[ℝ] F))
          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)
Tactic: calc
        _ ≤ ‖x‖ ^ k * ∑ i ∈ Finset.range (n + 1), (n.choose i) *
            ‖iteratedFDeriv ℝ i L x‖ * ‖iteratedFDeriv ℝ (n - i) f x‖ := by
          gcongr 1
          exact norm_iteratedFDeriv_le_of_bilinear_of_le_one (smulRightL ℝ G F)
            (by fun_prop) (f.smooth ⊤) x (mod_cast le_top) norm_smulRightL_le
        _ ≤ ‖x‖ ^ k *
            (‖L x‖ * ‖iteratedFDeriv ℝ n f x‖ + n * ‖L‖ * ‖iteratedFDeriv ℝ (n - 1) f x‖) := by
          gcongr 1
          rw [Finset.sum_range_succ', add_comm]
          cases n with
          | zero => simp
          | succ n =>
            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]
            simp [Finset.sum_range_succ', this]
        _ = ‖x‖ ^ k * ‖L x‖ * ‖iteratedFDeriv ℝ n f x‖ +
              ‖x‖ ^ k * n * ‖L‖ * ‖iteratedFDeriv ℝ (n - 1) f x‖ := by ring
        _ ≤ ‖L‖ * 1 * (SchwartzMap.seminorm 𝕜 (k + 1) n) f +
              ‖L‖ * n * (SchwartzMap.seminorm 𝕜 k (n - 1) f) := by
          grw [le_opNorm, ← le_seminorm 𝕜 (k + 1) n f x, ← le_seminorm 𝕜 k (n - 1) f x]
          apply le_of_eq
          ring
        _ ≤ ‖L‖ * max 1 n *
            max ((SchwartzMap.seminorm 𝕜 (k + 1) n) f) ((SchwartzMap.seminorm 𝕜 k (n - 1)) f) +
            ‖L‖ * max 1 n *
            max ((SchwartzMap.seminorm 𝕜 (k + 1) n) f) ((SchwartzMap.seminorm 𝕜 k (n - 1)) f) := by
          gcongr <;> simp
        _ = _ := by
          simp only [Finset.sup_insert, schwartzSeminormFamily_apply, Finset.sup_singleton,
            Seminorm.coe_sup, Pi.sup_apply]
          ring