awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.Monoidal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : HasZeroObject.{v_1, u_1} C
inst_4 : Functor.Additive (D := CategoryTheory.Functor.{v_1, v_1, u_1, u_1} C C) (curriedTensor C)
inst_5 : ∀ (X₁ : C), Functor.Additive.{v_1, u_1, v_1, u_1} (Functor.obj (curriedTensor C) X₁)
I : Type u_2
inst_6 : AddMonoid I
c : ComplexShape I
inst_7 : c.TensorSigns
inst_8 : ∀ (X₁ X₂ : GradedObject I C), GradedObject.HasTensor.{u_2, v_1, u_1} X₁ X₂
inst_9 : ∀ (X₁ : C), PreservesColimit.{0, 0, v_1, v_1, u_1, u_1} (Functor.empty C) (Functor.obj (curriedTensor C) X₁)
inst_10 :
  ∀ (X₂ : C),
    PreservesColimit.{0, 0, v_1, v_1, u_1, u_1} (Functor.empty C) (Functor.obj (Functor.flip (curriedTensor C)) X₂)
inst_11 : ∀ (X₁ X₂ X₃ X₄ : GradedObject I C), GradedObject.HasTensor₄ObjExt.{u_2, v_1, u_1} X₁ X₂ X₃ X₄
inst_12 : ∀ (X₁ X₂ X₃ : GradedObject I C), GradedObject.HasGoodTensor₁₂Tensor.{u_2, v_1, u_1} X₁ X₂ X₃
inst_13 : ∀ (X₁ X₂ X₃ : GradedObject I C), GradedObject.HasGoodTensorTensor₂₃.{u_2, v_1, u_1} X₁ X₂ X₃
inst_14 : DecidableEq I
K : HomologicalComplex.{v_1, u_1, u_2} C c
rw :
  Eq (α :=
    Functor.obj (forget C c)
        (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) K
          ((𝟙_ (HomologicalComplex.{v_1, u_1, u_2} C c)) (𝒞 := instCategory))) ⟶
      Functor.obj (forget C c) K)
    (CategoryTheory.Functor.map (forget C c) (Iso.hom (ρ_ K)))
    (𝟙
        (MonoidalCategoryStruct.tensorObj (𝒞 := GradedObject.categoryOfGradedObjects.{u_2, v_1, u_1} I)
          (Functor.obj (forget C c) K)
          (Functor.obj (C := HomologicalComplex.{v_1, u_1, u_2} C c) (forget C c)
            ((𝟙_ (HomologicalComplex.{v_1, u_1, u_2} C c)) (𝒞 := instCategory)))) ≫
      (𝟙 (Functor.obj (forget C c) K) ⊗ₘ Iso.inv (tensorUnitIso C c)) ≫ Iso.hom (ρ_ (Functor.obj (forget C c) K)))
⊢ CategoryTheory.Functor.map (forget C c) (Iso.hom (ρ_ K)) =
    (𝟙
          (MonoidalCategoryStruct.tensorObj (𝒞 := GradedObject.categoryOfGradedObjects.{u_2, v_1, u_1} I)
            (Functor.obj (forget C c) K)
            (Functor.obj (C := HomologicalComplex.{v_1, u_1, u_2} C c) (forget C c)
              ((𝟙_ (HomologicalComplex.{v_1, u_1, u_2} C c)) (𝒞 := instCategory)))) ≫
        (𝟙 (Functor.obj (forget C c) K) ⊗ₘ Iso.inv (tensorUnitIso C c))) ≫
      Iso.hom (ρ_ (Functor.obj (forget C c) K))

Tactic:
rw [assoc]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.Algebra.Homology.Monoidal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : HasZeroObject.{v_1, u_1} C
inst_4 : Functor.Additive (D := CategoryTheory.Functor.{v_1, v_1, u_1, u_1} C C) (curriedTensor C)
inst_5 : ∀ (X₁ : C), Functor.Additive.{v_1, u_1, v_1, u_1} (Functor.obj (curriedTensor C) X₁)
I : Type u_2
inst_6 : AddMonoid I
c : ComplexShape I
inst_7 : c.TensorSigns
inst_8 : ∀ (X₁ X₂ : GradedObject I C), GradedObject.HasTensor.{u_2, v_1, u_1} X₁ X₂
inst_9 : ∀ (X₁ : C), PreservesColimit.{0, 0, v_1, v_1, u_1, u_1} (Functor.empty C) (Functor.obj (curriedTensor C) X₁)
inst_10 :
  ∀ (X₂ : C),
    PreservesColimit.{0, 0, v_1, v_1, u_1, u_1} (Functor.empty C) (Functor.obj (Functor.flip (curriedTensor C)) X₂)
