awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.SingleHomology (goal)
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 :
  CategoryStruct.comp (Y := homology.{v, u, u_1} (Functor.obj (single C c j) B) j)
      (Iso.inv (singleObjHomologySelfIso c j A) ≫ homologyMap (CategoryTheory.Functor.map (single C c j) f) j)
      (Iso.hom (singleObjHomologySelfIso c j B)) =
    CategoryStruct.comp (Y := homology.{v, u, u_1} (Functor.obj (single C c j) B) j)
      (f ≫ Iso.inv (singleObjHomologySelfIso c j B)) (Iso.hom (singleObjHomologySelfIso c j B))
rw₁ :
  CategoryStruct.comp (Y := homology.{v, u, u_1} (Functor.obj (single C c j) A) j)
      (Iso.inv (singleObjHomologySelfIso c j A))
      (homologyMap (CategoryTheory.Functor.map (single C c j) f) j ≫ Iso.hom (singleObjHomologySelfIso c j B)) =
    CategoryStruct.comp (Y := homology.{v, u, u_1} (Functor.obj (single C c j) B) j)
      (f ≫ Iso.inv (singleObjHomologySelfIso c j B)) (Iso.hom (singleObjHomologySelfIso c j B))
rw₂ :
  CategoryStruct.comp (Y := homology.{v, u, u_1} (Functor.obj (single C c j) A) j)
      (Iso.inv (singleObjHomologySelfIso c j A))
      (homologyMap (CategoryTheory.Functor.map (single C c j) f) j ≫ Iso.hom (singleObjHomologySelfIso c j B)) =
    f ≫
      CategoryStruct.comp (Y := homology.{v, u, u_1} (Functor.obj (single C c j) B) j)
        (Iso.inv (singleObjHomologySelfIso c j B)) (Iso.hom (singleObjHomologySelfIso c j B))
⊢ Eq (α := A ⟶ homology.{v, u, u_1} (Functor.obj (single C c j) B) j)
    (Iso.inv (singleObjHomologySelfIso c j A) ≫ homologyMap (CategoryTheory.Functor.map (single C c j) f) j)
    (f ≫ Iso.inv (singleObjHomologySelfIso c j B))
have rw₃ : 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) ≫ f) =
  f ≫
    CategoryStruct.comp (Y := homology.{v, u, u_1} (Functor.obj (single C c j) B) j)
      (Iso.inv (singleObjHomologySelfIso c j B)) (Iso.hom (singleObjHomologySelfIso c j B))
Tactic: rw [← cancel_mono (singleObjHomologySelfIso c j B).hom, assoc, assoc,
    singleObjHomologySelfIso_hom_naturality,
    Iso.inv_hom_id_assoc, Iso.inv_hom_id, comp_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SingleHomology (goal)
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 :
  CategoryStruct.comp (Y := homology.{v, u, u_1} (Functor.obj (single C c j) B) j)
      (Iso.inv (singleObjHomologySelfIso c j A) ≫ homologyMap (CategoryTheory.Functor.map (single C c j) f) j)
      (Iso.hom (singleObjHomologySelfIso c j B)) =
    CategoryStruct.comp (Y := homology.{v, u, u_1} (Functor.obj (single C c j) B) j)
      (f ≫ Iso.inv (singleObjHomologySelfIso c j B)) (Iso.hom (singleObjHomologySelfIso c j B))
rw₁ :
  CategoryStruct.comp (Y := homology.{v, u, u_1} (Functor.obj (single C c j) A) j)
      (Iso.inv (singleObjHomologySelfIso c j A))
      (homologyMap (CategoryTheory.Functor.map (single C c j) f) j ≫ Iso.hom (singleObjHomologySelfIso c j B)) =
    CategoryStruct.comp (Y := homology.{v, u, u_1} (Functor.obj (single C c j) B) j)
      (f ≫ Iso.inv (singleObjHomologySelfIso c j B)) (Iso.hom (singleObjHomologySelfIso c j B))
rw₂ :
  CategoryStruct.comp (Y := homology.{v, u, u_1} (Functor.obj (single C c j) A) j)
      (Iso.inv (singleObjHomologySelfIso c j A))
      (homologyMap (CategoryTheory.Functor.map (single C c j) f) j ≫ Iso.hom (singleObjHomologySelfIso c j B)) =
    f ≫
      CategoryStruct.comp (Y := homology.{v, u, u_1} (Functor.obj (single C c j) B) j)
        (Iso.inv (singleObjHomologySelfIso c j B)) (Iso.hom (singleObjHomologySelfIso c j B))
rw₃ :
  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) ≫ f) =
    f ≫
      CategoryStruct.comp (Y := homology.{v, u, u_1} (Functor.obj (single C c j) B) j)
        (Iso.inv (singleObjHomologySelfIso c j B)) (Iso.hom (singleObjHomologySelfIso c j B))
