awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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} (α := unop (X.X i) ⟶ unop (X.X j)) (Quiver.Hom.unop 0) 0
rw₁ rw₂ : Eq.{v_1 + 1} (α := unop (X.X i) ⟶ unop (X.X j)) 0 0
⊢ (X.d j i).unop = 0

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

Premises used: CategoryTheory.Limits.unop_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).unop = 0
rw₁ : Eq.{v_1 + 1} (α := unop (X.X x) ⟶ unop (X.X x_2)) (Quiver.Hom.unop 0) 0
rw₂ rw₃ : Eq.{v_1 + 1} (α := unop (X.X x) ⟶ unop (X.X x_2)) 0 0
⊢ (X.d x_1 x).unop ≫ (X.d x_2 x_1).unop = 0

Tactic:
rw [← unop_comp, X.d_comp_d, unop_zero]

Premises used: CategoryTheory.unop_comp, CategoryTheory.Limits.unop_zero, HomologicalComplex.d_comp_d
-- 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} (α := unop (X.X i) ⟶ unop (X.X j)) (Quiver.Hom.unop 0) 0
rw₁ rw₂ : Eq.{v_1 + 1} (α := unop (X.X i) ⟶ unop (X.X j)) 0 0
⊢ (X.d j i).unop = 0

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

Premises used: CategoryTheory.Limits.unop_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).unop = 0
rw₁ : Eq.{v_1 + 1} (α := unop (X.X x) ⟶ unop (X.X x_2)) (Quiver.Hom.unop 0) 0
rw₂ rw₃ : Eq.{v_1 + 1} (α := unop (X.X x) ⟶ unop (X.X x_2)) 0 0
⊢ (X.d x_1 x).unop ≫ (X.d x_2 x_1).unop = 0

Tactic:
rw [← unop_comp, X.d_comp_d, unop_zero]

Premises used: CategoryTheory.unop_comp, CategoryTheory.Limits.unop_zero, HomologicalComplex.d_comp_d
-- 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 Y : (HomologicalComplex.{v_1, u_2, u_1} V c)ᵒᵖ
f : X ⟶ Y
i j : ι
h : c.symm.Rel i j
⊢ (f.unop.f i).op ≫ (unop Y).op.d i j = (unop X).op.d i j ≫ (f.unop.f j).op

Tactic:
simp only [op_d, ← op_comp, f.unop.comm]

Premises used: CategoryTheory.op_comp, HomologicalComplex.op_d, Quiver.Hom.unop, HomologicalComplex.Hom.comm
-- 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 Y : HomologicalComplex.{v_1, u_2, u_1} Vᵒᵖ c.symm
f : X ⟶ Y
i j : ι
h : c.Rel i j
⊢ (f.f i).unop ≫ X.unopSymm.d i j = Y.unopSymm.d i j ≫ (f.f j).unop

Tactic:
simp only [unopSymm_d, ← unop_comp, f.comm]

Premises used: CategoryTheory.unop_comp, HomologicalComplex.unopSymm_d, HomologicalComplex.Hom.comm
-- 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 : ι
h : c.Rel i j
⊢ Iso.hom
        ((fun (x : ι) ↦ (Iso.refl ((unop X).op.unopSymm.X x) : (unop X).op.unopSymm.X x ≅ (unop X).op.unopSymm.X x))
          i) ≫
      (unop X).d i j =
    (unop X).op.unopSymm.d i j ≫
      Iso.hom
        ((fun (x : ι) ↦ (Iso.refl ((unop X).op.unopSymm.X x) : (unop X).op.unopSymm.X x ≅ (unop X).op.unopSymm.X x)) j)

Tactic:
simp only [Iso.refl_hom, Category.id_comp, unopSymm_d, op_d, Quiver.Hom.unop_op,
              Category.comp_id]

