no goals
α : Type u_1
β : Type u_2
γ : Type u_3
f : SingleObj α ⥤q SingleObj β
g : SingleObj β ⥤q SingleObj γ
⊢ ↑toPrefunctor.symm (f ⋙q g) = ↑toPrefunctor.symm g ∘ ↑toPrefunctor.symm f
simp only [Equiv.symm_apply_eq, toPrefunctor_comp, Equiv.apply_symm_apply]