awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.Additive
Goal:
ι : Type u_1
W₁ : Type u_3
W₂ : Type u_4
inst : Category.{v_2, u_3} W₁
inst_1 : Category.{v_3, u_4} W₂
inst_2 : HasZeroMorphisms.{v_2, u_3} W₁
inst_3 : HasZeroMorphisms.{v_3, u_4} W₂
inst_4 : HasZeroObject.{v_2, u_3} W₁
inst_5 : HasZeroObject.{v_3, u_4} W₂
F : CategoryTheory.Functor.{v_2, v_3, u_3, u_4} W₁ W₂
inst_6 : F.PreservesZeroMorphisms
c : ComplexShape ι
inst_7 : DecidableEq ι
j : ι
X : W₁
⊢ Eq (α :=
    HomologicalComplex.X
        (Functor.obj
          (Functor.comp (D := HomologicalComplex.{v_2, u_3, u_1} W₁ c) (single W₁ c j) (F.mapHomologicalComplex c)) X)
        j ⟶
      HomologicalComplex.X (Functor.obj (F ⋙ single W₂ c j) X) j)
    (Hom.f (NatTrans.app (Iso.hom (singleMapHomologicalComplex F c j)) X) j)
    (F.map (Iso.hom (singleObjXSelf c j X)) ≫ Iso.inv (singleObjXSelf c j (F.obj X)))

Tactic:
simp [singleMapHomologicalComplex, singleObjXSelf, singleObjXIsoOfEq, eqToHom_map]

Premises used: CategoryTheory.eqToHom_map, HomologicalComplex.singleMapHomologicalComplex, HomologicalComplex.singleObjXIsoOfEq, HomologicalComplex.singleObjXSelf
-- Module: Mathlib.Algebra.Homology.Additive
Goal:
ι : Type u_1
W₁ : Type u_3
W₂ : Type u_4
inst : Category.{v_2, u_3} W₁
inst_1 : Category.{v_3, u_4} W₂
inst_2 : HasZeroMorphisms.{v_2, u_3} W₁
inst_3 : HasZeroMorphisms.{v_3, u_4} W₂
inst_4 : HasZeroObject.{v_2, u_3} W₁
inst_5 : HasZeroObject.{v_3, u_4} W₂
F : CategoryTheory.Functor.{v_2, v_3, u_3, u_4} W₁ W₂
inst_6 : F.PreservesZeroMorphisms
c : ComplexShape ι
inst_7 : DecidableEq ι
i j : ι
h : i ≠ j
X : W₁
⊢ Eq (α :=
    HomologicalComplex.X
        (Functor.obj
          (Functor.comp (D := HomologicalComplex.{v_2, u_3, u_1} W₁ c) (single W₁ c j) (F.mapHomologicalComplex c)) X)
        i ⟶
      HomologicalComplex.X (Functor.obj (F ⋙ single W₂ c j) X) i)
    (Hom.f (NatTrans.app (Iso.hom (singleMapHomologicalComplex F c j)) X) i) 0

Tactic:
simp [singleMapHomologicalComplex, h]

Premises used: HomologicalComplex.singleMapHomologicalComplex
-- Module: Mathlib.Algebra.Homology.Additive
Goal:
ι : Type u_1
W₁ : Type u_3
W₂ : Type u_4
inst : Category.{v_2, u_3} W₁
inst_1 : Category.{v_3, u_4} W₂
inst_2 : HasZeroMorphisms.{v_2, u_3} W₁
inst_3 : HasZeroMorphisms.{v_3, u_4} W₂
inst_4 : HasZeroObject.{v_2, u_3} W₁
inst_5 : HasZeroObject.{v_3, u_4} W₂
F : CategoryTheory.Functor.{v_2, v_3, u_3, u_4} W₁ W₂
inst_6 : F.PreservesZeroMorphisms
c : ComplexShape ι
inst_7 : DecidableEq ι
j : ι
X : W₁
⊢ Eq (α :=
    HomologicalComplex.X (Functor.obj (F ⋙ single W₂ c j) X) j ⟶
      HomologicalComplex.X
        (Functor.obj
          (Functor.comp (D := HomologicalComplex.{v_2, u_3, u_1} W₁ c) (single W₁ c j) (F.mapHomologicalComplex c)) X)
        j)
    (Hom.f (NatTrans.app (Iso.inv (singleMapHomologicalComplex F c j)) X) j)
    (Iso.hom (singleObjXSelf c j (F.obj X)) ≫ F.map (Iso.inv (singleObjXSelf c j X)))

