no goals
α : Type u_1
β : Type ?u.1924351
ι : Type ?u.1924354
E : Type ?u.1924357
F : Type ?u.1924360
𝕜 : Type ?u.1924363
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
f g : { x // x ∈ simpleFunc G p μ }
⊢ ↑↑↑f ≤ᵐ[μ] ↑↑↑g ↔ f ≤ g
rw [← Subtype.coe_le_coe, ← Lp.coeFn_le]