awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
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) ≫ 𝟙 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)
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)
⊢ 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) ≫ 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)
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)
⊢ Hom.f (ι ≫ mkHomToSingle (Injective.factorThru (𝟙 I) α) ⋯) i = Hom.f (𝟙 (Functor.obj (singleFunctor C i) I)) i
have 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))
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
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
⊢ φ = 0
have 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
Tactic: obtain ⟨L, _, g, ι, h, rfl⟩ := left_fac_of_isStrictlyGE φ i
Cleared hypotheses: φ
-- 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
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 ι
have h₁ : QuasiIso ι
Tactic: rw [isIso_Q_map_iff_quasiIso] at h
Cleared hypotheses: h
-- 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
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 ι)
⊢ 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
have hπ : IsSplitMono ι
Tactic: have hπ : IsSplitMono ι := by
    rw [isIso_Q_map_iff_quasiIso] at h
    exact CochainComplex.isSplitMono_from_singleFunctor_obj_of_injective ι
-- 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
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 ι))
have 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 ι))
Tactic: rw [← cancel_epi (Q.map ι), IsIso.hom_inv_id, ← Q.map_comp, IsSplitMono.id, Q.map_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
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 ι))
⊢ 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 ι))
have 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 ι))
Tactic: rw [← cancel_epi (Q.map ι), IsIso.hom_inv_id, ← Q.map_comp, IsSplitMono.id, Q.map_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
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 ι))
⊢ 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 ι))
have 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 ι))
Tactic: rw [← cancel_epi (Q.map ι), IsIso.hom_inv_id, ← Q.map_comp, IsSplitMono.id, Q.map_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
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 ι))
⊢ 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 ι))
have 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)))
Tactic: rw [← cancel_epi (Q.map ι), IsIso.hom_inv_id, ← Q.map_comp, IsSplitMono.id, Q.map_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
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)))
⊢ 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 ι))
have 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)))
Tactic: rw [← cancel_epi (Q.map ι), IsIso.hom_inv_id, ← Q.map_comp, IsSplitMono.id, Q.map_id]
-- 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
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 K)
      (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C i) I)))
    (CategoryTheory.Functor.map Q g ≫ inv (CategoryTheory.Functor.map Q ι)) 0
have 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 ι))
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]
-- 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
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
have hfg : (g ≫ retraction ι).f i = HomologicalComplex.Hom.f 0 i
Tactic: apply HomologicalComplex.to_single_hom_ext
-- 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
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 ι))
⊢ 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
have h₂ : 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
-- 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
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 ι))
h₂ : g ≫ retraction ι = 0
⊢ 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
have rw : 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 ≫ CategoryTheory.Functor.map Q (retraction ι)) 0
Tactic: rw [h₁, ← Q.map_comp, h₂, Q.map_zero]