⊢ Eq (α := A ⟶ homology.{v, u, u_1} (Functor.obj (single C c j) B) j)
    (Iso.inv (singleObjHomologySelfIso c j A) ≫ homologyMap (CategoryTheory.Functor.map (single C c j) f) j)
    (f ≫ Iso.inv (singleObjHomologySelfIso c j B))
have rw₄ : f =
  f ≫
    CategoryStruct.comp (Y := homology.{v, u, u_1} (Functor.obj (single C c j) B) j)
      (Iso.inv (singleObjHomologySelfIso c j B)) (Iso.hom (singleObjHomologySelfIso c j B))
Tactic: rw [← cancel_mono (singleObjHomologySelfIso c j B).hom, assoc, assoc,
    singleObjHomologySelfIso_hom_naturality,
    Iso.inv_hom_id_assoc, Iso.inv_hom_id, comp_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SingleHomology (goal)
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 :
  CategoryStruct.comp (Y := homology.{v, u, u_1} (Functor.obj (single C c j) B) j)
      (Iso.inv (singleObjHomologySelfIso c j A) ≫ homologyMap (CategoryTheory.Functor.map (single C c j) f) j)
      (Iso.hom (singleObjHomologySelfIso c j B)) =
    CategoryStruct.comp (Y := homology.{v, u, u_1} (Functor.obj (single C c j) B) j)
      (f ≫ Iso.inv (singleObjHomologySelfIso c j B)) (Iso.hom (singleObjHomologySelfIso c j B))
rw₁ :
  CategoryStruct.comp (Y := homology.{v, u, u_1} (Functor.obj (single C c j) A) j)
      (Iso.inv (singleObjHomologySelfIso c j A))
      (homologyMap (CategoryTheory.Functor.map (single C c j) f) j ≫ Iso.hom (singleObjHomologySelfIso c j B)) =
    CategoryStruct.comp (Y := homology.{v, u, u_1} (Functor.obj (single C c j) B) j)
      (f ≫ Iso.inv (singleObjHomologySelfIso c j B)) (Iso.hom (singleObjHomologySelfIso c j B))
rw₂ :
  CategoryStruct.comp (Y := homology.{v, u, u_1} (Functor.obj (single C c j) A) j)
      (Iso.inv (singleObjHomologySelfIso c j A))
      (homologyMap (CategoryTheory.Functor.map (single C c j) f) j ≫ Iso.hom (singleObjHomologySelfIso c j B)) =
    f ≫
      CategoryStruct.comp (Y := homology.{v, u, u_1} (Functor.obj (single C c j) B) j)
        (Iso.inv (singleObjHomologySelfIso c j B)) (Iso.hom (singleObjHomologySelfIso c j B))
rw₃ :
  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) ≫ f) =
    f ≫
      CategoryStruct.comp (Y := homology.{v, u, u_1} (Functor.obj (single C c j) B) j)
        (Iso.inv (singleObjHomologySelfIso c j B)) (Iso.hom (singleObjHomologySelfIso c j B))
rw₄ :
  f =
    f ≫
      CategoryStruct.comp (Y := homology.{v, u, u_1} (Functor.obj (single C c j) B) j)
        (Iso.inv (singleObjHomologySelfIso c j B)) (Iso.hom (singleObjHomologySelfIso c j B))
⊢ Eq (α := A ⟶ homology.{v, u, u_1} (Functor.obj (single C c j) B) j)
    (Iso.inv (singleObjHomologySelfIso c j A) ≫ homologyMap (CategoryTheory.Functor.map (single C c j) f) j)
    (f ≫ Iso.inv (singleObjHomologySelfIso c j B))
