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
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
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
⊢ 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 ≫ retraction ι)) 0
Tactic: rw [h₁, ← Q.map_comp, h₂, Q.map_zero]
-- 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
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
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 ≫ 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 0) 0
Tactic: rw [h₁, ← Q.map_comp, h₂, Q.map_zero]
-- 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
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
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 ≫ retraction ι)) 0
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 0) 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)))
  0 0
Tactic: rw [h₁, ← Q.map_comp, h₂, Q.map_zero]
-- 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 : HasExt.{w, v, u} C
X I : C
n : ℕ
inst_3 : Injective.{v, u} I
e : Ext.{w, v, u} X I (n + 1)
K : CochainComplex.{v, u, 0} C ℤ := Functor.obj (CochainComplex.singleFunctor C 0) X
⊢ e = 0
have this : K.IsStrictlyGE (-(↑n : ℤ))
Tactic: have := K.isStrictlyGE_of_ge (-n) 0 (by lia)
-- 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 : HasExt.{w, v, u} C
X I : C
n : ℕ
inst_3 : Injective.{v, u} I
e : Ext.{w, v, u} X I (n + 1)
K : CochainComplex.{v, u, 0} C ℤ := Functor.obj (CochainComplex.singleFunctor C 0) X
this_1 : K.IsStrictlyGE (-(↑n : ℤ))
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ e = 0
have a : Eq (α :=
  ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (singleFunctor C 0) X) (Functor.obj (singleFunctor C 0) I)
    (↑(n + 1) : ℤ))
  ((homEquiv :
        (a : Ext X I (n + 1)) → ShiftedHom ((singleFunctor C 0).obj X) ((singleFunctor C 0).obj I) (↑(n + 1) : ℤ))
      e :
    ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (singleFunctor C 0) X) (Functor.obj (singleFunctor C 0) I)
      (↑(n + 1) : ℤ))
  ((homEquiv :
        (a : Ext X I (n + 1)) → ShiftedHom ((singleFunctor C 0).obj X) ((singleFunctor C 0).obj I) (↑(n + 1) : ℤ))
      0 :
    ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (singleFunctor C 0) X) (Functor.obj (singleFunctor C 0) I)
      (↑(n + 1) : ℤ))
Tactic: apply homEquiv.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 : HasExt.{w, v, u} C
X I : C
n : ℕ
inst_3 : Injective.{v, u} I
e : Ext.{w, v, u} X I (n + 1)
K : CochainComplex.{v, u, 0} C ℤ := Functor.obj (CochainComplex.singleFunctor C 0) X
this_1 : K.IsStrictlyGE (-(↑n : ℤ))
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ Eq (α :=
    ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (singleFunctor C 0) X) (Functor.obj (singleFunctor C 0) I)
      (↑(n + 1) : ℤ))
    ((homEquiv :
          (a : Ext X I (n + 1)) → ShiftedHom ((singleFunctor C 0).obj X) ((singleFunctor C 0).obj I) (↑(n + 1) : ℤ))
        e :
      ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (singleFunctor C 0) X)
        (Functor.obj (singleFunctor C 0) I) (↑(n + 1) : ℤ))
    ((homEquiv :
          (a : Ext X I (n + 1)) → ShiftedHom ((singleFunctor C 0).obj X) ((singleFunctor C 0).obj I) (↑(n + 1) : ℤ))
        0 :
      ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (singleFunctor C 0) X)
        (Functor.obj (singleFunctor C 0) I) (↑(n + 1) : ℤ))
