no goals
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
T T' T'' : D
Y✝ Y' : C
S : C ⥤ D
X Y : CostructuredArrow S T
h : X = Y
⊢ X.left = Y.left
rw [h]
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
T T' T'' : D
Y Y' : C
S : C ⥤ D
X : CostructuredArrow S T
⊢ (eqToHom (_ : X = X)).left = eqToHom (_ : X.left = X.left)
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
T T' T'' : D
Y✝ Y' : C
S : C ⥤ D
X Y : CostructuredArrow S T
h : X = Y
⊢ (eqToHom h).left = eqToHom (_ : X.left = Y.left)
subst h
no goals
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
T T' T'' : D
Y Y' : C
S : C ⥤ D
X : CostructuredArrow S T
⊢ (eqToHom (_ : X = X)).left = eqToHom (_ : X.left = X.left)
simp only [eqToHom_refl, id_left]