Premises used: HomologicalComplex.op_d, Quiver.Hom.unop_op, CategoryTheory.Category.comp_id, HomologicalComplex.unopSymm_d, CategoryTheory.Iso.refl_hom, CategoryTheory.Category.id_comp
-- 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 Y : (HomologicalComplex.{v_1, u_2, u_1} V c)ᵒᵖ
f : X ⟶ Y
⊢ Eq (α := Functor.obj (𝟭 (HomologicalComplex.{v_1, u_2, u_1} V c)ᵒᵖ) X ⟶ Functor.obj (opFunctor V c ⋙ opInverse V c) Y)
    (CategoryTheory.Functor.map (𝟭 (HomologicalComplex.{v_1, u_2, u_1} V c)ᵒᵖ) f ≫
      Iso.hom
        ((fun (X : (HomologicalComplex.{v_1, u_2, u_1} V c)ᵒᵖ) ↦
            (Iso.op (Hom.isoOfComponents (fun (x : ι) ↦ Iso.refl ((unop X).op.unopSymm.X x)) ⋯) :
              op (unop X) ≅ op (unop X).op.unopSymm))
          Y))
    (Iso.hom
        ((fun (X : (HomologicalComplex.{v_1, u_2, u_1} V c)ᵒᵖ) ↦
            (Iso.op (Hom.isoOfComponents (fun (x : ι) ↦ Iso.refl ((unop X).op.unopSymm.X x)) ⋯) :
              op (unop X) ≅ op (unop X).op.unopSymm))
          X) ≫
      CategoryTheory.Functor.map (opFunctor V c ⋙ opInverse V c) f)

Tactic:
Quiver.Hom.unop_inj ?_

Premises used: Quiver.Hom.unop_inj
-- 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 Y : (HomologicalComplex.{v_1, u_2, u_1} V c)ᵒᵖ
f : X ⟶ Y
refine :
  Eq (α :=
    unop (Functor.obj (opFunctor V c ⋙ opInverse V c) Y) ⟶
      unop (Functor.obj (𝟭 (HomologicalComplex.{v_1, u_2, u_1} V c)ᵒᵖ) X))
    (Quiver.Hom.unop
      (CategoryTheory.Functor.map (𝟭 (HomologicalComplex.{v_1, u_2, u_1} V c)ᵒᵖ) f ≫
        Iso.hom
          ((fun (X : (HomologicalComplex.{v_1, u_2, u_1} V c)ᵒᵖ) ↦
              (Iso.op (Hom.isoOfComponents (fun (x : ι) ↦ Iso.refl ((unop X).op.unopSymm.X x)) ⋯) :
                op (unop X) ≅ op (unop X).op.unopSymm))
            Y)))
    (Quiver.Hom.unop
      (Iso.hom
          ((fun (X : (HomologicalComplex.{v_1, u_2, u_1} V c)ᵒᵖ) ↦
              (Iso.op (Hom.isoOfComponents (fun (x : ι) ↦ Iso.refl ((unop X).op.unopSymm.X x)) ⋯) :
                op (unop X) ≅ op (unop X).op.unopSymm))
            X) ≫
        CategoryTheory.Functor.map (opFunctor V c ⋙ opInverse V c) f))
⊢ Eq (α := Functor.obj (𝟭 (HomologicalComplex.{v_1, u_2, u_1} V c)ᵒᵖ) X ⟶ Functor.obj (opFunctor V c ⋙ opInverse V c) Y)
    (CategoryTheory.Functor.map (𝟭 (HomologicalComplex.{v_1, u_2, u_1} V c)ᵒᵖ) f ≫
      Iso.hom
        ((fun (X : (HomologicalComplex.{v_1, u_2, u_1} V c)ᵒᵖ) ↦
            (Iso.op (Hom.isoOfComponents (fun (x : ι) ↦ Iso.refl ((unop X).op.unopSymm.X x)) ⋯) :
              op (unop X) ≅ op (unop X).op.unopSymm))
          Y))
    (Iso.hom
        ((fun (X : (HomologicalComplex.{v_1, u_2, u_1} V c)ᵒᵖ) ↦
            (Iso.op (Hom.isoOfComponents (fun (x : ι) ↦ Iso.refl ((unop X).op.unopSymm.X x)) ⋯) :
              op (unop X) ≅ op (unop X).op.unopSymm))
          X) ≫
      CategoryTheory.Functor.map (opFunctor V c ⋙ opInverse V c) f)

Tactic:
refine Quiver.Hom.unop_inj ?_

