no goals
C : Type u₁
inst✝ : Category C
X X' Y : C
p : X = X'
f : X ⟶ Y
g : X' ⟶ Y
h : eqToHom p ≫ g = f
⊢ g = eqToHom (_ : X' = X) ≫ eqToHom p ≫ g
simp
no goals
C : Type u₁
inst✝ : Category C
X X' Y : C
p : X = X'
f : X ⟶ Y
g : X' ⟶ Y
h : g = eqToHom (_ : X' = X) ≫ f
⊢ eqToHom p ≫ eqToHom (_ : X' = X) ≫ f = f
simp [whisker_eq _ h]