-- 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
this :
  HPow.hPow (β := ℕ) ‖w‖ 2 ^ n *
      Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin k) ↦ V) E)
        (iteratedFDeriv ℝ k (fourierIntegral 𝐞 (volume : Measure V) (ContinuousLinearMap.toLinearMap₁₂ (innerSL ℝ)) 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 _ _ _ _ inst_5 (volume : Measure V) 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)))
rwa :
  ∀
    (this :
      (‖w‖ * ‖w‖) ^ n *
          Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin k) ↦ V) E)
            (iteratedFDeriv ℝ k
              (fourierIntegral 𝐞 (volume : Measure V) (ContinuousLinearMap.toLinearMap₁₂ (innerSL ℝ)) 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 _ _ _ _ inst_5 (volume : Measure V) 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 *
        (‖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)))
rwa₁ :
  ∀
    (this :
      ‖w‖ ^ n * ‖w‖ ^ n *
          Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin k) ↦ V) E)
            (iteratedFDeriv ℝ k
              (fourierIntegral 𝐞 (volume : Measure V) (ContinuousLinearMap.toLinearMap₁₂ (innerSL ℝ)) 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 _ _ _ _ inst_5 (volume : Measure V) 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 *
        (‖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)))
⊢ ‖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)))
have rwa₂ : ∀
  (this :
    ‖w‖ ^ n *
        (‖w‖ ^ n *
          Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin k) ↦ V) E)
            (iteratedFDeriv ℝ k
              (fourierIntegral 𝐞 (volume : Measure V) (ContinuousLinearMap.toLinearMap₁₂ (innerSL ℝ)) 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 _ _ _ _ inst_5 (volume : Measure V) 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 *
      (‖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)))
Tactic: rwa [pow_two, mul_pow, mul_assoc] at this
Cleared hypotheses: this