V : Type u
inst✝⁵ : Category V
inst✝⁴ : HasImages V
inst✝³ : HasZeroObject V
inst✝² : Preadditive V
inst✝¹ : HasKernels V
inst✝ : HasCokernels V
A₁ B₁ C₁ A₂ B₂ C₂ : V
f₁ : A₁ ⟶ B₁
g₁ : B₁ ⟶ C₁
f₂ : A₂ ⟶ B₂
g₂ : B₂ ⟶ C₂
α : Arrow.mk f₁ ≅ Arrow.mk f₂
β : Arrow.mk g₁ ≅ Arrow.mk g₂
p : α.hom.right = β.hom.left
⊢ α.symm.hom.right ≫ α.hom.right = β.symm.hom.left ≫ α.hom.right
V : Type u
inst✝⁵ : Category V
inst✝⁴ : HasImages V
inst✝³ : HasZeroObject V
inst✝² : Preadditive V
inst✝¹ : HasKernels V
inst✝ : HasCokernels V
A₁ B₁ C₁ A₂ B₂ C₂ : V
f₁ : A₁ ⟶ B₁
g₁ : B₁ ⟶ C₁
f₂ : A₂ ⟶ B₂
g₂ : B₂ ⟶ C₂
α : Arrow.mk f₁ ≅ Arrow.mk f₂
β : Arrow.mk g₁ ≅ Arrow.mk g₂
p : α.hom.right = β.hom.left
⊢ α.symm.hom.right = β.symm.hom.left
rw [← cancel_mono α.hom.right]
V : Type u
inst✝⁵ : Category V
inst✝⁴ : HasImages V
inst✝³ : HasZeroObject V
inst✝² : Preadditive V
inst✝¹ : HasKernels V
inst✝ : HasCokernels V
A₁ B₁ C₁ A₂ B₂ C₂ : V
f₁ : A₁ ⟶ B₁
g₁ : B₁ ⟶ C₁
f₂ : A₂ ⟶ B₂
g₂ : B₂ ⟶ C₂
α : Arrow.mk f₁ ≅ Arrow.mk f₂
β : Arrow.mk g₁ ≅ Arrow.mk g₂
p : α.hom.right = β.hom.left
⊢ (𝟙 (Arrow.mk f₂)).right = β.inv.left ≫ α.hom.right
V : Type u
inst✝⁵ : Category V
inst✝⁴ : HasImages V
inst✝³ : HasZeroObject V
inst✝² : Preadditive V
inst✝¹ : HasKernels V
inst✝ : HasCokernels V
A₁ B₁ C₁ A₂ B₂ C₂ : V
f₁ : A₁ ⟶ B₁
g₁ : B₁ ⟶ C₁
f₂ : A₂ ⟶ B₂
g₂ : B₂ ⟶ C₂
α : Arrow.mk f₁ ≅ Arrow.mk f₂
β : Arrow.mk g₁ ≅ Arrow.mk g₂
p : α.hom.right = β.hom.left
⊢ α.symm.hom.right ≫ α.hom.right = β.symm.hom.left ≫ α.hom.right
simp only [Iso.symm_hom, ← Arrow.comp_right, α.inv_hom_id]
V : Type u
inst✝⁵ : Category V
inst✝⁴ : HasImages V
inst✝³ : HasZeroObject V
inst✝² : Preadditive V
inst✝¹ : HasKernels V
inst✝ : HasCokernels V
A₁ B₁ C₁ A₂ B₂ C₂ : V
f₁ : A₁ ⟶ B₁
g₁ : B₁ ⟶ C₁
f₂ : A₂ ⟶ B₂
g₂ : B₂ ⟶ C₂
α : Arrow.mk f₁ ≅ Arrow.mk f₂
β : Arrow.mk g₁ ≅ Arrow.mk g₂
p : α.hom.right = β.hom.left
⊢ 𝟙 (Arrow.mk f₂).right = 𝟙 (Arrow.mk g₂).left
V : Type u
inst✝⁵ : Category V
inst✝⁴ : HasImages V
inst✝³ : HasZeroObject V
inst✝² : Preadditive V
inst✝¹ : HasKernels V
inst✝ : HasCokernels V
A₁ B₁ C₁ A₂ B₂ C₂ : V
f₁ : A₁ ⟶ B₁
g₁ : B₁ ⟶ C₁
f₂ : A₂ ⟶ B₂
g₂ : B₂ ⟶ C₂
α : Arrow.mk f₁ ≅ Arrow.mk f₂
β : Arrow.mk g₁ ≅ Arrow.mk g₂
p : α.hom.right = β.hom.left
⊢ (𝟙 (Arrow.mk f₂)).right = β.inv.left ≫ α.hom.right
simp only [p, ← Arrow.comp_left, Arrow.id_right, Arrow.id_left, Iso.inv_hom_id]
no goals
V : Type u
inst✝⁵ : Category V
inst✝⁴ : HasImages V
inst✝³ : HasZeroObject V
inst✝² : Preadditive V
inst✝¹ : HasKernels V
inst✝ : HasCokernels V
A₁ B₁ C₁ A₂ B₂ C₂ : V
f₁ : A₁ ⟶ B₁
g₁ : B₁ ⟶ C₁
f₂ : A₂ ⟶ B₂
g₂ : B₂ ⟶ C₂
α : Arrow.mk f₁ ≅ Arrow.mk f₂
β : Arrow.mk g₁ ≅ Arrow.mk g₂
p : α.hom.right = β.hom.left
⊢ 𝟙 (Arrow.mk f₂).right = 𝟙 (Arrow.mk g₂).left
rfl