-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
𝕜 : Type u_2
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : MeasurableSpace E
inst_5 : OpensMeasurableSpace E
inst_6 : NormedField 𝕜
inst_7 : NormedSpace 𝕜 F
inst_8 : SMulCommClass ℝ 𝕜 F
p : ℝ≥0∞
μ : Measure E
hμ : μ.HasTemperateGrowth
k : ℕ
hk : eLpNorm (ε := ℝ) (fun (x : E) ↦ HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑k : ℝ))) p μ < ∞
f : 𝓢(E, F)
h_one_add : ∀ (x : E), 0 < 1 + ‖x‖
calc :
  eLpNorm.{u_5, u_6} (ε := F) (⇑f : (a : E) → F) p μ =
    eLpNorm
      (HSMul.hSMul (α := (x : E) → ℝ) (β := (x : E) → F) (fun (x : E) ↦ HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑k : ℝ)))
        fun (x : E) ↦ HSMul.hSMul (β := F) ((1 + ‖x‖) ^ k) ((f : (a : E) → F) x : F))
      p μ
calc₁ :
  eLpNorm
      (HSMul.hSMul (α := (x : E) → ℝ) (β := (x : E) → F) (fun (x : E) ↦ HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑k : ℝ)))
        fun (x : E) ↦ HSMul.hSMul (β := F) ((1 + ‖x‖) ^ k) ((f : (a : E) → F) x : F))
      p μ ≤
    eLpNorm (ε := ℝ) (fun (x : E) ↦ HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑k : ℝ))) p μ *
      eLpNorm.{u_5, u_6} (ε := F) (fun (x : E) ↦ HSMul.hSMul (β := F) ((1 + ‖x‖) ^ k) ((f : (a : E) → F) x : F)) ∞ μ
calc₂ :
  eLpNorm (ε := ℝ) (fun (x : E) ↦ HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑k : ℝ))) p μ *
      eLpNorm.{u_5, u_6} (ε := F) (fun (x : E) ↦ HSMul.hSMul (β := F) ((1 + ‖x‖) ^ k) ((f : (a : E) → F) x : F)) ∞ μ ≤
    eLpNorm (ε := ℝ) (fun (x : E) ↦ HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑k : ℝ))) p μ *
      (HPow.hPow (α := ℝ≥0∞) 2 k *
        ENNReal.ofReal ((Finset.sup (Finset.Iic (k, 0)) (schwartzSeminormFamily 𝕜 E F) : (a : 𝓢(E, F)) → ℝ) f))
calc₃ :
  eLpNorm (ε := ℝ) (fun (x : E) ↦ HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑k : ℝ))) p μ *
      (HPow.hPow (α := ℝ≥0∞) 2 k *
        ENNReal.ofReal ((Finset.sup (Finset.Iic (k, 0)) (schwartzSeminormFamily 𝕜 E F) : (a : 𝓢(E, F)) → ℝ) f)) =
    (↑((eLpNorm (ε := ℝ) (fun (x : E) ↦ HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑k : ℝ))) p μ).toNNReal *
            HPow.hPow (α := ℝ≥0) 2 k) :
        ℝ≥0∞) *
      ENNReal.ofReal ((Finset.sup (Finset.Iic (k, 0)) (schwartzSeminormFamily 𝕜 E F) : (a : 𝓢(E, F)) → ℝ) f)
⊢ eLpNorm.{u_5, u_6} (ε := F) (⇑f : (a : E) → F) p μ ≤
    (↑((eLpNorm (ε := ℝ) (fun (x : E) ↦ HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑k : ℝ))) p μ).toNNReal *
            HPow.hPow (α := ℝ≥0) 2 k) :
        ℝ≥0∞) *
      ENNReal.ofReal ((Finset.sup (Finset.Iic (k, 0)) (schwartzSeminormFamily 𝕜 E F) : (a : 𝓢(E, F)) → ℝ) f)

Tactic:
calc eLpNorm (⇑f) p μ
  _ = eLpNorm ((fun x : E ↦ (1 + ‖x‖) ^ (-k : ℝ)) • fun x ↦ (1 + ‖x‖) ^ k • f x) p μ := by
    refine congrArg (eLpNorm · p μ) (funext fun x ↦ ?_)
    simp [(h_one_add x).ne']
  _ ≤ eLpNorm (fun x ↦ (1 + ‖x‖) ^ (-k : ℝ)) p μ * eLpNorm (fun x ↦ (1 + ‖x‖) ^ k • f x) ⊤ μ := by
    refine eLpNorm_smul_le_eLpNorm_mul_eLpNorm_top p _ ?_
    refine Continuous.aestronglyMeasurable ?_
    exact .rpow_const (by fun_prop) fun x ↦ .inl (h_one_add x).ne'
  _ ≤ eLpNorm (fun x ↦ (1 + ‖x‖) ^ (-k : ℝ)) p μ *
      (2 ^ k * ENNReal.ofReal (((Finset.Iic (k, 0)).sup (schwartzSeminormFamily 𝕜 E F)) f)) := by
    gcongr
    refine eLpNormEssSup_le_of_ae_nnnorm_bound (ae_of_all μ fun x ↦ ?_)
    rw [← norm_toNNReal, Real.toNNReal_le_iff_le_coe]
    simpa [norm_smul, abs_of_nonneg (h_one_add x).le] using
      one_add_le_sup_seminorm_apply (m := (k, 0)) (le_refl k) (le_refl 0) f x
  _ = _ := by
    rw [ENNReal.coe_mul, ENNReal.coe_toNNReal hk.ne]
    simp only [ENNReal.coe_pow, ENNReal.coe_ofNat]
    ring

Premises used: Norm.norm, HMul.hMul, ENNReal.ofReal, Prod.mk, Nat.cast, HPow.hPow, HAdd.hAdd, schwartzSeminormFamily, Finset.Iic, Finset.sup, HSMul.hSMul, Top.top, OfNat.ofNat, DFunLike.coe, Neg.neg, MeasureTheory.eLpNorm