inst_11 : ∀ (X₁ X₂ X₃ X₄ : GradedObject I C), GradedObject.HasTensor₄ObjExt.{u_2, v_1, u_1} X₁ X₂ X₃ X₄
inst_12 : ∀ (X₁ X₂ X₃ : GradedObject I C), GradedObject.HasGoodTensor₁₂Tensor.{u_2, v_1, u_1} X₁ X₂ X₃
inst_13 : ∀ (X₁ X₂ X₃ : GradedObject I C), GradedObject.HasGoodTensorTensor₂₃.{u_2, v_1, u_1} X₁ X₂ X₃
inst_14 : DecidableEq I
K : HomologicalComplex.{v_1, u_1, u_2} C c
erw :
  Eq (α :=
    Functor.obj (forget C c)
        (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) K
          ((𝟙_ (HomologicalComplex.{v_1, u_1, u_2} C c)) (𝒞 := instCategory))) ⟶
      Functor.obj (forget C c) K)
    (CategoryTheory.Functor.map (forget C c) (Iso.hom (ρ_ K)))
    ((𝟙 (Functor.obj (forget C c) K) ⊗ₘ Iso.inv (tensorUnitIso C c)) ≫ Iso.hom (ρ_ (Functor.obj (forget C c) K)))
⊢ Eq (α :=
    Functor.obj (forget C c)
        (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) K
          ((𝟙_ (HomologicalComplex.{v_1, u_1, u_2} C c)) (𝒞 := instCategory))) ⟶
      Functor.obj (forget C c) K)
    (CategoryTheory.Functor.map (forget C c) (Iso.hom (ρ_ K)))
    (𝟙
        (MonoidalCategoryStruct.tensorObj (𝒞 := GradedObject.categoryOfGradedObjects.{u_2, v_1, u_1} I)
          (Functor.obj (forget C c) K)
          (Functor.obj (C := HomologicalComplex.{v_1, u_1, u_2} C c) (forget C c)
            ((𝟙_ (HomologicalComplex.{v_1, u_1, u_2} C c)) (𝒞 := instCategory)))) ≫
      (𝟙 (Functor.obj (forget C c) K) ⊗ₘ Iso.inv (tensorUnitIso C c)) ≫ Iso.hom (ρ_ (Functor.obj (forget C c) K)))

Tactic:
erw [id_comp]

Premises used: CategoryTheory.Category.id_comp
-- Module: Mathlib.Algebra.Homology.Monoidal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : HasZeroObject.{v_1, u_1} C
inst_4 : Functor.Additive (D := CategoryTheory.Functor.{v_1, v_1, u_1, u_1} C C) (curriedTensor C)
inst_5 : ∀ (X₁ : C), Functor.Additive.{v_1, u_1, v_1, u_1} (Functor.obj (curriedTensor C) X₁)
I : Type u_2
inst_6 : AddMonoid I
c : ComplexShape I
inst_7 : c.TensorSigns
inst_8 : ∀ (X₁ X₂ : GradedObject I C), GradedObject.HasTensor.{u_2, v_1, u_1} X₁ X₂
inst_9 : ∀ (X₁ : C), PreservesColimit.{0, 0, v_1, v_1, u_1, u_1} (Functor.empty C) (Functor.obj (curriedTensor C) X₁)
inst_10 :
  ∀ (X₂ : C),
    PreservesColimit.{0, 0, v_1, v_1, u_1, u_1} (Functor.empty C) (Functor.obj (Functor.flip (curriedTensor C)) X₂)
inst_11 : ∀ (X₁ X₂ X₃ X₄ : GradedObject I C), GradedObject.HasTensor₄ObjExt.{u_2, v_1, u_1} X₁ X₂ X₃ X₄
inst_12 : ∀ (X₁ X₂ X₃ : GradedObject I C), GradedObject.HasGoodTensor₁₂Tensor.{u_2, v_1, u_1} X₁ X₂ X₃
inst_13 : ∀ (X₁ X₂ X₃ : GradedObject I C), GradedObject.HasGoodTensorTensor₂₃.{u_2, v_1, u_1} X₁ X₂ X₃
inst_14 : DecidableEq I
K : HomologicalComplex.{v_1, u_1, u_2} C c
⊢ Eq (α :=
    Functor.obj (forget C c)
        (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) K
          ((𝟙_ (HomologicalComplex.{v_1, u_1, u_2} C c)) (𝒞 := instCategory))) ⟶
      Functor.obj (forget C c) K)
    (CategoryTheory.Functor.map (forget C c) (Iso.hom (ρ_ K)))
    ((𝟙 (Functor.obj (forget C c) K) ⊗ₘ Iso.inv (tensorUnitIso C c)) ≫ Iso.hom (ρ_ (Functor.obj (forget C c) K)))