Premises used: Quiver.Hom.unop_inj
-- 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 Y : (HomologicalComplex.{v_1, u_2, u_1} V c)ᵒᵖ
f : X ⟶ Y
h :
  ∀ (x : ι),
    Eq (α :=
      (unop (Functor.obj (opFunctor V c ⋙ opInverse V c) Y)).X x ⟶
        (unop (Functor.obj (𝟭 (HomologicalComplex.{v_1, u_2, u_1} V c)ᵒᵖ) X)).X x)
      (Hom.f
        (Quiver.Hom.unop
          (CategoryTheory.Functor.map (𝟭 (HomologicalComplex.{v_1, u_2, u_1} V c)ᵒᵖ) f ≫
            Iso.hom
              ((fun (X : (HomologicalComplex.{v_1, u_2, u_1} V c)ᵒᵖ) ↦
                  (Iso.op (Hom.isoOfComponents (fun (x : ι) ↦ Iso.refl ((unop X).op.unopSymm.X x)) ⋯) :
                    op (unop X) ≅ op (unop X).op.unopSymm))
                Y)))
        x)
      (Hom.f
        (Quiver.Hom.unop
          (Iso.hom
              ((fun (X : (HomologicalComplex.{v_1, u_2, u_1} V c)ᵒᵖ) ↦
                  (Iso.op (Hom.isoOfComponents (fun (x : ι) ↦ Iso.refl ((unop X).op.unopSymm.X x)) ⋯) :
                    op (unop X) ≅ op (unop X).op.unopSymm))
                X) ≫
            CategoryTheory.Functor.map (opFunctor V c ⋙ opInverse V c) f))
        x)
⊢ Eq (α :=
    unop (Functor.obj (opFunctor V c ⋙ opInverse V c) Y) ⟶
      unop (Functor.obj (𝟭 (HomologicalComplex.{v_1, u_2, u_1} V c)ᵒᵖ) X))
    (Quiver.Hom.unop
      (CategoryTheory.Functor.map (𝟭 (HomologicalComplex.{v_1, u_2, u_1} V c)ᵒᵖ) f ≫
        Iso.hom
          ((fun (X : (HomologicalComplex.{v_1, u_2, u_1} V c)ᵒᵖ) ↦
              (Iso.op (Hom.isoOfComponents (fun (x : ι) ↦ Iso.refl ((unop X).op.unopSymm.X x)) ⋯) :
                op (unop X) ≅ op (unop X).op.unopSymm))
            Y)))
    (Quiver.Hom.unop
      (Iso.hom
          ((fun (X : (HomologicalComplex.{v_1, u_2, u_1} V c)ᵒᵖ) ↦
              (Iso.op (Hom.isoOfComponents (fun (x : ι) ↦ Iso.refl ((unop X).op.unopSymm.X x)) ⋯) :
                op (unop X) ≅ op (unop X).op.unopSymm))
            X) ≫
        CategoryTheory.Functor.map (opFunctor V c ⋙ opInverse V c) f))

Tactic:
ext x
-- 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 Y : (HomologicalComplex.{v_1, u_2, u_1} V c)ᵒᵖ
f : X ⟶ Y
x : ι
⊢ Eq (α :=
    (unop (Functor.obj (opFunctor V c ⋙ opInverse V c) Y)).X x ⟶
      (unop (Functor.obj (𝟭 (HomologicalComplex.{v_1, u_2, u_1} V c)ᵒᵖ) X)).X x)
    (Hom.f
      (Quiver.Hom.unop
        (CategoryTheory.Functor.map (𝟭 (HomologicalComplex.{v_1, u_2, u_1} V c)ᵒᵖ) f ≫
          Iso.hom
            ((fun (X : (HomologicalComplex.{v_1, u_2, u_1} V c)ᵒᵖ) ↦
                (Iso.op (Hom.isoOfComponents (fun (x : ι) ↦ Iso.refl ((unop X).op.unopSymm.X x)) ⋯) :
                  op (unop X) ≅ op (unop X).op.unopSymm))
              Y)))
      x)
    (Hom.f
      (Quiver.Hom.unop
        (Iso.hom
            ((fun (X : (HomologicalComplex.{v_1, u_2, u_1} V c)ᵒᵖ) ↦
                (Iso.op (Hom.isoOfComponents (fun (x : ι) ↦ Iso.refl ((unop X).op.unopSymm.X x)) ⋯) :
                  op (unop X) ≅ op (unop X).op.unopSymm))
              X) ≫
          CategoryTheory.Functor.map (opFunctor V c ⋙ opInverse V c) f))
      x)

