no goals
C : Type u
inst✝ : Category C
X Y Z : C
α : X ≅ Y
f : X ⟶ Z
g : Y ⟶ Z
H : α.inv ≫ f = g
⊢ f = α.hom ≫ g
simp [H.symm]
no goals
C : Type u
inst✝ : Category C
X Y Z : C
α : X ≅ Y
f : X ⟶ Z
g : Y ⟶ Z
H : f = α.hom ≫ g
⊢ α.inv ≫ f = g
simp [H]