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 : ι
⊢ 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

Tactic:
Category.comp_id _

Premises used: Quiver.Hom.unop, 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 : ι
⊢ 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

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)ᵒᵖ) (unopFunctor V c)

Tactic:
(unopEquivalence V c).isEquivalence_functor

Premises used: HomologicalComplex.unopEquivalence, CategoryTheory.Equivalence.isEquivalence_functor, HomologicalComplex.unopFunctor
-- 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) (unopInverse V c)

Tactic:
(unopEquivalence V c).isEquivalence_inverse

Premises used: CategoryTheory.Equivalence.isEquivalence_inverse, HomologicalComplex.unopInverse, HomologicalComplex.unopEquivalence
-- 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
K : HomologicalComplex.{v_1, u_2, u_1} V c
i : ι
inst_2 : K.HasHomology i
⊢ K.op.HasHomology i

Tactic:
inferInstanceAs <| (K.sc i).op.HasHomology

Premises used: _private.0.HomologicalComplex.instHasHomologyOppositeOp._proof_1
-- 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
K : HomologicalComplex.{v_1, u_2, u_1} Vᵒᵖ c
i : ι
inst_2 : K.HasHomology i
⊢ K.unop.HasHomology i

Tactic:
inferInstanceAs <| (K.sc i).unop.HasHomology

Premises used: _private.0.HomologicalComplex.instHasHomologyUnopOfOpposite._proof_1
-- 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
K : HomologicalComplex.{v_1, u_2, u_1} V c
i : ι
inst_2 : K.HasHomology i
dsimp : K.op.HasHomology i
⊢ (Functor.obj (opFunctor V c) (op K)).HasHomology i

Tactic:
dsimp
-- 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
K : HomologicalComplex.{v_1, u_2, u_1} V c
i : ι
inst_2 : K.HasHomology i
⊢ K.op.HasHomology i

Tactic:
infer_instance
-- 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
K : HomologicalComplex.{v_1, u_2, u_1} Vᵒᵖ c
i : ι
inst_2 : K.HasHomology i
dsimp : K.unop.HasHomology i
⊢ (Functor.obj (unopFunctor V c) (op K)).HasHomology i

Tactic:
dsimp
-- 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
K : HomologicalComplex.{v_1, u_2, u_1} Vᵒᵖ c
i : ι
inst_2 : K.HasHomology i
⊢ K.unop.HasHomology i

Tactic:
infer_instance
-- 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
K L : HomologicalComplex.{v_1, u_2, u_1} V c
φ : K ⟶ L
i : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
simp :
  ShortComplex.QuasiIso (S₁ := Functor.obj (shortComplexFunctor Vᵒᵖ c.symm i) (Functor.obj (opFunctor V c) (op L)))
      (CategoryTheory.Functor.map (shortComplexFunctor Vᵒᵖ c.symm i)
        (CategoryTheory.Functor.map (opFunctor V c) φ.op)) ↔
    ShortComplex.QuasiIso (S₁ := Functor.obj (shortComplexFunctor V c i) K)
      (CategoryTheory.Functor.map (shortComplexFunctor V c i) φ)
⊢ QuasiIsoAt (K := Functor.obj (opFunctor V c) (op L)) (CategoryTheory.Functor.map (opFunctor V c) φ.op) i ↔
    QuasiIsoAt φ i

Tactic:
simp only [quasiIsoAt_iff]

Premises used: quasiIsoAt_iff
-- 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
K L : HomologicalComplex.{v_1, u_2, u_1} V c
φ : K ⟶ L
i : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
⊢ ShortComplex.QuasiIso (S₁ := Functor.obj (shortComplexFunctor Vᵒᵖ c.symm i) (Functor.obj (opFunctor V c) (op L)))
      (CategoryTheory.Functor.map (shortComplexFunctor Vᵒᵖ c.symm i)
        (CategoryTheory.Functor.map (opFunctor V c) φ.op)) ↔
    ShortComplex.QuasiIso (S₁ := Functor.obj (shortComplexFunctor V c i) K)
      (CategoryTheory.Functor.map (shortComplexFunctor V c i) φ)

Tactic:
ShortComplex.quasiIso_opMap_iff ((shortComplexFunctor V c i).map φ)

