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 : 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))
⊢ 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))
have 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))
Tactic: rw [← cancel_epi (((single C c j).obj A).iCycles j),
    ← HomologicalComplex.homology_π_ι_assoc, homologyι_singleObjOpcyclesSelfIso_inv,
    homologyπ_singleObjHomologySelfIso_hom, singleObjCyclesSelfIso_hom]
-- 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 (α := 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)
have 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)
Tactic: rw [← cancel_mono (singleObjCyclesSelfIso c j B).inv, assoc, assoc, Iso.hom_inv_id, comp_id,
    ← cancel_mono (iCycles _ _)]
-- 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 ⟶ cycles.{v, u, u_1} (Functor.obj (single C c j) B) j)
    (Iso.inv (singleObjCyclesSelfIso c j A) ≫ cyclesMap (CategoryTheory.Functor.map (single C c j) f) j)
    (f ≫ Iso.inv (singleObjCyclesSelfIso c j B))
have rw : Eq (α := cycles.{v, u, u_1} (Functor.obj (single C c j) A) j ⟶ cycles.{v, u, u_1} (Functor.obj (single C c j) B) j)
  (Iso.hom (singleObjCyclesSelfIso c j A) ≫
    Iso.inv (singleObjCyclesSelfIso c j A) ≫ cyclesMap (CategoryTheory.Functor.map (single C c j) f) j)
  (Iso.hom (singleObjCyclesSelfIso c j A) ≫ f ≫ Iso.inv (singleObjCyclesSelfIso c j B))