have a : Eq (α :=
  Quiver.Hom (V := DerivedCategory C) (Functor.obj (singleFunctor C 0) X)
    (Functor.obj (SingleFunctors.functor (singleFunctors C) (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) I))
  ((homEquiv :
          (a : Ext X I (n + 1)) → ShiftedHom ((singleFunctor C 0).obj X) ((singleFunctor C 0).obj I) (↑(n + 1) : ℤ))
        e ≫
      NatTrans.app
        (Iso.hom
          (SingleFunctors.shiftIso (singleFunctors C) (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) 0
            sorry))
        I :
    Quiver.Hom (V := DerivedCategory C) (Functor.obj (singleFunctor C 0) X)
      (Functor.obj (SingleFunctors.functor (singleFunctors C) (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) I))
  (0 :
    Quiver.Hom (V := DerivedCategory C) (Functor.obj (singleFunctor C 0) X)
      (Functor.obj (SingleFunctors.functor (singleFunctors C) (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) I))
Tactic: simp only [← cancel_mono (((singleFunctors C).shiftIso (n + 1) (-(n + 1)) 0
    (by lia)).hom.app _), zero_hom, Limits.zero_comp]
-- 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 : LocallySmall.{w, v, u} C
inst_3 : EnoughInjectives.{v, u} C
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ HasExt.{w, v, u} C
have this₁ : HasExt C
Tactic: have := hasExt_of_hasDerivedCategory C
-- 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 : LocallySmall.{w, v, u} C
inst_3 : EnoughInjectives.{v, u} C
this_1 : HasDerivedCategory C := HasDerivedCategory.standard C
this : HasExt C
⊢ HasExt.{w, v, u} C
have rw : ∀ (X Y : C) (n : ℕ), Small.{w, max u v} (Ext X Y n)
Tactic: rw [hasExt_iff_small_ext.{w}]
-- 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 : LocallySmall.{w, v, u} C
inst_3 : EnoughInjectives.{v, u} C
this_1 : HasDerivedCategory C := HasDerivedCategory.standard C
this : HasExt C
X Y : C
⊢ Small.{w, max u v} (Ext X Y 0)
have zero : Small.{w, v} (X ⟶ Y)
Tactic: rw [small_congr Ext.homEquiv₀]
-- 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 : LocallySmall.{w, v, u} C
inst_3 : EnoughInjectives.{v, u} C
this_1 : HasDerivedCategory C := HasDerivedCategory.standard C
this : HasExt C
n : ℕ
hn : ∀ (X Y : C), Small.{w, max u v} (Ext X Y n)
X Y : C
S : ShortComplex.{v, u} C :=
  ShortComplex.mk (X₂ := Injective.under.{v, u} Y) (X₃ :=
    cokernel.{v, u} (Y := Injective.under.{v, u} Y) (Injective.ι Y)) (Injective.ι Y) (cokernel.π (Injective.ι Y)) ⋯
⊢ Small.{w, max u v} (Ext X Y (n + 1))
have hS : S.ShortExact
Tactic: have hS : S.ShortExact :=
        { exact := ShortComplex.exact_of_g_is_cokernel _ (cokernelIsCokernel S.f) }
-- 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 : LocallySmall.{w, v, u} C
inst_3 : EnoughInjectives.{v, u} C
this_1 : HasDerivedCategory C := HasDerivedCategory.standard C
this : HasExt C
n : ℕ
hn : ∀ (X Y : C), Small.{w, max u v} (Ext X Y n)
X Y : C
S : ShortComplex.{v, u} C :=
  ShortComplex.mk (X₂ := Injective.under.{v, u} Y) (X₃ :=
    cokernel.{v, u} (Y := Injective.under.{v, u} Y) (Injective.ι Y)) (Injective.ι Y) (cokernel.π (Injective.ι Y)) ⋯
hS : S.ShortExact
⊢ Small.{w, max u v} (Ext X Y (n + 1))
have this₁ : Function.Surjective (α := Ext X S.X₃ n) (β := Ext X S.X₁ (n + 1))
  (⇑(Ext.postcomp hS.extClass X sorry) : (a : Ext X S.X₃ n) → Ext X S.X₁ (n + 1))
Tactic: have : Function.Surjective (Ext.postcomp hS.extClass X (rfl : n + 1 = _)) :=
        fun y₁ ↦ Ext.covariant_sequence_exact₁ X hS y₁ (Ext.eq_zero_of_injective _) rfl
-- 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 : LocallySmall.{w, v, u} C
inst_3 : EnoughInjectives.{v, u} C
this_1 : HasDerivedCategory C := HasDerivedCategory.standard C
this : HasExt C
X Y : C
n : ℕ
⊢ Small.{w, max u v} (Ext X Y n)
have zero : ∀ (X Y : C), Small.{w, max u v} (Ext X Y 0)
Tactic: induction n generalizing X Y with
    | zero =>
      rw [small_congr Ext.homEquiv₀]
      infer_instance
    | succ n hn =>
      let S := ShortComplex.mk _ _ (cokernel.condition (Injective.ι Y))
      have hS : S.ShortExact :=
        { exact := ShortComplex.exact_of_g_is_cokernel _ (cokernelIsCokernel S.f) }
      have : Function.Surjective (Ext.postcomp hS.extClass X (rfl : n + 1 = _)) :=
        fun y₁ ↦ Ext.covariant_sequence_exact₁ X hS y₁ (Ext.eq_zero_of_injective _) rfl
      exact small_of_surjective.{w} this
Cleared hypotheses: X, Y, n
-- 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 : LocallySmall.{w, v, u} C
inst_3 : EnoughInjectives.{v, u} C
this_1 : HasDerivedCategory C := HasDerivedCategory.standard C
this : HasExt C
X Y : C
n : ℕ
zero : ∀ (X Y : C), Small.{w, max u v} (Ext X Y 0)
⊢ Small.{w, max u v} (Ext X Y n)
have succ : ∀ (n : ℕ) (hn : ∀ (X Y : C), Small.{w, max u v} (Ext X Y n)) (X Y : C), Small.{w, max u v} (Ext X Y (n + 1))
Tactic: induction n generalizing X Y with
    | zero =>
      rw [small_congr Ext.homEquiv₀]
      infer_instance
    | succ n hn =>
      let S := ShortComplex.mk _ _ (cokernel.condition (Injective.ι Y))
      have hS : S.ShortExact :=
        { exact := ShortComplex.exact_of_g_is_cokernel _ (cokernelIsCokernel S.f) }
      have : Function.Surjective (Ext.postcomp hS.extClass X (rfl : n + 1 = _)) :=
        fun y₁ ↦ Ext.covariant_sequence_exact₁ X hS y₁ (Ext.eq_zero_of_injective _) rfl
      exact small_of_surjective.{w} this
Cleared hypotheses: X, Y, n
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P : C
inst_2 : Projective.{v, u} P
K : CochainComplex.{v, u, 0} C ℤ
i : ℤ
π : K ⟶ Functor.obj (singleFunctor C i) P
inst_3 : K.IsStrictlyLE i
inst_4 : QuasiIsoAt π i
e : cycles K i ≅ K.X i := iCyclesIso K i (i + 1) ⋯ ⋯
α : K.X i ⟶ P := e.inv ≫ homologyπ K i ≫ homologyMap π i ≫ Iso.hom (singleObjHomologySelfIso (ComplexShape.up ℤ) i P)
⊢ π.f i = α ≫ Iso.inv (singleObjXSelf (ComplexShape.up ℤ) i P)
have rw : e.hom ≫ π.f i = e.hom ≫ α ≫ Iso.inv (singleObjXSelf (ComplexShape.up ℤ) i P)
Tactic: rw [← cancel_epi e.hom]
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P : C
inst_2 : Projective.{v, u} P
K : CochainComplex.{v, u, 0} C ℤ
i : ℤ
π : K ⟶ Functor.obj (singleFunctor C i) P
inst_3 : K.IsStrictlyLE i
inst_4 : QuasiIsoAt π i
e : cycles K i ≅ K.X i := iCyclesIso K i (i + 1) ⋯ ⋯
α : K.X i ⟶ P := e.inv ≫ homologyπ K i ≫ homologyMap π i ≫ Iso.hom (singleObjHomologySelfIso (ComplexShape.up ℤ) i P)
⊢ e.hom ≫ π.f i = e.hom ≫ α ≫ Iso.inv (singleObjXSelf (ComplexShape.up ℤ) i P)
have dsimp : Eq (α := cycles K i ⟶ X.{v, u, 0} (Functor.obj (singleFunctor C i) P) i) (iCycles K i ≫ π.f i)
  (iCycles K i ≫
    CategoryStruct.comp (Y := cycles K i) (Iso.inv (iCyclesIso K i (i + 1) sorry sorry))
        (homologyπ K i ≫ homologyMap π i ≫ Iso.hom (singleObjHomologySelfIso (ComplexShape.up ℤ) i P)) ≫
      Iso.inv (singleObjXSelf (ComplexShape.up ℤ) i P))
Tactic: dsimp [α, e]
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P : C
inst_2 : Projective.{v, u} P
K : CochainComplex.{v, u, 0} C ℤ
i : ℤ
π : K ⟶ Functor.obj (singleFunctor C i) P
inst_3 : K.IsStrictlyLE i
inst_4 : QuasiIsoAt π i
e : cycles K i ≅ K.X i := iCyclesIso K i (i + 1) ⋯ ⋯
α : K.X i ⟶ P := e.inv ≫ homologyπ K i ≫ homologyMap π i ≫ Iso.hom (singleObjHomologySelfIso (ComplexShape.up ℤ) i P)
⊢ Eq (α := cycles K i ⟶ X.{v, u, 0} (Functor.obj (singleFunctor C i) P) i) (iCycles K i ≫ π.f i)
    (iCycles K i ≫
      CategoryStruct.comp (Y := cycles K i) (Iso.inv (iCyclesIso K i (i + 1) ⋯ ⋯))
          (homologyπ K i ≫ homologyMap π i ≫ Iso.hom (singleObjHomologySelfIso (ComplexShape.up ℤ) i P)) ≫
        Iso.inv (singleObjXSelf (ComplexShape.up ℤ) i P))
have rw : Eq (α := cycles K i ⟶ X.{v, u, 0} (Functor.obj (singleFunctor C i) P) i) (iCycles K i ≫ π.f i)
  (cyclesMap π i ≫
    homologyπ (Functor.obj (singleFunctor C i) P) i ≫
      Iso.hom (singleObjHomologySelfIso (ComplexShape.up ℤ) i P) ≫ Iso.inv (singleObjXSelf (ComplexShape.up ℤ) i P))
Tactic: rw [assoc, assoc, assoc, iCyclesIso_hom_inv_id_assoc,
      homologyπ_naturality_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P : C
inst_2 : Projective.{v, u} P
K : CochainComplex.{v, u, 0} C ℤ
i : ℤ
π : K ⟶ Functor.obj (singleFunctor C i) P
inst_3 : K.IsStrictlyLE i
inst_4 : QuasiIsoAt π i
e : cycles K i ≅ K.X i := iCyclesIso K i (i + 1) ⋯ ⋯
α : K.X i ⟶ P := e.inv ≫ homologyπ K i ≫ homologyMap π i ≫ Iso.hom (singleObjHomologySelfIso (ComplexShape.up ℤ) i P)
⊢ Eq (α := cycles K i ⟶ X.{v, u, 0} (Functor.obj (singleFunctor C i) P) i) (iCycles K i ≫ π.f i)
    (cyclesMap π i ≫
      homologyπ (Functor.obj (singleFunctor C i) P) i ≫
        Iso.hom (singleObjHomologySelfIso (ComplexShape.up ℤ) i P) ≫ Iso.inv (singleObjXSelf (ComplexShape.up ℤ) i P))
have dsimp : Eq (α := cycles K i ⟶ X.{v, u, 0} (Functor.obj (single C (ComplexShape.up ℤ) i) P) i) (iCycles K i ≫ π.f i)
  (cyclesMap π i ≫
    homologyπ (Functor.obj (single C (ComplexShape.up ℤ) i) P) i ≫
      Iso.hom (singleObjHomologySelfIso (ComplexShape.up ℤ) i P) ≫ Iso.inv (singleObjXSelf (ComplexShape.up ℤ) i P))
Tactic: dsimp [singleFunctor, singleFunctors]
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P : C
inst_2 : Projective.{v, u} P
K : CochainComplex.{v, u, 0} C ℤ
i : ℤ
π : K ⟶ Functor.obj (singleFunctor C i) P
inst_3 : K.IsStrictlyLE i
inst_4 : QuasiIsoAt π i
e : cycles K i ≅ K.X i := iCyclesIso K i (i + 1) ⋯ ⋯
α : K.X i ⟶ P := e.inv ≫ homologyπ K i ≫ homologyMap π i ≫ Iso.hom (singleObjHomologySelfIso (ComplexShape.up ℤ) i P)
⊢ Eq (α := cycles K i ⟶ X.{v, u, 0} (Functor.obj (single C (ComplexShape.up ℤ) i) P) i) (iCycles K i ≫ π.f i)
    (cyclesMap π i ≫
      homologyπ (Functor.obj (single C (ComplexShape.up ℤ) i) P) i ≫
        Iso.hom (singleObjHomologySelfIso (ComplexShape.up ℤ) i P) ≫ Iso.inv (singleObjXSelf (ComplexShape.up ℤ) i P))
have rw : Eq (α := cycles K i ⟶ X.{v, u, 0} (Functor.obj (single C (ComplexShape.up ℤ) i) P) i) (iCycles K i ≫ π.f i)
  (cyclesMap π i ≫
    Iso.hom (singleObjCyclesSelfIso (ComplexShape.up ℤ) i P) ≫ Iso.inv (singleObjXSelf (ComplexShape.up ℤ) i P))
Tactic: rw [homologyπ_singleObjHomologySelfIso_hom_assoc,
      ← singleObjCyclesSelfIso_inv_iCycles, Iso.hom_inv_id_assoc, ← cyclesMap_i]
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P : C
inst_2 : Projective.{v, u} P
K : CochainComplex.{v, u, 0} C ℤ
i : ℤ
π : K ⟶ Functor.obj (singleFunctor C i) P
inst_3 : K.IsStrictlyLE i
inst_4 : QuasiIsoAt π i
e : cycles K i ≅ K.X i := iCyclesIso K i (i + 1) ⋯ ⋯
α : K.X i ⟶ P := e.inv ≫ homologyπ K i ≫ homologyMap π i ≫ Iso.hom (singleObjHomologySelfIso (ComplexShape.up ℤ) i P)
rw :
  Eq (α := cycles K i ⟶ X.{v, u, 0} (Functor.obj (single C (ComplexShape.up ℤ) i) P) i) (iCycles K i ≫ π.f i)
    (cyclesMap π i ≫
      Iso.hom (singleObjCyclesSelfIso (ComplexShape.up ℤ) i P) ≫ Iso.inv (singleObjXSelf (ComplexShape.up ℤ) i P))
⊢ Eq (α := cycles K i ⟶ X.{v, u, 0} (Functor.obj (single C (ComplexShape.up ℤ) i) P) i) (iCycles K i ≫ π.f i)
    (cyclesMap π i ≫
      homologyπ (Functor.obj (single C (ComplexShape.up ℤ) i) P) i ≫
        Iso.hom (singleObjHomologySelfIso (ComplexShape.up ℤ) i P) ≫ Iso.inv (singleObjXSelf (ComplexShape.up ℤ) i P))
have rw₁ : Eq (α := cycles K i ⟶ X.{v, u, 0} (Functor.obj (single C (ComplexShape.up ℤ) i) P) i) (iCycles K i ≫ π.f i)
  (cyclesMap π i ≫
    Iso.hom (singleObjCyclesSelfIso (ComplexShape.up ℤ) i P) ≫
      Iso.inv (singleObjCyclesSelfIso (ComplexShape.up ℤ) i P) ≫
        iCycles (Functor.obj (single C (ComplexShape.up ℤ) i) P) i)
Tactic: rw [homologyπ_singleObjHomologySelfIso_hom_assoc,
      ← singleObjCyclesSelfIso_inv_iCycles, Iso.hom_inv_id_assoc, ← cyclesMap_i]
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P : C
inst_2 : Projective.{v, u} P
K : CochainComplex.{v, u, 0} C ℤ
i : ℤ
π : K ⟶ Functor.obj (singleFunctor C i) P
inst_3 : K.IsStrictlyLE i
inst_4 : QuasiIsoAt π i
e : cycles K i ≅ K.X i := iCyclesIso K i (i + 1) ⋯ ⋯
α : K.X i ⟶ P := e.inv ≫ homologyπ K i ≫ homologyMap π i ≫ Iso.hom (singleObjHomologySelfIso (ComplexShape.up ℤ) i P)
rw :
  Eq (α := cycles K i ⟶ X.{v, u, 0} (Functor.obj (single C (ComplexShape.up ℤ) i) P) i) (iCycles K i ≫ π.f i)
    (cyclesMap π i ≫
      Iso.hom (singleObjCyclesSelfIso (ComplexShape.up ℤ) i P) ≫ Iso.inv (singleObjXSelf (ComplexShape.up ℤ) i P))
rw₁ :
  Eq (α := cycles K i ⟶ X.{v, u, 0} (Functor.obj (single C (ComplexShape.up ℤ) i) P) i) (iCycles K i ≫ π.f i)
    (cyclesMap π i ≫
      Iso.hom (singleObjCyclesSelfIso (ComplexShape.up ℤ) i P) ≫
        Iso.inv (singleObjCyclesSelfIso (ComplexShape.up ℤ) i P) ≫
          iCycles (Functor.obj (single C (ComplexShape.up ℤ) i) P) i)
⊢ Eq (α := cycles K i ⟶ X.{v, u, 0} (Functor.obj (single C (ComplexShape.up ℤ) i) P) i) (iCycles K i ≫ π.f i)
    (cyclesMap π i ≫
      homologyπ (Functor.obj (single C (ComplexShape.up ℤ) i) P) i ≫
        Iso.hom (singleObjHomologySelfIso (ComplexShape.up ℤ) i P) ≫ Iso.inv (singleObjXSelf (ComplexShape.up ℤ) i P))
have rw₂ : Eq (α := cycles K i ⟶ X.{v, u, 0} (Functor.obj (single C (ComplexShape.up ℤ) i) P) i) (iCycles K i ≫ π.f i)
  (CategoryStruct.comp (Y := cycles.{v, u, 0} (Functor.obj (single C (ComplexShape.up ℤ) i) P) i) (cyclesMap π i)
    (iCycles (Functor.obj (single C (ComplexShape.up ℤ) i) P) i))
Tactic: rw [homologyπ_singleObjHomologySelfIso_hom_assoc,
      ← singleObjCyclesSelfIso_inv_iCycles, Iso.hom_inv_id_assoc, ← cyclesMap_i]