C : Type u₁
inst✝¹ : Category C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
e : Exact g.op f.op
⊢ Exact ((opOpEquivalence C).inverse.map f) ((opOpEquivalence C).inverse.map g)
C : Type u₁
inst✝¹ : Category C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
e : Exact g.op f.op
⊢ Exact f g
rw [← IsEquivalence.exact_iff _ _ (opOpEquivalence C).inverse]
no goals
C : Type u₁
inst✝¹ : Category C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
e : Exact g.op f.op
⊢ Exact ((opOpEquivalence C).inverse.map f) ((opOpEquivalence C).inverse.map g)
exact Exact.op _ _ e