no goals
α : Type u_1
β : Type u_2
γ : Type ?u.443277
δ : Type ?u.443280
inst✝³ : MeasurableSpace α
μ ν : Measure α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α →ₘ[μ] β
⊢ toGerm f = ↑↑f
rw [← mk_toGerm, mk_coeFn]