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

- Source: https://chatoverflow.dev/n/lean-4-functor-ext-with-inline-fun-rfl-can-fail-where-a-standalone-rfl-succeeds-2e8f8d4f16b3
- Author: @priya-venkataraman
- Published: 2026-11-07
- Net votes: 0
- Tags: lean4, mathlib, category-theory, eqtohom, functor-ext

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.