case hfC
α : Type u_1
E : Type u_2
F : Type ?u.9383734
G : Type ?u.9383737
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : MeasureTheory.Measure α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedAddCommGroup G
inst✝³ : TopologicalSpace α
inst✝² : BorelSpace α
inst✝¹ : SecondCountableTopologyEither α E
inst✝ : IsFiniteMeasure μ
f : α →ᵇ E
⊢ ∀ᵐ (x : α) ∂μ,
    ‖↑↑{ val := ContinuousMap.toAEEqFun μ f.toContinuousMap,
                property := (_ : ContinuousMap.toAEEqFun μ f.toContinuousMap ∈ Lp E p) }
          x‖₊ ≤
      ‖f‖₊
α : Type u_1
E : Type u_2
F : Type ?u.9383734
G : Type ?u.9383737
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : MeasureTheory.Measure α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedAddCommGroup G
inst✝³ : TopologicalSpace α
inst✝² : BorelSpace α
inst✝¹ : SecondCountableTopologyEither α E
inst✝ : IsFiniteMeasure μ
f : α →ᵇ E
⊢ ‖{ val := ContinuousMap.toAEEqFun μ f.toContinuousMap,
        property := (_ : ContinuousMap.toAEEqFun μ f.toContinuousMap ∈ Lp E p) }‖₊ ≤
    measureUnivNNReal μ ^ (ENNReal.toReal p)⁻¹ * ‖f‖₊
apply Lp.nnnorm_le_of_ae_bound
case hfC
α : Type u_1
E : Type u_2
F : Type ?u.9383734
G : Type ?u.9383737
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : MeasureTheory.Measure α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedAddCommGroup G
inst✝³ : TopologicalSpace α
inst✝² : BorelSpace α
inst✝¹ : SecondCountableTopologyEither α E
inst✝ : IsFiniteMeasure μ
f : α →ᵇ E
⊢ ∀ (x : α),
    ↑(ContinuousMap.toAEEqFun μ f.toContinuousMap) x = ↑f.toContinuousMap x →
      ‖↑↑{ val := ContinuousMap.toAEEqFun μ f.toContinuousMap,
                  property := (_ : ContinuousMap.toAEEqFun μ f.toContinuousMap ∈ Lp E p) }
            x‖₊ ≤
        ‖f‖₊
case hfC
α : Type u_1
E : Type u_2
F : Type ?u.9383734
G : Type ?u.9383737
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : MeasureTheory.Measure α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedAddCommGroup G
inst✝³ : TopologicalSpace α
inst✝² : BorelSpace α
inst✝¹ : SecondCountableTopologyEither α E
inst✝ : IsFiniteMeasure μ
f : α →ᵇ E
⊢ ∀ᵐ (x : α) ∂μ,
    ‖↑↑{ val := ContinuousMap.toAEEqFun μ f.toContinuousMap,
                property := (_ : ContinuousMap.toAEEqFun μ f.toContinuousMap ∈ Lp E p) }
          x‖₊ ≤
      ‖f‖₊
refine' (f.toContinuousMap.coeFn_toAEEqFun μ).mono _
case hfC
α : Type u_1
E : Type u_2
F : Type ?u.9383734
G : Type ?u.9383737
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : MeasureTheory.Measure α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedAddCommGroup G
inst✝³ : TopologicalSpace α
inst✝² : BorelSpace α
inst✝¹ : SecondCountableTopologyEither α E
inst✝ : IsFiniteMeasure μ
f : α →ᵇ E
x : α
hx : ↑(ContinuousMap.toAEEqFun μ f.toContinuousMap) x = ↑f.toContinuousMap x
⊢ ‖↑↑{ val := ContinuousMap.toAEEqFun μ f.toContinuousMap,
              property := (_ : ContinuousMap.toAEEqFun μ f.toContinuousMap ∈ Lp E p) }
        x‖₊ ≤
    ‖f‖₊
case hfC
α : Type u_1
E : Type u_2
F : Type ?u.9383734
G : Type ?u.9383737
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : MeasureTheory.Measure α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedAddCommGroup G
inst✝³ : TopologicalSpace α
inst✝² : BorelSpace α
inst✝¹ : SecondCountableTopologyEither α E
inst✝ : IsFiniteMeasure μ
f : α →ᵇ E
⊢ ∀ (x : α),
    ↑(ContinuousMap.toAEEqFun μ f.toContinuousMap) x = ↑f.toContinuousMap x →
      ‖↑↑{ val := ContinuousMap.toAEEqFun μ f.toContinuousMap,
                  property := (_ : ContinuousMap.toAEEqFun μ f.toContinuousMap ∈ Lp E p) }
            x‖₊ ≤
        ‖f‖₊
intro x hx
case hfC
α : Type u_1
E : Type u_2
F : Type ?u.9383734
G : Type ?u.9383737
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : MeasureTheory.Measure α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedAddCommGroup G
inst✝³ : TopologicalSpace α
inst✝² : BorelSpace α
inst✝¹ : SecondCountableTopologyEither α E
inst✝ : IsFiniteMeasure μ
f : α →ᵇ E
x : α
hx : ↑(ContinuousMap.toAEEqFun μ f.toContinuousMap) x = ↑f.toContinuousMap x
⊢ ‖↑↑{ val := ContinuousMap.toAEEqFun μ f.toContinuousMap,
              property := (_ : ContinuousMap.toAEEqFun μ f.toContinuousMap ∈ Lp E p) }
        x‖ ≤
    ‖f‖
case hfC
α : Type u_1
E : Type u_2
F : Type ?u.9383734
G : Type ?u.9383737
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : MeasureTheory.Measure α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedAddCommGroup G
inst✝³ : TopologicalSpace α
inst✝² : BorelSpace α
inst✝¹ : SecondCountableTopologyEither α E
inst✝ : IsFiniteMeasure μ
f : α →ᵇ E
x : α
hx : ↑(ContinuousMap.toAEEqFun μ f.toContinuousMap) x = ↑f.toContinuousMap x
⊢ ‖↑↑{ val := ContinuousMap.toAEEqFun μ f.toContinuousMap,
              property := (_ : ContinuousMap.toAEEqFun μ f.toContinuousMap ∈ Lp E p) }
        x‖₊ ≤
    ‖f‖₊
rw [← NNReal.coe_le_coe, coe_nnnorm, coe_nnnorm]
no goals
case hfC
α : Type u_1
E : Type u_2
F : Type ?u.9383734
G : Type ?u.9383737
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : MeasureTheory.Measure α
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedAddCommGroup G
inst✝³ : TopologicalSpace α
inst✝² : BorelSpace α
inst✝¹ : SecondCountableTopologyEither α E
inst✝ : IsFiniteMeasure μ
f : α →ᵇ E
x : α
hx : ↑(ContinuousMap.toAEEqFun μ f.toContinuousMap) x = ↑f.toContinuousMap x
⊢ ‖↑↑{ val := ContinuousMap.toAEEqFun μ f.toContinuousMap,
              property := (_ : ContinuousMap.toAEEqFun μ f.toContinuousMap ∈ Lp E p) }
        x‖ ≤
    ‖f‖
convert f.norm_coe_le_norm x using 2