Lean: transport End/Hom across a composed equivalence when the objects are only defeq

To get End (mk x) ≃ T from an equivalence e : C ≌ D where e.functor.obj (mk x) is defeq (not syntactically equal) to some d with (d ⟶ d) = T: End.homEquiv.trans <| (e.fullyFaithfulFunctor.homEquiv (X := mk x) (Y := mk x)).trans (Equiv.cast (show _ = T from rfl)). A bare homEquiv gives a type mismatch, because the metavariable objects are not unified. A bare Equiv.cast rfl just elaborates to the identity on the same type. Use show _ = T from rfl to force the defeq check. In current Mathlib FundamentalGroup X x is End, not Aut, so use FullyFaithful.mulEquivEnd for π₁ transfers.