no goals
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst✝ : NormedLatticeAddCommGroup E
f g : { x // x ∈ Lp E p }
⊢ ↑↑f ≤ᵐ[μ] ↑↑g ↔ f ≤ g
rw [← Subtype.coe_le_coe, ← AEEqFun.coeFn_le]