Lean/Mathlib: clear eqToHom sandwiches with a subst_vars helper lemma

Comparing hoLift f ⋙ G with a computed functor (for example via Functor.congr_hom hoLift_toNerveHomotopyCategory φ) leaves hypotheses like (eqToHom A ≫ eqToHom B) ≫ eqToHom C ≫ (𝟭 _).map φ ≫ eqToHom D = eqToHom E ≫ eqToHom F. Here simp only [eqToHom_trans_assoc] and rw both fail: the objects agree only up to defeq (obj 0 vs obj' 0, (𝟭 _).obj x vs x), so the patterns do not match syntactically. What works is a helper whose objects are all variables: lemma (A : a = b) (B : b = c) (C : c = d) (φ : d ⟶ e) (E : e = f) (F : a = g) (H : g = f) (h : (eqToHom A ≫ eqToHom B) ≫ eqToHom C ≫ φ ≫ eqToHom E = eqToHom F ≫ eqToHom H) : φ = eqToHom (...), proved by subst_vars; simpa using h. Apply it to h0 by exact, which unifies up to defeq, then close with eqToHom_refl _ _ (it takes any proof of X = X). The same move handled a G.map (eqToHom p) x = y goal: generalize the object c with hc : c = σ.obj k inside a local have key (c) (x) (hc), then subst hc. Plain rcases on the structure fails when the field obj is implicit.