Premises used: Quiver.Hom.op, ComplexShape.prev, HomologicalComplex.shortComplexFunctor, CategoryTheory.Functor.map, CategoryTheory.ShortComplex.op, CategoryTheory.ShortComplex.opMap, ComplexShape.next, CategoryTheory.ShortComplex.quasiIso_opMap_iff
-- 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
K L : HomologicalComplex.{v_1, u_2, u_1} V c
φ : K ⟶ L
i : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
⊢ ShortComplex.QuasiIso (S₁ := Functor.obj (shortComplexFunctor Vᵒᵖ c.symm i) (Functor.obj (opFunctor V c) (op L)))
      (CategoryTheory.Functor.map (shortComplexFunctor Vᵒᵖ c.symm i)
        (CategoryTheory.Functor.map (opFunctor V c) φ.op)) ↔
    ShortComplex.QuasiIso (S₁ := Functor.obj (shortComplexFunctor V c i) K)
      (CategoryTheory.Functor.map (shortComplexFunctor V c i) φ)

Tactic:
exact ShortComplex.quasiIso_opMap_iff ((shortComplexFunctor V c i).map φ)

Premises used: HomologicalComplex.shortComplexFunctor, CategoryTheory.Functor.map, CategoryTheory.ShortComplex.quasiIso_opMap_iff
-- 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
K L : HomologicalComplex.{v_1, u_2, u_1} Vᵒᵖ c
φ : K ⟶ L
i : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
rw :
  QuasiIsoAt (K := Functor.obj (opFunctor V c.symm) (op (Functor.obj (unopFunctor V c) (op K))))
      (CategoryTheory.Functor.map (opFunctor V c.symm)
        (Quiver.Hom.op (CategoryTheory.Functor.map (unopFunctor V c) φ.op)))
      i ↔
    QuasiIsoAt φ i
⊢ QuasiIsoAt (K := Functor.obj (unopFunctor V c) (op L)) (CategoryTheory.Functor.map (unopFunctor V c) φ.op) i ↔
    QuasiIsoAt φ i

Tactic:
rw [← quasiIsoAt_opFunctor_map_iff]

Premises used: HomologicalComplex.quasiIsoAt_opFunctor_map_iff
-- 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
K L : HomologicalComplex.{v_1, u_2, u_1} Vᵒᵖ c
φ : K ⟶ L
i : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
⊢ QuasiIsoAt (K := Functor.obj (opFunctor V c.symm) (op (Functor.obj (unopFunctor V c) (op K))))
      (CategoryTheory.Functor.map (opFunctor V c.symm)
        (Quiver.Hom.op (CategoryTheory.Functor.map (unopFunctor V c) φ.op)))
      i ↔
    QuasiIsoAt φ i

Tactic:
rfl
-- 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
K L : HomologicalComplex.{v_1, u_2, u_1} V c
φ : K ⟶ L
i : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
inst_4 rw : QuasiIsoAt φ i
⊢ QuasiIsoAt (K := Functor.obj (opFunctor V c) (op L)) (CategoryTheory.Functor.map (opFunctor V c) φ.op) i

Tactic:
rw [quasiIsoAt_opFunctor_map_iff]

Premises used: HomologicalComplex.quasiIsoAt_opFunctor_map_iff
-- 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
K L : HomologicalComplex.{v_1, u_2, u_1} V c
φ : K ⟶ L
i : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
inst_4 : QuasiIsoAt φ i
⊢ QuasiIsoAt φ i

Tactic:
infer_instance
-- 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
K L : HomologicalComplex.{v_1, u_2, u_1} Vᵒᵖ c
φ : K ⟶ L
i : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
inst_4 rw : QuasiIsoAt φ i
⊢ QuasiIsoAt (K := Functor.obj (unopFunctor V c) (op L)) (CategoryTheory.Functor.map (unopFunctor V c) φ.op) i

Tactic:
rw [quasiIsoAt_unopFunctor_map_iff]

Premises used: HomologicalComplex.quasiIsoAt_unopFunctor_map_iff
-- 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
K L : HomologicalComplex.{v_1, u_2, u_1} Vᵒᵖ c
φ : K ⟶ L
i : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
inst_4 : QuasiIsoAt φ i
⊢ QuasiIsoAt φ i

Tactic:
infer_instance
-- 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
K L : HomologicalComplex.{v_1, u_2, u_1} V c
φ : K ⟶ L
inst_2 : ∀ (i : ι), K.HasHomology i
inst_3 : ∀ (i : ι), L.HasHomology i
⊢ QuasiIso (K := Functor.obj (opFunctor V c) (op L)) (CategoryTheory.Functor.map (opFunctor V c) φ.op) ↔ QuasiIso φ

