awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
n : ℤ
X : C
⊢ Eq.{w + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w, v, u} C)
      (Functor.obj (SingleFunctors.functor (SingleFunctors.postcomp (CochainComplex.singleFunctors C) Q) n) X)
      (Functor.obj (SingleFunctors.functor (singleFunctors C) n) X))
    (NatTrans.app (SingleFunctors.Hom.hom (Iso.inv (singleFunctorsPostcompQIso C)) n) X)
    (NatTrans.app (𝟙 (SingleFunctors.functor (SingleFunctors.postcomp (CochainComplex.singleFunctors C) Q) n)) X)
have w : Eq.{w + 1} (α :=
  Quiver.Hom (V := DerivedCategory.{w, v, u} C)
    (Functor.obj Q (Functor.obj (SingleFunctors.functor (CochainComplex.singleFunctors C) n) X))
    (Functor.obj (SingleFunctors.functor (singleFunctors C) n) X))
  (NatTrans.app (Iso.inv (quotientCompQhIso C))
    (Functor.obj (SingleFunctors.functor (CochainComplex.singleFunctors C) n) X))
  (𝟙 (Functor.obj Q (Functor.obj (SingleFunctors.functor (CochainComplex.singleFunctors C) n) X)))
Tactic: simp [singleFunctorsPostcompQIso, HomotopyCategory.singleFunctorsPostcompQuotientIso]
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.ExactFunctor (goal)
Goal:
C₁ : Type u₁
inst : Category.{v₁, u₁} C₁
inst_1 : Abelian.{v₁, u₁} C₁
inst_2 : HasDerivedCategory.{w₁, v₁, u₁} C₁
C₂ : Type u₂
inst_3 : Category.{v₂, u₂} C₂
inst_4 : Abelian.{v₂, u₂} C₂
inst_5 : HasDerivedCategory.{w₂, v₂, u₂} C₂
F : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
inst_6 : F.Additive
inst_7 : PreservesFiniteLimits F
inst_8 : PreservesFiniteColimits F
⊢ Eq (α :=
    Quiver.Hom (V := CochainComplex.{v₁, u₁, 0} C₁ ℤ ⥤ DerivedCategory.{w₂, v₂, u₂} C₂)
      (comp (D := DerivedCategory.{w₁, v₁, u₁} C₁) DerivedCategory.Q F.mapDerivedCategory)
      (F.mapHomologicalComplex (ComplexShape.up ℤ) ⋙ DerivedCategory.Q))
    (Iso.hom F.mapDerivedCategoryFactors)
    (whiskerRight (Iso.inv (DerivedCategory.quotientCompQhIso C₁)) F.mapDerivedCategory ≫
      Iso.hom (associator (HomotopyCategory.quotient C₁ (ComplexShape.up ℤ)) DerivedCategory.Qh F.mapDerivedCategory) ≫
        whiskerLeft (HomotopyCategory.quotient C₁ (ComplexShape.up ℤ)) (Iso.hom F.mapDerivedCategoryFactorsh) ≫
          Iso.inv
              (associator (HomotopyCategory.quotient C₁ (ComplexShape.up ℤ)) (F.mapHomotopyCategory (ComplexShape.up ℤ))
                DerivedCategory.Qh) ≫
            whiskerRight (Iso.hom (F.mapHomotopyCategoryFactors (ComplexShape.up ℤ))) DerivedCategory.Qh ≫
              Iso.hom
                  (associator (F.mapHomologicalComplex (ComplexShape.up ℤ))
                    (HomotopyCategory.quotient C₂ (ComplexShape.up ℤ)) DerivedCategory.Qh) ≫
                whiskerLeft (F.mapHomologicalComplex (ComplexShape.up ℤ))
                  (Iso.hom (DerivedCategory.quotientCompQhIso C₂)))
