awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives
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 (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)
⊢ 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)

Tactic:
rw [assoc, assoc, assoc, assoc, pOpcyclesIso_inv_hom_id, comp_id, homologyι_naturality]

Premises used: CategoryTheory.Category.assoc, HomologicalComplex.pOpcyclesIso_inv_hom_id, CategoryTheory.Category.comp_id, HomologicalComplex.homologyι_naturality
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives
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
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)
⊢ 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:
dsimp [singleFunctor, singleFunctors]

Premises used: CochainComplex.singleFunctor, CochainComplex.singleFunctors
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives
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))
rw₃ 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)
⊢ 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:
rw [singleObjHomologySelfIso_inv_homologyι_assoc,
      ← pOpcycles_singleObjOpcyclesSelfIso_inv_assoc, Iso.inv_hom_id_assoc, p_opcyclesMap]

Premises used: HomologicalComplex.p_opcyclesMap, HomologicalComplex.singleObjHomologySelfIso_inv_homologyι_assoc, CategoryTheory.Iso.inv_hom_id_assoc, HomologicalComplex.pOpcycles_singleObjOpcyclesSelfIso_inv_assoc
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives
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) ≫ α

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]
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives
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 ℤ
j : ℤ
ι : Functor.obj (singleFunctor C (j + 1)) I ⟶ L
inst_3 : L.IsStrictlyGE (j + 1)
inst_4 : QuasiIsoAt ι (j + 1)
e : L.X (j + 1) ≅ opcycles L (j + 1) := pOpcyclesIso L (j + 1 - 1) (j + 1) ⋯ ⋯
α : I ⟶ L.X (j + 1) :=
  Iso.inv (singleObjHomologySelfIso (ComplexShape.up ℤ) (j + 1) I) ≫ homologyMap ι (j + 1) ≫ homologyι L (j + 1) ≫ e.inv
this : ι.f (j + 1) = Iso.hom (singleObjXSelf (ComplexShape.up ℤ) (j + 1) I) ≫ α
⊢ j < j + 1

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives
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 ℤ
j : ℤ
ι : Functor.obj (singleFunctor C (j + 1)) I ⟶ L
inst_3 : L.IsStrictlyGE (j + 1)
inst_4 : QuasiIsoAt ι (j + 1)
e : L.X (j + 1) ≅ opcycles L (j + 1) := pOpcyclesIso L (j + 1 - 1) (j + 1) ⋯ ⋯
α : I ⟶ L.X (j + 1) :=
  Iso.inv (singleObjHomologySelfIso (ComplexShape.up ℤ) (j + 1) I) ≫ homologyMap ι (j + 1) ≫ homologyι L (j + 1) ≫ e.inv
this : ι.f (j + 1) = Iso.hom (singleObjXSelf (ComplexShape.up ℤ) (j + 1) I) ≫ α
⊢ L.d j (j + 1) ≫ Injective.factorThru (𝟙 I) α = 0

Tactic:
apply (L.isZero_of_isStrictlyGE (j + 1) j (by simp)).eq_of_src

Premises used: CochainComplex.isZero_of_isStrictlyGE, HAdd.hAdd, CategoryTheory.Limits.IsZero.eq_of_src, OfNat.ofNat
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives
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 : Hom.f (ι ≫ mkHomToSingle (Injective.factorThru (𝟙 I) α) ⋯) i = Hom.f (𝟙 (Functor.obj (singleFunctor C i) I)) i
⊢ ι ≫ mkHomToSingle (Injective.factorThru (𝟙 I) α) ⋯ = 𝟙 (Functor.obj (singleFunctor C i) I)

Tactic:
apply HomologicalComplex.to_single_hom_ext

Premises used: HomologicalComplex.to_single_hom_ext
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives
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)
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)
hfg₅ :
  Iso.hom (singleObjXSelf (ComplexShape.up ℤ) i I) ≫ 𝟙 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) ≫ Iso.inv (singleObjXSelf (ComplexShape.up ℤ) i I) =
    𝟙 (X.{v, u, 0} (Functor.obj (singleFunctor C i) I) i)