Tactic:
simp
-- 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)ᵒᵖ
h :
  ∀ (i : ι),
    Hom.f
        (CategoryTheory.Functor.map (opFunctor V c) (NatTrans.app (Iso.hom (opUnitIso V c)) X) ≫
          NatTrans.app (Iso.hom (opCounitIso V c)) (Functor.obj (opFunctor V c) X))
        i =
      Hom.f (𝟙 (Functor.obj (opFunctor V c) X)) i
⊢ CategoryTheory.Functor.map (opFunctor V c) (NatTrans.app (Iso.hom (opUnitIso V c)) X) ≫
      NatTrans.app (Iso.hom (opCounitIso V c)) (Functor.obj (opFunctor V c) X) =
    𝟙 (Functor.obj (opFunctor V c) X)

Tactic:
ext
-- 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 : ι
h :
  Quiver.Hom.op
        (Hom.f
          (Quiver.Hom.unop
            (Quiver.Hom.op (Iso.hom (Hom.isoOfComponents (fun (x : ι) ↦ Iso.refl ((unop X).op.unopSymm.X x)) ⋯))))
          i) ≫
      Iso.hom (Iso.refl ((Functor.obj (opInverse V c ⋙ opFunctor V c) (Functor.obj (opFunctor V c) X)).X i)) =
    Hom.f (𝟙 (Functor.obj (opFunctor V c) X)) i
⊢ Hom.f
      (CategoryTheory.Functor.map (opFunctor V c) (NatTrans.app (Iso.hom (opUnitIso V c)) X) ≫
        NatTrans.app (Iso.hom (opCounitIso V c)) (Functor.obj (opFunctor V c) X))
      i =
    Hom.f (𝟙 (Functor.obj (opFunctor V c) X)) i

Tactic:
simp only [opUnitIso, opCounitIso, NatIso.ofComponents_hom_app, Iso.op_hom, comp_f,
      opFunctor_map_f, Hom.isoOfComponents_hom_f]

Premises used: CategoryTheory.Iso.op_hom, HomologicalComplex.opFunctor_map_f, HomologicalComplex.Hom.isoOfComponents_hom_f, HomologicalComplex.opCounitIso, HomologicalComplex.opUnitIso, HomologicalComplex.comp_f, CategoryTheory.NatIso.ofComponents_hom_app
-- 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 : ι
⊢ Quiver.Hom.op
        (Hom.f
          (Quiver.Hom.unop
            (Quiver.Hom.op (Iso.hom (Hom.isoOfComponents (fun (x : ι) ↦ Iso.refl ((unop X).op.unopSymm.X x)) ⋯))))
          i) ≫
      Iso.hom (Iso.refl ((Functor.obj (opInverse V c ⋙ opFunctor V c) (Functor.obj (opFunctor V c) X)).X i)) =
    Hom.f (𝟙 (Functor.obj (opFunctor V c) X)) i

Tactic:
Category.comp_id _

Premises used: Quiver.Hom.op, CategoryTheory.Category.comp_id
-- 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 : ι
⊢ Quiver.Hom.op
        (Hom.f
          (Quiver.Hom.unop
            (Quiver.Hom.op (Iso.hom (Hom.isoOfComponents (fun (x : ι) ↦ Iso.refl ((unop X).op.unopSymm.X x)) ⋯))))
          i) ≫
      Iso.hom (Iso.refl ((Functor.obj (opInverse V c ⋙ opFunctor V c) (Functor.obj (opFunctor V c) X)).X i)) =
    Hom.f (𝟙 (Functor.obj (opFunctor V c) X)) i

Tactic:
exact Category.comp_id _

Premises used: CategoryTheory.Category.comp_id
-- 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
⊢ Functor.IsEquivalence (C := (HomologicalComplex.{v_1, u_2, u_1} V c)ᵒᵖ) (opFunctor V c)

Tactic:
(opEquivalence V c).isEquivalence_functor

Premises used: HomologicalComplex.opEquivalence, HomologicalComplex.opFunctor, CategoryTheory.Equivalence.isEquivalence_functor
-- 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
⊢ Functor.IsEquivalence (C := HomologicalComplex.{v_1, u_2, u_1} Vᵒᵖ c.symm) (opInverse V c)

Tactic:
(opEquivalence V c).isEquivalence_inverse

Premises used: CategoryTheory.Equivalence.isEquivalence_inverse, HomologicalComplex.opInverse, HomologicalComplex.opEquivalence
-- 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 Y : (HomologicalComplex.{v_1, u_2, u_1} Vᵒᵖ c)ᵒᵖ
f : X ⟶ Y
i j : ι
h : c.symm.Rel i j
⊢ (f.unop.f i).unop ≫ (unop Y).unop.d i j = (unop X).unop.d i j ≫ (f.unop.f j).unop

