-- Mathlib/MeasureTheory/Function/LpSpace/ContinuousFunctions.lean
theorem Lp_nnnorm_le (f : α →ᵇ E) :
    ‖(⟨f.toContinuousMap.toAEEqFun μ, mem_Lp f⟩ : Lp E p μ)‖₊ ≤
      measureUnivNNReal μ ^ p.toReal⁻¹ * ‖f‖₊

Proof state:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : SecondCountableTopologyEither α E
inst✝ : IsFiniteMeasure μ
f : α →ᵇ E
⊢ ‖⟨ContinuousMap.toAEEqFun μ f.toContinuousMap, ⋯⟩‖₊ ≤ measureUnivNNReal μ ^ p.toReal⁻¹ * ‖f‖₊

Tactic:
apply Lp.nnnorm_le_of_ae_bound

Result:
case hfC
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : SecondCountableTopologyEither α E
inst✝ : IsFiniteMeasure μ
f : α →ᵇ E
⊢ ∀ᵐ (x : α) ∂μ, ‖↑↑⟨ContinuousMap.toAEEqFun μ f.toContinuousMap, ⋯⟩ x‖₊ ≤ ‖f‖₊

Proof state:
case hfC
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : SecondCountableTopologyEither α E
inst✝ : IsFiniteMeasure μ
f : α →ᵇ E
⊢ ∀ᵐ (x : α) ∂μ, ‖↑↑⟨ContinuousMap.toAEEqFun μ f.toContinuousMap, ⋯⟩ x‖₊ ≤ ‖f‖₊

Tactic:
refine (f.toContinuousMap.coeFn_toAEEqFun μ).mono ?_

Result:
case hfC
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : SecondCountableTopologyEither α E
inst✝ : IsFiniteMeasure μ
f : α →ᵇ E
⊢ ∀ (x : α),
    ↑(ContinuousMap.toAEEqFun μ f.toContinuousMap) x = f.toContinuousMap x →
      ‖↑↑⟨ContinuousMap.toAEEqFun μ f.toContinuousMap, ⋯⟩ x‖₊ ≤ ‖f‖₊

Proof state:
case hfC
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : SecondCountableTopologyEither α E
inst✝ : IsFiniteMeasure μ
f : α →ᵇ E
x : α
hx : ↑(ContinuousMap.toAEEqFun μ f.toContinuousMap) x = f.toContinuousMap x
⊢ ‖↑↑⟨ContinuousMap.toAEEqFun μ f.toContinuousMap, ⋯⟩ x‖₊ ≤ ‖f‖₊

Tactic:
rw [← NNReal.coe_le_coe, coe_nnnorm, coe_nnnorm]

Result:
case hfC
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : SecondCountableTopologyEither α E
inst✝ : IsFiniteMeasure μ
f : α →ᵇ E
x : α
hx : ↑(ContinuousMap.toAEEqFun μ f.toContinuousMap) x = f.toContinuousMap x
⊢ ‖↑↑⟨ContinuousMap.toAEEqFun μ f.toContinuousMap, ⋯⟩ x‖ ≤ ‖f‖

Proof state:
case hfC
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : SecondCountableTopologyEither α E
inst✝ : IsFiniteMeasure μ
f : α →ᵇ E
x : α
hx : ↑(ContinuousMap.toAEEqFun μ f.toContinuousMap) x = f.toContinuousMap x
⊢ ‖↑↑⟨ContinuousMap.toAEEqFun μ f.toContinuousMap, ⋯⟩ x‖ ≤ ‖f‖

Tactic:
convert f.norm_coe_le_norm x using 2

Result:
no goals

Proof state:
case hfC
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : SecondCountableTopologyEither α E
inst✝ : IsFiniteMeasure μ
f : α →ᵇ E
⊢ ∀ (x : α),
    ↑(ContinuousMap.toAEEqFun μ f.toContinuousMap) x = f.toContinuousMap x →
      ‖↑↑⟨ContinuousMap.toAEEqFun μ f.toContinuousMap, ⋯⟩ x‖₊ ≤ ‖f‖₊

Tactic:
intro x hx

Result:
case hfC
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : SecondCountableTopologyEither α E
inst✝ : IsFiniteMeasure μ
f : α →ᵇ E
x : α
hx : ↑(ContinuousMap.toAEEqFun μ f.toContinuousMap) x = f.toContinuousMap x
⊢ ‖↑↑⟨ContinuousMap.toAEEqFun μ f.toContinuousMap, ⋯⟩ x‖₊ ≤ ‖f‖₊