have w : ∀ (K : CochainComplex.{v₁, u₁, 0} C₁ ℤ),
  Eq.{w₂ + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w₂, v₂, u₂} C₂)
      (obj (comp (D := DerivedCategory.{w₁, v₁, u₁} C₁) DerivedCategory.Q F.mapDerivedCategory) K)
      (obj (F.mapHomologicalComplex (ComplexShape.up ℤ) ⋙ DerivedCategory.Q) K))
    (NatTrans.app (Iso.hom F.mapDerivedCategoryFactors) K)
    (NatTrans.app
      (whiskerRight (Iso.inv (DerivedCategory.quotientCompQhIso C₁)) F.mapDerivedCategory ≫
        Iso.hom
            (associator (HomotopyCategory.quotient C₁ (ComplexShape.up ℤ)) DerivedCategory.Qh F.mapDerivedCategory) ≫
          whiskerLeft (HomotopyCategory.quotient C₁ (ComplexShape.up ℤ)) (Iso.hom F.mapDerivedCategoryFactorsh) ≫
            Iso.inv
                (associator (HomotopyCategory.quotient C₁ (ComplexShape.up ℤ))
                  (F.mapHomotopyCategory (ComplexShape.up ℤ)) DerivedCategory.Qh) ≫
              whiskerRight (Iso.hom (F.mapHomotopyCategoryFactors (ComplexShape.up ℤ))) DerivedCategory.Qh ≫
                Iso.hom
                    (associator (F.mapHomologicalComplex (ComplexShape.up ℤ))
                      (HomotopyCategory.quotient C₂ (ComplexShape.up ℤ)) DerivedCategory.Qh) ≫
                  whiskerLeft (F.mapHomologicalComplex (ComplexShape.up ℤ))
                    (Iso.hom (DerivedCategory.quotientCompQhIso C₂)))
      K)
Tactic: ext K
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.ExactFunctor (goal)
Goal:
C₁ : Type u₁
inst : Category.{v₁, u₁} C₁
inst_1 : Abelian.{v₁, u₁} C₁
inst_2 : HasDerivedCategory.{w₁, v₁, u₁} C₁
C₂ : Type u₂
inst_3 : Category.{v₂, u₂} C₂
inst_4 : Abelian.{v₂, u₂} C₂
inst_5 : HasDerivedCategory.{w₂, v₂, u₂} C₂
F : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
inst_6 : F.Additive
inst_7 : PreservesFiniteLimits F
inst_8 : PreservesFiniteColimits F
R : Type u_1
inst_9 : Ring R
inst_10 : CategoryTheory.Linear.{u_1, v₁, u₁} R C₁
inst_11 : CategoryTheory.Linear.{u_1, v₂, u₂} R C₂
inst_12 : Linear R F
⊢ Linear R (C := DerivedCategory.{w₁, v₁, u₁} C₁) (D := DerivedCategory.{w₂, v₂, u₂} C₂) F.mapDerivedCategory
have rw : Linear R (C := HomotopyCategory.{v₁, u₁, 0} C₁ (ComplexShape.up ℤ)) (D := DerivedCategory.{w₂, v₂, u₂} C₂)
  (F.mapHomotopyCategory (ComplexShape.up ℤ) ⋙ DerivedCategory.Qh)
Tactic: rw [← Localization.functor_linear_iff DerivedCategory.Qh (HomotopyCategory.quasiIso C₁
    (ComplexShape.up ℤ)) R ((F.mapHomotopyCategory (ComplexShape.up ℤ)).comp DerivedCategory.Qh)]
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
I : C
inst_2 : Injective.{v, u} I
L : CochainComplex.{v, u, 0} C ℤ
i : ℤ
ι : Functor.obj (singleFunctor C i) I ⟶ L
inst_3 : L.IsStrictlyGE i
inst_4 : QuasiIsoAt ι i
e : L.X i ≅ opcycles L i := pOpcyclesIso L (i - 1) i ⋯ ⋯
α : I ⟶ L.X i := Iso.inv (singleObjHomologySelfIso (ComplexShape.up ℤ) i I) ≫ homologyMap ι i ≫ homologyι L i ≫ e.inv
⊢ ι.f i = Iso.hom (singleObjXSelf (ComplexShape.up ℤ) i I) ≫ α
have rw : ι.f i ≫ e.hom = (Iso.hom (singleObjXSelf (ComplexShape.up ℤ) i I) ≫ α) ≫ e.hom
Tactic: rw [← cancel_mono e.hom]
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
I : C
inst_2 : Injective.{v, u} I
L : CochainComplex.{v, u, 0} C ℤ
i : ℤ
ι : Functor.obj (singleFunctor C i) I ⟶ L
inst_3 : L.IsStrictlyGE i
inst_4 : QuasiIsoAt ι i
e : L.X i ≅ opcycles L i := pOpcyclesIso L (i - 1) i ⋯ ⋯
α : I ⟶ L.X i := Iso.inv (singleObjHomologySelfIso (ComplexShape.up ℤ) i I) ≫ homologyMap ι i ≫ homologyι L i ≫ e.inv
⊢ ι.f i ≫ e.hom = (Iso.hom (singleObjXSelf (ComplexShape.up ℤ) i I) ≫ α) ≫ e.hom
have dsimp : Eq (α := X.{v, u, 0} (Functor.obj (singleFunctor C i) I) i ⟶ opcycles L i) (ι.f i ≫ pOpcycles L i)
  ((Iso.hom (singleObjXSelf (ComplexShape.up ℤ) i I) ≫
      Iso.inv (singleObjHomologySelfIso (ComplexShape.up ℤ) i I) ≫
        CategoryStruct.comp (Y := homology L i) (homologyMap ι i)
          (homologyι L i ≫ Iso.inv (pOpcyclesIso L (i - 1) i sorry sorry))) ≫
    pOpcycles L i)
