α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst✝ : NormedLatticeAddCommGroup E
f : { x // x ∈ Lp E p }
⊢ 0 ≤ᵐ[μ] ↑↑f ↔ ↑↑0 ≤ᵐ[μ] ↑↑f
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst✝ : NormedLatticeAddCommGroup E
f : { x // x ∈ Lp E p }
⊢ 0 ≤ᵐ[μ] ↑↑f ↔ 0 ≤ f
rw [← coeFn_le]
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst✝ : NormedLatticeAddCommGroup E
f : { x // x ∈ Lp E p }
h0 : ↑↑0 =ᵐ[μ] 0
⊢ 0 ≤ᵐ[μ] ↑↑f ↔ ↑↑0 ≤ᵐ[μ] ↑↑f
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst✝ : NormedLatticeAddCommGroup E
f : { x // x ∈ Lp E p }
⊢ 0 ≤ᵐ[μ] ↑↑f ↔ ↑↑0 ≤ᵐ[μ] ↑↑f
have h0 := Lp.coeFn_zero E p μ
case h
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst✝ : NormedLatticeAddCommGroup E
f : { x // x ∈ Lp E p }
h0 : ↑↑0 =ᵐ[μ] 0
h : 0 ≤ᵐ[μ] ↑↑f
a✝¹ : α
a✝ : OfNat.ofNat 0 a✝¹ ≤ ↑↑f a✝¹
h2 : ↑↑0 a✝¹ = OfNat.ofNat 0 a✝¹
⊢ ↑↑0 a✝¹ ≤ ↑↑f a✝¹

case h
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst✝ : NormedLatticeAddCommGroup E
f : { x // x ∈ Lp E p }
h0 : ↑↑0 =ᵐ[μ] 0
h : ↑↑0 ≤ᵐ[μ] ↑↑f
a✝¹ : α
a✝ : ↑↑0 a✝¹ ≤ ↑↑f a✝¹
h2 : ↑↑0 a✝¹ = OfNat.ofNat 0 a✝¹
⊢ OfNat.ofNat 0 a✝¹ ≤ ↑↑f a✝¹
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst✝ : NormedLatticeAddCommGroup E
f : { x // x ∈ Lp E p }
h0 : ↑↑0 =ᵐ[μ] 0
⊢ 0 ≤ᵐ[μ] ↑↑f ↔ ↑↑0 ≤ᵐ[μ] ↑↑f
constructor <;> intro h <;> filter_upwards [h, h0] with _ _ h2
no goals
case h
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst✝ : NormedLatticeAddCommGroup E
f : { x // x ∈ Lp E p }
h0 : ↑↑0 =ᵐ[μ] 0
h : 0 ≤ᵐ[μ] ↑↑f
a✝¹ : α
a✝ : OfNat.ofNat 0 a✝¹ ≤ ↑↑f a✝¹
h2 : ↑↑0 a✝¹ = OfNat.ofNat 0 a✝¹
⊢ ↑↑0 a✝¹ ≤ ↑↑f a✝¹
rwa [h2]
no goals
case h
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst✝ : NormedLatticeAddCommGroup E
f : { x // x ∈ Lp E p }
h0 : ↑↑0 =ᵐ[μ] 0
h : ↑↑0 ≤ᵐ[μ] ↑↑f
a✝¹ : α
a✝ : ↑↑0 a✝¹ ≤ ↑↑f a✝¹
h2 : ↑↑0 a✝¹ = OfNat.ofNat 0 a✝¹
⊢ OfNat.ofNat 0 a✝¹ ≤ ↑↑f a✝¹
rwa [← h2]