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