Tactic: dsimp [α, e]
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
I : C
inst_2 : Injective.{v, u} I
L : CochainComplex.{v, u, 0} C ℤ
i : ℤ
ι : Functor.obj (singleFunctor C i) I ⟶ L
inst_3 : L.IsStrictlyGE i
inst_4 : QuasiIsoAt ι i
e : L.X i ≅ opcycles L i := pOpcyclesIso L (i - 1) i ⋯ ⋯
α : I ⟶ L.X i := Iso.inv (singleObjHomologySelfIso (ComplexShape.up ℤ) i I) ≫ homologyMap ι i ≫ homologyι L i ≫ e.inv
⊢ Eq (α := X.{v, u, 0} (Functor.obj (singleFunctor C i) I) i ⟶ opcycles L i) (ι.f i ≫ pOpcycles L i)
    ((Iso.hom (singleObjXSelf (ComplexShape.up ℤ) i I) ≫
        Iso.inv (singleObjHomologySelfIso (ComplexShape.up ℤ) i I) ≫
          CategoryStruct.comp (Y := homology L i) (homologyMap ι i)
            (homologyι L i ≫ Iso.inv (pOpcyclesIso L (i - 1) i ⋯ ⋯))) ≫
      pOpcycles L i)
have rw : Eq (α := X.{v, u, 0} (Functor.obj (singleFunctor C i) I) i ⟶ opcycles L i) (ι.f i ≫ pOpcycles L i)
  (Iso.hom (singleObjXSelf (ComplexShape.up ℤ) i I) ≫
    Iso.inv (singleObjHomologySelfIso (ComplexShape.up ℤ) i I) ≫
      homologyι (Functor.obj (singleFunctor C i) I) i ≫ opcyclesMap ι i)
Tactic: rw [assoc, assoc, assoc, assoc, pOpcyclesIso_inv_hom_id, comp_id, homologyι_naturality]
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
I : C
inst_2 : Injective.{v, u} I
L : CochainComplex.{v, u, 0} C ℤ
i : ℤ
ι : Functor.obj (singleFunctor C i) I ⟶ L
inst_3 : L.IsStrictlyGE i
inst_4 : QuasiIsoAt ι i
e : L.X i ≅ opcycles L i := pOpcyclesIso L (i - 1) i ⋯ ⋯
α : I ⟶ L.X i := Iso.inv (singleObjHomologySelfIso (ComplexShape.up ℤ) i I) ≫ homologyMap ι i ≫ homologyι L i ≫ e.inv
⊢ Eq (α := X.{v, u, 0} (Functor.obj (singleFunctor C i) I) i ⟶ opcycles L i) (ι.f i ≫ pOpcycles L i)
    (Iso.hom (singleObjXSelf (ComplexShape.up ℤ) i I) ≫
      Iso.inv (singleObjHomologySelfIso (ComplexShape.up ℤ) i I) ≫
        homologyι (Functor.obj (singleFunctor C i) I) i ≫ opcyclesMap ι i)
have dsimp : Eq (α := X.{v, u, 0} (Functor.obj (single C (ComplexShape.up ℤ) i) I) i ⟶ opcycles L i) (ι.f i ≫ pOpcycles L i)
  (Iso.hom (singleObjXSelf (ComplexShape.up ℤ) i I) ≫
    Iso.inv (singleObjHomologySelfIso (ComplexShape.up ℤ) i I) ≫
      homologyι (Functor.obj (single C (ComplexShape.up ℤ) i) I) i ≫ opcyclesMap ι i)