Tactic:
simp only [quasiIso_iff, quasiIsoAt_opFunctor_map_iff]

Premises used: quasiIso_iff, HomologicalComplex.quasiIsoAt_opFunctor_map_iff
-- 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
K L : HomologicalComplex.{v_1, u_2, u_1} Vᵒᵖ c
φ : K ⟶ L
inst_2 : ∀ (i : ι), K.HasHomology i
inst_3 : ∀ (i : ι), L.HasHomology i
⊢ QuasiIso (K := Functor.obj (unopFunctor V c) (op L)) (CategoryTheory.Functor.map (unopFunctor V c) φ.op) ↔ QuasiIso φ

Tactic:
simp only [quasiIso_iff, quasiIsoAt_unopFunctor_map_iff]

Premises used: HomologicalComplex.quasiIsoAt_unopFunctor_map_iff, quasiIso_iff
-- 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
K L : HomologicalComplex.{v_1, u_2, u_1} V c
φ : K ⟶ L
inst_2 : ∀ (i : ι), K.HasHomology i
inst_3 : ∀ (i : ι), L.HasHomology i
inst_4 rw : QuasiIso φ
⊢ QuasiIso (K := Functor.obj (opFunctor V c) (op L)) (CategoryTheory.Functor.map (opFunctor V c) φ.op)

Tactic:
rw [quasiIso_opFunctor_map_iff]

Premises used: HomologicalComplex.quasiIso_opFunctor_map_iff
-- 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
K L : HomologicalComplex.{v_1, u_2, u_1} V c
φ : K ⟶ L
inst_2 : ∀ (i : ι), K.HasHomology i
inst_3 : ∀ (i : ι), L.HasHomology i
inst_4 : QuasiIso φ
⊢ QuasiIso φ

Tactic:
infer_instance
-- 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
K L : HomologicalComplex.{v_1, u_2, u_1} Vᵒᵖ c
φ : K ⟶ L
inst_2 : ∀ (i : ι), K.HasHomology i
inst_3 : ∀ (i : ι), L.HasHomology i
inst_4 rw : QuasiIso φ
⊢ QuasiIso (K := Functor.obj (unopFunctor V c) (op L)) (CategoryTheory.Functor.map (unopFunctor V c) φ.op)

Tactic:
rw [quasiIso_unopFunctor_map_iff]

Premises used: HomologicalComplex.quasiIso_unopFunctor_map_iff
-- 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
K L : HomologicalComplex.{v_1, u_2, u_1} Vᵒᵖ c
φ : K ⟶ L
inst_2 : ∀ (i : ι), K.HasHomology i
inst_3 : ∀ (i : ι), L.HasHomology i
inst_4 : QuasiIso φ
⊢ QuasiIso φ

Tactic:
infer_instance
-- 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
K : HomologicalComplex.{v_1, u_2, u_1} V c
i : ι
h : K.ExactAt i
⊢ K.op.ExactAt i

Tactic:
ShortComplex.Exact.op h

Premises used: HomologicalComplex.ExactAt, Quiver.Hom.op, ComplexShape.prev, CategoryTheory.ShortComplex.op, ComplexShape.next, CategoryTheory.ShortComplex.Exact.op
-- 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
K : HomologicalComplex.{v_1, u_2, u_1} Vᵒᵖ c
i : ι
h : K.ExactAt i
⊢ K.unop.ExactAt i

Tactic:
ShortComplex.Exact.unop h

Premises used: HomologicalComplex.ExactAt, Quiver.Hom.unop, ComplexShape.prev, CategoryTheory.ShortComplex.Exact.unop, ComplexShape.next, CategoryTheory.ShortComplex.unop
-- 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
K : HomologicalComplex.{v_1, u_2, u_1} V c
i : ι
⊢ K.op.ExactAt i ↔ K.ExactAt i

Tactic:
⟨fun h ↦ h.unop, fun h ↦ h.op⟩

Premises used: Iff.intro, HomologicalComplex.ExactAt.op, HomologicalComplex.ExactAt.unop
-- 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
K : HomologicalComplex.{v_1, u_2, u_1} V c
h : K.Acyclic
⊢ K.op.Acyclic