Tactic:
simp only [unop_d, ← unop_comp, f.unop.comm]

Premises used: Quiver.Hom.unop, CategoryTheory.unop_comp, HomologicalComplex.unop_d, HomologicalComplex.Hom.comm
-- 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 Y : HomologicalComplex.{v_1, u_2, u_1} V c.symm
f : X ⟶ Y
i j : ι
h : c.Rel i j
⊢ (f.f i).op ≫ X.opSymm.d i j = Y.opSymm.d i j ≫ (f.f j).op

Tactic:
simp only [opSymm_d, ← op_comp, f.comm]

Premises used: CategoryTheory.op_comp, HomologicalComplex.opSymm_d, HomologicalComplex.Hom.comm
-- 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 : ι
h : c.Rel i j
⊢ Iso.hom
        ((fun (x : ι) ↦ (Iso.refl ((unop X).op.unopSymm.X x) : (unop X).op.unopSymm.X x ≅ (unop X).op.unopSymm.X x))
          i) ≫
      (unop X).d i j =
    (unop X).op.unopSymm.d i j ≫
      Iso.hom
        ((fun (x : ι) ↦ (Iso.refl ((unop X).op.unopSymm.X x) : (unop X).op.unopSymm.X x ≅ (unop X).op.unopSymm.X x)) j)

Tactic:
simp only [Iso.refl_hom, Category.id_comp, unopSymm_d, op_d, Quiver.Hom.unop_op,
              Category.comp_id]

Premises used: HomologicalComplex.op_d, Quiver.Hom.unop_op, CategoryTheory.Category.comp_id, HomologicalComplex.unopSymm_d, CategoryTheory.Iso.refl_hom, CategoryTheory.Category.id_comp
-- 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 Y : (HomologicalComplex.{v_1, u_2, u_1} Vᵒᵖ c)ᵒᵖ
f : X ⟶ Y
⊢ Eq (α :=
    Functor.obj (𝟭 (HomologicalComplex.{v_1, u_2, u_1} Vᵒᵖ c)ᵒᵖ) X ⟶ Functor.obj (unopFunctor V c ⋙ unopInverse V c) Y)
    (CategoryTheory.Functor.map (𝟭 (HomologicalComplex.{v_1, u_2, u_1} Vᵒᵖ c)ᵒᵖ) f ≫
      Iso.hom
        ((fun (X : (HomologicalComplex.{v_1, u_2, u_1} Vᵒᵖ c)ᵒᵖ) ↦
            (Iso.op (Hom.isoOfComponents (fun (x : ι) ↦ Iso.refl ((unop X).op.unopSymm.X x)) ⋯) :
              op (unop X) ≅ op (unop X).op.unopSymm))
          Y))
    (Iso.hom
        ((fun (X : (HomologicalComplex.{v_1, u_2, u_1} Vᵒᵖ c)ᵒᵖ) ↦
            (Iso.op (Hom.isoOfComponents (fun (x : ι) ↦ Iso.refl ((unop X).op.unopSymm.X x)) ⋯) :
              op (unop X) ≅ op (unop X).op.unopSymm))
          X) ≫
      CategoryTheory.Functor.map (unopFunctor V c ⋙ unopInverse V c) f)

Tactic:
Quiver.Hom.unop_inj ?_

Premises used: Quiver.Hom.unop_inj
-- 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 Y : (HomologicalComplex.{v_1, u_2, u_1} Vᵒᵖ c)ᵒᵖ
f : X ⟶ Y
refine :
  Eq (α :=
    unop (Functor.obj (unopFunctor V c ⋙ unopInverse V c) Y) ⟶
      unop (Functor.obj (𝟭 (HomologicalComplex.{v_1, u_2, u_1} Vᵒᵖ c)ᵒᵖ) X))
    (Quiver.Hom.unop
      (CategoryTheory.Functor.map (𝟭 (HomologicalComplex.{v_1, u_2, u_1} Vᵒᵖ c)ᵒᵖ) f ≫
        Iso.hom
          ((fun (X : (HomologicalComplex.{v_1, u_2, u_1} Vᵒᵖ c)ᵒᵖ) ↦
              (Iso.op (Hom.isoOfComponents (fun (x : ι) ↦ Iso.refl ((unop X).op.unopSymm.X x)) ⋯) :
                op (unop X) ≅ op (unop X).op.unopSymm))
            Y)))
    (Quiver.Hom.unop
      (Iso.hom
          ((fun (X : (HomologicalComplex.{v_1, u_2, u_1} Vᵒᵖ c)ᵒᵖ) ↦
              (Iso.op (Hom.isoOfComponents (fun (x : ι) ↦ Iso.refl ((unop X).op.unopSymm.X x)) ⋯) :
                op (unop X) ≅ op (unop X).op.unopSymm))
            X) ≫
        CategoryTheory.Functor.map (unopFunctor V c ⋙ unopInverse V c) f))