Tactic: dsimp [singleFunctor, singleFunctors]
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
I : C
inst_2 : Injective.{v, u} I
L : CochainComplex.{v, u, 0} C ℤ
i : ℤ
ι : Functor.obj (singleFunctor C i) I ⟶ L
inst_3 : L.IsStrictlyGE i
inst_4 : QuasiIsoAt ι i
e : L.X i ≅ opcycles L i := pOpcyclesIso L (i - 1) i ⋯ ⋯
α : I ⟶ L.X i := Iso.inv (singleObjHomologySelfIso (ComplexShape.up ℤ) i I) ≫ homologyMap ι i ≫ homologyι L i ≫ e.inv
⊢ Eq (α := X.{v, u, 0} (Functor.obj (single C (ComplexShape.up ℤ) i) I) i ⟶ opcycles L i) (ι.f i ≫ pOpcycles L i)
    (Iso.hom (singleObjXSelf (ComplexShape.up ℤ) i I) ≫
      Iso.inv (singleObjHomologySelfIso (ComplexShape.up ℤ) i I) ≫
        homologyι (Functor.obj (single C (ComplexShape.up ℤ) i) I) i ≫ opcyclesMap ι i)
have rw : Eq (α := X.{v, u, 0} (Functor.obj (single C (ComplexShape.up ℤ) i) I) i ⟶ opcycles L i) (ι.f i ≫ pOpcycles L i)
  (Iso.hom (singleObjXSelf (ComplexShape.up ℤ) i I) ≫
    Iso.hom (singleObjOpcyclesSelfIso (ComplexShape.up ℤ) i I) ≫ opcyclesMap ι i)
Tactic: rw [singleObjHomologySelfIso_inv_homologyι_assoc,
      ← pOpcycles_singleObjOpcyclesSelfIso_inv_assoc, Iso.inv_hom_id_assoc, p_opcyclesMap]
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
I : C
inst_2 : Injective.{v, u} I
L : CochainComplex.{v, u, 0} C ℤ
i : ℤ
ι : Functor.obj (singleFunctor C i) I ⟶ L
inst_3 : L.IsStrictlyGE i
inst_4 : QuasiIsoAt ι i
e : L.X i ≅ opcycles L i := pOpcyclesIso L (i - 1) i ⋯ ⋯
α : I ⟶ L.X i := Iso.inv (singleObjHomologySelfIso (ComplexShape.up ℤ) i I) ≫ homologyMap ι i ≫ homologyι L i ≫ e.inv
rw :
  Eq (α := X.{v, u, 0} (Functor.obj (single C (ComplexShape.up ℤ) i) I) i ⟶ opcycles L i) (ι.f i ≫ pOpcycles L i)
    (Iso.hom (singleObjXSelf (ComplexShape.up ℤ) i I) ≫
      Iso.hom (singleObjOpcyclesSelfIso (ComplexShape.up ℤ) i I) ≫ opcyclesMap ι i)
⊢ Eq (α := X.{v, u, 0} (Functor.obj (single C (ComplexShape.up ℤ) i) I) i ⟶ opcycles L i) (ι.f i ≫ pOpcycles L i)
    (Iso.hom (singleObjXSelf (ComplexShape.up ℤ) i I) ≫
      Iso.inv (singleObjHomologySelfIso (ComplexShape.up ℤ) i I) ≫
        homologyι (Functor.obj (single C (ComplexShape.up ℤ) i) I) i ≫ opcyclesMap ι i)
have rw₁ : Eq (α := X.{v, u, 0} (Functor.obj (single C (ComplexShape.up ℤ) i) I) i ⟶ opcycles L i) (ι.f i ≫ pOpcycles L i)
  (pOpcycles (Functor.obj (single C (ComplexShape.up ℤ) i) I) i ≫
    Iso.inv (singleObjOpcyclesSelfIso (ComplexShape.up ℤ) i I) ≫
      Iso.hom (singleObjOpcyclesSelfIso (ComplexShape.up ℤ) i I) ≫ opcyclesMap ι i)