Tactic:
rfl
-- Module: Mathlib.Algebra.Homology.Opposite
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
inst_1 : Abelian.{v_1, u_1} V
X Y Z : V
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
rw : (f ≫ g).op = 0
rw₁ : Eq.{v_1 + 1} (α := op Z ⟶ op X) (Quiver.Hom.op 0) 0
rw₂ rw₃ : Eq.{v_1 + 1} (α := op Z ⟶ op X) 0 0
⊢ Eq.{v_1 + 1} (α := op Z ⟶ op X) (g.op ≫ f.op) 0

Tactic:
rw [← op_comp, w, op_zero]

Premises used: CategoryTheory.op_comp, CategoryTheory.Limits.op_zero
-- Module: Mathlib.Algebra.Homology.Opposite
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
inst_1 : Abelian.{v_1, u_1} V
X Y Z : V
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
rw :
  CategoryStruct.comp (Y := image g) (f ≫ factorThruImage g) (image.ι g) =
    CategoryStruct.comp (Y := image g) 0 (image.ι g)
rw₁ :
  f ≫ CategoryStruct.comp (Y := image g) (factorThruImage g) (image.ι g) =
    CategoryStruct.comp (Y := image g) 0 (image.ι g)
rw₂ : f ≫ g = CategoryStruct.comp (Y := image g) 0 (image.ι g)
rw₃ : Eq (α := X ⟶ Z) 0 (CategoryStruct.comp (Y := image g) 0 (image.ι g))
rw₄ rw₅ : Eq.{v_1 + 1} (α := X ⟶ Z) 0 0
⊢ Eq (α := X ⟶ image g) (f ≫ factorThruImage g) 0