⊢ Eq (α :=
    Functor.obj (𝟭 (HomologicalComplex.{v_1, u_2, u_1} Vᵒᵖ c)ᵒᵖ) X ⟶ Functor.obj (unopFunctor V c ⋙ unopInverse V c) Y)
    (CategoryTheory.Functor.map (𝟭 (HomologicalComplex.{v_1, u_2, u_1} Vᵒᵖ c)ᵒᵖ) f ≫
      Iso.hom
        ((fun (X : (HomologicalComplex.{v_1, u_2, u_1} Vᵒᵖ c)ᵒᵖ) ↦
            (Iso.op (Hom.isoOfComponents (fun (x : ι) ↦ Iso.refl ((unop X).op.unopSymm.X x)) ⋯) :
              op (unop X) ≅ op (unop X).op.unopSymm))
          Y))
    (Iso.hom
        ((fun (X : (HomologicalComplex.{v_1, u_2, u_1} Vᵒᵖ c)ᵒᵖ) ↦
            (Iso.op (Hom.isoOfComponents (fun (x : ι) ↦ Iso.refl ((unop X).op.unopSymm.X x)) ⋯) :
              op (unop X) ≅ op (unop X).op.unopSymm))
          X) ≫
      CategoryTheory.Functor.map (unopFunctor V c ⋙ unopInverse V c) f)

Tactic:
refine Quiver.Hom.unop_inj ?_

Premises used: Quiver.Hom.unop_inj
-- 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 Y : (HomologicalComplex.{v_1, u_2, u_1} Vᵒᵖ c)ᵒᵖ
f : X ⟶ Y
h :
  ∀ (x : ι),
    Eq (α :=
      (unop (Functor.obj (unopFunctor V c ⋙ unopInverse V c) Y)).X x ⟶
        (unop (Functor.obj (𝟭 (HomologicalComplex.{v_1, u_2, u_1} Vᵒᵖ c)ᵒᵖ) X)).X x)
      (Hom.f
        (Quiver.Hom.unop
          (CategoryTheory.Functor.map (𝟭 (HomologicalComplex.{v_1, u_2, u_1} Vᵒᵖ c)ᵒᵖ) f ≫
            Iso.hom
              ((fun (X : (HomologicalComplex.{v_1, u_2, u_1} Vᵒᵖ c)ᵒᵖ) ↦
                  (Iso.op (Hom.isoOfComponents (fun (x : ι) ↦ Iso.refl ((unop X).op.unopSymm.X x)) ⋯) :
                    op (unop X) ≅ op (unop X).op.unopSymm))
                Y)))
        x)
      (Hom.f
        (Quiver.Hom.unop
          (Iso.hom
              ((fun (X : (HomologicalComplex.{v_1, u_2, u_1} Vᵒᵖ c)ᵒᵖ) ↦
                  (Iso.op (Hom.isoOfComponents (fun (x : ι) ↦ Iso.refl ((unop X).op.unopSymm.X x)) ⋯) :
                    op (unop X) ≅ op (unop X).op.unopSymm))
                X) ≫
            CategoryTheory.Functor.map (unopFunctor V c ⋙ unopInverse V c) f))
        x)
