Exactness in opposite category

Stream: Is there code for X?

[Jujian Zhang]

If we have [exact f g], do we have [exact g.op f.op] in mathlib?

import algebra.homology.exact

open category_theory
open category_theory.limits

universes v u

namespace category_theory
variables {C : Type u} [category.{v} C]

instance exact.op [has_zero_morphisms C] [has_equalizers C] [has_images C]
  [has_equalizers Cᵒᵖ] [has_images Cᵒᵖ] {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} [exact f g] :
  exact g.op f.op :=
⟨begin
  have w : f ≫ g = 0:= exact.w,
  convert congr_arg quiver.hom.op w,
end, ⟨λ A h1 h2 eq1, begin
  sorry,
end⟩⟩

end category_theory

[Kevin Buzzard]

@Amelia Livingston were you thinking about this recently?

[Johan Commelin]

lean-liquid$ rg "exact g.op f.op"
src/for_mathlib/exact_seq.lean
101:instance [exact f g] : exact g.op f.op :=
280:  have hgf : exact g.op f.op, { resetI, apply_instance },

[Kevin Buzzard]

who needs library-search when you have ripgrep