C : Type u₁
inst✝¹ : Category C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h : Exact f g
⊢ g.op ≫ f.op = 0 ∧ kernel.ι f.op ≫ cokernel.π g.op = 0
C : Type u₁
inst✝¹ : Category C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h : Exact f g
⊢ Exact g.op f.op
rw [exact_iff]
C : Type u₁
inst✝¹ : Category C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h : Exact f g
⊢ (kernel.ι f.op ≫ cokernel.π g.op).unop = 0.unop
C : Type u₁
inst✝¹ : Category C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h : Exact f g
⊢ g.op ≫ f.op = 0 ∧ kernel.ι f.op ≫ cokernel.π g.op = 0
refine' ⟨by simp [← op_comp, h.w], Quiver.Hom.unop_inj _⟩
no goals
C : Type u₁
inst✝¹ : Category C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h : Exact f g
⊢ (kernel.ι f.op ≫ cokernel.π g.op).unop = 0.unop
simp only [unop_comp, cokernel.π_op, eqToHom_refl, kernel.ι_op, Category.id_comp,
  Category.assoc, kernel_comp_cokernel_assoc _ _ h, zero_comp, comp_zero, unop_zero]
no goals
C : Type u₁
inst✝¹ : Category C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h : Exact f g
⊢ g.op ≫ f.op = 0
simp [← op_comp, h.w]