-- 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
⊢ (↑(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)
have hbc : (↑(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: 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]
Cleared hypotheses: n