case h
α : Type u_1
β : Type ?u.1580552
ι : Type ?u.1580555
E : Type u_2
F : Type ?u.1580561
𝕜 : Type ?u.1580564
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
a✝¹ : α
h₁ : ↑(toSimpleFunc 0) a✝¹ = ↑↑↑0 a✝¹
a✝ : ↑↑0 a✝¹ = OfNat.ofNat 0 a✝¹
⊢ ↑(toSimpleFunc 0) a✝¹ = OfNat.ofNat 0 a✝¹
α : Type u_1
β : Type ?u.1580552
ι : Type ?u.1580555
E : Type u_2
F : Type ?u.1580561
𝕜 : Type ?u.1580564
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
⊢ ↑(toSimpleFunc 0) =ᵐ[μ] 0
filter_upwards [toSimpleFunc_eq_toFun (0 : Lp.simpleFunc E p μ),
  Lp.coeFn_zero E 1 μ] with _ h₁ _
no goals
case h
α : Type u_1
β : Type ?u.1580552
ι : Type ?u.1580555
E : Type u_2
F : Type ?u.1580561
𝕜 : Type ?u.1580564
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
a✝¹ : α
h₁ : ↑(toSimpleFunc 0) a✝¹ = ↑↑↑0 a✝¹
a✝ : ↑↑0 a✝¹ = OfNat.ofNat 0 a✝¹
⊢ ↑(toSimpleFunc 0) a✝¹ = OfNat.ofNat 0 a✝¹
rwa [h₁]