α : Type u_1
E : Type u_2
F : Type ?u.345761
𝕜 : Type ?u.345764
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
m : MeasurableSpace α
μ : Measure α
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
F' : Type ?u.348139
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace ℝ F'
E' : Type ?u.348235
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace ℝ E'
inst✝ : NormedSpace 𝕜 E'
f : { x // x ∈ simpleFunc E 1 μ }
⊢ ‖↑{
            toAddHom :=
              { toFun := integral,
                map_add' := (_ : ∀ (f g : { x // x ∈ simpleFunc E 1 μ }), integral (f + g) = integral f + integral g) },
            map_smul' := (_ : ∀ (c : ℝ) (f : { x // x ∈ simpleFunc E 1 μ }), integral (c • f) = c • integral f) }
        f‖ ≤
    ‖f‖
α : Type u_1
E : Type u_2
F : Type ?u.345761
𝕜 : Type ?u.345764
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
m : MeasurableSpace α
μ : Measure α
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
F' : Type ?u.348139
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace ℝ F'
E' : Type ?u.348235
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace ℝ E'
inst✝ : NormedSpace 𝕜 E'
f : { x // x ∈ simpleFunc E 1 μ }
⊢ ‖↑{
            toAddHom :=
              { toFun := integral,
                map_add' := (_ : ∀ (f g : { x // x ∈ simpleFunc E 1 μ }), integral (f + g) = integral f + integral g) },
            map_smul' := (_ : ∀ (c : ℝ) (f : { x // x ∈ simpleFunc E 1 μ }), integral (c • f) = c • integral f) }
        f‖ ≤
    1 * ‖f‖
rw [one_mul]
no goals
α : Type u_1
E : Type u_2
F : Type ?u.345761
𝕜 : Type ?u.345764
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
m : MeasurableSpace α
μ : Measure α
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
F' : Type ?u.348139
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace ℝ F'
E' : Type ?u.348235
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace ℝ E'
inst✝ : NormedSpace 𝕜 E'
f : { x // x ∈ simpleFunc E 1 μ }
⊢ ‖↑{
            toAddHom :=
              { toFun := integral,
                map_add' := (_ : ∀ (f g : { x // x ∈ simpleFunc E 1 μ }), integral (f + g) = integral f + integral g) },
            map_smul' := (_ : ∀ (c : ℝ) (f : { x // x ∈ simpleFunc E 1 μ }), integral (c • f) = c • integral f) }
        f‖ ≤
    ‖f‖
exact norm_integral_le_norm f