Tactic: rw [singleObjHomologySelfIso_inv_homologyι_assoc,
      ← pOpcycles_singleObjOpcyclesSelfIso_inv_assoc, Iso.inv_hom_id_assoc, p_opcyclesMap]
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
I : C
inst_2 : Injective.{v, u} I
L : CochainComplex.{v, u, 0} C ℤ
i : ℤ
ι : Functor.obj (singleFunctor C i) I ⟶ L
inst_3 : L.IsStrictlyGE i
inst_4 : QuasiIsoAt ι i
e : L.X i ≅ opcycles L i := pOpcyclesIso L (i - 1) i ⋯ ⋯
α : I ⟶ L.X i := Iso.inv (singleObjHomologySelfIso (ComplexShape.up ℤ) i I) ≫ homologyMap ι i ≫ homologyι L i ≫ e.inv
rw :
  Eq (α := X.{v, u, 0} (Functor.obj (single C (ComplexShape.up ℤ) i) I) i ⟶ opcycles L i) (ι.f i ≫ pOpcycles L i)
    (Iso.hom (singleObjXSelf (ComplexShape.up ℤ) i I) ≫
      Iso.hom (singleObjOpcyclesSelfIso (ComplexShape.up ℤ) i I) ≫ opcyclesMap ι i)
rw₁ :
  Eq (α := X.{v, u, 0} (Functor.obj (single C (ComplexShape.up ℤ) i) I) i ⟶ opcycles L i) (ι.f i ≫ pOpcycles L i)
    (pOpcycles (Functor.obj (single C (ComplexShape.up ℤ) i) I) i ≫
      Iso.inv (singleObjOpcyclesSelfIso (ComplexShape.up ℤ) i I) ≫
        Iso.hom (singleObjOpcyclesSelfIso (ComplexShape.up ℤ) i I) ≫ opcyclesMap ι i)
⊢ Eq (α := X.{v, u, 0} (Functor.obj (single C (ComplexShape.up ℤ) i) I) i ⟶ opcycles L i) (ι.f i ≫ pOpcycles L i)
    (Iso.hom (singleObjXSelf (ComplexShape.up ℤ) i I) ≫
      Iso.inv (singleObjHomologySelfIso (ComplexShape.up ℤ) i I) ≫
        homologyι (Functor.obj (single C (ComplexShape.up ℤ) i) I) i ≫ opcyclesMap ι i)
have rw₂ : Eq (α := X.{v, u, 0} (Functor.obj (single C (ComplexShape.up ℤ) i) I) i ⟶ opcycles L i) (ι.f i ≫ pOpcycles L i)
  (CategoryStruct.comp (Y := opcycles.{v, u, 0} (Functor.obj (single C (ComplexShape.up ℤ) i) I) i)
    (pOpcycles (Functor.obj (single C (ComplexShape.up ℤ) i) I) i) (opcyclesMap ι i))
Tactic: rw [singleObjHomologySelfIso_inv_homologyι_assoc,
      ← pOpcycles_singleObjOpcyclesSelfIso_inv_assoc, Iso.inv_hom_id_assoc, p_opcyclesMap]
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
I : C
inst_2 : Injective.{v, u} I
L : CochainComplex.{v, u, 0} C ℤ
i : ℤ
ι : Functor.obj (singleFunctor C i) I ⟶ L
inst_3 : L.IsStrictlyGE i
inst_4 : QuasiIsoAt ι i
e : L.X i ≅ opcycles L i := pOpcyclesIso L (i - 1) i ⋯ ⋯
α : I ⟶ L.X i := Iso.inv (singleObjHomologySelfIso (ComplexShape.up ℤ) i I) ≫ homologyMap ι i ≫ homologyι L i ≫ e.inv
rw :
  Eq (α := X.{v, u, 0} (Functor.obj (single C (ComplexShape.up ℤ) i) I) i ⟶ opcycles L i) (ι.f i ≫ pOpcycles L i)
    (Iso.hom (singleObjXSelf (ComplexShape.up ℤ) i I) ≫
      Iso.hom (singleObjOpcyclesSelfIso (ComplexShape.up ℤ) i I) ≫ opcyclesMap ι i)
rw₁ :
  Eq (α := X.{v, u, 0} (Functor.obj (single C (ComplexShape.up ℤ) i) I) i ⟶ opcycles L i) (ι.f i ≫ pOpcycles L i)
    (pOpcycles (Functor.obj (single C (ComplexShape.up ℤ) i) I) i ≫
      Iso.inv (singleObjOpcyclesSelfIso (ComplexShape.up ℤ) i I) ≫
        Iso.hom (singleObjOpcyclesSelfIso (ComplexShape.up ℤ) i I) ≫ opcyclesMap ι i)
rw₂ :
  Eq (α := X.{v, u, 0} (Functor.obj (single C (ComplexShape.up ℤ) i) I) i ⟶ opcycles L i) (ι.f i ≫ pOpcycles L i)
    (CategoryStruct.comp (Y := opcycles.{v, u, 0} (Functor.obj (single C (ComplexShape.up ℤ) i) I) i)
      (pOpcycles (Functor.obj (single C (ComplexShape.up ℤ) i) I) i) (opcyclesMap ι i))