have rw₅ : f = f ≫ 𝟙 B
Tactic: rw [← cancel_mono (singleObjHomologySelfIso c j B).hom, assoc, assoc,
    singleObjHomologySelfIso_hom_naturality,
    Iso.inv_hom_id_assoc, Iso.inv_hom_id, comp_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SingleHomology (goal)
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 :
  CategoryStruct.comp (Y := homology.{v, u, u_1} (Functor.obj (single C c j) B) j)
      (Iso.inv (singleObjHomologySelfIso c j A) ≫ homologyMap (CategoryTheory.Functor.map (single C c j) f) j)
      (Iso.hom (singleObjHomologySelfIso c j B)) =
    CategoryStruct.comp (Y := homology.{v, u, u_1} (Functor.obj (single C c j) B) j)
      (f ≫ Iso.inv (singleObjHomologySelfIso c j B)) (Iso.hom (singleObjHomologySelfIso c j B))
rw₁ :
  CategoryStruct.comp (Y := homology.{v, u, u_1} (Functor.obj (single C c j) A) j)
      (Iso.inv (singleObjHomologySelfIso c j A))
      (homologyMap (CategoryTheory.Functor.map (single C c j) f) j ≫ Iso.hom (singleObjHomologySelfIso c j B)) =
    CategoryStruct.comp (Y := homology.{v, u, u_1} (Functor.obj (single C c j) B) j)
      (f ≫ Iso.inv (singleObjHomologySelfIso c j B)) (Iso.hom (singleObjHomologySelfIso c j B))
rw₂ :
  CategoryStruct.comp (Y := homology.{v, u, u_1} (Functor.obj (single C c j) A) j)
      (Iso.inv (singleObjHomologySelfIso c j A))
      (homologyMap (CategoryTheory.Functor.map (single C c j) f) j ≫ Iso.hom (singleObjHomologySelfIso c j B)) =
    f ≫
      CategoryStruct.comp (Y := homology.{v, u, u_1} (Functor.obj (single C c j) B) j)
        (Iso.inv (singleObjHomologySelfIso c j B)) (Iso.hom (singleObjHomologySelfIso c j B))
rw₃ :
  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) ≫ f) =
    f ≫
      CategoryStruct.comp (Y := homology.{v, u, u_1} (Functor.obj (single C c j) B) j)
        (Iso.inv (singleObjHomologySelfIso c j B)) (Iso.hom (singleObjHomologySelfIso c j B))
rw₄ :
  f =
    f ≫
      CategoryStruct.comp (Y := homology.{v, u, u_1} (Functor.obj (single C c j) B) j)
        (Iso.inv (singleObjHomologySelfIso c j B)) (Iso.hom (singleObjHomologySelfIso c j B))
rw₅ : f = f ≫ 𝟙 B
⊢ Eq (α := A ⟶ homology.{v, u, u_1} (Functor.obj (single C c j) B) j)
    (Iso.inv (singleObjHomologySelfIso c j A) ≫ homologyMap (CategoryTheory.Functor.map (single C c j) f) j)
    (f ≫ Iso.inv (singleObjHomologySelfIso c j B))