Tactic: rw [← cancel_epi (singleObjCyclesSelfIso c j A).hom, Iso.hom_inv_id_assoc,
    ← singleObjCyclesSelfIso_hom_naturality_assoc, Iso.hom_inv_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 :
  Eq (α := cycles.{v, u, u_1} (Functor.obj (single C c j) A) j ⟶ cycles.{v, u, u_1} (Functor.obj (single C c j) B) j)
    (Iso.hom (singleObjCyclesSelfIso c j A) ≫
      Iso.inv (singleObjCyclesSelfIso c j A) ≫ cyclesMap (CategoryTheory.Functor.map (single C c j) f) j)
    (Iso.hom (singleObjCyclesSelfIso c j A) ≫ f ≫ Iso.inv (singleObjCyclesSelfIso c j B))
⊢ Eq (α := A ⟶ cycles.{v, u, u_1} (Functor.obj (single C c j) B) j)
    (Iso.inv (singleObjCyclesSelfIso c j A) ≫ cyclesMap (CategoryTheory.Functor.map (single C c j) f) j)
    (f ≫ Iso.inv (singleObjCyclesSelfIso c j B))
have rw₁ : Eq (α := cycles.{v, u, u_1} (Functor.obj (single C c j) A) j ⟶ cycles.{v, u, u_1} (Functor.obj (single C c j) B) j)
  (cyclesMap (CategoryTheory.Functor.map (single C c j) f) j)
  (Iso.hom (singleObjCyclesSelfIso c j A) ≫ f ≫ Iso.inv (singleObjCyclesSelfIso c j B))
Tactic: rw [← cancel_epi (singleObjCyclesSelfIso c j A).hom, Iso.hom_inv_id_assoc,
    ← singleObjCyclesSelfIso_hom_naturality_assoc, Iso.hom_inv_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 :
  Eq (α := cycles.{v, u, u_1} (Functor.obj (single C c j) A) j ⟶ cycles.{v, u, u_1} (Functor.obj (single C c j) B) j)
    (Iso.hom (singleObjCyclesSelfIso c j A) ≫
      Iso.inv (singleObjCyclesSelfIso c j A) ≫ cyclesMap (CategoryTheory.Functor.map (single C c j) f) j)
    (Iso.hom (singleObjCyclesSelfIso c j A) ≫ f ≫ Iso.inv (singleObjCyclesSelfIso c j B))
rw₁ :
  Eq (α := cycles.{v, u, u_1} (Functor.obj (single C c j) A) j ⟶ cycles.{v, u, u_1} (Functor.obj (single C c j) B) j)
    (cyclesMap (CategoryTheory.Functor.map (single C c j) f) j)
    (Iso.hom (singleObjCyclesSelfIso c j A) ≫ f ≫ Iso.inv (singleObjCyclesSelfIso c j B))
⊢ Eq (α := A ⟶ cycles.{v, u, u_1} (Functor.obj (single C c j) B) j)
    (Iso.inv (singleObjCyclesSelfIso c j A) ≫ cyclesMap (CategoryTheory.Functor.map (single C c j) f) j)
    (f ≫ Iso.inv (singleObjCyclesSelfIso c j B))
have rw₂ : Eq (α := cycles.{v, u, u_1} (Functor.obj (single C c j) A) j ⟶ cycles.{v, u, u_1} (Functor.obj (single C c j) B) j)
  (cyclesMap (CategoryTheory.Functor.map (single C c j) f) j)
  (cyclesMap (CategoryTheory.Functor.map (single C c j) f) j ≫
    Iso.hom (singleObjCyclesSelfIso c j B) ≫ Iso.inv (singleObjCyclesSelfIso c j B))
Tactic: rw [← cancel_epi (singleObjCyclesSelfIso c j A).hom, Iso.hom_inv_id_assoc,
    ← singleObjCyclesSelfIso_hom_naturality_assoc, Iso.hom_inv_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 :
  Eq (α := cycles.{v, u, u_1} (Functor.obj (single C c j) A) j ⟶ cycles.{v, u, u_1} (Functor.obj (single C c j) B) j)
    (Iso.hom (singleObjCyclesSelfIso c j A) ≫
      Iso.inv (singleObjCyclesSelfIso c j A) ≫ cyclesMap (CategoryTheory.Functor.map (single C c j) f) j)
    (Iso.hom (singleObjCyclesSelfIso c j A) ≫ f ≫ Iso.inv (singleObjCyclesSelfIso c j B))
rw₁ :
  Eq (α := cycles.{v, u, u_1} (Functor.obj (single C c j) A) j ⟶ cycles.{v, u, u_1} (Functor.obj (single C c j) B) j)
    (cyclesMap (CategoryTheory.Functor.map (single C c j) f) j)
    (Iso.hom (singleObjCyclesSelfIso c j A) ≫ f ≫ Iso.inv (singleObjCyclesSelfIso c j B))
rw₂ :
  Eq (α := cycles.{v, u, u_1} (Functor.obj (single C c j) A) j ⟶ cycles.{v, u, u_1} (Functor.obj (single C c j) B) j)
    (cyclesMap (CategoryTheory.Functor.map (single C c j) f) j)
    (cyclesMap (CategoryTheory.Functor.map (single C c j) f) j ≫
      Iso.hom (singleObjCyclesSelfIso c j B) ≫ Iso.inv (singleObjCyclesSelfIso c j B))
⊢ Eq (α := A ⟶ cycles.{v, u, u_1} (Functor.obj (single C c j) B) j)
    (Iso.inv (singleObjCyclesSelfIso c j A) ≫ cyclesMap (CategoryTheory.Functor.map (single C c j) f) j)
    (f ≫ Iso.inv (singleObjCyclesSelfIso c j B))
have rw₃ : Eq (α := cycles.{v, u, u_1} (Functor.obj (single C c j) A) j ⟶ cycles.{v, u, u_1} (Functor.obj (single C c j) B) j)
  (cyclesMap (CategoryTheory.Functor.map (single C c j) f) j)
  (cyclesMap (CategoryTheory.Functor.map (single C c j) f) j ≫ 𝟙 (cycles.{v, u, u_1} (Functor.obj (single C c j) B) j))
Tactic: rw [← cancel_epi (singleObjCyclesSelfIso c j A).hom, Iso.hom_inv_id_assoc,
    ← singleObjCyclesSelfIso_hom_naturality_assoc, Iso.hom_inv_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 :
  Eq (α := cycles.{v, u, u_1} (Functor.obj (single C c j) A) j ⟶ cycles.{v, u, u_1} (Functor.obj (single C c j) B) j)
    (Iso.hom (singleObjCyclesSelfIso c j A) ≫
      Iso.inv (singleObjCyclesSelfIso c j A) ≫ cyclesMap (CategoryTheory.Functor.map (single C c j) f) j)
    (Iso.hom (singleObjCyclesSelfIso c j A) ≫ f ≫ Iso.inv (singleObjCyclesSelfIso c j B))
rw₁ :
  Eq (α := cycles.{v, u, u_1} (Functor.obj (single C c j) A) j ⟶ cycles.{v, u, u_1} (Functor.obj (single C c j) B) j)
    (cyclesMap (CategoryTheory.Functor.map (single C c j) f) j)
    (Iso.hom (singleObjCyclesSelfIso c j A) ≫ f ≫ Iso.inv (singleObjCyclesSelfIso c j B))
rw₂ :
  Eq (α := cycles.{v, u, u_1} (Functor.obj (single C c j) A) j ⟶ cycles.{v, u, u_1} (Functor.obj (single C c j) B) j)
    (cyclesMap (CategoryTheory.Functor.map (single C c j) f) j)
    (cyclesMap (CategoryTheory.Functor.map (single C c j) f) j ≫
      Iso.hom (singleObjCyclesSelfIso c j B) ≫ Iso.inv (singleObjCyclesSelfIso c j B))
rw₃ :
  Eq (α := cycles.{v, u, u_1} (Functor.obj (single C c j) A) j ⟶ cycles.{v, u, u_1} (Functor.obj (single C c j) B) j)
    (cyclesMap (CategoryTheory.Functor.map (single C c j) f) j)
    (cyclesMap (CategoryTheory.Functor.map (single C c j) f) j ≫
      𝟙 (cycles.{v, u, u_1} (Functor.obj (single C c j) B) j))
⊢ Eq (α := A ⟶ cycles.{v, u, u_1} (Functor.obj (single C c j) B) j)
    (Iso.inv (singleObjCyclesSelfIso c j A) ≫ cyclesMap (CategoryTheory.Functor.map (single C c j) f) j)
    (f ≫ Iso.inv (singleObjCyclesSelfIso c j B))
have rw₄ : Eq (α := cycles.{v, u, u_1} (Functor.obj (single C c j) A) j ⟶ cycles.{v, u, u_1} (Functor.obj (single C c j) B) j)
  (cyclesMap (CategoryTheory.Functor.map (single C c j) f) j)
  (cyclesMap (CategoryTheory.Functor.map (single C c j) f) j)
Tactic: rw [← cancel_epi (singleObjCyclesSelfIso c j A).hom, Iso.hom_inv_id_assoc,
    ← singleObjCyclesSelfIso_hom_naturality_assoc, Iso.hom_inv_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 (α := homology.{v, u, u_1} (Functor.obj (single C c j) A) j ⟶ B)
    (homologyMap (CategoryTheory.Functor.map (single C c j) f) j ≫ Iso.hom (singleObjHomologySelfIso c j B))
    (Iso.hom (singleObjHomologySelfIso c j A) ≫ f)
have rw : Eq (α := cycles.{v, u, u_1} (Functor.obj (single C c j) A) j ⟶ B)
  (homologyπ (Functor.obj (single C c j) A) j ≫
    homologyMap (CategoryTheory.Functor.map (single C c j) f) j ≫ Iso.hom (singleObjHomologySelfIso c j B))
  (homologyπ (Functor.obj (single C c j) A) j ≫ Iso.hom (singleObjHomologySelfIso c j A) ≫ f)
Tactic: rw [← cancel_epi (((single C c j).obj A).homologyπ j),
    homologyπ_naturality_assoc, homologyπ_singleObjHomologySelfIso_hom,
    singleObjCyclesSelfIso_hom_naturality, homologyπ_singleObjHomologySelfIso_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 ⟶ B)
    (homologyπ (Functor.obj (single C c j) A) j ≫
      homologyMap (CategoryTheory.Functor.map (single C c j) f) j ≫ Iso.hom (singleObjHomologySelfIso c j B))
    (homologyπ (Functor.obj (single C c j) A) j ≫ Iso.hom (singleObjHomologySelfIso c j A) ≫ f)
⊢ Eq (α := homology.{v, u, u_1} (Functor.obj (single C c j) A) j ⟶ B)
    (homologyMap (CategoryTheory.Functor.map (single C c j) f) j ≫ Iso.hom (singleObjHomologySelfIso c j B))
    (Iso.hom (singleObjHomologySelfIso c j A) ≫ f)
have rw₁ : 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 ≫
    homologyπ (Functor.obj (single C c j) B) j ≫ Iso.hom (singleObjHomologySelfIso c j B))
  (homologyπ (Functor.obj (single C c j) A) j ≫ Iso.hom (singleObjHomologySelfIso c j A) ≫ f)
Tactic: rw [← cancel_epi (((single C c j).obj A).homologyπ j),
    homologyπ_naturality_assoc, homologyπ_singleObjHomologySelfIso_hom,
    singleObjCyclesSelfIso_hom_naturality, homologyπ_singleObjHomologySelfIso_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 ⟶ B)
    (homologyπ (Functor.obj (single C c j) A) j ≫
      homologyMap (CategoryTheory.Functor.map (single C c j) f) j ≫ Iso.hom (singleObjHomologySelfIso c j B))
    (homologyπ (Functor.obj (single C c j) A) j ≫ Iso.hom (singleObjHomologySelfIso c j A) ≫ f)
rw₁ :
  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 ≫
      homologyπ (Functor.obj (single C c j) B) j ≫ Iso.hom (singleObjHomologySelfIso c j B))
    (homologyπ (Functor.obj (single C c j) A) j ≫ Iso.hom (singleObjHomologySelfIso c j A) ≫ f)
⊢ Eq (α := homology.{v, u, u_1} (Functor.obj (single C c j) A) j ⟶ B)
    (homologyMap (CategoryTheory.Functor.map (single C c j) f) j ≫ Iso.hom (singleObjHomologySelfIso c j B))
    (Iso.hom (singleObjHomologySelfIso c j A) ≫ f)
have rw₂ : 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))
  (homologyπ (Functor.obj (single C c j) A) j ≫ Iso.hom (singleObjHomologySelfIso c j A) ≫ f)
Tactic: rw [← cancel_epi (((single C c j).obj A).homologyπ j),
    homologyπ_naturality_assoc, homologyπ_singleObjHomologySelfIso_hom,
    singleObjCyclesSelfIso_hom_naturality, homologyπ_singleObjHomologySelfIso_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 ⟶ B)
    (homologyπ (Functor.obj (single C c j) A) j ≫
      homologyMap (CategoryTheory.Functor.map (single C c j) f) j ≫ Iso.hom (singleObjHomologySelfIso c j B))
    (homologyπ (Functor.obj (single C c j) A) j ≫ Iso.hom (singleObjHomologySelfIso c j A) ≫ f)
rw₁ :
  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 ≫
      homologyπ (Functor.obj (single C c j) B) j ≫ Iso.hom (singleObjHomologySelfIso c j B))
    (homologyπ (Functor.obj (single C c j) A) j ≫ Iso.hom (singleObjHomologySelfIso c j A) ≫ f)
