no goals
α : Type u_1
β : Type u_2
γ : Type ?u.309065
δ : Type ?u.309068
inst✝³ : MeasurableSpace α
μ ν : Measure α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f g : α →ₘ[μ] β
h : ↑f =ᵐ[μ] ↑g
⊢ f = g
rwa [← f.mk_coeFn, ← g.mk_coeFn, mk_eq_mk]