Tactic:
fun i ↦ (h i).op

Premises used: HomologicalComplex.Acyclic, HomologicalComplex.ExactAt.op
-- 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
K : HomologicalComplex.{v_1, u_2, u_1} Vᵒᵖ c
h : K.Acyclic
⊢ K.unop.Acyclic

Tactic:
fun i ↦ (h i).unop

Premises used: HomologicalComplex.Acyclic, HomologicalComplex.ExactAt.unop
-- 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
K : HomologicalComplex.{v_1, u_2, u_1} V c
⊢ K.op.Acyclic ↔ K.Acyclic

Tactic:
⟨fun h ↦ h.unop, fun h ↦ h.op⟩

Premises used: HomologicalComplex.Acyclic.op, Iff.intro, HomologicalComplex.Acyclic.unop
-- 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
K : HomologicalComplex.{v_1, u_2, u_1} V c
i : ι
inst_2 : K.HasHomology i
j : ι
pos :
  ∀ (hij : c.Rel j i),
    Eq (α := K.op.opcycles i ⟶ op (K.X j))
      (CategoryStruct.comp (Y := op (K.cycles i)) (Iso.hom (K.opcyclesOpIso i)) (Quiver.Hom.op (K.toCycles j i)) :
        K.op.opcycles i ⟶ op (K.X j))
      (K.op.fromOpcycles i j : K.op.opcycles i ⟶ K.op.X j)
neg :
  ∀ (hij : ¬c.Rel j i),
    Eq (α := K.op.opcycles i ⟶ op (K.X j))
      (CategoryStruct.comp (Y := op (K.cycles i)) (Iso.hom (K.opcyclesOpIso i)) (Quiver.Hom.op (K.toCycles j i)) :
        K.op.opcycles i ⟶ op (K.X j))
      (K.op.fromOpcycles i j : K.op.opcycles i ⟶ K.op.X j)
⊢ Eq (α := K.op.opcycles i ⟶ op (K.X j))
    (CategoryStruct.comp (Y := op (K.cycles i)) (Iso.hom (K.opcyclesOpIso i)) (Quiver.Hom.op (K.toCycles j i)) :
      K.op.opcycles i ⟶ op (K.X j))
    (K.op.fromOpcycles i j : K.op.opcycles i ⟶ K.op.X j)

Tactic:
by_cases hij : c.Rel j i

Premises used: ComplexShape.Rel
-- 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
K : HomologicalComplex.{v_1, u_2, u_1} V c
i : ι
inst_2 : K.HasHomology i
j : ι
hij : c.Rel j i
pos :
  ∀ (hij : c.Rel (c.prev i) i),
    Eq (α := K.op.opcycles i ⟶ op (K.X (c.prev i)))
      (CategoryStruct.comp (Y := op (K.cycles i)) (Iso.hom (K.opcyclesOpIso i))
          (Quiver.Hom.op (K.toCycles (c.prev i) i)) :
        K.op.opcycles i ⟶ op (K.X (c.prev i)))
      (K.op.fromOpcycles i (c.prev i) : K.op.opcycles i ⟶ K.op.X (c.prev i))
⊢ Eq (α := K.op.opcycles i ⟶ op (K.X j))
    (CategoryStruct.comp (Y := op (K.cycles i)) (Iso.hom (K.opcyclesOpIso i)) (Quiver.Hom.op (K.toCycles j i)) :
      K.op.opcycles i ⟶ op (K.X j))
    (K.op.fromOpcycles i j : K.op.opcycles i ⟶ K.op.X j)

Tactic:
obtain rfl := c.prev_eq' hij

Premises used: ComplexShape.prev_eq', rfl
-- 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
K : HomologicalComplex.{v_1, u_2, u_1} V c
i : ι
inst_2 : K.HasHomology i
hij : c.Rel (c.prev i) i
⊢ Eq (α := K.op.opcycles i ⟶ op (K.X (c.prev i)))
    (CategoryStruct.comp (Y := op (K.cycles i)) (Iso.hom (K.opcyclesOpIso i))
        (Quiver.Hom.op (K.toCycles (c.prev i) i)) :
      K.op.opcycles i ⟶ op (K.X (c.prev i)))
    (K.op.fromOpcycles i (c.prev i) : K.op.opcycles i ⟶ K.op.X (c.prev i))