rw₂ :
  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))
    (homologyπ (Functor.obj (single C c j) A) j ≫ Iso.hom (singleObjHomologySelfIso c j A) ≫ f)
⊢ Eq (α := homology.{v, u, u_1} (Functor.obj (single C c j) A) j ⟶ B)
    (homologyMap (CategoryTheory.Functor.map (single C c j) f) j ≫ Iso.hom (singleObjHomologySelfIso c j B))
    (Iso.hom (singleObjHomologySelfIso c j A) ≫ f)
have rw₃ : Eq (α := cycles.{v, u, u_1} (Functor.obj (single C c j) A) j ⟶ B) (Iso.hom (singleObjCyclesSelfIso c j A) ≫ f)
  (homologyπ (Functor.obj (single C c j) A) j ≫ Iso.hom (singleObjHomologySelfIso c j A) ≫ f)
Tactic: rw [← cancel_epi (((single C c j).obj A).homologyπ j),
    homologyπ_naturality_assoc, homologyπ_singleObjHomologySelfIso_hom,
    singleObjCyclesSelfIso_hom_naturality, homologyπ_singleObjHomologySelfIso_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 ⟶ B)
    (homologyπ (Functor.obj (single C c j) A) j ≫
      homologyMap (CategoryTheory.Functor.map (single C c j) f) j ≫ Iso.hom (singleObjHomologySelfIso c j B))
    (homologyπ (Functor.obj (single C c j) A) j ≫ Iso.hom (singleObjHomologySelfIso c j A) ≫ f)