⊢ Eq (α :=
    unop (Functor.obj (unopFunctor V c ⋙ unopInverse V c) Y) ⟶
      unop (Functor.obj (𝟭 (HomologicalComplex.{v_1, u_2, u_1} Vᵒᵖ c)ᵒᵖ) X))
    (Quiver.Hom.unop
      (CategoryTheory.Functor.map (𝟭 (HomologicalComplex.{v_1, u_2, u_1} Vᵒᵖ c)ᵒᵖ) f ≫
        Iso.hom
          ((fun (X : (HomologicalComplex.{v_1, u_2, u_1} Vᵒᵖ c)ᵒᵖ) ↦
              (Iso.op (Hom.isoOfComponents (fun (x : ι) ↦ Iso.refl ((unop X).op.unopSymm.X x)) ⋯) :
                op (unop X) ≅ op (unop X).op.unopSymm))
            Y)))
    (Quiver.Hom.unop
      (Iso.hom
          ((fun (X : (HomologicalComplex.{v_1, u_2, u_1} Vᵒᵖ c)ᵒᵖ) ↦
              (Iso.op (Hom.isoOfComponents (fun (x : ι) ↦ Iso.refl ((unop X).op.unopSymm.X x)) ⋯) :
                op (unop X) ≅ op (unop X).op.unopSymm))
            X) ≫
        CategoryTheory.Functor.map (unopFunctor V c ⋙ unopInverse V c) f))

Tactic:
ext x
-- 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 Y : (HomologicalComplex.{v_1, u_2, u_1} Vᵒᵖ c)ᵒᵖ
f : X ⟶ Y
x : ι
⊢ Eq (α :=
    (unop (Functor.obj (unopFunctor V c ⋙ unopInverse V c) Y)).X x ⟶
      (unop (Functor.obj (𝟭 (HomologicalComplex.{v_1, u_2, u_1} Vᵒᵖ c)ᵒᵖ) X)).X x)
    (Hom.f
      (Quiver.Hom.unop
        (CategoryTheory.Functor.map (𝟭 (HomologicalComplex.{v_1, u_2, u_1} Vᵒᵖ c)ᵒᵖ) f ≫
          Iso.hom
            ((fun (X : (HomologicalComplex.{v_1, u_2, u_1} Vᵒᵖ c)ᵒᵖ) ↦
                (Iso.op (Hom.isoOfComponents (fun (x : ι) ↦ Iso.refl ((unop X).op.unopSymm.X x)) ⋯) :
                  op (unop X) ≅ op (unop X).op.unopSymm))
              Y)))
      x)
    (Hom.f
      (Quiver.Hom.unop
        (Iso.hom
            ((fun (X : (HomologicalComplex.{v_1, u_2, u_1} Vᵒᵖ c)ᵒᵖ) ↦
                (Iso.op (Hom.isoOfComponents (fun (x : ι) ↦ Iso.refl ((unop X).op.unopSymm.X x)) ⋯) :
                  op (unop X) ≅ op (unop X).op.unopSymm))
              X) ≫
          CategoryTheory.Functor.map (unopFunctor V c ⋙ unopInverse V c) f))
      x)

Tactic:
simp
-- 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)ᵒᵖ
h :
  ∀ (i : ι),
    Hom.f
        (CategoryTheory.Functor.map (unopFunctor V c) (NatTrans.app (Iso.hom (unopUnitIso V c)) X) ≫
          NatTrans.app (Iso.hom (unopCounitIso V c)) (Functor.obj (unopFunctor V c) X))
        i =
      Hom.f (𝟙 (Functor.obj (unopFunctor V c) X)) i
⊢ CategoryTheory.Functor.map (unopFunctor V c) (NatTrans.app (Iso.hom (unopUnitIso V c)) X) ≫
      NatTrans.app (Iso.hom (unopCounitIso V c)) (Functor.obj (unopFunctor V c) X) =
    𝟙 (Functor.obj (unopFunctor V c) X)

Tactic:
ext
-- 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 : ι
h :
  Hom.f (CategoryTheory.Functor.map (unopFunctor V c) (NatTrans.app (Iso.hom (unopUnitIso V c)) X)) i ≫
      (NatTrans.app (Iso.hom (unopCounitIso V c)) (Functor.obj (unopFunctor V c) X)).f i =
    Hom.f (𝟙 (Functor.obj (unopFunctor V c) X)) i
⊢ Hom.f
      (CategoryTheory.Functor.map (unopFunctor V c) (NatTrans.app (Iso.hom (unopUnitIso V c)) X) ≫
        NatTrans.app (Iso.hom (unopCounitIso V c)) (Functor.obj (unopFunctor V c) X))
      i =
    Hom.f (𝟙 (Functor.obj (unopFunctor V c) X)) i

Tactic:
simp only [comp_f]

Premises used: HomologicalComplex.comp_f