-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Fourier (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℂ E
inst_3 : NormedSpace 𝕜 E
inst_4 : SMulCommClass ℂ 𝕜 E
V : Type u_3
inst_5 : NormedAddCommGroup V
inst_6 : InnerProductSpace ℝ V
inst_7 : FiniteDimensional ℝ V
inst_8 : MeasurableSpace V
inst_9 : BorelSpace V
k n : ℕ
f : 𝓢(V, E)
x : V
_ :
  LE.le (α := ℝ)
    (∑ p ∈ Finset.range (n + 1) ×ˢ Finset.range (k + 1),
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
        ‖v‖ ^ p.1 *
          Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_3, u_2} ℝ (fun (i : Fin p.2) ↦ V) E)
            (iteratedFDeriv ℝ p.2 (⇑f : (a : V) → E) v))
    (∑ x ∈ Finset.range (n + 1) ×ˢ Finset.range (k + 1),
      HMul.hMul (β := ℝ)
        ((HPow.hPow (α := ℝ) 2 (integrablePower.{u_3} (E := V) volume) *
            @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : V) ↦
              HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑(integrablePower.{u_3} (E := V) volume) : ℝ))) *
          2)
        (((Finset.range (n + integrablePower.{u_3} (E := V) volume + 1) ×ˢ Finset.range (k + 1)).sup
                (schwartzSeminormFamily 𝕜 V E) :
              (a : 𝓢(V, E)) → ℝ)
            f :
          ℝ))
⊢ (∑ p ∈ Finset.range (n + 1) ×ˢ Finset.range (k + 1),
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
        ‖v‖ ^ p.1 *
          Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_3, u_2} ℝ (fun (i : Fin p.2) ↦ V) E)
            (iteratedFDeriv ℝ p.2 (⇑f : (a : V) → E) v)) ≤
    (↑(Finset.range (n + 1) ×ˢ Finset.range (k + 1)).card : ℝ) *
      (HPow.hPow (α := ℝ) 2 (integrablePower.{u_3} (E := V) volume) *
        ((@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : V) ↦
            HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑(integrablePower.{u_3} (E := V) volume) : ℝ))) *
          HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ)
            (((Finset.range (n + integrablePower.{u_3} (E := V) volume + 1) ×ˢ Finset.range (k + 1)).sup
                    (schwartzSeminormFamily 𝕜 V E) :
                  (a : 𝓢(V, E)) → ℝ)
                f :
              ℝ)))
have _₁ : ∑ x ∈ Finset.range (n + 1) ×ˢ Finset.range (k + 1),
    HMul.hMul (β := ℝ)
      ((HPow.hPow (α := ℝ) 2 (integrablePower.{u_3} (E := V) volume) *
          @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : V) ↦
            HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑(integrablePower.{u_3} (E := V) volume) : ℝ))) *
        2)
      (((Finset.range (n + integrablePower.{u_3} (E := V) volume + 1) ×ˢ Finset.range (k + 1)).sup
              (schwartzSeminormFamily 𝕜 V E) :
            (a : 𝓢(V, E)) → ℝ)
          f :
        ℝ) =
  (↑(Finset.range (n + 1) ×ˢ Finset.range (k + 1)).card : ℝ) *
    (HPow.hPow (α := ℝ) 2 (integrablePower.{u_3} (E := V) volume) *
      ((@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : V) ↦
          HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑(integrablePower.{u_3} (E := V) volume) : ℝ))) *
        HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ)
          (((Finset.range (n + integrablePower.{u_3} (E := V) volume + 1) ×ˢ Finset.range (k + 1)).sup
                  (schwartzSeminormFamily 𝕜 V E) :
                (a : 𝓢(V, E)) → ℝ)
              f :
            ℝ)))
Tactic: calc
    _ ≤ ∑ _ ∈ Finset.range (n + 1) ×ˢ Finset.range (k + 1),
        2 ^ integrablePower (volume : Measure V) *
          (∫ x : V, (1 + ‖x‖) ^ (- integrablePower (volume : Measure V) : ℝ)) * 2 *
          (Finset.range (n + integrablePower (volume : Measure V) + 1) ×ˢ Finset.range (k + 1)).sup
          (schwartzSeminormFamily 𝕜 V E) f := by
      gcongr with p
      apply (f.integral_pow_mul_iteratedFDeriv_le 𝕜 ..).trans
      simp only [mul_assoc, two_mul]
      gcongr
      · have : (0, p.2) ∈ Finset.range (n + integrablePower (volume : Measure V) + 1) ×ˢ
            Finset.range (k + 1) := by simp_all
        apply Seminorm.le_def.mp (Finset.le_sup (f := fun p ↦ SchwartzMap.seminorm 𝕜 p.1 p.2) this)
      · have : (p.1 + integrablePower (volume : Measure V), p.2) ∈ Finset.range
            (n + integrablePower (volume : Measure V) + 1) ×ˢ Finset.range (k + 1) := by simp_all
        apply Seminorm.le_def.mp (Finset.le_sup (f := fun p ↦ SchwartzMap.seminorm 𝕜 p.1 p.2) this)
    _ = _ := by simp [mul_assoc]