awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.Single
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
inst_2 : HasZeroObject.{v, u} V
C : ChainComplex.{v, u, 0} V ℕ
X : V
f : C.X 0 ⟶ X
hf : Eq (α := C.X 1 ⟶ X) (C.d 1 0 ≫ f) 0
⊢ HomologicalComplex.Hom.f
      ((Equiv.symm (C.toSingle₀Equiv X) : (a : { f : C.X 0 ⟶ X // C.d 1 0 ≫ f = 0 }) → C ⟶ (single₀ V).obj X)
        (Subtype.mk (p := fun (f : C.X 0 ⟶ X) ↦ Eq (α := C.X 1 ⟶ X) (C.d 1 0 ≫ f) 0) f hf))
      0 =
    f

Tactic:
simp [toSingle₀Equiv]

Premises used: ChainComplex.toSingle₀Equiv
-- Module: Mathlib.Algebra.Homology.Single
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
inst_2 : HasZeroObject.{v, u} V
C : ChainComplex.{v, u, 0} V ℕ
X : V
f : X ⟶ C.X 0
i : ℕ
hi : (ComplexShape.down ℕ).Rel 0 i
⊢ f ≫ C.d 0 i = 0

Tactic:
simp at hi
-- Module: Mathlib.Algebra.Homology.Single
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
inst_2 : HasZeroObject.{v, u} V
C : ChainComplex.{v, u, 0} V ℕ
X : V
f : X ⟶ C.X 0
⊢ HomologicalComplex.Hom.f ((Equiv.symm (C.fromSingle₀Equiv X) : (a : X ⟶ C.X 0) → (single₀ V).obj X ⟶ C) f) 0 = f

Tactic:
simp [fromSingle₀Equiv]

Premises used: ChainComplex.fromSingle₀Equiv
-- Module: Mathlib.Algebra.Homology.Single
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
inst_2 : HasZeroObject.{v, u} V
C : ChainComplex.{v, u, 0} V ℕ
X : V
f : X ⟶ C.X 0
n : ℕ
⊢ Eq.{v + 1} (α := HomologicalComplex.X.{v, u, 0} (Functor.obj (single₀ V) X) (n + 1) ⟶ C.X (n + 1))
    (HomologicalComplex.Hom.f ((Equiv.symm (C.fromSingle₀Equiv X) : (a : X ⟶ C.X 0) → (single₀ V).obj X ⟶ C) f) (n + 1))
    0

Tactic:
rfl

Premises used: dite, rfl
-- Module: Mathlib.Algebra.Homology.Single
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
inst_2 : HasZeroObject.{v, u} V
A B : V
f : A ⟶ B
rw :
  Iso.hom (HomologicalComplex.singleObjXSelf (ComplexShape.up ℕ) 0 A) ≫
      f ≫ Iso.inv (HomologicalComplex.singleObjXSelf (ComplexShape.up ℕ) 0 B) =
    f
⊢ HomologicalComplex.Hom.f (CategoryTheory.Functor.map (single₀ V) f) 0 = f

Tactic:
rw [HomologicalComplex.single_map_f_self]

Premises used: HomologicalComplex.single_map_f_self
-- Module: Mathlib.Algebra.Homology.Single
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
inst_2 : HasZeroObject.{v, u} V
A B : V
f : A ⟶ B
dsimp : 𝟙 A ≫ f ≫ 𝟙 B = f
⊢ Iso.hom (HomologicalComplex.singleObjXSelf (ComplexShape.up ℕ) 0 A) ≫
      f ≫ Iso.inv (HomologicalComplex.singleObjXSelf (ComplexShape.up ℕ) 0 B) =
    f

Tactic:
dsimp [HomologicalComplex.singleObjXSelf, HomologicalComplex.singleObjXIsoOfEq]

Premises used: HomologicalComplex.singleObjXIsoOfEq, HomologicalComplex.singleObjXSelf
-- Module: Mathlib.Algebra.Homology.Single
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
inst_2 : HasZeroObject.{v, u} V
X : V
⊢ HomologicalComplex.singleObjXSelf (ComplexShape.up ℕ) 0 X =
    Iso.refl (HomologicalComplex.X.{v, u, 0} (Functor.obj (HomologicalComplex.single V (ComplexShape.up ℕ) 0) X) 0)

Tactic:
rfl

Premises used: Eq.mpr, CategoryTheory.eqToHom, CategoryTheory.eqToIso, CategoryTheory.Iso.refl, HomologicalComplex.singleObjXIsoOfEq, HomologicalComplex.singleObjXSelf, rfl, ite
-- Module: Mathlib.Algebra.Homology.Single
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
inst_2 : HasZeroObject.{v, u} V
C : CochainComplex.{v, u, 0} V ℕ
X : V
φ : Functor.obj (single₀ V) X ⟶ C
rw :
  Eq (α := X ⟶ C.X 1)
    (HomologicalComplex.d (Functor.obj (single₀ V) X) 0 1 ≫ φ.f 1 :
      HomologicalComplex.X.{v, u, 0} (Functor.obj (single₀ V) X) 0 ⟶ C.X 1)
    0
rw₁ : Eq (α := X ⟶ C.X 1) (0 ≫ φ.f 1) 0
rw₂ rw₃ : Eq.{v + 1} (α := X ⟶ C.X 1) 0 0
⊢ Eq (α := X ⟶ C.X 1) (CategoryStruct.comp (Y := C.X 0) (φ.f 0) (C.d 0 1) : X ⟶ C.X 1) (0 : X ⟶ C.X 1)

Tactic:
rw [φ.comm 0 1, HomologicalComplex.single_obj_d, zero_comp]

Premises used: HomologicalComplex.single_obj_d, CategoryTheory.Limits.zero_comp, OfNat.ofNat, HomologicalComplex.Hom.comm
-- Module: Mathlib.Algebra.Homology.Single
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
inst_2 : HasZeroObject.{v, u} V
C : CochainComplex.{v, u, 0} V ℕ
X : V
f : { f : X ⟶ C.X 0 // Eq (α := X ⟶ C.X 1) (f ≫ C.d 0 1) 0 }
i : ℕ
hi : (ComplexShape.up ℕ).Rel 0 i
⊢ i = 1

Tactic:
simpa using hi.symm

Premises used: Eq.symm
-- Module: Mathlib.Algebra.Homology.Single
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
inst_2 : HasZeroObject.{v, u} V
C : CochainComplex.{v, u, 0} V ℕ
X : V
f : { f : X ⟶ C.X 0 // Eq (α := X ⟶ C.X 1) (f ≫ C.d 0 1) 0 }
i : ℕ
hi : (ComplexShape.up ℕ).Rel 0 i
obtain : ∀ (hi : (ComplexShape.up ℕ).Rel 0 1), Eq (α := X ⟶ C.X 1) ((↑f : X ⟶ C.X 0) ≫ C.d 0 1) 0
⊢ (↑f : X ⟶ C.X 0) ≫ C.d 0 i = 0

Tactic:
obtain rfl : i = 1 := by simpa using hi.symm

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.Single
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
inst_2 : HasZeroObject.{v, u} V
C : CochainComplex.{v, u, 0} V ℕ
X : V
f : { f : X ⟶ C.X 0 // Eq (α := X ⟶ C.X 1) (f ≫ C.d 0 1) 0 }
hi : (ComplexShape.up ℕ).Rel 0 1
⊢ Eq (α := X ⟶ C.X 1) ((↑f : X ⟶ C.X 0) ≫ C.d 0 1) 0

Tactic:
f.2

Premises used: Subtype.property
-- Module: Mathlib.Algebra.Homology.Single
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
inst_2 : HasZeroObject.{v, u} V
C : CochainComplex.{v, u, 0} V ℕ
X : V
f : { f : X ⟶ C.X 0 // Eq (α := X ⟶ C.X 1) (f ≫ C.d 0 1) 0 }
hi : (ComplexShape.up ℕ).Rel 0 1
⊢ Eq (α := X ⟶ C.X 1) ((↑f : X ⟶ C.X 0) ≫ C.d 0 1) 0

Tactic:
exact f.2

Premises used: Subtype.property
-- Module: Mathlib.Algebra.Homology.Single
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
inst_2 : HasZeroObject.{v, u} V
C : CochainComplex.{v, u, 0} V ℕ
X : V
f : X ⟶ C.X 0
hf : Eq (α := X ⟶ C.X 1) (f ≫ C.d 0 1) 0
⊢ HomologicalComplex.Hom.f
      ((Equiv.symm (C.fromSingle₀Equiv X) : (a : { f : X ⟶ C.X 0 // f ≫ C.d 0 1 = 0 }) → (single₀ V).obj X ⟶ C)
        (Subtype.mk (p := fun (f : X ⟶ C.X 0) ↦ Eq (α := X ⟶ C.X 1) (f ≫ C.d 0 1) 0) f hf))
      0 =
    f

Tactic:
simp [fromSingle₀Equiv]

Premises used: CochainComplex.fromSingle₀Equiv
-- Module: Mathlib.Algebra.Homology.Single
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
inst_2 : HasZeroObject.{v, u} V
C : CochainComplex.{v, u, 0} V ℕ
X : V
f : C.X 0 ⟶ X
i : ℕ
hi : (ComplexShape.up ℕ).Rel i 0
⊢ C.d i 0 ≫ f = 0

Tactic:
simp at hi
-- Module: Mathlib.Algebra.Homology.Single
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
inst_2 : HasZeroObject.{v, u} V
C : CochainComplex.{v, u, 0} V ℕ
X : V
f : C.X 0 ⟶ X
⊢ HomologicalComplex.Hom.f ((Equiv.symm (C.toSingle₀Equiv X) : (a : C.X 0 ⟶ X) → C ⟶ (single₀ V).obj X) f) 0 = f

Tactic:
simp [toSingle₀Equiv]

Premises used: CochainComplex.toSingle₀Equiv
-- Module: Mathlib.Algebra.Homology.Single
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
inst_2 : HasZeroObject.{v, u} V
C : CochainComplex.{v, u, 0} V ℕ
X : V
f : C.X 0 ⟶ X
n : ℕ
⊢ Eq.{v + 1} (α := C.X (n + 1) ⟶ HomologicalComplex.X.{v, u, 0} (Functor.obj (single₀ V) X) (n + 1))
    (HomologicalComplex.Hom.f ((Equiv.symm (C.toSingle₀Equiv X) : (a : C.X 0 ⟶ X) → C ⟶ (single₀ V).obj X) f) (n + 1)) 0

Tactic:
rfl
-- Module: Mathlib.Algebra.Homology.SingleHomology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasZeroObject.{v, u} C
ι : Type u_1
inst_3 : DecidableEq ι
c : ComplexShape ι
j : ι
A : C
i : ι
⊢ HasHomology.{v, u, u_1} (Functor.obj (single C c j) A) i

Tactic:
apply ShortComplex.hasHomology_of_zeros

Premises used: CategoryTheory.ShortComplex.hasHomology_of_zeros
-- Module: Mathlib.Algebra.Homology.SingleHomology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasZeroObject.{v, u} C
ι : Type u_1
inst_3 : DecidableEq ι
c : ComplexShape ι
j : ι
A : C
i : ι
hi : i ≠ j
⊢ ExactAt.{v, u, u_1} (Functor.obj (single C c j) A) i

Tactic:
ShortComplex.exact_of_isZero_X₂ _ (isZero_single_obj_X c _ _ _ hi)

Premises used: HomologicalComplex.isZero_single_obj_X, HomologicalComplex.ExactAt, CategoryTheory.ShortComplex.exact_of_isZero_X₂
-- Module: Mathlib.Algebra.Homology.SingleHomology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasZeroObject.{v, u} C
ι : Type u_1
inst_3 : DecidableEq ι
c : ComplexShape ι
j : ι
A : C
i : ι
hi : i ≠ j
⊢ IsZero.{v, u} (homology.{v, u, u_1} (Functor.obj (single C c j) A) i)

Tactic:
simpa only [← exactAt_iff_isZero_homology]
    using exactAt_single_obj c j A i hi

Premises used: HomologicalComplex.exactAt_iff_isZero_homology, HomologicalComplex.exactAt_single_obj
-- Module: Mathlib.Algebra.Homology.SingleHomology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasZeroObject.{v, u} C
ι : Type u_1
inst_3 : DecidableEq ι
c : ComplexShape ι
j : ι
A : C
⊢ Eq.{v + 1} (α := cycles.{v, u, u_1} (Functor.obj (single C c j) A) j ⟶ A) (Iso.hom (singleObjCyclesSelfIso c j A))
    (iCycles (Functor.obj (single C c j) A) j ≫ Iso.hom (singleObjXSelf c j A))

Tactic:
rfl

Premises used: HomologicalComplex.iCycles, CategoryTheory.ShortComplex.iCycles, rfl
-- Module: Mathlib.Algebra.Homology.SingleHomology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasZeroObject.{v, u} C
ι : Type u_1
inst_3 : DecidableEq ι
c : ComplexShape ι
j : ι
A : C
⊢ Eq.{v + 1} (α := A ⟶ opcycles.{v, u, u_1} (Functor.obj (single C c j) A) j) (Iso.hom (singleObjOpcyclesSelfIso c j A))
    (Iso.inv (singleObjXSelf c j A) ≫ pOpcycles (Functor.obj (single C c j) A) j)

Tactic:
rfl

Premises used: Eq.mpr, CategoryTheory.eqToHom, CategoryTheory.ShortComplex.pOpcycles, HomologicalComplex.pOpcycles, rfl, ite
-- Module: Mathlib.Algebra.Homology.SingleHomology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasZeroObject.{v, u} C
ι : Type u_1
inst_3 : DecidableEq ι
c : ComplexShape ι
j : ι
A : C
⊢ Eq.{v + 1} (α := A ⟶ X.{v, u, u_1} (Functor.obj (single C c j) A) j)
    (Iso.inv (singleObjCyclesSelfIso c j A) ≫ iCycles (Functor.obj (single C c j) A) j) (Iso.inv (singleObjXSelf c j A))

Tactic:
simp [singleObjCyclesSelfIso]

Premises used: HomologicalComplex.singleObjCyclesSelfIso
-- Module: Mathlib.Algebra.Homology.SingleHomology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasZeroObject.{v, u} C
ι : Type u_1
inst_3 : DecidableEq ι
c : ComplexShape ι
j : ι
A : C
⊢ Eq.{v + 1} (α := cycles.{v, u, u_1} (Functor.obj (single C c j) A) j ⟶ A)
    (homologyπ (Functor.obj (single C c j) A) j ≫ Iso.hom (singleObjHomologySelfIso c j A))
    (Iso.hom (singleObjCyclesSelfIso c j A))

Tactic:
simp [singleObjCyclesSelfIso, singleObjHomologySelfIso]

Premises used: HomologicalComplex.singleObjHomologySelfIso, HomologicalComplex.singleObjCyclesSelfIso
-- Module: Mathlib.Algebra.Homology.SingleHomology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasZeroObject.{v, u} C
ι : Type u_1
inst_3 : DecidableEq ι
c : ComplexShape ι
j : ι
A : C
⊢ Eq.{v + 1} (α :=
    cycles.{v, u, u_1} (Functor.obj (single C c j) A) j ⟶ homology.{v, u, u_1} (Functor.obj (single C c j) A) j)
    (Iso.hom (singleObjCyclesSelfIso c j A) ≫ Iso.inv (singleObjHomologySelfIso c j A))
    (homologyπ (Functor.obj (single C c j) A) j)

Tactic:
simp only [← cancel_mono (singleObjHomologySelfIso _ _ _).hom, assoc,
    Iso.inv_hom_id, comp_id, homologyπ_singleObjHomologySelfIso_hom]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.inv_hom_id, HomologicalComplex.singleObjHomologySelfIso, CategoryTheory.cancel_mono, CategoryTheory.Category.comp_id, HomologicalComplex.homologyπ_singleObjHomologySelfIso_hom, CategoryTheory.Iso.hom
-- Module: Mathlib.Algebra.Homology.SingleHomology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasZeroObject.{v, u} C
ι : Type u_1
inst_3 : DecidableEq ι
c : ComplexShape ι
j : ι
A : C
⊢ Eq.{v + 1} (α :=
    cycles.{v, u, u_1} (Functor.obj (single C c j) A) j ⟶ opcycles.{v, u, u_1} (Functor.obj (single C c j) A) j)
    (Iso.hom (singleObjCyclesSelfIso c j A) ≫ Iso.hom (singleObjOpcyclesSelfIso c j A))
    (iCycles (Functor.obj (single C c j) A) j ≫ pOpcycles (Functor.obj (single C c j) A) j)

Tactic:
simp [singleObjCyclesSelfIso, singleObjOpcyclesSelfIso]

Premises used: HomologicalComplex.singleObjCyclesSelfIso, HomologicalComplex.singleObjOpcyclesSelfIso
-- Module: Mathlib.Algebra.Homology.SingleHomology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasZeroObject.{v, u} C
ι : Type u_1
inst_3 : DecidableEq ι
c : ComplexShape ι
j : ι
A : C
⊢ Eq.{v + 1} (α := A ⟶ homology.{v, u, u_1} (Functor.obj (single C c j) A) j)
    (Iso.inv (singleObjCyclesSelfIso c j A) ≫ homologyπ (Functor.obj (single C c j) A) j)
    (Iso.inv (singleObjHomologySelfIso c j A))

Tactic:
simp [singleObjCyclesSelfIso, singleObjHomologySelfIso]

Premises used: HomologicalComplex.singleObjHomologySelfIso, HomologicalComplex.singleObjCyclesSelfIso
-- Module: Mathlib.Algebra.Homology.SingleHomology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasZeroObject.{v, u} C
ι : Type u_1
inst_3 : DecidableEq ι
c : ComplexShape ι
j : ι
A : C
rw :
  Eq.{v + 1} (α :=
    cycles.{v, u, u_1} (Functor.obj (single C c j) A) j ⟶ opcycles.{v, u, u_1} (Functor.obj (single C c j) A) j)
    (Iso.hom (singleObjCyclesSelfIso c j A) ≫
      Iso.inv (singleObjHomologySelfIso c j A) ≫ homologyι (Functor.obj (single C c j) A) j)
    (Iso.hom (singleObjCyclesSelfIso c j A) ≫ Iso.hom (singleObjOpcyclesSelfIso c j A))
rw₁ :
  Eq.{v + 1} (α :=
    cycles.{v, u, u_1} (Functor.obj (single C c j) A) j ⟶ opcycles.{v, u, u_1} (Functor.obj (single C c j) A) j)
    (homologyπ (Functor.obj (single C c j) A) j ≫ homologyι (Functor.obj (single C c j) A) j)
    (Iso.hom (singleObjCyclesSelfIso c j A) ≫ Iso.hom (singleObjOpcyclesSelfIso c j A))
rw₂ :
  Eq.{v + 1} (α :=
    cycles.{v, u, u_1} (Functor.obj (single C c j) A) j ⟶ opcycles.{v, u, u_1} (Functor.obj (single C c j) A) j)
    (iCycles (Functor.obj (single C c j) A) j ≫ pOpcycles (Functor.obj (single C c j) A) j)
    (Iso.hom (singleObjCyclesSelfIso c j A) ≫ Iso.hom (singleObjOpcyclesSelfIso c j A))
rw₃ rw₄ :
  Eq.{v + 1} (α :=
    cycles.{v, u, u_1} (Functor.obj (single C c j) A) j ⟶ opcycles.{v, u, u_1} (Functor.obj (single C c j) A) j)
    (iCycles (Functor.obj (single C c j) A) j ≫ pOpcycles (Functor.obj (single C c j) A) j)
    (iCycles (Functor.obj (single C c j) A) j ≫ pOpcycles (Functor.obj (single C c j) A) j)
⊢ Eq.{v + 1} (α := A ⟶ opcycles.{v, u, u_1} (Functor.obj (single C c j) A) j)
    (Iso.inv (singleObjHomologySelfIso c j A) ≫ homologyι (Functor.obj (single C c j) A) j)
    (Iso.hom (singleObjOpcyclesSelfIso c j A))

Tactic:
rw [← cancel_epi (singleObjCyclesSelfIso c j A).hom,
    singleObjHomologySelfIso_hom_singleObjHomologySelfIso_inv_assoc, homology_π_ι,
    singleObjCyclesSelfIso_hom_singleObjOpcyclesSelfIso_hom]

Premises used: HomologicalComplex.singleObjCyclesSelfIso, HomologicalComplex.singleObjHomologySelfIso_hom_singleObjHomologySelfIso_inv_assoc, HomologicalComplex.singleObjCyclesSelfIso_hom_singleObjOpcyclesSelfIso_hom, HomologicalComplex.homology_π_ι, CategoryTheory.cancel_epi, CategoryTheory.Iso.hom
-- Module: Mathlib.Algebra.Homology.SingleHomology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasZeroObject.{v, u} C
ι : Type u_1
inst_3 : DecidableEq ι
c : ComplexShape ι
j : ι
A : C
rw :
  Eq.{v + 1} (α := A ⟶ A)
    (CategoryStruct.comp (Y := homology.{v, u, u_1} (Functor.obj (single C c j) A) j)
      (Iso.inv (singleObjHomologySelfIso c j A))
      (homologyι (Functor.obj (single C c j) A) j ≫ Iso.inv (singleObjOpcyclesSelfIso c j A)))
    (CategoryStruct.comp (Y := homology.{v, u, u_1} (Functor.obj (single C c j) A) j)
      (Iso.inv (singleObjHomologySelfIso c j A)) (Iso.hom (singleObjHomologySelfIso c j A)))
rw₁ :
  Eq.{v + 1} (α := A ⟶ A)
    (CategoryStruct.comp (Y := opcycles.{v, u, u_1} (Functor.obj (single C c j) A) j)
      (Iso.hom (singleObjOpcyclesSelfIso c j A)) (Iso.inv (singleObjOpcyclesSelfIso c j A)))
    (CategoryStruct.comp (Y := homology.{v, u, u_1} (Functor.obj (single C c j) A) j)
      (Iso.inv (singleObjHomologySelfIso c j A)) (Iso.hom (singleObjHomologySelfIso c j A)))
rw₂ :
  Eq.{v + 1} (α := A ⟶ A) (𝟙 A)
    (CategoryStruct.comp (Y := homology.{v, u, u_1} (Functor.obj (single C c j) A) j)
      (Iso.inv (singleObjHomologySelfIso c j A)) (Iso.hom (singleObjHomologySelfIso c j A)))
rw₃ rw₄ : Eq.{v + 1} (α := A ⟶ A) (𝟙 A) (𝟙 A)
⊢ Eq.{v + 1} (α := homology.{v, u, u_1} (Functor.obj (single C c j) A) j ⟶ A)
    (homologyι (Functor.obj (single C c j) A) j ≫ Iso.inv (singleObjOpcyclesSelfIso c j A))
    (Iso.hom (singleObjHomologySelfIso c j A))

Tactic:
rw [← cancel_epi (singleObjHomologySelfIso _ _ _).inv,
    singleObjHomologySelfIso_inv_homologyι_assoc, Iso.hom_inv_id, Iso.inv_hom_id]

Premises used: CategoryTheory.Iso.inv_hom_id, HomologicalComplex.singleObjHomologySelfIso, CategoryTheory.Iso.hom_inv_id, HomologicalComplex.singleObjHomologySelfIso_inv_homologyι_assoc, CategoryTheory.cancel_epi, CategoryTheory.Iso.inv
-- Module: Mathlib.Algebra.Homology.SingleHomology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasZeroObject.{v, u} C
ι : Type u_1
inst_3 : DecidableEq ι
c : ComplexShape ι
j : ι
A : C
rw :
  Eq.{v + 1} (α := A ⟶ opcycles.{v, u, u_1} (Functor.obj (single C c j) A) j)
    (CategoryStruct.comp (Y := homology.{v, u, u_1} (Functor.obj (single C c j) A) j)
      (Iso.inv (singleObjHomologySelfIso c j A))
      (Iso.hom (singleObjHomologySelfIso c j A) ≫ Iso.hom (singleObjOpcyclesSelfIso c j A)))
    (Iso.inv (singleObjHomologySelfIso c j A) ≫ homologyι (Functor.obj (single C c j) A) j)
rw₁ :
  Eq.{v + 1} (α := A ⟶ opcycles.{v, u, u_1} (Functor.obj (single C c j) A) j) (Iso.hom (singleObjOpcyclesSelfIso c j A))
    (Iso.inv (singleObjHomologySelfIso c j A) ≫ homologyι (Functor.obj (single C c j) A) j)
rw₂ rw₃ :
  Eq.{v + 1} (α := A ⟶ opcycles.{v, u, u_1} (Functor.obj (single C c j) A) j) (Iso.hom (singleObjOpcyclesSelfIso c j A))
    (Iso.hom (singleObjOpcyclesSelfIso c j A))
⊢ Eq.{v + 1} (α :=
    homology.{v, u, u_1} (Functor.obj (single C c j) A) j ⟶ opcycles.{v, u, u_1} (Functor.obj (single C c j) A) j)
    (Iso.hom (singleObjHomologySelfIso c j A) ≫ Iso.hom (singleObjOpcyclesSelfIso c j A))
    (homologyι (Functor.obj (single C c j) A) j)

Tactic:
rw [← cancel_epi (singleObjHomologySelfIso _ _ _).inv,
    Iso.inv_hom_id_assoc, singleObjHomologySelfIso_inv_homologyι]

Premises used: HomologicalComplex.singleObjHomologySelfIso, CategoryTheory.Iso.inv_hom_id_assoc, CategoryTheory.cancel_epi, CategoryTheory.Iso.inv, HomologicalComplex.singleObjHomologySelfIso_inv_homologyι
-- Module: Mathlib.Algebra.Homology.SingleHomology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasZeroObject.{v, u} C
ι : Type u_1
inst_3 : DecidableEq ι
c : ComplexShape ι
j : ι
A : C
⊢ Eq.{v + 1} (α :=
    X.{v, u, u_1} (Functor.obj (single C c j) A) j ⟶ X.{v, u, u_1} (Functor.obj (single C c j) A) (c.next j))
    (d (Functor.obj (single C c j) A) j (c.next j)) 0

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.SingleHomology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasZeroObject.{v, u} C
ι : Type u_1
inst_3 : DecidableEq ι
c : ComplexShape ι
j : ι
A : C
⊢ IsIso.{v, u} (X := cycles.{v, u, u_1} (Functor.obj (single C c j) A) j) (iCycles (Functor.obj (single C c j) A) j)

Tactic:
have := ((single C c j).obj A).isIso_iCycles j _ rfl (by simp)
-- Module: Mathlib.Algebra.Homology.SingleHomology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasZeroObject.{v, u} C
ι : Type u_1
inst_3 : DecidableEq ι
c : ComplexShape ι
j : ι
A : C
this :
  IsIso.{v, u} (X := cycles.{v, u, u_1} (Functor.obj (single C c j) A) j) (iCycles (Functor.obj (single C c j) A) j)
rw :
  Eq.{v + 1} (α := cycles.{v, u, u_1} (Functor.obj (single C c j) A) j ⟶ A)
    (iCycles (Functor.obj (single C c j) A) j ≫
      pOpcycles (Functor.obj (single C c j) A) j ≫ Iso.inv (singleObjOpcyclesSelfIso c j A))
    (iCycles (Functor.obj (single C c j) A) j ≫ Iso.hom (singleObjXSelf c j A))
rw₁ :
  Eq.{v + 1} (α := cycles.{v, u, u_1} (Functor.obj (single C c j) A) j ⟶ A)
    (homologyπ (Functor.obj (single C c j) A) j ≫
      homologyι (Functor.obj (single C c j) A) j ≫ Iso.inv (singleObjOpcyclesSelfIso c j A))
    (iCycles (Functor.obj (single C c j) A) j ≫ Iso.hom (singleObjXSelf c j A))
rw₂ :
  Eq.{v + 1} (α := cycles.{v, u, u_1} (Functor.obj (single C c j) A) j ⟶ A)
    (homologyπ (Functor.obj (single C c j) A) j ≫ Iso.hom (singleObjHomologySelfIso c j A))
    (iCycles (Functor.obj (single C c j) A) j ≫ Iso.hom (singleObjXSelf c j A))
rw₃ :
  Eq.{v + 1} (α := cycles.{v, u, u_1} (Functor.obj (single C c j) A) j ⟶ A) (Iso.hom (singleObjCyclesSelfIso c j A))
    (iCycles (Functor.obj (single C c j) A) j ≫ Iso.hom (singleObjXSelf c j A))
rw₄ rw₅ :
  Eq.{v + 1} (α := cycles.{v, u, u_1} (Functor.obj (single C c j) A) j ⟶ A)
    (iCycles (Functor.obj (single C c j) A) j ≫ Iso.hom (singleObjXSelf c j A))
    (iCycles (Functor.obj (single C c j) A) j ≫ Iso.hom (singleObjXSelf c j A))
⊢ Eq.{v + 1} (α := X.{v, u, u_1} (Functor.obj (single C c j) A) j ⟶ A)
    (pOpcycles (Functor.obj (single C c j) A) j ≫ Iso.inv (singleObjOpcyclesSelfIso c j A))
    (Iso.hom (singleObjXSelf c j A))

Tactic:
rw [← cancel_epi (((single C c j).obj A).iCycles j),
    ← HomologicalComplex.homology_π_ι_assoc, homologyι_singleObjOpcyclesSelfIso_inv,
    homologyπ_singleObjHomologySelfIso_hom, singleObjCyclesSelfIso_hom]

Premises used: HomologicalComplex.homologyι_singleObjOpcyclesSelfIso_inv, HomologicalComplex.iCycles, HomologicalComplex.homologyπ_singleObjHomologySelfIso_hom, HomologicalComplex.homology_π_ι_assoc, CategoryTheory.cancel_epi, HomologicalComplex.singleObjCyclesSelfIso_hom, CategoryTheory.Functor.obj, HomologicalComplex.single
-- Module: Mathlib.Algebra.Homology.SingleHomology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasZeroObject.{v, u} C
ι : Type u_1
inst_3 : DecidableEq ι
c : ComplexShape ι
j : ι
A B : C
f : A ⟶ B
rw :
  Eq (α := cycles.{v, u, u_1} (Functor.obj (single C c j) A) j ⟶ X.{v, u, u_1} (Functor.obj (single C c j) B) j)
    (CategoryStruct.comp (Y := cycles.{v, u, u_1} (Functor.obj (single C c j) B) j)
      (cyclesMap (CategoryTheory.Functor.map (single C c j) f) j) (iCycles (Functor.obj (single C c j) B) j))
    ((Iso.hom (singleObjCyclesSelfIso c j A) ≫ f ≫ Iso.inv (singleObjCyclesSelfIso c j B)) ≫
      iCycles (Functor.obj (single C c j) B) j)
⊢ Eq (α := cycles.{v, u, u_1} (Functor.obj (single C c j) A) j ⟶ B)
    (cyclesMap (CategoryTheory.Functor.map (single C c j) f) j ≫ Iso.hom (singleObjCyclesSelfIso c j B))
    (Iso.hom (singleObjCyclesSelfIso c j A) ≫ f)

Tactic:
rw [← cancel_mono (singleObjCyclesSelfIso c j B).inv, assoc, assoc, Iso.hom_inv_id, comp_id,
    ← cancel_mono (iCycles _ _)]

Premises used: CategoryTheory.Category.assoc, HomologicalComplex.singleObjCyclesSelfIso, HomologicalComplex.iCycles, CategoryTheory.Iso.hom_inv_id, CategoryTheory.cancel_mono, CategoryTheory.Category.comp_id, CategoryTheory.Iso.inv