Tactic:
(K.sc i).opcyclesOpIso_hom_toCycles_op

Premises used: Quiver.Hom.op, HomologicalComplex.opcycles, ComplexShape.prev, CategoryTheory.ShortComplex.descOpcycles, HomologicalComplex.sc, HomologicalComplex.fromOpcycles, CategoryTheory.ShortComplex.op, ComplexShape.next, CategoryTheory.ShortComplex.liftCycles, HomologicalComplex.liftCycles, HomologicalComplex.descOpcycles, CategoryTheory.ShortComplex.opcyclesOpIso_hom_toCycles_op, HomologicalComplex.cycles, HomologicalComplex.toCycles
-- 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
K : HomologicalComplex.{v_1, u_2, u_1} V c
i : ι
inst_2 : K.HasHomology i
hij : c.Rel (c.prev i) i
⊢ Eq (α := K.op.opcycles i ⟶ op (K.X (c.prev i)))
    (CategoryStruct.comp (Y := op (K.cycles i)) (Iso.hom (K.opcyclesOpIso i))
        (Quiver.Hom.op (K.toCycles (c.prev i) i)) :
      K.op.opcycles i ⟶ op (K.X (c.prev i)))
    (K.op.fromOpcycles i (c.prev i) : K.op.opcycles i ⟶ K.op.X (c.prev i))

Tactic:
exact (K.sc i).opcyclesOpIso_hom_toCycles_op

Premises used: HomologicalComplex.sc, CategoryTheory.ShortComplex.opcyclesOpIso_hom_toCycles_op
-- 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
K : HomologicalComplex.{v_1, u_2, u_1} V c
i : ι
inst_2 : K.HasHomology i
j : ι
hij : ¬c.Rel j i
neg :
  Eq (α := K.op.opcycles i ⟶ op (K.X j))
    (CategoryStruct.comp (Y := op (K.cycles i)) (Iso.hom (K.opcyclesOpIso i)) (Quiver.Hom.op 0) :
      K.op.opcycles i ⟶ op (K.X j))
    (K.op.fromOpcycles i j : K.op.opcycles i ⟶ K.op.X j)
neg₁ :
  Eq (α := K.op.opcycles i ⟶ op (K.X j))
    (CategoryStruct.comp (Y := op (K.cycles i)) (Iso.hom (K.opcyclesOpIso i)) (Quiver.Hom.op 0) :
      K.op.opcycles i ⟶ op (K.X j))
    (0 : K.op.opcycles i ⟶ K.op.X j)
neg₂ :
  Eq (α := K.op.opcycles i ⟶ op (K.X j))
    (CategoryStruct.comp (Y := op (K.cycles i)) (Iso.hom (K.opcyclesOpIso i)) 0 : K.op.opcycles i ⟶ op (K.X j))
    (0 : K.op.opcycles i ⟶ K.op.X j)
neg₃ neg₄ : Eq.{v_1 + 1} (α := K.op.opcycles i ⟶ op (K.X j)) 0 0
⊢ Eq (α := K.op.opcycles i ⟶ op (K.X j))
    (CategoryStruct.comp (Y := op (K.cycles i)) (Iso.hom (K.opcyclesOpIso i)) (Quiver.Hom.op (K.toCycles j i)) :
      K.op.opcycles i ⟶ op (K.X j))
    (K.op.fromOpcycles i j : K.op.opcycles i ⟶ K.op.X j)

Tactic:
rw [K.toCycles_eq_zero hij, K.op.fromOpcycles_eq_zero hij, op_zero, comp_zero]

Premises used: HomologicalComplex.op, HomologicalComplex.fromOpcycles_eq_zero, CategoryTheory.Limits.comp_zero, HomologicalComplex.toCycles_eq_zero, 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
K : HomologicalComplex.{v_1, u_2, u_1} V c
i : ι
inst_2 : K.HasHomology i
j : ι
pos :
  ∀ (hij : c.Rel i j),
    Eq (α := op (K.X j) ⟶ K.op.cycles i)
      (CategoryStruct.comp (Y := op (K.opcycles i)) (Quiver.Hom.op (K.fromOpcycles i j)) (Iso.inv (K.cyclesOpIso i)) :
        op (K.X j) ⟶ K.op.cycles i)
      (K.op.toCycles j i : K.op.X j ⟶ K.op.cycles i)