hfg₇ hfg₈ :
  Eq.{v + 1} (α :=
    X.{v, u, 0} (Functor.obj (singleFunctor C i) I) i ⟶ X.{v, u, 0} (Functor.obj (single C (ComplexShape.up ℤ) i) I) i)
    (𝟙 (X.{v, u, 0} (Functor.obj (singleFunctor C i) 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

Tactic:
rw [comp_f, mkHomToSingle_f, id_f, this, assoc, Injective.comp_factorThru_assoc,
        id_comp, Iso.hom_inv_id]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Injective.comp_factorThru_assoc, HomologicalComplex.id_f, CategoryTheory.Iso.hom_inv_id, HomologicalComplex.comp_f, HomologicalComplex.mkHomToSingle_f, CategoryTheory.Category.id_comp
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives
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) ≫ α
⊢ IsSplitMono ι

Tactic:
exact ⟨⟨{
    retraction := mkHomToSingle (Injective.factorThru (𝟙 I) α) (by
      rintro j rfl
      apply (L.isZero_of_isStrictlyGE (j + 1) j (by simp)).eq_of_src)
    id := by
      apply HomologicalComplex.to_single_hom_ext
      rw [comp_f, mkHomToSingle_f, id_f, this, assoc, Injective.comp_factorThru_assoc,
        id_comp, Iso.hom_inv_id] }⟩⟩
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
I : C
inst_3 : Injective.{v, u} I
K : CochainComplex.{v, u, 0} C ℤ
i : ℤ
φ :
  Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q K)
    (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C i) I))
n : ℤ
hn : i < n
inst_4 : K.IsStrictlyGE n
obtain :
  ∀ (L : CochainComplex.{v, u, 0} C ℤ),
    L.IsStrictlyGE i →
      ∀ (g : K ⟶ L) (ι : Functor.obj (CochainComplex.singleFunctor C i) I ⟶ L)
        (h :
          IsIso (C := DerivedCategory.{w, v, u} C) (X :=
            Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C i) I)) (CategoryTheory.Functor.map Q ι)),
        Eq.{w + 1} (α :=
          Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q K)
            (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C i) I)))
          (CategoryTheory.Functor.map Q g ≫ inv (CategoryTheory.Functor.map Q ι)) 0
⊢ φ = 0

Tactic:
obtain ⟨L, _, g, ι, h, rfl⟩ := left_fac_of_isStrictlyGE φ i

Premises used: DerivedCategory.left_fac_of_isStrictlyGE, rfl
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
I : C
inst_3 : Injective.{v, u} I
K : CochainComplex.{v, u, 0} C ℤ
i n : ℤ
hn : i < n
inst_4 : K.IsStrictlyGE n
L : CochainComplex.{v, u, 0} C ℤ
w : L.IsStrictlyGE i
g : K ⟶ L
ι : Functor.obj (CochainComplex.singleFunctor C i) I ⟶ L
h :
  IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C i) I))
    (CategoryTheory.Functor.map Q ι)
⊢ QuasiIso ι

Tactic:
rw [isIso_Q_map_iff_quasiIso] at h

Premises used: DerivedCategory.isIso_Q_map_iff_quasiIso
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
I : C
inst_3 : Injective.{v, u} I
K : CochainComplex.{v, u, 0} C ℤ
i n : ℤ
hn : i < n
inst_4 : K.IsStrictlyGE n
L : CochainComplex.{v, u, 0} C ℤ
w : L.IsStrictlyGE i
g : K ⟶ L
ι : Functor.obj (CochainComplex.singleFunctor C i) I ⟶ L
h : QuasiIso ι
⊢ IsSplitMono ι

Tactic:
CochainComplex.isSplitMono_from_singleFunctor_obj_of_injective ι