have rw₆ : f = f
Tactic: rw [← cancel_mono (singleObjHomologySelfIso c j B).hom, assoc, assoc,
    singleObjHomologySelfIso_hom_naturality,
    Iso.inv_hom_id_assoc, Iso.inv_hom_id, comp_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SingleHomology (goal)
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
⊢ Eq (α := A ⟶ opcycles.{v, u, u_1} (Functor.obj (single C c j) B) j)
    (Iso.hom (singleObjOpcyclesSelfIso c j A) ≫ opcyclesMap (CategoryTheory.Functor.map (single C c j) f) j)
    (f ≫ Iso.hom (singleObjOpcyclesSelfIso c j B))
have rw : Eq (α := cycles.{v, u, u_1} (Functor.obj (single C c j) A) j ⟶ opcycles.{v, u, u_1} (Functor.obj (single C c j) B) j)
  (Iso.hom (singleObjCyclesSelfIso c j A) ≫
    Iso.hom (singleObjOpcyclesSelfIso c j A) ≫ opcyclesMap (CategoryTheory.Functor.map (single C c j) f) j)
  (Iso.hom (singleObjCyclesSelfIso c j A) ≫ f ≫ Iso.hom (singleObjOpcyclesSelfIso c j B))
Tactic: rw [← cancel_epi (singleObjCyclesSelfIso c j A).hom,
    singleObjCyclesSelfIso_hom_singleObjOpcyclesSelfIso_hom_assoc, p_opcyclesMap,
    single_map_f_self, assoc, assoc, singleObjCyclesSelfIso_hom,
    singleObjOpcyclesSelfIso_hom, assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SingleHomology (goal)
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 ⟶ opcycles.{v, u, u_1} (Functor.obj (single C c j) B) j)
    (Iso.hom (singleObjCyclesSelfIso c j A) ≫
      Iso.hom (singleObjOpcyclesSelfIso c j A) ≫ opcyclesMap (CategoryTheory.Functor.map (single C c j) f) j)
    (Iso.hom (singleObjCyclesSelfIso c j A) ≫ f ≫ Iso.hom (singleObjOpcyclesSelfIso c j B))
⊢ Eq (α := A ⟶ opcycles.{v, u, u_1} (Functor.obj (single C c j) B) j)
    (Iso.hom (singleObjOpcyclesSelfIso c j A) ≫ opcyclesMap (CategoryTheory.Functor.map (single C c j) f) j)
    (f ≫ Iso.hom (singleObjOpcyclesSelfIso c j B))
have rw₁ : Eq (α := cycles.{v, u, u_1} (Functor.obj (single C c j) A) j ⟶ opcycles.{v, u, u_1} (Functor.obj (single C c j) B) j)
  (iCycles (Functor.obj (single C c j) A) j ≫
    CategoryStruct.comp (Y := opcycles.{v, u, u_1} (Functor.obj (single C c j) A) j)
      (pOpcycles (Functor.obj (single C c j) A) j) (opcyclesMap (CategoryTheory.Functor.map (single C c j) f) j))
  (Iso.hom (singleObjCyclesSelfIso c j A) ≫ f ≫ Iso.hom (singleObjOpcyclesSelfIso c j B))
Tactic: rw [← cancel_epi (singleObjCyclesSelfIso c j A).hom,
    singleObjCyclesSelfIso_hom_singleObjOpcyclesSelfIso_hom_assoc, p_opcyclesMap,
    single_map_f_self, assoc, assoc, singleObjCyclesSelfIso_hom,
    singleObjOpcyclesSelfIso_hom, assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SingleHomology (goal)
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 ⟶ opcycles.{v, u, u_1} (Functor.obj (single C c j) B) j)
    (Iso.hom (singleObjCyclesSelfIso c j A) ≫
      Iso.hom (singleObjOpcyclesSelfIso c j A) ≫ opcyclesMap (CategoryTheory.Functor.map (single C c j) f) j)
    (Iso.hom (singleObjCyclesSelfIso c j A) ≫ f ≫ Iso.hom (singleObjOpcyclesSelfIso c j B))
rw₁ :
  Eq (α := cycles.{v, u, u_1} (Functor.obj (single C c j) A) j ⟶ opcycles.{v, u, u_1} (Functor.obj (single C c j) B) j)
    (iCycles (Functor.obj (single C c j) A) j ≫
      CategoryStruct.comp (Y := opcycles.{v, u, u_1} (Functor.obj (single C c j) A) j)
        (pOpcycles (Functor.obj (single C c j) A) j) (opcyclesMap (CategoryTheory.Functor.map (single C c j) f) j))
    (Iso.hom (singleObjCyclesSelfIso c j A) ≫ f ≫ Iso.hom (singleObjOpcyclesSelfIso c j B))
⊢ Eq (α := A ⟶ opcycles.{v, u, u_1} (Functor.obj (single C c j) B) j)
    (Iso.hom (singleObjOpcyclesSelfIso c j A) ≫ opcyclesMap (CategoryTheory.Functor.map (single C c j) f) j)
    (f ≫ Iso.hom (singleObjOpcyclesSelfIso c j B))
have rw₂ : Eq (α := cycles.{v, u, u_1} (Functor.obj (single C c j) A) j ⟶ opcycles.{v, u, u_1} (Functor.obj (single C c j) B) j)
  (iCycles (Functor.obj (single C c j) A) j ≫
    Hom.f (CategoryTheory.Functor.map (single C c j) f) j ≫ pOpcycles (Functor.obj (single C c j) B) j)
  (Iso.hom (singleObjCyclesSelfIso c j A) ≫ f ≫ Iso.hom (singleObjOpcyclesSelfIso c j B))
Tactic: rw [← cancel_epi (singleObjCyclesSelfIso c j A).hom,
    singleObjCyclesSelfIso_hom_singleObjOpcyclesSelfIso_hom_assoc, p_opcyclesMap,
    single_map_f_self, assoc, assoc, singleObjCyclesSelfIso_hom,
    singleObjOpcyclesSelfIso_hom, assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SingleHomology (goal)
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 ⟶ opcycles.{v, u, u_1} (Functor.obj (single C c j) B) j)
    (Iso.hom (singleObjCyclesSelfIso c j A) ≫
      Iso.hom (singleObjOpcyclesSelfIso c j A) ≫ opcyclesMap (CategoryTheory.Functor.map (single C c j) f) j)
    (Iso.hom (singleObjCyclesSelfIso c j A) ≫ f ≫ Iso.hom (singleObjOpcyclesSelfIso c j B))
rw₁ :
  Eq (α := cycles.{v, u, u_1} (Functor.obj (single C c j) A) j ⟶ opcycles.{v, u, u_1} (Functor.obj (single C c j) B) j)
    (iCycles (Functor.obj (single C c j) A) j ≫
      CategoryStruct.comp (Y := opcycles.{v, u, u_1} (Functor.obj (single C c j) A) j)
        (pOpcycles (Functor.obj (single C c j) A) j) (opcyclesMap (CategoryTheory.Functor.map (single C c j) f) j))
    (Iso.hom (singleObjCyclesSelfIso c j A) ≫ f ≫ Iso.hom (singleObjOpcyclesSelfIso c j B))
rw₂ :
  Eq (α := cycles.{v, u, u_1} (Functor.obj (single C c j) A) j ⟶ opcycles.{v, u, u_1} (Functor.obj (single C c j) B) j)
    (iCycles (Functor.obj (single C c j) A) j ≫
      Hom.f (CategoryTheory.Functor.map (single C c j) f) j ≫ pOpcycles (Functor.obj (single C c j) B) j)
    (Iso.hom (singleObjCyclesSelfIso c j A) ≫ f ≫ Iso.hom (singleObjOpcyclesSelfIso c j B))
⊢ Eq (α := A ⟶ opcycles.{v, u, u_1} (Functor.obj (single C c j) B) j)
    (Iso.hom (singleObjOpcyclesSelfIso c j A) ≫ opcyclesMap (CategoryTheory.Functor.map (single C c j) f) j)
    (f ≫ Iso.hom (singleObjOpcyclesSelfIso c j B))
have rw₃ : Eq (α := cycles.{v, u, u_1} (Functor.obj (single C c j) A) j ⟶ opcycles.{v, u, u_1} (Functor.obj (single C c j) B) j)
  (iCycles (Functor.obj (single C c j) A) j ≫
    (Iso.hom (singleObjXSelf c j A) ≫ f ≫ Iso.inv (singleObjXSelf c j B)) ≫ pOpcycles (Functor.obj (single C c j) B) j)
  (Iso.hom (singleObjCyclesSelfIso c j A) ≫ f ≫ Iso.hom (singleObjOpcyclesSelfIso c j B))
Tactic: rw [← cancel_epi (singleObjCyclesSelfIso c j A).hom,
    singleObjCyclesSelfIso_hom_singleObjOpcyclesSelfIso_hom_assoc, p_opcyclesMap,
    single_map_f_self, assoc, assoc, singleObjCyclesSelfIso_hom,
    singleObjOpcyclesSelfIso_hom, assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SingleHomology (goal)
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 ⟶ opcycles.{v, u, u_1} (Functor.obj (single C c j) B) j)
    (Iso.hom (singleObjCyclesSelfIso c j A) ≫
      Iso.hom (singleObjOpcyclesSelfIso c j A) ≫ opcyclesMap (CategoryTheory.Functor.map (single C c j) f) j)
    (Iso.hom (singleObjCyclesSelfIso c j A) ≫ f ≫ Iso.hom (singleObjOpcyclesSelfIso c j B))
rw₁ :
  Eq (α := cycles.{v, u, u_1} (Functor.obj (single C c j) A) j ⟶ opcycles.{v, u, u_1} (Functor.obj (single C c j) B) j)
    (iCycles (Functor.obj (single C c j) A) j ≫
      CategoryStruct.comp (Y := opcycles.{v, u, u_1} (Functor.obj (single C c j) A) j)
        (pOpcycles (Functor.obj (single C c j) A) j) (opcyclesMap (CategoryTheory.Functor.map (single C c j) f) j))
    (Iso.hom (singleObjCyclesSelfIso c j A) ≫ f ≫ Iso.hom (singleObjOpcyclesSelfIso c j B))
rw₂ :
  Eq (α := cycles.{v, u, u_1} (Functor.obj (single C c j) A) j ⟶ opcycles.{v, u, u_1} (Functor.obj (single C c j) B) j)
    (iCycles (Functor.obj (single C c j) A) j ≫
      Hom.f (CategoryTheory.Functor.map (single C c j) f) j ≫ pOpcycles (Functor.obj (single C c j) B) j)
    (Iso.hom (singleObjCyclesSelfIso c j A) ≫ f ≫ Iso.hom (singleObjOpcyclesSelfIso c j B))
rw₃ :
  Eq (α := cycles.{v, u, u_1} (Functor.obj (single C c j) A) j ⟶ opcycles.{v, u, u_1} (Functor.obj (single C c j) B) j)
    (iCycles (Functor.obj (single C c j) A) j ≫
      (Iso.hom (singleObjXSelf c j A) ≫ f ≫ Iso.inv (singleObjXSelf c j B)) ≫
        pOpcycles (Functor.obj (single C c j) B) j)
    (Iso.hom (singleObjCyclesSelfIso c j A) ≫ f ≫ Iso.hom (singleObjOpcyclesSelfIso c j B))
⊢ Eq (α := A ⟶ opcycles.{v, u, u_1} (Functor.obj (single C c j) B) j)
    (Iso.hom (singleObjOpcyclesSelfIso c j A) ≫ opcyclesMap (CategoryTheory.Functor.map (single C c j) f) j)
    (f ≫ Iso.hom (singleObjOpcyclesSelfIso c j B))
have rw₄ : Eq (α := cycles.{v, u, u_1} (Functor.obj (single C c j) A) j ⟶ opcycles.{v, u, u_1} (Functor.obj (single C c j) B) j)
  (iCycles (Functor.obj (single C c j) A) j ≫
    Iso.hom (singleObjXSelf c j A) ≫ (f ≫ Iso.inv (singleObjXSelf c j B)) ≫ pOpcycles (Functor.obj (single C c j) B) j)
  (Iso.hom (singleObjCyclesSelfIso c j A) ≫ f ≫ Iso.hom (singleObjOpcyclesSelfIso c j B))
Tactic: rw [← cancel_epi (singleObjCyclesSelfIso c j A).hom,
    singleObjCyclesSelfIso_hom_singleObjOpcyclesSelfIso_hom_assoc, p_opcyclesMap,
    single_map_f_self, assoc, assoc, singleObjCyclesSelfIso_hom,
    singleObjOpcyclesSelfIso_hom, assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SingleHomology (goal)
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 ⟶ opcycles.{v, u, u_1} (Functor.obj (single C c j) B) j)
    (Iso.hom (singleObjCyclesSelfIso c j A) ≫
      Iso.hom (singleObjOpcyclesSelfIso c j A) ≫ opcyclesMap (CategoryTheory.Functor.map (single C c j) f) j)
    (Iso.hom (singleObjCyclesSelfIso c j A) ≫ f ≫ Iso.hom (singleObjOpcyclesSelfIso c j B))
rw₁ :
  Eq (α := cycles.{v, u, u_1} (Functor.obj (single C c j) A) j ⟶ opcycles.{v, u, u_1} (Functor.obj (single C c j) B) j)
    (iCycles (Functor.obj (single C c j) A) j ≫
      CategoryStruct.comp (Y := opcycles.{v, u, u_1} (Functor.obj (single C c j) A) j)
        (pOpcycles (Functor.obj (single C c j) A) j) (opcyclesMap (CategoryTheory.Functor.map (single C c j) f) j))
    (Iso.hom (singleObjCyclesSelfIso c j A) ≫ f ≫ Iso.hom (singleObjOpcyclesSelfIso c j B))
rw₂ :
  Eq (α := cycles.{v, u, u_1} (Functor.obj (single C c j) A) j ⟶ opcycles.{v, u, u_1} (Functor.obj (single C c j) B) j)
    (iCycles (Functor.obj (single C c j) A) j ≫
      Hom.f (CategoryTheory.Functor.map (single C c j) f) j ≫ pOpcycles (Functor.obj (single C c j) B) j)
    (Iso.hom (singleObjCyclesSelfIso c j A) ≫ f ≫ Iso.hom (singleObjOpcyclesSelfIso c j B))
rw₃ :
  Eq (α := cycles.{v, u, u_1} (Functor.obj (single C c j) A) j ⟶ opcycles.{v, u, u_1} (Functor.obj (single C c j) B) j)
    (iCycles (Functor.obj (single C c j) A) j ≫
      (Iso.hom (singleObjXSelf c j A) ≫ f ≫ Iso.inv (singleObjXSelf c j B)) ≫
        pOpcycles (Functor.obj (single C c j) B) j)
    (Iso.hom (singleObjCyclesSelfIso c j A) ≫ f ≫ Iso.hom (singleObjOpcyclesSelfIso c j B))
rw₄ :
  Eq (α := cycles.{v, u, u_1} (Functor.obj (single C c j) A) j ⟶ opcycles.{v, u, u_1} (Functor.obj (single C c j) B) j)
    (iCycles (Functor.obj (single C c j) A) j ≫
      Iso.hom (singleObjXSelf c j A) ≫
        (f ≫ Iso.inv (singleObjXSelf c j B)) ≫ pOpcycles (Functor.obj (single C c j) B) j)
    (Iso.hom (singleObjCyclesSelfIso c j A) ≫ f ≫ Iso.hom (singleObjOpcyclesSelfIso c j B))
⊢ Eq (α := A ⟶ opcycles.{v, u, u_1} (Functor.obj (single C c j) B) j)
    (Iso.hom (singleObjOpcyclesSelfIso c j A) ≫ opcyclesMap (CategoryTheory.Functor.map (single C c j) f) j)
    (f ≫ Iso.hom (singleObjOpcyclesSelfIso c j B))
have rw₅ : Eq (α := cycles.{v, u, u_1} (Functor.obj (single C c j) A) j ⟶ opcycles.{v, u, u_1} (Functor.obj (single C c j) B) j)
  (iCycles (Functor.obj (single C c j) A) j ≫
    Iso.hom (singleObjXSelf c j A) ≫ f ≫ Iso.inv (singleObjXSelf c j B) ≫ pOpcycles (Functor.obj (single C c j) B) j)
  (Iso.hom (singleObjCyclesSelfIso c j A) ≫ f ≫ Iso.hom (singleObjOpcyclesSelfIso c j B))
Tactic: rw [← cancel_epi (singleObjCyclesSelfIso c j A).hom,
    singleObjCyclesSelfIso_hom_singleObjOpcyclesSelfIso_hom_assoc, p_opcyclesMap,
    single_map_f_self, assoc, assoc, singleObjCyclesSelfIso_hom,
    singleObjOpcyclesSelfIso_hom, assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SingleHomology (goal)
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
⊢ Eq (α := opcycles.{v, u, u_1} (Functor.obj (single C c j) A) j ⟶ B)
    (opcyclesMap (CategoryTheory.Functor.map (single C c j) f) j ≫ Iso.inv (singleObjOpcyclesSelfIso c j B))
    (Iso.inv (singleObjOpcyclesSelfIso c j A) ≫ f)
have rw : Eq (α := opcycles.{v, u, u_1} (Functor.obj (single C c j) A) j ⟶ opcycles.{v, u, u_1} (Functor.obj (single C c j) B) j)
  ((opcyclesMap (CategoryTheory.Functor.map (single C c j) f) j ≫ Iso.inv (singleObjOpcyclesSelfIso c j B)) ≫
    Iso.hom (singleObjOpcyclesSelfIso c j B))
  ((Iso.inv (singleObjOpcyclesSelfIso c j A) ≫ f) ≫ Iso.hom (singleObjOpcyclesSelfIso c j B))
Tactic: rw [← cancel_mono (singleObjOpcyclesSelfIso c j B).hom, assoc, assoc, Iso.inv_hom_id,
    comp_id, ← singleObjOpcyclesSelfIso_hom_naturality, Iso.inv_hom_id_assoc]