⊢ Eq (α := X.{v, u, 0} (Functor.obj (single C (ComplexShape.up ℤ) i) I) i ⟶ opcycles L i) (ι.f i ≫ pOpcycles L i)
    (Iso.hom (singleObjXSelf (ComplexShape.up ℤ) i I) ≫
      Iso.inv (singleObjHomologySelfIso (ComplexShape.up ℤ) i I) ≫
        homologyι (Functor.obj (single C (ComplexShape.up ℤ) i) I) i ≫ opcyclesMap ι i)
have rw₃ : Eq (α := X.{v, u, 0} (Functor.obj (single C (ComplexShape.up ℤ) i) I) i ⟶ opcycles L i) (ι.f i ≫ pOpcycles L i)
  (ι.f i ≫ pOpcycles L i)
Tactic: rw [singleObjHomologySelfIso_inv_homologyι_assoc,
      ← pOpcycles_singleObjOpcyclesSelfIso_inv_assoc, Iso.inv_hom_id_assoc, p_opcyclesMap]
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
I : C
inst_2 : Injective.{v, u} I
L : CochainComplex.{v, u, 0} C ℤ
i : ℤ
ι : Functor.obj (singleFunctor C i) I ⟶ L
inst_3 : L.IsStrictlyGE i
inst_4 : QuasiIsoAt ι i
e : L.X i ≅ opcycles L i := pOpcyclesIso L (i - 1) i ⋯ ⋯
α : I ⟶ L.X i := Iso.inv (singleObjHomologySelfIso (ComplexShape.up ℤ) i I) ≫ homologyMap ι i ≫ homologyι L i ≫ e.inv
⊢ IsSplitMono ι
have this : ι.f i = Iso.hom (singleObjXSelf (ComplexShape.up ℤ) i I) ≫ α
Tactic: have : ι.f i = (singleObjXSelf (ComplexShape.up ℤ) i I).hom ≫ α := by
    rw [← cancel_mono e.hom]
    dsimp [α, e]
    rw [assoc, assoc, assoc, assoc, pOpcyclesIso_inv_hom_id, comp_id, homologyι_naturality]
    dsimp [singleFunctor, singleFunctors]
    rw [singleObjHomologySelfIso_inv_homologyι_assoc,
      ← pOpcycles_singleObjOpcyclesSelfIso_inv_assoc, Iso.inv_hom_id_assoc, p_opcyclesMap]
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
I : C
inst_2 : Injective.{v, u} I
L : CochainComplex.{v, u, 0} C ℤ
i : ℤ
ι : Functor.obj (singleFunctor C i) I ⟶ L
inst_3 : L.IsStrictlyGE i
inst_4 : QuasiIsoAt ι i
e : L.X i ≅ opcycles L i := pOpcyclesIso L (i - 1) i ⋯ ⋯
α : I ⟶ L.X i := Iso.inv (singleObjHomologySelfIso (ComplexShape.up ℤ) i I) ≫ homologyMap ι i ≫ homologyι L i ≫ e.inv
this : ι.f i = Iso.hom (singleObjXSelf (ComplexShape.up ℤ) i I) ≫ α
⊢ ι ≫ mkHomToSingle (Injective.factorThru (𝟙 I) α) ⋯ = 𝟙 (Functor.obj (singleFunctor C i) I)
have hfg : Hom.f (ι ≫ mkHomToSingle (Injective.factorThru (𝟙 I) α) sorry) i = Hom.f (𝟙 (Functor.obj (singleFunctor C i) I)) i
Tactic: apply HomologicalComplex.to_single_hom_ext
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
I : C
inst_2 : Injective.{v, u} I
L : CochainComplex.{v, u, 0} C ℤ
i : ℤ
ι : Functor.obj (singleFunctor C i) I ⟶ L
inst_3 : L.IsStrictlyGE i
inst_4 : QuasiIsoAt ι i
e : L.X i ≅ opcycles L i := pOpcyclesIso L (i - 1) i ⋯ ⋯
α : I ⟶ L.X i := Iso.inv (singleObjHomologySelfIso (ComplexShape.up ℤ) i I) ≫ homologyMap ι i ≫ homologyι L i ≫ e.inv
this : ι.f i = Iso.hom (singleObjXSelf (ComplexShape.up ℤ) i I) ≫ α
⊢ Hom.f (ι ≫ mkHomToSingle (Injective.factorThru (𝟙 I) α) ⋯) i = Hom.f (𝟙 (Functor.obj (singleFunctor C i) I)) i
have hfg : ι.f i ≫ Hom.f (mkHomToSingle (Injective.factorThru (𝟙 I) α) sorry) i = Hom.f (𝟙 (Functor.obj (singleFunctor C i) I)) i
Tactic: rw [comp_f, mkHomToSingle_f, id_f, this, assoc, Injective.comp_factorThru_assoc,
        id_comp, Iso.hom_inv_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
I : C
inst_2 : Injective.{v, u} I
L : CochainComplex.{v, u, 0} C ℤ
i : ℤ
ι : Functor.obj (singleFunctor C i) I ⟶ L
inst_3 : L.IsStrictlyGE i
inst_4 : QuasiIsoAt ι i
e : L.X i ≅ opcycles L i := pOpcyclesIso L (i - 1) i ⋯ ⋯
α : I ⟶ L.X i := Iso.inv (singleObjHomologySelfIso (ComplexShape.up ℤ) i I) ≫ homologyMap ι i ≫ homologyι L i ≫ e.inv
this : ι.f i = Iso.hom (singleObjXSelf (ComplexShape.up ℤ) i I) ≫ α
hfg : ι.f i ≫ Hom.f (mkHomToSingle (Injective.factorThru (𝟙 I) α) ⋯) i = Hom.f (𝟙 (Functor.obj (singleFunctor C i) I)) i
⊢ Hom.f (ι ≫ mkHomToSingle (Injective.factorThru (𝟙 I) α) ⋯) i = Hom.f (𝟙 (Functor.obj (singleFunctor C i) I)) i
have hfg₁ : ι.f i ≫ Injective.factorThru (𝟙 I) α ≫ Iso.inv (singleObjXSelf (ComplexShape.up ℤ) i I) =
  Hom.f (𝟙 (Functor.obj (singleFunctor C i) I)) i
Tactic: rw [comp_f, mkHomToSingle_f, id_f, this, assoc, Injective.comp_factorThru_assoc,
        id_comp, Iso.hom_inv_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
I : C
inst_2 : Injective.{v, u} I
L : CochainComplex.{v, u, 0} C ℤ
i : ℤ
ι : Functor.obj (singleFunctor C i) I ⟶ L
inst_3 : L.IsStrictlyGE i
inst_4 : QuasiIsoAt ι i
e : L.X i ≅ opcycles L i := pOpcyclesIso L (i - 1) i ⋯ ⋯
α : I ⟶ L.X i := Iso.inv (singleObjHomologySelfIso (ComplexShape.up ℤ) i I) ≫ homologyMap ι i ≫ homologyι L i ≫ e.inv
this : ι.f i = Iso.hom (singleObjXSelf (ComplexShape.up ℤ) i I) ≫ α
hfg : ι.f i ≫ Hom.f (mkHomToSingle (Injective.factorThru (𝟙 I) α) ⋯) i = Hom.f (𝟙 (Functor.obj (singleFunctor C i) I)) i
hfg₁ :
  ι.f i ≫ Injective.factorThru (𝟙 I) α ≫ Iso.inv (singleObjXSelf (ComplexShape.up ℤ) i I) =
    Hom.f (𝟙 (Functor.obj (singleFunctor C i) I)) i
⊢ Hom.f (ι ≫ mkHomToSingle (Injective.factorThru (𝟙 I) α) ⋯) i = Hom.f (𝟙 (Functor.obj (singleFunctor C i) I)) i
have hfg₂ : ι.f i ≫ Injective.factorThru (𝟙 I) α ≫ Iso.inv (singleObjXSelf (ComplexShape.up ℤ) i I) =
  𝟙 (X.{v, u, 0} (Functor.obj (singleFunctor C i) I) i)
Tactic: rw [comp_f, mkHomToSingle_f, id_f, this, assoc, Injective.comp_factorThru_assoc,
        id_comp, Iso.hom_inv_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
I : C
inst_2 : Injective.{v, u} I
L : CochainComplex.{v, u, 0} C ℤ
i : ℤ
ι : Functor.obj (singleFunctor C i) I ⟶ L
inst_3 : L.IsStrictlyGE i
inst_4 : QuasiIsoAt ι i
e : L.X i ≅ opcycles L i := pOpcyclesIso L (i - 1) i ⋯ ⋯
α : I ⟶ L.X i := Iso.inv (singleObjHomologySelfIso (ComplexShape.up ℤ) i I) ≫ homologyMap ι i ≫ homologyι L i ≫ e.inv
this : ι.f i = Iso.hom (singleObjXSelf (ComplexShape.up ℤ) i I) ≫ α
hfg : ι.f i ≫ Hom.f (mkHomToSingle (Injective.factorThru (𝟙 I) α) ⋯) i = Hom.f (𝟙 (Functor.obj (singleFunctor C i) I)) i
hfg₁ :
  ι.f i ≫ Injective.factorThru (𝟙 I) α ≫ Iso.inv (singleObjXSelf (ComplexShape.up ℤ) i I) =
    Hom.f (𝟙 (Functor.obj (singleFunctor C i) I)) i
hfg₂ :
  ι.f i ≫ Injective.factorThru (𝟙 I) α ≫ Iso.inv (singleObjXSelf (ComplexShape.up ℤ) i I) =
    𝟙 (X.{v, u, 0} (Functor.obj (singleFunctor C i) I) i)
⊢ Hom.f (ι ≫ mkHomToSingle (Injective.factorThru (𝟙 I) α) ⋯) i = Hom.f (𝟙 (Functor.obj (singleFunctor C i) I)) i
have hfg₃ : (Iso.hom (singleObjXSelf (ComplexShape.up ℤ) i I) ≫ α) ≫
    Injective.factorThru (𝟙 I) α ≫ Iso.inv (singleObjXSelf (ComplexShape.up ℤ) i I) =
  𝟙 (X.{v, u, 0} (Functor.obj (singleFunctor C i) I) i)
Tactic: rw [comp_f, mkHomToSingle_f, id_f, this, assoc, Injective.comp_factorThru_assoc,
        id_comp, Iso.hom_inv_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
I : C
inst_2 : Injective.{v, u} I
L : CochainComplex.{v, u, 0} C ℤ
i : ℤ
ι : Functor.obj (singleFunctor C i) I ⟶ L
inst_3 : L.IsStrictlyGE i
inst_4 : QuasiIsoAt ι i
e : L.X i ≅ opcycles L i := pOpcyclesIso L (i - 1) i ⋯ ⋯
α : I ⟶ L.X i := Iso.inv (singleObjHomologySelfIso (ComplexShape.up ℤ) i I) ≫ homologyMap ι i ≫ homologyι L i ≫ e.inv
this : ι.f i = Iso.hom (singleObjXSelf (ComplexShape.up ℤ) i I) ≫ α
hfg : ι.f i ≫ Hom.f (mkHomToSingle (Injective.factorThru (𝟙 I) α) ⋯) i = Hom.f (𝟙 (Functor.obj (singleFunctor C i) I)) i
hfg₁ :
  ι.f i ≫ Injective.factorThru (𝟙 I) α ≫ Iso.inv (singleObjXSelf (ComplexShape.up ℤ) i I) =
    Hom.f (𝟙 (Functor.obj (singleFunctor C i) I)) i
hfg₂ :
  ι.f i ≫ Injective.factorThru (𝟙 I) α ≫ Iso.inv (singleObjXSelf (ComplexShape.up ℤ) i I) =
    𝟙 (X.{v, u, 0} (Functor.obj (singleFunctor C i) I) i)
hfg₃ :
  (Iso.hom (singleObjXSelf (ComplexShape.up ℤ) i I) ≫ α) ≫
      Injective.factorThru (𝟙 I) α ≫ Iso.inv (singleObjXSelf (ComplexShape.up ℤ) i I) =
    𝟙 (X.{v, u, 0} (Functor.obj (singleFunctor C i) I) i)
⊢ Hom.f (ι ≫ mkHomToSingle (Injective.factorThru (𝟙 I) α) ⋯) i = Hom.f (𝟙 (Functor.obj (singleFunctor C i) I)) i
have hfg₄ : Iso.hom (singleObjXSelf (ComplexShape.up ℤ) i I) ≫
    α ≫ Injective.factorThru (𝟙 I) α ≫ Iso.inv (singleObjXSelf (ComplexShape.up ℤ) i I) =
  𝟙 (X.{v, u, 0} (Functor.obj (singleFunctor C i) I) i)
Tactic: rw [comp_f, mkHomToSingle_f, id_f, this, assoc, Injective.comp_factorThru_assoc,
        id_comp, Iso.hom_inv_id]