Premises used: CochainComplex.isSplitMono_from_singleFunctor_obj_of_injective
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
I : C
inst_3 : Injective.{v, u} I
K : CochainComplex.{v, u, 0} C ℤ
i n : ℤ
hn : i < n
inst_4 : K.IsStrictlyGE n
L : CochainComplex.{v, u, 0} C ℤ
w : L.IsStrictlyGE i
g : K ⟶ L
ι : Functor.obj (CochainComplex.singleFunctor C i) I ⟶ L
h : QuasiIso ι
⊢ IsSplitMono ι

Tactic:
exact CochainComplex.isSplitMono_from_singleFunctor_obj_of_injective ι

Premises used: CochainComplex.isSplitMono_from_singleFunctor_obj_of_injective
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
I : C
inst_3 : Injective.{v, u} I
K : CochainComplex.{v, u, 0} C ℤ
i n : ℤ
hn : i < n
inst_4 : K.IsStrictlyGE n
L : CochainComplex.{v, u, 0} C ℤ
w : L.IsStrictlyGE i
g : K ⟶ L
ι : Functor.obj (CochainComplex.singleFunctor C i) I ⟶ L
h :
  IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C i) I))
    (CategoryTheory.Functor.map Q ι)
⊢ IsSplitMono ι

Tactic:
have hπ : IsSplitMono ι := by
    rw [isIso_Q_map_iff_quasiIso] at h
    exact CochainComplex.isSplitMono_from_singleFunctor_obj_of_injective ι
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
I : C
inst_3 : Injective.{v, u} I
K : CochainComplex.{v, u, 0} C ℤ
i n : ℤ
hn : i < n
inst_4 : K.IsStrictlyGE n
L : CochainComplex.{v, u, 0} C ℤ
w : L.IsStrictlyGE i
g : K ⟶ L
ι : Functor.obj (CochainComplex.singleFunctor C i) I ⟶ L
h :
  IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C i) I))
    (CategoryTheory.Functor.map Q ι)
hπ : IsSplitMono ι
rw :
  Eq.{w + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C i) I))
      (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C i) I)))
    (CategoryTheory.Functor.map Q ι ≫ inv (CategoryTheory.Functor.map Q ι))
    (CategoryTheory.Functor.map Q ι ≫ CategoryTheory.Functor.map Q (retraction ι))
rw₁ :
  Eq.{w + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C i) I))
      (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C i) I)))
    (𝟙 (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C i) I)))
    (CategoryTheory.Functor.map Q ι ≫ CategoryTheory.Functor.map Q (retraction ι))
rw₂ :
  Eq.{w + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C i) I))
      (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C i) I)))
    (𝟙 (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C i) I)))
    (CategoryTheory.Functor.map Q (ι ≫ retraction ι))
rw₃ :
  Eq.{w + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C i) I))
      (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C i) I)))
    (𝟙 (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C i) I)))
    (CategoryTheory.Functor.map Q (𝟙 (Functor.obj (CochainComplex.singleFunctor C i) I)))
rw₄ rw₅ :
  Eq.{w + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C i) I))
      (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C i) I)))
    (𝟙 (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C i) I)))
    (𝟙 (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C i) I)))
⊢ Eq.{w + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q L)
      (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C i) I)))
    (inv (CategoryTheory.Functor.map Q ι)) (CategoryTheory.Functor.map Q (retraction ι))

Tactic:
rw [← cancel_epi (Q.map ι), IsIso.hom_inv_id, ← Q.map_comp, IsSplitMono.id, Q.map_id]