rw₁ :
  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 ≫
      homologyπ (Functor.obj (single C c j) B) j ≫ Iso.hom (singleObjHomologySelfIso c j B))
    (homologyπ (Functor.obj (single C c j) A) j ≫ Iso.hom (singleObjHomologySelfIso c j A) ≫ f)
rw₂ :
  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))
    (homologyπ (Functor.obj (single C c j) A) j ≫ Iso.hom (singleObjHomologySelfIso c j A) ≫ f)
rw₃ :
  Eq (α := cycles.{v, u, u_1} (Functor.obj (single C c j) A) j ⟶ B) (Iso.hom (singleObjCyclesSelfIso c j A) ≫ f)
    (homologyπ (Functor.obj (single C c j) A) j ≫ Iso.hom (singleObjHomologySelfIso c j A) ≫ f)
⊢ Eq (α := homology.{v, u, u_1} (Functor.obj (single C c j) A) j ⟶ B)
    (homologyMap (CategoryTheory.Functor.map (single C c j) f) j ≫ Iso.hom (singleObjHomologySelfIso c j B))
    (Iso.hom (singleObjHomologySelfIso c j A) ≫ f)
have rw₄ : Eq (α := cycles.{v, u, u_1} (Functor.obj (single C c j) A) j ⟶ B) (Iso.hom (singleObjCyclesSelfIso c j A) ≫ f)
  (Iso.hom (singleObjCyclesSelfIso c j A) ≫ f)
Tactic: rw [← cancel_epi (((single C c j).obj A).homologyπ j),
    homologyπ_naturality_assoc, homologyπ_singleObjHomologySelfIso_hom,
    singleObjCyclesSelfIso_hom_naturality, homologyπ_singleObjHomologySelfIso_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 (α := 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) 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))
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))
⊢ 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))
    (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))
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))
⊢ 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))
    (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))
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]