awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.Opposite (goal)
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 (α :=
    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))
have 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)) sorry) :
                  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)) sorry) :
                  op (unop X) ≅ op (unop X).op.unopSymm))
              X) ≫
          CategoryTheory.Functor.map (opFunctor V c ⋙ opInverse V c) f))
      x)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Homology.Opposite (goal)
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)ᵒᵖ
⊢ 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)
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Homology.Opposite (goal)
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 (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
have 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)) sorry))))
        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: simp only [opUnitIso, opCounitIso, NatIso.ofComponents_hom_app, Iso.op_hom, comp_f,
      opFunctor_map_f, Hom.isoOfComponents_hom_f]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Opposite (goal)
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)
have 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)) sorry) :
              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)) sorry) :
              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 ?_
-- Lean 4 proof step from Mathlib.Algebra.Homology.Opposite (goal)
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 (α :=
    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))
have 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)) sorry) :
                  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)) sorry) :
                  op (unop X) ≅ op (unop X).op.unopSymm))
              X) ≫
          CategoryTheory.Functor.map (unopFunctor V c ⋙ unopInverse V c) f))
      x)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Homology.Opposite (goal)
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)ᵒᵖ
⊢ 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)
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Homology.Opposite (goal)
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) ≫
        NatTrans.app (Iso.hom (unopCounitIso V c)) (Functor.obj (unopFunctor V c) X))
      i =
    Hom.f (𝟙 (Functor.obj (unopFunctor V c) X)) i
have 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
Tactic: simp only [comp_f]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Opposite (goal)
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
⊢ (Functor.obj (opFunctor V c) (op K)).HasHomology i
have dsimp : K.op.HasHomology i
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.Opposite (goal)
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
⊢ (Functor.obj (unopFunctor V c) (op K)).HasHomology i
have dsimp : K.unop.HasHomology i
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.Opposite (goal)
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) (op L)) (CategoryTheory.Functor.map (opFunctor V c) φ.op) i ↔
    QuasiIsoAt φ i
have 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) φ)
Tactic: simp only [quasiIsoAt_iff]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Opposite (goal)
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 (unopFunctor V c) (op L)) (CategoryTheory.Functor.map (unopFunctor V c) φ.op) i ↔
    QuasiIsoAt φ i
have 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
Tactic: rw [← quasiIsoAt_opFunctor_map_iff]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Opposite (goal)
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 : ι
⊢ 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)
have 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)
Tactic: by_cases hij : c.Rel j i
-- Lean 4 proof step from Mathlib.Algebra.Homology.Opposite (goal)
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)
⊢ 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)
have 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)
Tactic: by_cases hij : c.Rel j i
-- Lean 4 proof step from Mathlib.Algebra.Homology.Opposite (goal)
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
⊢ 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)
have 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))
Tactic: obtain rfl := c.prev_eq' hij
Cleared hypotheses: j, hij
-- Lean 4 proof step from Mathlib.Algebra.Homology.Opposite (goal)
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
⊢ 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)
have 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)
Tactic: rw [K.toCycles_eq_zero hij, K.op.fromOpcycles_eq_zero hij, op_zero, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Opposite (goal)
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)
⊢ 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)
have 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)
Tactic: rw [K.toCycles_eq_zero hij, K.op.fromOpcycles_eq_zero hij, op_zero, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Opposite (goal)
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)
⊢ 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)
have 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)
Tactic: rw [K.toCycles_eq_zero hij, K.op.fromOpcycles_eq_zero hij, op_zero, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Opposite (goal)
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)
⊢ 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)
have neg₃ : Eq.{v_1 + 1} (α := K.op.opcycles i ⟶ op (K.X j)) 0 0
Tactic: rw [K.toCycles_eq_zero hij, K.op.fromOpcycles_eq_zero hij, op_zero, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Opposite (goal)
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 : ι
⊢ 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)
have 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)
Tactic: by_cases hij : c.Rel i j
-- Lean 4 proof step from Mathlib.Algebra.Homology.Opposite (goal)
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)
⊢ 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)
have 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)
Tactic: by_cases hij : c.Rel i j
-- Lean 4 proof step from Mathlib.Algebra.Homology.Opposite (goal)
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
⊢ 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)
have 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)
Tactic: obtain rfl := c.next_eq' hij
Cleared hypotheses: j, hij
-- Lean 4 proof step from Mathlib.Algebra.Homology.Opposite (goal)
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
⊢ 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)
have neg : 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)
  (0 : K.op.X j ⟶ K.op.cycles i)
Tactic: rw [K.op.toCycles_eq_zero hij, K.fromOpcycles_eq_zero hij, op_zero, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Opposite (goal)
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
neg :
  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)
    (0 : 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)
have neg₁ : Eq (α := op (K.X j) ⟶ K.op.cycles i)
  (CategoryStruct.comp (Y := op (K.opcycles i)) (Quiver.Hom.op 0) (Iso.inv (K.cyclesOpIso i)) :
    op (K.X j) ⟶ K.op.cycles i)
  (0 : K.op.X j ⟶ K.op.cycles i)
Tactic: rw [K.op.toCycles_eq_zero hij, K.fromOpcycles_eq_zero hij, op_zero, zero_comp]