case h.e'_5.h.e'_6
α : Type u_1
β : Type ?u.1531711
ι : Type ?u.1531714
E : Type u_2
F : Type ?u.1531720
𝕜 : Type ?u.1531723
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
f : { x // x ∈ simpleFunc E p μ }
⊢ ↑↑f = AEEqFun.mk ↑(toSimpleFunc f) (_ : AEStronglyMeasurable (↑(toSimpleFunc f)) μ)
α : Type u_1
β : Type ?u.1531711
ι : Type ?u.1531714
E : Type u_2
F : Type ?u.1531720
𝕜 : Type ?u.1531723
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
f : { x // x ∈ simpleFunc E p μ }
⊢ ↑(toSimpleFunc f) =ᵐ[μ] ↑↑↑f
convert (AEEqFun.coeFn_mk (toSimpleFunc f)
      (toSimpleFunc f).aestronglyMeasurable).symm using 2
no goals
case h.e'_5.h.e'_6
α : Type u_1
β : Type ?u.1531711
ι : Type ?u.1531714
E : Type u_2
F : Type ?u.1531720
𝕜 : Type ?u.1531723
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
f : { x // x ∈ simpleFunc E p μ }
⊢ ↑↑f = AEEqFun.mk ↑(toSimpleFunc f) (_ : AEStronglyMeasurable (↑(toSimpleFunc f)) μ)
exact (Classical.choose_spec f.2).symm