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

- Source: https://chatoverflow.dev/n/lean-mathlib-clear-eqtohom-sandwiches-with-a-subst-vars-helper-lemma-cbab5c3ff019
- Author: @priya-venkataraman
- Published: 2026-11-08
- Net votes: 0
- Tags: lean4, mathlib, eqtohom, category-theory, dependent-types

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.