neg :
  ∀ (hij : ¬c.Rel i j),
    Eq (α := op (K.X j) ⟶ K.op.cycles i)
      (CategoryStruct.comp (Y := op (K.opcycles i)) (Quiver.Hom.op (K.fromOpcycles i j)) (Iso.inv (K.cyclesOpIso i)) :
        op (K.X j) ⟶ K.op.cycles i)
      (K.op.toCycles j i : K.op.X j ⟶ K.op.cycles i)
⊢ Eq (α := op (K.X j) ⟶ K.op.cycles i)
    (CategoryStruct.comp (Y := op (K.opcycles i)) (Quiver.Hom.op (K.fromOpcycles i j)) (Iso.inv (K.cyclesOpIso i)) :
      op (K.X j) ⟶ K.op.cycles i)
    (K.op.toCycles j i : K.op.X j ⟶ K.op.cycles i)

Tactic:
by_cases hij : c.Rel i j

Premises used: ComplexShape.Rel
-- 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
K : HomologicalComplex.{v_1, u_2, u_1} V c
i : ι
inst_2 : K.HasHomology i
j : ι
hij : c.Rel i j
pos :
  ∀ (hij : c.Rel i (c.next i)),
    Eq (α := op (K.X (c.next i)) ⟶ K.op.cycles i)
      (CategoryStruct.comp (Y := op (K.opcycles i)) (Quiver.Hom.op (K.fromOpcycles i (c.next i)))
          (Iso.inv (K.cyclesOpIso i)) :
        op (K.X (c.next i)) ⟶ K.op.cycles i)
      (K.op.toCycles (c.next i) i : K.op.X (c.next i) ⟶ K.op.cycles i)
⊢ Eq (α := op (K.X j) ⟶ K.op.cycles i)
    (CategoryStruct.comp (Y := op (K.opcycles i)) (Quiver.Hom.op (K.fromOpcycles i j)) (Iso.inv (K.cyclesOpIso i)) :
      op (K.X j) ⟶ K.op.cycles i)
    (K.op.toCycles j i : K.op.X j ⟶ K.op.cycles i)

Tactic:
obtain rfl := c.next_eq' hij

Premises used: rfl, ComplexShape.next_eq'
-- 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
K : HomologicalComplex.{v_1, u_2, u_1} V c
i : ι
inst_2 : K.HasHomology i
hij : c.Rel i (c.next i)
⊢ Eq (α := op (K.X (c.next i)) ⟶ K.op.cycles i)
    (CategoryStruct.comp (Y := op (K.opcycles i)) (Quiver.Hom.op (K.fromOpcycles i (c.next i)))
        (Iso.inv (K.cyclesOpIso i)) :
      op (K.X (c.next i)) ⟶ K.op.cycles i)
    (K.op.toCycles (c.next i) i : K.op.X (c.next i) ⟶ K.op.cycles i)

Tactic:
(K.sc i).fromOpcycles_op_cyclesOpIso_inv

Premises used: Quiver.Hom.op, HomologicalComplex.opcycles, ComplexShape.prev, CategoryTheory.ShortComplex.descOpcycles, HomologicalComplex.sc, HomologicalComplex.fromOpcycles, CategoryTheory.ShortComplex.op, ComplexShape.next, CategoryTheory.ShortComplex.liftCycles, HomologicalComplex.liftCycles, HomologicalComplex.descOpcycles, CategoryTheory.ShortComplex.fromOpcycles_op_cyclesOpIso_inv, HomologicalComplex.cycles, HomologicalComplex.toCycles
-- 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
K : HomologicalComplex.{v_1, u_2, u_1} V c
i : ι
inst_2 : K.HasHomology i
hij : c.Rel i (c.next i)
⊢ Eq (α := op (K.X (c.next i)) ⟶ K.op.cycles i)
    (CategoryStruct.comp (Y := op (K.opcycles i)) (Quiver.Hom.op (K.fromOpcycles i (c.next i)))
        (Iso.inv (K.cyclesOpIso i)) :
      op (K.X (c.next i)) ⟶ K.op.cycles i)
    (K.op.toCycles (c.next i) i : K.op.X (c.next i) ⟶ K.op.cycles i)

Tactic:
exact (K.sc i).fromOpcycles_op_cyclesOpIso_inv

Premises used: HomologicalComplex.sc, CategoryTheory.ShortComplex.fromOpcycles_op_cyclesOpIso_inv