Premises used: DerivedCategory.Q, CategoryTheory.Functor.map, CategoryTheory.Functor.map_id, CategoryTheory.IsSplitMono.id, CategoryTheory.Functor.map_comp, CategoryTheory.IsIso.hom_inv_id, CategoryTheory.cancel_epi
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
I : C
inst_3 : Injective.{v, u} I
K : CochainComplex.{v, u, 0} C ℤ
i n : ℤ
hn : i < n
inst_4 : K.IsStrictlyGE n
L : CochainComplex.{v, u, 0} C ℤ
w : L.IsStrictlyGE i
g : K ⟶ L
ι : Functor.obj (CochainComplex.singleFunctor C i) I ⟶ L
h :
  IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C i) I))
    (CategoryTheory.Functor.map Q ι)
hπ : IsSplitMono ι
⊢ Eq.{w + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q L)
      (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C i) I)))
    (inv (CategoryTheory.Functor.map Q ι)) (CategoryTheory.Functor.map Q (retraction ι))

Tactic:
have h₁ : inv (Q.map ι) = Q.map (retraction ι) := by
    rw [← cancel_epi (Q.map ι), IsIso.hom_inv_id, ← Q.map_comp, IsSplitMono.id, Q.map_id]
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
I : C
inst_3 : Injective.{v, u} I
K : CochainComplex.{v, u, 0} C ℤ
i n : ℤ
hn : i < n
inst_4 : K.IsStrictlyGE n
L : CochainComplex.{v, u, 0} C ℤ
w : L.IsStrictlyGE i
g : K ⟶ L
ι : Functor.obj (CochainComplex.singleFunctor C i) I ⟶ L
h :
  IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C i) I))
    (CategoryTheory.Functor.map Q ι)
hπ : IsSplitMono ι
h₁ :
  Eq.{w + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q L)
      (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C i) I)))
    (inv (CategoryTheory.Functor.map Q ι)) (CategoryTheory.Functor.map Q (retraction ι))
hfg : (g ≫ retraction ι).f i = HomologicalComplex.Hom.f 0 i
⊢ g ≫ retraction ι = 0

Tactic:
apply HomologicalComplex.to_single_hom_ext

Premises used: HomologicalComplex.to_single_hom_ext
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
I : C
inst_3 : Injective.{v, u} I
K : CochainComplex.{v, u, 0} C ℤ
i n : ℤ
hn : i < n
inst_4 : K.IsStrictlyGE n
L : CochainComplex.{v, u, 0} C ℤ
w : L.IsStrictlyGE i
g : K ⟶ L
ι : Functor.obj (CochainComplex.singleFunctor C i) I ⟶ L
h :
  IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C i) I))
    (CategoryTheory.Functor.map Q ι)
hπ : IsSplitMono ι
h₁ :
  Eq.{w + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q L)
      (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C i) I)))
    (inv (CategoryTheory.Functor.map Q ι)) (CategoryTheory.Functor.map Q (retraction ι))
⊢ (g ≫ retraction ι).f i = HomologicalComplex.Hom.f 0 i

Tactic:
apply (K.isZero_of_isStrictlyGE n i hn).eq_of_src

Premises used: CochainComplex.isZero_of_isStrictlyGE, CategoryTheory.Limits.IsZero.eq_of_src
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
I : C
inst_3 : Injective.{v, u} I
K : CochainComplex.{v, u, 0} C ℤ
i n : ℤ
hn : i < n
inst_4 : K.IsStrictlyGE n
L : CochainComplex.{v, u, 0} C ℤ
w : L.IsStrictlyGE i
g : K ⟶ L
ι : Functor.obj (CochainComplex.singleFunctor C i) I ⟶ L
h :
  IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C i) I))
    (CategoryTheory.Functor.map Q ι)
hπ : IsSplitMono ι
h₁ :
  Eq.{w + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q L)
      (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C i) I)))
    (inv (CategoryTheory.Functor.map Q ι)) (CategoryTheory.Functor.map Q (retraction ι))
⊢ g ≫ retraction ι = 0

Tactic:
have h₂ : g ≫ retraction ι = 0 := by
    apply HomologicalComplex.to_single_hom_ext
    apply (K.isZero_of_isStrictlyGE n i hn).eq_of_src