Tactic:
simp [singleMapHomologicalComplex, singleObjXSelf, singleObjXIsoOfEq, eqToHom_map]

Premises used: CategoryTheory.eqToHom_map, HomologicalComplex.singleMapHomologicalComplex, HomologicalComplex.singleObjXIsoOfEq, HomologicalComplex.singleObjXSelf
-- Module: Mathlib.Algebra.Homology.Additive
Goal:
ι : Type u_1
W₁ : Type u_3
W₂ : Type u_4
inst : Category.{v_2, u_3} W₁
inst_1 : Category.{v_3, u_4} W₂
inst_2 : HasZeroMorphisms.{v_2, u_3} W₁
inst_3 : HasZeroMorphisms.{v_3, u_4} W₂
inst_4 : HasZeroObject.{v_2, u_3} W₁
inst_5 : HasZeroObject.{v_3, u_4} W₂
F : CategoryTheory.Functor.{v_2, v_3, u_3, u_4} W₁ W₂
inst_6 : F.PreservesZeroMorphisms
c : ComplexShape ι
inst_7 : DecidableEq ι
i j : ι
h : i ≠ j
X : W₁
⊢ Eq (α :=
    HomologicalComplex.X (Functor.obj (F ⋙ single W₂ c j) X) i ⟶
      HomologicalComplex.X
        (Functor.obj
          (Functor.comp (D := HomologicalComplex.{v_2, u_3, u_1} W₁ c) (single W₁ c j) (F.mapHomologicalComplex c)) X)
        i)
    (Hom.f (NatTrans.app (Iso.inv (singleMapHomologicalComplex F c j)) X) i) 0

Tactic:
simp [singleMapHomologicalComplex, h]

Premises used: HomologicalComplex.singleMapHomologicalComplex
-- Module: Mathlib.Algebra.Homology.AlternatingConst
Goal:
i j : ℕ
h : (up ℕ).Rel i j
subst : Odd (i + (i + 1))
⊢ Odd (i + j)

Tactic:
subst h
-- Module: Mathlib.Algebra.Homology.AlternatingConst
Goal:
i : ℕ
⊢ Odd (i + (i + 1))

Tactic:
norm_num
-- Module: Mathlib.Algebra.Homology.AlternatingConst
Goal:
i j : ℕ
h : (down ℕ).Rel i j
subst : Odd (j + 1 + j)
⊢ Odd (i + j)

Tactic:
subst h
-- Module: Mathlib.Algebra.Homology.AlternatingConst
Goal:
j : ℕ
⊢ Odd (j + 1 + j)

Tactic:
norm_num
-- Module: Mathlib.Algebra.Homology.AlternatingConst
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
A : C
φ ψ : A ⟶ A
hOdd : φ ≫ ψ = 0
hEven : ψ ≫ φ = 0
c : ComplexShape ℕ
inst_2 : DecidableRel c.Rel
hc : ∀ (i j : ℕ), c.Rel i j → Odd (i + j)
i j : ℕ
⊢ ¬c.Rel i j → Eq.{v_1 + 1} (α := A ⟶ A) (if hij : c.Rel i j then if hi : Even i then φ else ψ else 0) 0

Tactic:
aesop
-- Module: Mathlib.Algebra.Homology.AlternatingConst
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
A : C
φ ψ : A ⟶ A
hOdd : φ ≫ ψ = 0
hEven : ψ ≫ φ = 0
c : ComplexShape ℕ
inst_2 : DecidableRel c.Rel
hc : ∀ (i j : ℕ), c.Rel i j → Odd (i + j)
i j k : ℕ
hij : c.Rel i j
hjk : c.Rel j k
⊢ Odd (i + j)

Tactic:
have := hc i j hij
-- Module: Mathlib.Algebra.Homology.AlternatingConst
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
A : C
φ ψ : A ⟶ A
hOdd : φ ≫ ψ = 0
hEven : ψ ≫ φ = 0
c : ComplexShape ℕ
inst_2 : DecidableRel c.Rel
hc : ∀ (i j : ℕ), c.Rel i j → Odd (i + j)
i j k : ℕ
hij : c.Rel i j
hjk : c.Rel j k
this : Odd (i + j)
pos : ∀ (hi : Even i) (hj : Even j), φ ≫ φ = 0
neg : ∀ (hi : Even i) (hj : ¬Even j), φ ≫ ψ = 0
pos₁ : ∀ (hi : ¬Even i) (hj : Even j), ψ ≫ φ = 0
neg₁ : ∀ (hi : ¬Even i) (hj : ¬Even j), ψ ≫ ψ = 0
⊢ Eq.{v_1 + 1} (α := A ⟶ A)
    (CategoryStruct.comp (Y := A) (if hij : c.Rel i j then if hi : Even i then φ else ψ else 0)
      (if hij : c.Rel j k then if hi : Even j then φ else ψ else 0))
    0

