-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransformDeriv (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_2
inst_2 : NormedAddCommGroup V
inst_3 : InnerProductSpace ℝ V
inst_4 : FiniteDimensional ℝ V
inst_5 : MeasurableSpace V
inst_6 : BorelSpace V
f : V → E
K N : ℕ∞
hf : ContDiff ℝ (↑N : ℕ∞ω) f
h'f :
  ∀ (k n : ℕ),
    (↑k : ℕ∞) ≤ K →
      (↑n : ℕ∞) ≤ N →
        @Integrable ℝ _ _ _ inst_5
          (fun (v : V) ↦
            ‖v‖ ^ k *
              Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin n) ↦ V) E)
                (iteratedFDeriv ℝ n f v))
          (volume : Measure V)
k n : ℕ
hk : (↑k : ℕ∞) ≤ K
hn : (↑n : ℕ∞) ≤ N
w : V
Z :
  ‖w‖ ^ n *
      (‖w‖ ^ n *
        Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin k) ↦ V) E)
          (iteratedFDeriv ℝ k (𝓕 f) w)) ≤
    ‖w‖ ^ n *
      ((2 * (π * Norm.norm.{u_2} (E := V →L⋆[ℝ] V →L[ℝ] ℝ) (innerSL ℝ))) ^ k *
        ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 2) ^ n *
          ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1),
            @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
              ‖v‖ ^ p.1 *
                Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin p.2) ↦ V) E)
                  (iteratedFDeriv ℝ p.2 f v)))
inl :
  ∀ (hn : (↑0 : ℕ∞) ≤ N)
    (Z :
      HPow.hPow (β := ℕ) ‖w‖ 0 *
          (HPow.hPow (β := ℕ) ‖w‖ 0 *
            Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin k) ↦ V) E)
              (iteratedFDeriv ℝ k (𝓕 f) w)) ≤
        HPow.hPow (β := ℕ) ‖w‖ 0 *
          ((2 * (π * Norm.norm.{u_2} (E := V →L⋆[ℝ] V →L[ℝ] ℝ) (innerSL ℝ))) ^ k *
            (HPow.hPow (β := ℕ) (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 2) 0 *
              ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (HAdd.hAdd (α := ℕ) 0 1),
                @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
                  ‖v‖ ^ p.1 *
                    Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin p.2) ↦ V) E)
                      (iteratedFDeriv ℝ p.2 f v)))),
    HPow.hPow (β := ℕ) ‖w‖ 0 *
        Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin k) ↦ V) E)
          (iteratedFDeriv ℝ k (𝓕 f) w) ≤
      (2 * π) ^ k * HPow.hPow (β := ℕ) (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 2) 0 *
        ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (HAdd.hAdd (α := ℕ) 0 1),
          @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
            ‖v‖ ^ p.1 *
              Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin p.2) ↦ V) E)
                (iteratedFDeriv ℝ p.2 f v)
⊢ ‖w‖ ^ n *
      Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin k) ↦ V) E)
        (iteratedFDeriv ℝ k (𝓕 f) w) ≤
    (2 * π) ^ k * (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 2) ^ n *
      ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1),
        @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
          ‖v‖ ^ p.1 *
            Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin p.2) ↦ V) E)
              (iteratedFDeriv ℝ p.2 f v)
have inr : ∀ (hn : n ≠ 0),
  ‖w‖ ^ n *
      Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin k) ↦ V) E)
        (iteratedFDeriv ℝ k (𝓕 f) w) ≤
    (2 * π) ^ k * (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 2) ^ n *
      ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1),
        @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
          ‖v‖ ^ p.1 *
            Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin p.2) ↦ V) E)
              (iteratedFDeriv ℝ p.2 f v)
Tactic: rcases eq_or_ne n 0 with rfl | hn