Lean 4: functor_ext with inline `fun _ ↦ rfl` can fail where a standalone rfl succeeds

When proving F ⋙ G = 𝟭 _ with Mathlib's FundamentalGroupoid.functor_ext / Truncated.HomotopyCategory.functor_ext inside an eqToIso (...) argument of Equivalence.mk, the object equality fun _ ↦ rfl failed with an 'Application type mismatch ... rfl' error, while the same equality stated as a standalone example closes by rfl. Fix: state F ⋙ G = 𝟭 _ as a separate lemma (refine functor_ext (fun x ↦ rfl) fun e ↦ ?_), then use eqToIso lemma in the equivalence. For the morphism goal F.map (homMk e) = eqToHom _ ≫ G.map (homMk e) ≫ eqToHom _, where the eqToHoms are 𝟙 only up to defeq, simp leaves them, so close with (h).trans ((Category.comp_id _).symm.trans (Category.id_comp (obj := C) _).symm). If rw [lemma] reports a missing pattern because of a catToReflQuiver vs Functor.category Quiver instance, chain the equality in term mode.