Tactic:
split_ifs with hi hj hj
-- Module: Mathlib.Algebra.Homology.AlternatingConst
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
A : C
φ ψ : A ⟶ A
hOdd : φ ≫ ψ = 0
hEven : ψ ≫ φ = 0
c : ComplexShape ℕ
inst_2 : DecidableRel c.Rel
hc : ∀ (i j : ℕ), c.Rel i j → Odd (i + j)
i j k : ℕ
hij : c.Rel i j
hjk : c.Rel j k
this : Odd (i + j)
hi : Even i
hj : Even j
⊢ Odd i

Tactic:
simp_all [Nat.odd_add]

Premises used: Nat.odd_add
-- Module: Mathlib.Algebra.Homology.AlternatingConst
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
A : C
φ ψ : A ⟶ A
hOdd : φ ≫ ψ = 0
hEven : ψ ≫ φ = 0
c : ComplexShape ℕ
inst_2 : DecidableRel c.Rel
hc : ∀ (i j : ℕ), c.Rel i j → Odd (i + j)
i j k : ℕ
hij : c.Rel i j
hjk : c.Rel j k
this : Odd (i + j)
hi : Even i
hj : Even j
⊢ φ ≫ φ = 0

Tactic:
exact False.elim <| Nat.not_odd_iff_even.2 hi <| by simp_all [Nat.odd_add]

Premises used: Iff.mpr, False.elim, Nat.not_odd_iff_even
-- Module: Mathlib.Algebra.Homology.AlternatingConst
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
A : C
φ ψ : A ⟶ A
hOdd : φ ≫ ψ = 0
hEven : ψ ≫ φ = 0
c : ComplexShape ℕ
inst_2 : DecidableRel c.Rel
hc : ∀ (i j : ℕ), c.Rel i j → Odd (i + j)
i j k : ℕ
hij : c.Rel i j
hjk : c.Rel j k
this : Odd (i + j)
hi : Even i
hj : ¬Even j
⊢ φ ≫ ψ = 0

Tactic:
assumption
-- Module: Mathlib.Algebra.Homology.AlternatingConst
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
A : C
φ ψ : A ⟶ A
hOdd : φ ≫ ψ = 0
hEven : ψ ≫ φ = 0
c : ComplexShape ℕ
inst_2 : DecidableRel c.Rel
hc : ∀ (i j : ℕ), c.Rel i j → Odd (i + j)
i j k : ℕ
hij : c.Rel i j
hjk : c.Rel j k
this : Odd (i + j)
hi : ¬Even i
hj : Even j
⊢ ψ ≫ φ = 0

Tactic:
assumption
-- Module: Mathlib.Algebra.Homology.AlternatingConst
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
A : C
φ ψ : A ⟶ A
hOdd : φ ≫ ψ = 0
hEven : ψ ≫ φ = 0
c : ComplexShape ℕ
inst_2 : DecidableRel c.Rel
hc : ∀ (i j : ℕ), c.Rel i j → Odd (i + j)
i j k : ℕ
hij : c.Rel i j
hjk : c.Rel j k
this : Odd (i + j)
hi : ¬Even i
hj : ¬Even j
⊢ Even j

Tactic:
simp_all [Nat.odd_add]

Premises used: Nat.odd_add
-- Module: Mathlib.Algebra.Homology.AlternatingConst
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
A : C
φ ψ : A ⟶ A
hOdd : φ ≫ ψ = 0
hEven : ψ ≫ φ = 0
c : ComplexShape ℕ
inst_2 : DecidableRel c.Rel
hc : ∀ (i j : ℕ), c.Rel i j → Odd (i + j)
i j k : ℕ
hij : c.Rel i j
hjk : c.Rel j k
this : Odd (i + j)
hi : ¬Even i
hj : ¬Even j
⊢ ψ ≫ ψ = 0

Tactic:
exact False.elim <| hj <| by simp_all [Nat.odd_add]