Tactic:
rw [← cancel_mono (image.ι g), Category.assoc, image.fac, w, zero_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.image.ι, CategoryTheory.Limits.image.fac, CategoryTheory.cancel_mono, CategoryTheory.Limits.zero_comp
-- Module: Mathlib.Algebra.Homology.Opposite
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
inst_1 : Abelian.{v_1, u_1} V
X Y Z : V
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
h :
  Eq (α := Functor.obj (C := Subobject.{v_1, u_1} (op Y)) Subobject.underlying (imageSubobject g.op) ⟶ op Y)
    (CategoryStruct.comp (Y :=
        Functor.obj (C := Subobject.{v_1, u_1} (op Y)) Subobject.underlying (kernelSubobject f.op))
        (imageToKernel g.op f.op ⋯) (Subobject.arrow (kernelSubobject f.op)) :
      Functor.obj (C := Subobject.{v_1, u_1} (op Y)) Subobject.underlying (imageSubobject g.op) ⟶ op Y)
    (CategoryStruct.comp (Y :=
        Functor.obj (C := Subobject.{v_1, u_1} (op Y)) Subobject.underlying (kernelSubobject f.op))
        (CategoryStruct.comp (Y := op (image g))
          (Iso.hom (imageSubobjectIso g.op ≪≫ Iso.symm (imageOpOp g)) :
            Functor.obj (C := Subobject.{v_1, u_1} (op Y)) Subobject.underlying (imageSubobject g.op) ⟶ op (image g))
          (Quiver.Hom.op (cokernel.desc f (factorThruImage g) ⋯) ≫ Iso.inv (kernelSubobjectIso f.op ≪≫ kernelOpOp f) :
            op (image g) ⟶ Functor.obj (C := Subobject.{v_1, u_1} (op Y)) Subobject.underlying (kernelSubobject f.op)))
        (Subobject.arrow (kernelSubobject f.op)) :
      Functor.obj (C := Subobject.{v_1, u_1} (op Y)) Subobject.underlying (imageSubobject g.op) ⟶ op Y)
⊢ Eq (α :=
    Quiver.Hom.{v_1, u_1} (V := Vᵒᵖ)
      (Functor.obj (C := Subobject.{v_1, u_1} (op Y)) Subobject.underlying (imageSubobject g.op))
      (Functor.obj (C := Subobject.{v_1, u_1} (op Y)) Subobject.underlying (kernelSubobject f.op)))
    (imageToKernel g.op f.op ⋯ :
      Quiver.Hom.{v_1, u_1} (V := Vᵒᵖ)
        (Functor.obj (C := Subobject.{v_1, u_1} (op Y)) Subobject.underlying (imageSubobject g.op))
        (Functor.obj (C := Subobject.{v_1, u_1} (op Y)) Subobject.underlying (kernelSubobject f.op)))
    (CategoryStruct.comp (Y := op (image g))
        (Iso.hom (imageSubobjectIso g.op ≪≫ Iso.symm (imageOpOp g)) :
          Functor.obj (C := Subobject.{v_1, u_1} (op Y)) Subobject.underlying (imageSubobject g.op) ⟶ op (image g))
        (Quiver.Hom.op (cokernel.desc f (factorThruImage g) ⋯) ≫ Iso.inv (kernelSubobjectIso f.op ≪≫ kernelOpOp f) :
          op (image g) ⟶ Functor.obj (C := Subobject.{v_1, u_1} (op Y)) Subobject.underlying (kernelSubobject f.op)) :
      Quiver.Hom.{v_1, u_1} (V := Vᵒᵖ)
        (Functor.obj (C := Subobject.{v_1, u_1} (op Y)) Subobject.underlying (imageSubobject g.op))
        (Functor.obj (C := Subobject.{v_1, u_1} (op Y)) Subobject.underlying (kernelSubobject f.op)))

Tactic:
ext
-- Module: Mathlib.Algebra.Homology.Opposite
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
inst_1 : Abelian.{v_1, u_1} V
X Y Z : V
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
h :
  Eq (α := Functor.obj (C := Subobject.{v_1, u_1} (op Y)) Subobject.underlying (imageSubobject g.op) ⟶ op Y)
    (Iso.hom (imageSubobjectIso g.op) ≫
        CategoryStruct.comp (Y := op (image g.op.unop))
          (Iso.inv (imageUnopOp g.op) : image.{v_1, u_1} (X := op Z) (Y := op Y) g.op ⟶ op (image g.op.unop))
          (Quiver.Hom.op (factorThruImage g.op.unop) : op (image g.op.unop) ⟶ op Y) :
      Functor.obj (C := Subobject.{v_1, u_1} (op Y)) Subobject.underlying (imageSubobject g.op) ⟶ op Y)
    (Iso.hom (imageSubobjectIso g.op) ≫
        CategoryStruct.comp (Y := op (image g))
          (Iso.inv (imageOpOp g) : image.{v_1, u_1} (X := op Z) (Y := op Y) g.op ⟶ op (image g))
          (Quiver.Hom.op (factorThruImage g) : op (image g) ⟶ op Y) :
      Functor.obj (C := Subobject.{v_1, u_1} (op Y)) Subobject.underlying (imageSubobject g.op) ⟶ op Y)
⊢ Eq (α := Functor.obj (C := Subobject.{v_1, u_1} (op Y)) Subobject.underlying (imageSubobject g.op) ⟶ op Y)
    (CategoryStruct.comp (Y :=
        Functor.obj (C := Subobject.{v_1, u_1} (op Y)) Subobject.underlying (kernelSubobject f.op))
        (imageToKernel g.op f.op ⋯) (Subobject.arrow (kernelSubobject f.op)) :
      Functor.obj (C := Subobject.{v_1, u_1} (op Y)) Subobject.underlying (imageSubobject g.op) ⟶ op Y)
    (CategoryStruct.comp (Y :=
        Functor.obj (C := Subobject.{v_1, u_1} (op Y)) Subobject.underlying (kernelSubobject f.op))
        (CategoryStruct.comp (Y := op (image g))
          (Iso.hom (imageSubobjectIso g.op ≪≫ Iso.symm (imageOpOp g)) :
            Functor.obj (C := Subobject.{v_1, u_1} (op Y)) Subobject.underlying (imageSubobject g.op) ⟶ op (image g))
          (Quiver.Hom.op (cokernel.desc f (factorThruImage g) ⋯) ≫ Iso.inv (kernelSubobjectIso f.op ≪≫ kernelOpOp f) :
            op (image g) ⟶ Functor.obj (C := Subobject.{v_1, u_1} (op Y)) Subobject.underlying (kernelSubobject f.op)))
        (Subobject.arrow (kernelSubobject f.op)) :
      Functor.obj (C := Subobject.{v_1, u_1} (op Y)) Subobject.underlying (imageSubobject g.op) ⟶ op Y)

Tactic:
simp only [Iso.trans_hom, Iso.symm_hom, Iso.trans_inv, kernelOpOp_inv, Category.assoc,
    imageToKernel_arrow, kernelSubobject_arrow', kernel.lift_ι, ← op_comp, cokernel.π_desc,
    ← imageSubobject_arrow, ← imageUnopOp_inv_comp_op_factorThruImage g.op]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.op_comp, Quiver.Hom.op, CategoryTheory.Iso.symm_hom, imageToKernel_arrow, CategoryTheory.Limits.cokernel.π_desc, CategoryTheory.Limits.imageSubobject_arrow, CategoryTheory.Iso.trans_hom, CategoryTheory.Limits.kernel.lift_ι, CategoryTheory.kernelOpOp_inv, CategoryTheory.imageUnopOp_inv_comp_op_factorThruImage, CategoryTheory.Iso.trans_inv, CategoryTheory.Limits.kernelSubobject_arrow'
-- Module: Mathlib.Algebra.Homology.Opposite
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
inst_1 : Abelian.{v_1, u_1} V
X Y Z : V
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
⊢ Eq (α := Functor.obj (C := Subobject.{v_1, u_1} (op Y)) Subobject.underlying (imageSubobject g.op) ⟶ op Y)
    (Iso.hom (imageSubobjectIso g.op) ≫
        CategoryStruct.comp (Y := op (image g.op.unop))
          (Iso.inv (imageUnopOp g.op) : image.{v_1, u_1} (X := op Z) (Y := op Y) g.op ⟶ op (image g.op.unop))
          (Quiver.Hom.op (factorThruImage g.op.unop) : op (image g.op.unop) ⟶ op Y) :
      Functor.obj (C := Subobject.{v_1, u_1} (op Y)) Subobject.underlying (imageSubobject g.op) ⟶ op Y)
    (Iso.hom (imageSubobjectIso g.op) ≫
        CategoryStruct.comp (Y := op (image g))
          (Iso.inv (imageOpOp g) : image.{v_1, u_1} (X := op Z) (Y := op Y) g.op ⟶ op (image g))
          (Quiver.Hom.op (factorThruImage g) : op (image g) ⟶ op Y) :
      Functor.obj (C := Subobject.{v_1, u_1} (op Y)) Subobject.underlying (imageSubobject g.op) ⟶ op Y)

Tactic:
rfl
-- Module: Mathlib.Algebra.Homology.Opposite
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
inst_1 : Abelian.{v_1, u_1} V
X Y Z : Vᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
w : Eq.{v_1 + 1} (α := X ⟶ Z) (f ≫ g) 0
rw : Eq.{v_1 + 1} (α := unop Z ⟶ unop X) (Quiver.Hom.unop (f ≫ g)) 0
rw₁ : Eq.{v_1 + 1} (α := unop Z ⟶ unop X) (Quiver.Hom.unop 0) 0
rw₂ rw₃ : Eq.{v_1 + 1} (α := unop Z ⟶ unop X) 0 0
⊢ g.unop ≫ f.unop = 0

Tactic:
rw [← unop_comp, w, unop_zero]

Premises used: CategoryTheory.unop_comp, CategoryTheory.Limits.unop_zero
-- Module: Mathlib.Algebra.Homology.Opposite
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
inst_1 : Abelian.{v_1, u_1} V
X Y Z : Vᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
w : Eq.{v_1 + 1} (α := X ⟶ Z) (f ≫ g) 0
rw :
  Eq.{v_1 + 1} (α := X ⟶ Z)
    (CategoryStruct.comp (Y := image.{v_1, u_1} (X := Y) (Y := Z) g) (f ≫ factorThruImage g) (image.ι g))
    (CategoryStruct.comp (Y := image.{v_1, u_1} (X := Y) (Y := Z) g) 0 (image.ι g))
rw₁ :
  Eq.{v_1 + 1} (α := X ⟶ Z)
    (f ≫ CategoryStruct.comp (Y := image.{v_1, u_1} (X := Y) (Y := Z) g) (factorThruImage g) (image.ι g))
    (CategoryStruct.comp (Y := image.{v_1, u_1} (X := Y) (Y := Z) g) 0 (image.ι g))
rw₂ : Eq.{v_1 + 1} (α := X ⟶ Z) (f ≫ g) (CategoryStruct.comp (Y := image.{v_1, u_1} (X := Y) (Y := Z) g) 0 (image.ι g))
rw₃ : Eq.{v_1 + 1} (α := X ⟶ Z) 0 (CategoryStruct.comp (Y := image.{v_1, u_1} (X := Y) (Y := Z) g) 0 (image.ι g))
rw₄ rw₅ : Eq.{v_1 + 1} (α := X ⟶ Z) 0 0
⊢ Eq.{v_1 + 1} (α := X ⟶ image.{v_1, u_1} (X := Y) (Y := Z) g) (f ≫ factorThruImage g) 0

Tactic:
rw [← cancel_mono (image.ι g), Category.assoc, image.fac, w, zero_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.image.ι, CategoryTheory.Limits.image.fac, CategoryTheory.cancel_mono, CategoryTheory.Limits.zero_comp
-- Module: Mathlib.Algebra.Homology.Opposite
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
inst_1 : Abelian.{v_1, u_1} V
X Y Z : Vᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
w : Eq.{v_1 + 1} (α := X ⟶ Z) (f ≫ g) 0
h :
  Eq (α := Functor.obj Subobject.underlying (imageSubobject g.unop) ⟶ unop Y)
    (imageToKernel g.unop f.unop ⋯ ≫ (kernelSubobject f.unop).arrow :
      Functor.obj Subobject.underlying (imageSubobject g.unop) ⟶ unop Y)
    (CategoryStruct.comp (Y := unop (image.{v_1, u_1} (X := Y) (Y := Z) g))
          (Iso.hom (imageSubobjectIso g.unop ≪≫ Iso.symm (imageUnopUnop g)) :
            Functor.obj Subobject.underlying (imageSubobject g.unop) ⟶ unop (image.{v_1, u_1} (X := Y) (Y := Z) g))
          (Quiver.Hom.unop (cokernel.desc f (factorThruImage g) ⋯) ≫
              Iso.inv (kernelSubobjectIso f.unop ≪≫ kernelUnopUnop f) :
            unop (image.{v_1, u_1} (X := Y) (Y := Z) g) ⟶ Functor.obj Subobject.underlying (kernelSubobject f.unop)) ≫
        (kernelSubobject f.unop).arrow :
      Functor.obj Subobject.underlying (imageSubobject g.unop) ⟶ unop Y)
⊢ Eq (α :=
    Functor.obj Subobject.underlying (imageSubobject g.unop) ⟶
      Functor.obj Subobject.underlying (kernelSubobject f.unop))
    (imageToKernel g.unop f.unop ⋯ :
      Functor.obj Subobject.underlying (imageSubobject g.unop) ⟶
        Functor.obj Subobject.underlying (kernelSubobject f.unop))
    (CategoryStruct.comp (Y := unop (image.{v_1, u_1} (X := Y) (Y := Z) g))
        (Iso.hom (imageSubobjectIso g.unop ≪≫ Iso.symm (imageUnopUnop g)) :
          Functor.obj Subobject.underlying (imageSubobject g.unop) ⟶ unop (image.{v_1, u_1} (X := Y) (Y := Z) g))
        (Quiver.Hom.unop (cokernel.desc f (factorThruImage g) ⋯) ≫
            Iso.inv (kernelSubobjectIso f.unop ≪≫ kernelUnopUnop f) :
          unop (image.{v_1, u_1} (X := Y) (Y := Z) g) ⟶ Functor.obj Subobject.underlying (kernelSubobject f.unop)) :
      Functor.obj Subobject.underlying (imageSubobject g.unop) ⟶
        Functor.obj Subobject.underlying (kernelSubobject f.unop))

Tactic:
ext
-- Module: Mathlib.Algebra.Homology.Opposite
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
inst_1 : Abelian.{v_1, u_1} V
X Y Z : Vᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
w : Eq.{v_1 + 1} (α := X ⟶ Z) (f ≫ g) 0
h :
  Eq (α := Functor.obj Subobject.underlying (imageSubobject g.unop) ⟶ unop Y)
    (imageToKernel g.unop f.unop ⋯ ≫ (kernelSubobject f.unop).arrow :
      Functor.obj Subobject.underlying (imageSubobject g.unop) ⟶ unop Y)
    (CategoryStruct.comp (Y := unop (image.{v_1, u_1} (X := Y) (Y := Z) g))
          (Iso.hom (imageSubobjectIso g.unop ≪≫ Iso.symm (Iso.unop (imageUnopOp g))) :
            Functor.obj Subobject.underlying (imageSubobject g.unop) ⟶ unop (image.{v_1, u_1} (X := Y) (Y := Z) g))
          (Quiver.Hom.unop (cokernel.desc f (factorThruImage g) ⋯) ≫
              Iso.inv (kernelSubobjectIso f.unop ≪≫ kernelUnopUnop f) :
            unop (image.{v_1, u_1} (X := Y) (Y := Z) g) ⟶ Functor.obj Subobject.underlying (kernelSubobject f.unop)) ≫
        (kernelSubobject f.unop).arrow :
      Functor.obj Subobject.underlying (imageSubobject g.unop) ⟶ unop Y)
⊢ Eq (α := Functor.obj Subobject.underlying (imageSubobject g.unop) ⟶ unop Y)
    (imageToKernel g.unop f.unop ⋯ ≫ (kernelSubobject f.unop).arrow :
      Functor.obj Subobject.underlying (imageSubobject g.unop) ⟶ unop Y)
    (CategoryStruct.comp (Y := unop (image.{v_1, u_1} (X := Y) (Y := Z) g))
          (Iso.hom (imageSubobjectIso g.unop ≪≫ Iso.symm (imageUnopUnop g)) :
            Functor.obj Subobject.underlying (imageSubobject g.unop) ⟶ unop (image.{v_1, u_1} (X := Y) (Y := Z) g))
          (Quiver.Hom.unop (cokernel.desc f (factorThruImage g) ⋯) ≫
              Iso.inv (kernelSubobjectIso f.unop ≪≫ kernelUnopUnop f) :
            unop (image.{v_1, u_1} (X := Y) (Y := Z) g) ⟶ Functor.obj Subobject.underlying (kernelSubobject f.unop)) ≫
        (kernelSubobject f.unop).arrow :
      Functor.obj Subobject.underlying (imageSubobject g.unop) ⟶ unop Y)

Tactic:
dsimp only [imageUnopUnop]

Premises used: CategoryTheory.imageUnopUnop
-- Module: Mathlib.Algebra.Homology.Opposite
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
inst_1 : Abelian.{v_1, u_1} V
X Y Z : Vᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
w : Eq.{v_1 + 1} (α := X ⟶ Z) (f ≫ g) 0
⊢ Eq (α := Functor.obj Subobject.underlying (imageSubobject g.unop) ⟶ unop Y)
    (imageToKernel g.unop f.unop ⋯ ≫ (kernelSubobject f.unop).arrow :
      Functor.obj Subobject.underlying (imageSubobject g.unop) ⟶ unop Y)
    (CategoryStruct.comp (Y := unop (image.{v_1, u_1} (X := Y) (Y := Z) g))
          (Iso.hom (imageSubobjectIso g.unop ≪≫ Iso.symm (Iso.unop (imageUnopOp g))) :
            Functor.obj Subobject.underlying (imageSubobject g.unop) ⟶ unop (image.{v_1, u_1} (X := Y) (Y := Z) g))
          (Quiver.Hom.unop (cokernel.desc f (factorThruImage g) ⋯) ≫
              Iso.inv (kernelSubobjectIso f.unop ≪≫ kernelUnopUnop f) :
            unop (image.{v_1, u_1} (X := Y) (Y := Z) g) ⟶ Functor.obj Subobject.underlying (kernelSubobject f.unop)) ≫
        (kernelSubobject f.unop).arrow :
      Functor.obj Subobject.underlying (imageSubobject g.unop) ⟶ unop Y)

Tactic:
simp only [Iso.trans_hom, Iso.symm_hom, Iso.trans_inv, kernelUnopUnop_inv, Category.assoc,
    imageToKernel_arrow, kernelSubobject_arrow', kernel.lift_ι, cokernel.π_desc, Iso.unop_inv,
    ← unop_comp, factorThruImage_comp_imageUnopOp_inv, Quiver.Hom.unop_op, imageSubobject_arrow]

Premises used: CategoryTheory.Category.assoc, Quiver.Hom.unop_op, CategoryTheory.kernelUnopUnop_inv, CategoryTheory.Iso.symm_hom, CategoryTheory.factorThruImage_comp_imageUnopOp_inv, CategoryTheory.unop_comp, imageToKernel_arrow, CategoryTheory.Limits.cokernel.π_desc, CategoryTheory.Limits.imageSubobject_arrow, CategoryTheory.Iso.unop_inv, CategoryTheory.Iso.trans_hom, CategoryTheory.Limits.kernel.lift_ι, CategoryTheory.Iso.trans_inv, CategoryTheory.Limits.kernelSubobject_arrow'
-- Module: Mathlib.Algebra.Homology.Opposite
Goal:
ι : Type u_1
V : Type u_2
inst : Category.{v_1, u_2} V
c : ComplexShape ι
inst_1 : HasZeroMorphisms.{v_1, u_2} V
X : HomologicalComplex.{v_1, u_2, u_1} V c
i j : ι
hij : ¬c.symm.Rel i j
rw : Eq.{v_1 + 1} (α := op (X.X i) ⟶ op (X.X j)) (Quiver.Hom.op 0) 0
rw₁ rw₂ : Eq.{v_1 + 1} (α := op (X.X i) ⟶ op (X.X j)) 0 0
⊢ (X.d j i).op = 0

Tactic:
rw [X.shape j i hij, op_zero]

Premises used: CategoryTheory.Limits.op_zero, HomologicalComplex.shape
-- Module: Mathlib.Algebra.Homology.Opposite
Goal:
ι : Type u_1
V : Type u_2
inst : Category.{v_1, u_2} V
c : ComplexShape ι
inst_1 : HasZeroMorphisms.{v_1, u_2} V
X : HomologicalComplex.{v_1, u_2, u_1} V c
x x_1 x_2 : ι
h : c.symm.Rel x x_1
h_1 : c.symm.Rel x_1 x_2
rw : (X.d x_2 x_1 ≫ X.d x_1 x).op = 0
rw₁ : Eq.{v_1 + 1} (α := op (X.X x) ⟶ op (X.X x_2)) (Quiver.Hom.op 0) 0
rw₂ rw₃ : Eq.{v_1 + 1} (α := op (X.X x) ⟶ op (X.X x_2)) 0 0
⊢ Eq.{v_1 + 1} (α := op (X.X x) ⟶ op (X.X x_2)) ((X.d x_1 x).op ≫ (X.d x_2 x_1).op) 0

Tactic:
rw [← op_comp, X.d_comp_d, op_zero]

Premises used: CategoryTheory.op_comp, HomologicalComplex.d_comp_d, CategoryTheory.Limits.op_zero
-- Module: Mathlib.Algebra.Homology.Opposite
Goal:
ι : Type u_1
V : Type u_2
inst : Category.{v_1, u_2} V
c : ComplexShape ι
inst_1 : HasZeroMorphisms.{v_1, u_2} V
X : HomologicalComplex.{v_1, u_2, u_1} V c.symm
i j : ι
hij : ¬c.Rel i j
rw : Eq.{v_1 + 1} (α := op (X.X i) ⟶ op (X.X j)) (Quiver.Hom.op 0) 0
rw₁ rw₂ : Eq.{v_1 + 1} (α := op (X.X i) ⟶ op (X.X j)) 0 0
⊢ (X.d j i).op = 0

Tactic:
rw [X.shape j i hij, op_zero]

Premises used: CategoryTheory.Limits.op_zero, HomologicalComplex.shape
-- Module: Mathlib.Algebra.Homology.Opposite
Goal:
ι : Type u_1
V : Type u_2
inst : Category.{v_1, u_2} V
c : ComplexShape ι
inst_1 : HasZeroMorphisms.{v_1, u_2} V
X : HomologicalComplex.{v_1, u_2, u_1} V c.symm
x x_1 x_2 : ι
h : c.Rel x x_1
h_1 : c.Rel x_1 x_2
rw : (X.d x_2 x_1 ≫ X.d x_1 x).op = 0
rw₁ : Eq.{v_1 + 1} (α := op (X.X x) ⟶ op (X.X x_2)) (Quiver.Hom.op 0) 0
rw₂ rw₃ : Eq.{v_1 + 1} (α := op (X.X x) ⟶ op (X.X x_2)) 0 0
⊢ Eq.{v_1 + 1} (α := op (X.X x) ⟶ op (X.X x_2)) ((X.d x_1 x).op ≫ (X.d x_2 x_1).op) 0

Tactic:
rw [← op_comp, X.d_comp_d, op_zero]

Premises used: CategoryTheory.op_comp, HomologicalComplex.d_comp_d, CategoryTheory.Limits.op_zero