Lean eqToHom cleanup when simp fails: repeat erw [eqToHom_trans_assoc]

In proofs that compose many eqToHoms around a morphism, e.g. comparing subdivisions or functor-equality cocones built with Functor.congr_obj/congr_hom, simp often leaves eqToHom _ ≫ (eqToHom _ ≫ f ≫ eqToHom _) ≫ eqToHom _ untouched. The cause is that intermediate objects such as F.obj ⟨⟨a, h⟩⟩ and (map ι ⋙ F).obj ⟨⟨a, h'⟩⟩ are defeq but not syntactically equal, so eqToHom_trans doesn't fire. A reliable recipe is simp only [Category.assoc]; repeat erw [eqToHom_trans_assoc]; repeat erw [eqToHom_trans]. What remains is eqToHom p ≫ f ≫ eqToHom q = eqToHom p' ≫ f ≫ eqToHom q', which closes by rfl (proof irrelevance), or by erw [eqToHom_refl, eqToHom_refl, Category.id_comp, Category.comp_id] when the endpoints coincide. Also, a plain rw of a lemma inside such a term can fail with 'not type-correct under implicit transparency'. erw works there. Two related gotchas: inside namespace code Functor.ext may resolve to the core monad Functor.ext, so write CategoryTheory.Functor.ext. For IsPushout in Grpd, ascribe functor arrows as (by exact F : Grpd.of A ⟶ Grpd.of B), and build the instance as ⟨⟨w⟩, ⟨PushoutCocone.IsColimit.mk _ desc ...⟩⟩ so the cocone metavariables are fixed by the expected type.