Premises used: False.elim
-- Module: Mathlib.Algebra.Homology.AlternatingConst
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
A : C
φ ψ : A ⟶ A
hOdd : φ ≫ ψ = 0
hEven : ψ ≫ φ = 0
c : ComplexShape ℕ
inst_2 : DecidableRel c.Rel
hc : ∀ (i j : ℕ), c.Rel i j → Odd (i + j)
i j k : ℕ
hij : c.Rel i j
hjk : c.Rel j k
h : Even j
simp_all : Even i → ψ = φ
⊢ Iso.hom (Iso.refl ((alternatingConst A hOdd hEven hc).sc' i j k).X₁) ≫
      { X₁ := A, X₂ := A, X₃ := A, f := ψ, g := φ, zero := hEven : ShortComplex.{v_1, u_1} C }.f =
    ((alternatingConst A hOdd hEven hc).sc' i j k).f ≫
      Iso.hom (Iso.refl ((alternatingConst A hOdd hEven hc).sc' i j k).X₂)

Tactic:
simp_all only [alternatingConst, dite_eq_ite, Iso.refl_hom, Category.id_comp,
        shortComplexFunctor'_obj_f, ↓reduceIte, Category.comp_id, right_eq_ite_iff]

Premises used: HomologicalComplex.alternatingConst, CategoryTheory.Category.comp_id, reduceIte, right_eq_ite_iff, dite_eq_ite, HomologicalComplex.shortComplexFunctor'_obj_f, CategoryTheory.Iso.refl_hom, CategoryTheory.Category.id_comp
-- Module: Mathlib.Algebra.Homology.AlternatingConst
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
A : C
φ ψ : A ⟶ A
hOdd : φ ≫ ψ = 0
hEven : ψ ≫ φ = 0
c : ComplexShape ℕ
inst_2 : DecidableRel c.Rel
hc : ∀ (i j : ℕ), c.Rel i j → Odd (i + j)
i j k : ℕ
hij : c.Rel i j
hjk : c.Rel j k
h : Even j
hi : Even i
⊢ Odd (i + j)

Tactic:
have := hc i j hij
-- Module: Mathlib.Algebra.Homology.AlternatingConst
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
A : C
φ ψ : A ⟶ A
hOdd : φ ≫ ψ = 0
hEven : ψ ≫ φ = 0
c : ComplexShape ℕ
inst_2 : DecidableRel c.Rel
hc : ∀ (i j : ℕ), c.Rel i j → Odd (i + j)
i j k : ℕ
hij : c.Rel i j
hjk : c.Rel j k
h : Even j
hi : Even i
this : Odd (i + j)
⊢ Odd i

Tactic:
simp_all [Nat.odd_add]

Premises used: Nat.odd_add
-- Module: Mathlib.Algebra.Homology.AlternatingConst
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
A : C
φ ψ : A ⟶ A
hOdd : φ ≫ ψ = 0
hEven : ψ ≫ φ = 0
c : ComplexShape ℕ
inst_2 : DecidableRel c.Rel
hc : ∀ (i j : ℕ), c.Rel i j → Odd (i + j)
i j k : ℕ
hij : c.Rel i j
hjk : c.Rel j k
h : Even j
hi : Even i
this : Odd (i + j)
⊢ ψ = φ

Tactic:
exact False.elim <| Nat.not_odd_iff_even.2 hi <| by simp_all [Nat.odd_add]

Premises used: Iff.mpr, False.elim, Nat.not_odd_iff_even
-- Module: Mathlib.Algebra.Homology.AlternatingConst
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
A : C
φ ψ : A ⟶ A
hOdd : φ ≫ ψ = 0
hEven : ψ ≫ φ = 0
c : ComplexShape ℕ
inst_2 : DecidableRel c.Rel
hc : ∀ (i j : ℕ), c.Rel i j → Odd (i + j)
i j k : ℕ
hij : c.Rel i j
hjk : c.Rel j k
h : Even j
⊢ Iso.hom (Iso.refl ((alternatingConst A hOdd hEven hc).sc' i j k).X₂) ≫
      { X₁ := A, X₂ := A, X₃ := A, f := ψ, g := φ, zero := hEven : ShortComplex.{v_1, u_1} C }.g =
    ((alternatingConst A hOdd hEven hc).sc' i j k).g ≫
      Iso.hom (Iso.refl ((alternatingConst A hOdd hEven hc).sc' i j k).X₃)

Tactic:
simp_all [alternatingConst]

Premises used: HomologicalComplex.alternatingConst
-- Module: Mathlib.Algebra.Homology.AlternatingConst
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
A : C
φ ψ : A ⟶ A
hOdd : φ ≫ ψ = 0
hEven : ψ ≫ φ = 0
c : ComplexShape ℕ
inst_2 : DecidableRel c.Rel
hc : ∀ (i j : ℕ), c.Rel i j → Odd (i + j)
i j k : ℕ
hij : c.Rel i j
hjk : c.Rel j k
h : Odd j
simp_all : ¬Even i → φ = ψ
⊢ Iso.hom (Iso.refl ((alternatingConst A hOdd hEven hc).sc' i j k).X₁) ≫
      { X₁ := A, X₂ := A, X₃ := A, f := φ, g := ψ, zero := hOdd : ShortComplex.{v_1, u_1} C }.f =
    ((alternatingConst A hOdd hEven hc).sc' i j k).f ≫
      Iso.hom (Iso.refl ((alternatingConst A hOdd hEven hc).sc' i j k).X₂)

Tactic:
simp_all only [alternatingConst, dite_eq_ite, Iso.refl_hom, Category.id_comp,
        shortComplexFunctor'_obj_f, ↓reduceIte, Category.comp_id, left_eq_ite_iff]

Premises used: HomologicalComplex.alternatingConst, left_eq_ite_iff, CategoryTheory.Category.comp_id, reduceIte, dite_eq_ite, HomologicalComplex.shortComplexFunctor'_obj_f, CategoryTheory.Iso.refl_hom, CategoryTheory.Category.id_comp
-- Module: Mathlib.Algebra.Homology.AlternatingConst
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
A : C
φ ψ : A ⟶ A
hOdd : φ ≫ ψ = 0
hEven : ψ ≫ φ = 0
c : ComplexShape ℕ
inst_2 : DecidableRel c.Rel
hc : ∀ (i j : ℕ), c.Rel i j → Odd (i + j)
i j k : ℕ
hij : c.Rel i j
hjk : c.Rel j k
h : Odd j
hi : ¬Even i
⊢ Odd (i + j)

Tactic:
have := hc i j hij
-- Module: Mathlib.Algebra.Homology.AlternatingConst
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
A : C
φ ψ : A ⟶ A
hOdd : φ ≫ ψ = 0
hEven : ψ ≫ φ = 0
c : ComplexShape ℕ
inst_2 : DecidableRel c.Rel
hc : ∀ (i j : ℕ), c.Rel i j → Odd (i + j)
i j k : ℕ
hij : c.Rel i j
hjk : c.Rel j k
h : Odd j
hi : ¬Even i
this : Odd (i + j)
⊢ Even j

Tactic:
simp_all [Nat.odd_add]

Premises used: Nat.odd_add
-- Module: Mathlib.Algebra.Homology.AlternatingConst
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
A : C
φ ψ : A ⟶ A
hOdd : φ ≫ ψ = 0
hEven : ψ ≫ φ = 0
c : ComplexShape ℕ
inst_2 : DecidableRel c.Rel
hc : ∀ (i j : ℕ), c.Rel i j → Odd (i + j)
i j k : ℕ
hij : c.Rel i j
hjk : c.Rel j k
h : Odd j
hi : ¬Even i
this : Odd (i + j)
⊢ φ = ψ

Tactic:
exact False.elim <| Nat.not_even_iff_odd.2 h <| by simp_all [Nat.odd_add]

Premises used: Iff.mpr, False.elim, Nat.not_even_iff_odd
-- Module: Mathlib.Algebra.Homology.AlternatingConst
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
A : C
φ ψ : A ⟶ A
hOdd : φ ≫ ψ = 0
hEven : ψ ≫ φ = 0
c : ComplexShape ℕ
inst_2 : DecidableRel c.Rel
hc : ∀ (i j : ℕ), c.Rel i j → Odd (i + j)
i j k : ℕ
hij : c.Rel i j
hjk : c.Rel j k
h : Odd j
⊢ Iso.hom (Iso.refl ((alternatingConst A hOdd hEven hc).sc' i j k).X₂) ≫
      { X₁ := A, X₂ := A, X₃ := A, f := φ, g := ψ, zero := hOdd : ShortComplex.{v_1, u_1} C }.g =
    ((alternatingConst A hOdd hEven hc).sc' i j k).g ≫
      Iso.hom (Iso.refl ((alternatingConst A hOdd hEven hc).sc' i j k).X₃)

Tactic:
simp_all [alternatingConst]

Premises used: HomologicalComplex.alternatingConst
-- Module: Mathlib.Algebra.Homology.AlternatingConst
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
A : C
φ ψ : A ⟶ A
hOdd : φ ≫ ψ = 0
hEven : ψ ≫ φ = 0
c : ComplexShape ℕ
inst_2 : DecidableRel c.Rel
hc : ∀ (i j : ℕ), c.Rel i j → Odd (i + j)
inst_3 : CategoryWithHomology.{v_1, u_1} C
j : ℕ
hpj : c.Rel (c.prev j) j
hnj : c.Rel j (c.next j)
h : Even j
rw :
  Eq (α := { X₁ := A, X₂ := A, X₃ := A, f := ψ, g := φ, zero := hEven : ShortComplex.{v_1, u_1} C }.cycles ⟶ A)
    (CategoryStruct.comp (Y := ((alternatingConst A hOdd hEven hc).sc' (c.prev j) j (c.next j)).cycles)
      (Iso.inv (ShortComplex.cyclesMapIso (alternatingConstScIsoEven A hOdd hEven hc hpj hnj h)) :
        { X₁ := A, X₂ := A, X₃ := A, f := ψ, g := φ, zero := hEven : ShortComplex.{v_1, u_1} C }.cycles ⟶
          ((alternatingConst A hOdd hEven hc).sc' (c.prev j) j (c.next j)).cycles)
      ((alternatingConst A hOdd hEven hc).iCycles j ≫ φ : (alternatingConst A hOdd hEven hc).cycles j ⟶ A))
    (CategoryStruct.comp (Y := ((alternatingConst A hOdd hEven hc).sc' (c.prev j) j (c.next j)).cycles)
      (Iso.inv (ShortComplex.cyclesMapIso (alternatingConstScIsoEven A hOdd hEven hc hpj hnj h))) 0)
⊢ Eq (α := (alternatingConst A hOdd hEven hc).cycles j ⟶ A) ((alternatingConst A hOdd hEven hc).iCycles j ≫ φ) 0

Tactic:
rw [← cancel_epi (ShortComplex.cyclesMapIso
    (alternatingConstScIsoEven A hOdd hEven hc hpj hnj h)).inv]

Premises used: CategoryTheory.ShortComplex.cyclesMapIso, HomologicalComplex.alternatingConstScIsoEven, CategoryTheory.cancel_epi, CategoryTheory.Iso.inv
-- Module: Mathlib.Algebra.Homology.AlternatingConst
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
A : C
φ ψ : A ⟶ A
hOdd : φ ≫ ψ = 0
hEven : ψ ≫ φ = 0
c : ComplexShape ℕ
inst_2 : DecidableRel c.Rel
hc : ∀ (i j : ℕ), c.Rel i j → Odd (i + j)
inst_3 : CategoryWithHomology.{v_1, u_1} C
j : ℕ
hpj : c.Rel (c.prev j) j
hnj : c.Rel j (c.next j)
h : Even j
⊢ Eq (α := { X₁ := A, X₂ := A, X₃ := A, f := ψ, g := φ, zero := hEven : ShortComplex.{v_1, u_1} C }.cycles ⟶ A)
    (CategoryStruct.comp (Y := ((alternatingConst A hOdd hEven hc).sc' (c.prev j) j (c.next j)).cycles)
      (Iso.inv (ShortComplex.cyclesMapIso (alternatingConstScIsoEven A hOdd hEven hc hpj hnj h)) :
        { X₁ := A, X₂ := A, X₃ := A, f := ψ, g := φ, zero := hEven : ShortComplex.{v_1, u_1} C }.cycles ⟶
          ((alternatingConst A hOdd hEven hc).sc' (c.prev j) j (c.next j)).cycles)
      ((alternatingConst A hOdd hEven hc).iCycles j ≫ φ : (alternatingConst A hOdd hEven hc).cycles j ⟶ A))
    (CategoryStruct.comp (Y := ((alternatingConst A hOdd hEven hc).sc' (c.prev j) j (c.next j)).cycles)
      (Iso.inv (ShortComplex.cyclesMapIso (alternatingConstScIsoEven A hOdd hEven hc hpj hnj h))) 0)

Tactic:
simpa [HomologicalComplex.iCycles, -Preadditive.IsIso.comp_left_eq_zero, HomologicalComplex.sc,
    HomologicalComplex.shortComplexFunctor, alternatingConstScIsoEven,
    Category.id_comp (X := (alternatingConst A hOdd hEven hc).X _)]
    using (ShortComplex.mk ψ φ hEven).iCycles_g

Premises used: CategoryTheory.Preadditive.IsIso.comp_left_eq_zero, CategoryTheory.ShortComplex.mk, CategoryTheory.ShortComplex.iCycles_g, HomologicalComplex.iCycles, HomologicalComplex.shortComplexFunctor, HomologicalComplex.sc, HomologicalComplex.alternatingConstScIsoEven, CategoryTheory.Category.id_comp
-- Module: Mathlib.Algebra.Homology.AlternatingConst
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
A : C
φ ψ : A ⟶ A
hOdd : φ ≫ ψ = 0
hEven : ψ ≫ φ = 0
c : ComplexShape ℕ
inst_2 : DecidableRel c.Rel
hc : ∀ (i j : ℕ), c.Rel i j → Odd (i + j)
inst_3 : CategoryWithHomology.{v_1, u_1} C
j : ℕ
hpj : c.Rel (c.prev j) j
hnj : c.Rel j (c.next j)
h : Odd j
rw :
  Eq (α := { X₁ := A, X₂ := A, X₃ := A, f := φ, g := ψ, zero := hOdd : ShortComplex.{v_1, u_1} C }.cycles ⟶ A)
    (CategoryStruct.comp (Y := ((alternatingConst A hOdd hEven hc).sc' (c.prev j) j (c.next j)).cycles)
      (Iso.inv (ShortComplex.cyclesMapIso (alternatingConstScIsoOdd A hOdd hEven hc hpj hnj h)) :
        { X₁ := A, X₂ := A, X₃ := A, f := φ, g := ψ, zero := hOdd : ShortComplex.{v_1, u_1} C }.cycles ⟶
          ((alternatingConst A hOdd hEven hc).sc' (c.prev j) j (c.next j)).cycles)
      ((alternatingConst A hOdd hEven hc).iCycles j ≫ ψ : (alternatingConst A hOdd hEven hc).cycles j ⟶ A))
    (CategoryStruct.comp (Y := ((alternatingConst A hOdd hEven hc).sc' (c.prev j) j (c.next j)).cycles)
      (Iso.inv (ShortComplex.cyclesMapIso (alternatingConstScIsoOdd A hOdd hEven hc hpj hnj h))) 0)
⊢ Eq (α := (alternatingConst A hOdd hEven hc).cycles j ⟶ A) ((alternatingConst A hOdd hEven hc).iCycles j ≫ ψ) 0

Tactic:
rw [← cancel_epi (ShortComplex.cyclesMapIso
    (alternatingConstScIsoOdd A hOdd hEven hc hpj hnj h)).inv]

Premises used: HomologicalComplex.alternatingConstScIsoOdd, CategoryTheory.ShortComplex.cyclesMapIso, CategoryTheory.cancel_epi, CategoryTheory.Iso.inv
-- Module: Mathlib.Algebra.Homology.AlternatingConst
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
A : C
φ ψ : A ⟶ A
hOdd : φ ≫ ψ = 0
hEven : ψ ≫ φ = 0
c : ComplexShape ℕ
inst_2 : DecidableRel c.Rel
hc : ∀ (i j : ℕ), c.Rel i j → Odd (i + j)
inst_3 : CategoryWithHomology.{v_1, u_1} C
j : ℕ
hpj : c.Rel (c.prev j) j
hnj : c.Rel j (c.next j)
h : Odd j
⊢ Eq (α := { X₁ := A, X₂ := A, X₃ := A, f := φ, g := ψ, zero := hOdd : ShortComplex.{v_1, u_1} C }.cycles ⟶ A)
    (CategoryStruct.comp (Y := ((alternatingConst A hOdd hEven hc).sc' (c.prev j) j (c.next j)).cycles)
      (Iso.inv (ShortComplex.cyclesMapIso (alternatingConstScIsoOdd A hOdd hEven hc hpj hnj h)) :
        { X₁ := A, X₂ := A, X₃ := A, f := φ, g := ψ, zero := hOdd : ShortComplex.{v_1, u_1} C }.cycles ⟶
          ((alternatingConst A hOdd hEven hc).sc' (c.prev j) j (c.next j)).cycles)
      ((alternatingConst A hOdd hEven hc).iCycles j ≫ ψ : (alternatingConst A hOdd hEven hc).cycles j ⟶ A))
    (CategoryStruct.comp (Y := ((alternatingConst A hOdd hEven hc).sc' (c.prev j) j (c.next j)).cycles)
      (Iso.inv (ShortComplex.cyclesMapIso (alternatingConstScIsoOdd A hOdd hEven hc hpj hnj h))) 0)

Tactic:
simpa [HomologicalComplex.iCycles, -Preadditive.IsIso.comp_left_eq_zero, HomologicalComplex.sc,
    HomologicalComplex.shortComplexFunctor, alternatingConstScIsoOdd,
    Category.id_comp (X := (alternatingConst A hOdd hEven hc).X _)]
    using (ShortComplex.mk φ ψ hOdd).iCycles_g

Premises used: CategoryTheory.Preadditive.IsIso.comp_left_eq_zero, CategoryTheory.ShortComplex.mk, CategoryTheory.ShortComplex.iCycles_g, HomologicalComplex.iCycles, HomologicalComplex.shortComplexFunctor, HomologicalComplex.alternatingConstScIsoOdd, HomologicalComplex.sc, CategoryTheory.Category.id_comp
-- Module: Mathlib.Algebra.Homology.AlternatingConst
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
X Y : C
f : X ⟶ Y
i j : ℕ
hij : (ComplexShape.down ℕ).Rel i j
pos :
  Even i →
    Eq (α :=
      HomologicalComplex.X.{v_1, u_1, 0} (c := ComplexShape.down ℕ) (HomologicalComplex.alternatingConst X ⋯ ⋯ ⋯) i ⟶
        HomologicalComplex.X.{v_1, u_1, 0} (c := ComplexShape.down ℕ) (HomologicalComplex.alternatingConst Y ⋯ ⋯ ⋯) j)
      (f ≫ HomologicalComplex.d (HomologicalComplex.alternatingConst Y ⋯ ⋯ ⋯) i j)
      (HomologicalComplex.d (HomologicalComplex.alternatingConst X ⋯ ⋯ ⋯) i j ≫ f)
neg :
  ¬Even i →
    Eq (α :=
      HomologicalComplex.X.{v_1, u_1, 0} (c := ComplexShape.down ℕ) (HomologicalComplex.alternatingConst X ⋯ ⋯ ⋯) i ⟶
        HomologicalComplex.X.{v_1, u_1, 0} (c := ComplexShape.down ℕ) (HomologicalComplex.alternatingConst Y ⋯ ⋯ ⋯) j)
      (f ≫ HomologicalComplex.d (HomologicalComplex.alternatingConst Y ⋯ ⋯ ⋯) i j)
      (HomologicalComplex.d (HomologicalComplex.alternatingConst X ⋯ ⋯ ⋯) i j ≫ f)
⊢ Eq (α :=
    HomologicalComplex.X.{v_1, u_1, 0} (c := ComplexShape.down ℕ) (HomologicalComplex.alternatingConst X ⋯ ⋯ ⋯) i ⟶
      HomologicalComplex.X.{v_1, u_1, 0} (c := ComplexShape.down ℕ) (HomologicalComplex.alternatingConst Y ⋯ ⋯ ⋯) j)
    (f ≫ HomologicalComplex.d (HomologicalComplex.alternatingConst Y ⋯ ⋯ ⋯) i j)
    (HomologicalComplex.d (HomologicalComplex.alternatingConst X ⋯ ⋯ ⋯) i j ≫ f)

Tactic:
by_cases Even i

Premises used: Even
-- Module: Mathlib.Algebra.Homology.AlternatingConst
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
X Y : C
f : X ⟶ Y
i j : ℕ
hij : (ComplexShape.down ℕ).Rel i j
h : Even i
⊢ Eq (α :=
    HomologicalComplex.X.{v_1, u_1, 0} (c := ComplexShape.down ℕ) (HomologicalComplex.alternatingConst X ⋯ ⋯ ⋯) i ⟶
      HomologicalComplex.X.{v_1, u_1, 0} (c := ComplexShape.down ℕ) (HomologicalComplex.alternatingConst Y ⋯ ⋯ ⋯) j)
    (f ≫ HomologicalComplex.d (HomologicalComplex.alternatingConst Y ⋯ ⋯ ⋯) i j)
    (HomologicalComplex.d (HomologicalComplex.alternatingConst X ⋯ ⋯ ⋯) i j ≫ f)

Tactic:
simp_all [-Nat.not_even_iff_odd]

Premises used: Nat.not_even_iff_odd