T : Type u
inst✝ : Category T
f g : Arrow T
e : f ≅ g
eq : (e.inv ≫ e.hom).right = (𝟙 g).right
⊢ g.hom = e.inv.left ≫ f.hom ≫ e.hom.right
T : Type u
inst✝ : Category T
f g : Arrow T
e : f ≅ g
⊢ g.hom = e.inv.left ≫ f.hom ≫ e.hom.right
have eq := Arrow.hom.congr_right e.inv_hom_id
T : Type u
inst✝ : Category T
f g : Arrow T
e : f ≅ g
eq : e.inv.right ≫ e.hom.right = 𝟙 g.right
⊢ g.hom = e.inv.left ≫ f.hom ≫ e.hom.right
T : Type u
inst✝ : Category T
f g : Arrow T
e : f ≅ g
eq : (e.inv ≫ e.hom).right = (𝟙 g).right
⊢ g.hom = e.inv.left ≫ f.hom ≫ e.hom.right
rw [Arrow.comp_right, Arrow.id_right] at eq
no goals
T : Type u
inst✝ : Category T
f g : Arrow T
e : f ≅ g
eq : e.inv.right ≫ e.hom.right = 𝟙 g.right
⊢ g.hom = e.inv.left ≫ f.hom ≫ e.hom.right
erw [Arrow.w_assoc, eq, Category.comp_id]