awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.Single (goal)
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
⊢ 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)
have rw₂ : Eq.{v + 1} (α := X ⟶ C.X 1) 0 0
Tactic: rw [φ.comm 0 1, HomologicalComplex.single_obj_d, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Single (goal)
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
⊢ (↑f : X ⟶ C.X 0) ≫ C.d 0 i = 0
have obtain : ∀ (hi : (ComplexShape.up ℕ).Rel 0 1), Eq (α := X ⟶ C.X 1) ((↑f : X ⟶ C.X 0) ≫ C.d 0 1) 0
Tactic: obtain rfl : i = 1 := by simpa using hi.symm
Cleared hypotheses: i, hi
-- 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
⊢ 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))
have 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))
Tactic: rw [← cancel_epi (singleObjCyclesSelfIso c j A).hom,
    singleObjHomologySelfIso_hom_singleObjHomologySelfIso_inv_assoc, homology_π_ι,
    singleObjCyclesSelfIso_hom_singleObjOpcyclesSelfIso_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 : 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))
⊢ 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))
have 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))
Tactic: rw [← cancel_epi (singleObjCyclesSelfIso c j A).hom,
    singleObjHomologySelfIso_hom_singleObjHomologySelfIso_inv_assoc, homology_π_ι,
    singleObjCyclesSelfIso_hom_singleObjOpcyclesSelfIso_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 : 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))
⊢ 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))
have 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))
Tactic: rw [← cancel_epi (singleObjCyclesSelfIso c j A).hom,
    singleObjHomologySelfIso_hom_singleObjHomologySelfIso_inv_assoc, homology_π_ι,
    singleObjCyclesSelfIso_hom_singleObjOpcyclesSelfIso_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 : 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))
⊢ 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))
have 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)
Tactic: rw [← cancel_epi (singleObjCyclesSelfIso c j A).hom,
    singleObjHomologySelfIso_hom_singleObjHomologySelfIso_inv_assoc, homology_π_ι,
    singleObjCyclesSelfIso_hom_singleObjOpcyclesSelfIso_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 : C
⊢ 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))
have 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)))
Tactic: rw [← cancel_epi (singleObjHomologySelfIso _ _ _).inv,
    singleObjHomologySelfIso_inv_homologyι_assoc, Iso.hom_inv_id, Iso.inv_hom_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 : 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)))
⊢ 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))
have 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)))
Tactic: rw [← cancel_epi (singleObjHomologySelfIso _ _ _).inv,
    singleObjHomologySelfIso_inv_homologyι_assoc, Iso.hom_inv_id, Iso.inv_hom_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 : 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)))
⊢ 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))
have 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)))
Tactic: rw [← cancel_epi (singleObjHomologySelfIso _ _ _).inv,
    singleObjHomologySelfIso_inv_homologyι_assoc, Iso.hom_inv_id, Iso.inv_hom_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 : 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)))
⊢ 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))
have rw₃ : Eq.{v + 1} (α := A ⟶ A) (𝟙 A) (𝟙 A)
Tactic: rw [← cancel_epi (singleObjHomologySelfIso _ _ _).inv,
    singleObjHomologySelfIso_inv_homologyι_assoc, Iso.hom_inv_id, Iso.inv_hom_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 : C
⊢ 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)
have 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)
Tactic: rw [← cancel_epi (singleObjHomologySelfIso _ _ _).inv,
    Iso.inv_hom_id_assoc, singleObjHomologySelfIso_inv_homologyι]
-- 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
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)
⊢ 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)
have 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)
Tactic: rw [← cancel_epi (singleObjHomologySelfIso _ _ _).inv,
    Iso.inv_hom_id_assoc, singleObjHomologySelfIso_inv_homologyι]
-- 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
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)
⊢ 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)
have 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))
Tactic: rw [← cancel_epi (singleObjHomologySelfIso _ _ _).inv,
    Iso.inv_hom_id_assoc, singleObjHomologySelfIso_inv_homologyι]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SingleHomology (hypothesis)
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 ⟶ A)
    (pOpcycles (Functor.obj (single C c j) A) j ≫ Iso.inv (singleObjOpcyclesSelfIso c j A))
    (Iso.hom (singleObjXSelf c j A))
have 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)
Tactic: have := ((single C c j).obj A).isIso_iCycles j _ rfl (by simp)
-- 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)
⊢ 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 ≫
    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))
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 : 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))
⊢ 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)
  (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))
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 : 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))
⊢ 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)
  (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))
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 : 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))
⊢ 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) (Iso.hom (singleObjCyclesSelfIso 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]