awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
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))
⊢ 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)
  (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))
  (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]
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives (hypothesis)
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)
⊢ IsSplitEpi π
have this : π.f i = α ≫ Iso.inv (singleObjXSelf (ComplexShape.up ℤ) i P)
Tactic: have : π.f i = α ≫ (singleObjXSelf (ComplexShape.up ℤ) i P).inv := by
    rw [← cancel_epi e.hom]
    dsimp [α, e]
    rw [assoc, assoc, assoc, iCyclesIso_hom_inv_id_assoc,
      homologyπ_naturality_assoc]
    dsimp [singleFunctor, singleFunctors]
    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)
this : π.f i = α ≫ Iso.inv (singleObjXSelf (ComplexShape.up ℤ) i P)
⊢ mkHomFromSingle (Projective.factorThru (𝟙 P) α) ⋯ ≫ π = 𝟙 (Functor.obj (singleFunctor C i) P)
have hfg : Hom.f (mkHomFromSingle (Projective.factorThru (𝟙 P) α) sorry ≫ π) i = Hom.f (𝟙 (Functor.obj (singleFunctor C i) P)) i
Tactic: apply HomologicalComplex.from_single_hom_ext
-- 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)
this : π.f i = α ≫ Iso.inv (singleObjXSelf (ComplexShape.up ℤ) i P)
⊢ Hom.f (mkHomFromSingle (Projective.factorThru (𝟙 P) α) ⋯ ≫ π) i = Hom.f (𝟙 (Functor.obj (singleFunctor C i) P)) i
have hfg : Eq.{v + 1} (α :=
  X.{v, u, 0} (Functor.obj (single C (ComplexShape.up ℤ) i) P) i ⟶ X.{v, u, 0} (Functor.obj (singleFunctor C i) P) i)
  (𝟙 (X.{v, u, 0} (Functor.obj (single C (ComplexShape.up ℤ) i) P) i))
  (𝟙 (X.{v, u, 0} (Functor.obj (singleFunctor C i) P) i))
Tactic: rw [comp_f, mkHomFromSingle_f, assoc, id_f, this, Projective.factorThru_comp_assoc,
        id_comp, Iso.hom_inv_id]
-- 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
inst_2 : HasDerivedCategory.{w, v, u} C
P : C
inst_3 : Projective.{v, u} P
L : CochainComplex.{v, u, 0} C ℤ
i : ℤ
φ :
  Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C i) P))
    (Functor.obj Q L)
n : ℤ
hn : n < i
inst_4 : L.IsStrictlyLE n
⊢ φ = 0
have obtain : ∀ (K : CochainComplex.{v, u, 0} C ℤ),
  K.IsStrictlyLE i →
    ∀ (π : K ⟶ Functor.obj (CochainComplex.singleFunctor C i) P)
      (h : IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q K) (CategoryTheory.Functor.map Q π))
      (g : K ⟶ L),
      Eq.{w + 1} (α :=
        Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C i) P))
          (Functor.obj Q L))
        (inv (CategoryTheory.Functor.map Q π) ≫ CategoryTheory.Functor.map Q g) 0
Tactic: obtain ⟨K, _, π, h, g, rfl⟩ := right_fac_of_isStrictlyLE φ i
Cleared hypotheses: φ
-- 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
inst_2 : HasDerivedCategory.{w, v, u} C
P : C
inst_3 : Projective.{v, u} P
L : CochainComplex.{v, u, 0} C ℤ
i n : ℤ
hn : n < i
inst_4 : L.IsStrictlyLE n
K : CochainComplex.{v, u, 0} C ℤ
w : K.IsStrictlyLE i
π : K ⟶ Functor.obj (CochainComplex.singleFunctor C i) P
h : IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q K) (CategoryTheory.Functor.map Q π)
g : K ⟶ L
⊢ IsSplitEpi π
have rw : ∀ (h : QuasiIso π) (g : K ⟶ L), IsSplitEpi π
Tactic: rw [isIso_Q_map_iff_quasiIso] at h
Cleared hypotheses: h, g
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
P : C
inst_3 : Projective.{v, u} P
L : CochainComplex.{v, u, 0} C ℤ
i n : ℤ
hn : n < i
inst_4 : L.IsStrictlyLE n
K : CochainComplex.{v, u, 0} C ℤ
w : K.IsStrictlyLE i
π : K ⟶ Functor.obj (CochainComplex.singleFunctor C i) P
h : IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q K) (CategoryTheory.Functor.map Q π)
g : K ⟶ L
⊢ Eq.{w + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C i) P))
      (Functor.obj Q L))
    (inv (CategoryTheory.Functor.map Q π) ≫ CategoryTheory.Functor.map Q g) 0
have hπ : IsSplitEpi π
Tactic: have hπ : IsSplitEpi π := by
    rw [isIso_Q_map_iff_quasiIso] at h
    exact CochainComplex.isSplitEpi_to_singleFunctor_obj_of_projective π
-- 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
inst_2 : HasDerivedCategory.{w, v, u} C
P : C
inst_3 : Projective.{v, u} P
L : CochainComplex.{v, u, 0} C ℤ
i n : ℤ
hn : n < i
inst_4 : L.IsStrictlyLE n
K : CochainComplex.{v, u, 0} C ℤ
w : K.IsStrictlyLE i
π : K ⟶ Functor.obj (CochainComplex.singleFunctor C i) P
h : IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q K) (CategoryTheory.Functor.map Q π)
g : K ⟶ L
hπ : IsSplitEpi π
⊢ Eq.{w + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C i) P))
      (Functor.obj Q K))
    (inv (CategoryTheory.Functor.map Q π)) (CategoryTheory.Functor.map Q (section_ π))
have rw : Eq.{w + 1} (α :=
  Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C i) P))
    (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C i) P)))
  (inv (CategoryTheory.Functor.map Q π) ≫ CategoryTheory.Functor.map Q π)
  (CategoryTheory.Functor.map Q (section_ π) ≫ CategoryTheory.Functor.map Q π)
Tactic: rw [← cancel_mono (Q.map π), IsIso.inv_hom_id, ← Q.map_comp, IsSplitEpi.id, Q.map_id]
-- 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
inst_2 : HasDerivedCategory.{w, v, u} C
P : C
inst_3 : Projective.{v, u} P
L : CochainComplex.{v, u, 0} C ℤ
i n : ℤ
hn : n < i
inst_4 : L.IsStrictlyLE n
K : CochainComplex.{v, u, 0} C ℤ
w : K.IsStrictlyLE i
π : K ⟶ Functor.obj (CochainComplex.singleFunctor C i) P
h : IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q K) (CategoryTheory.Functor.map Q π)
g : K ⟶ L
hπ : IsSplitEpi π
rw :
  Eq.{w + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C i) P))
      (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C i) P)))
    (inv (CategoryTheory.Functor.map Q π) ≫ CategoryTheory.Functor.map Q π)
    (CategoryTheory.Functor.map Q (section_ π) ≫ CategoryTheory.Functor.map Q π)
⊢ Eq.{w + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C i) P))
      (Functor.obj Q K))
    (inv (CategoryTheory.Functor.map Q π)) (CategoryTheory.Functor.map Q (section_ π))
have rw₁ : Eq.{w + 1} (α :=
  Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C i) P))
    (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C i) P)))
  (𝟙 (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C i) P)))
  (CategoryTheory.Functor.map Q (section_ π) ≫ CategoryTheory.Functor.map Q π)
Tactic: rw [← cancel_mono (Q.map π), IsIso.inv_hom_id, ← Q.map_comp, IsSplitEpi.id, Q.map_id]
-- 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
inst_2 : HasDerivedCategory.{w, v, u} C
P : C
inst_3 : Projective.{v, u} P
L : CochainComplex.{v, u, 0} C ℤ
i n : ℤ
hn : n < i
inst_4 : L.IsStrictlyLE n
K : CochainComplex.{v, u, 0} C ℤ
w : K.IsStrictlyLE i
π : K ⟶ Functor.obj (CochainComplex.singleFunctor C i) P
h : IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q K) (CategoryTheory.Functor.map Q π)
g : K ⟶ L
hπ : IsSplitEpi π
rw :
  Eq.{w + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C i) P))
      (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C i) P)))
    (inv (CategoryTheory.Functor.map Q π) ≫ CategoryTheory.Functor.map Q π)
    (CategoryTheory.Functor.map Q (section_ π) ≫ CategoryTheory.Functor.map Q π)
rw₁ :
  Eq.{w + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C i) P))
      (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C i) P)))
    (𝟙 (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C i) P)))
    (CategoryTheory.Functor.map Q (section_ π) ≫ CategoryTheory.Functor.map Q π)
⊢ Eq.{w + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C i) P))
      (Functor.obj Q K))
    (inv (CategoryTheory.Functor.map Q π)) (CategoryTheory.Functor.map Q (section_ π))
have rw₂ : Eq.{w + 1} (α :=
  Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C i) P))
    (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C i) P)))
  (𝟙 (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C i) P))) (CategoryTheory.Functor.map Q (section_ π ≫ π))
Tactic: rw [← cancel_mono (Q.map π), IsIso.inv_hom_id, ← Q.map_comp, IsSplitEpi.id, Q.map_id]
-- 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
inst_2 : HasDerivedCategory.{w, v, u} C
P : C
inst_3 : Projective.{v, u} P
L : CochainComplex.{v, u, 0} C ℤ
i n : ℤ
hn : n < i
inst_4 : L.IsStrictlyLE n
K : CochainComplex.{v, u, 0} C ℤ
w : K.IsStrictlyLE i
π : K ⟶ Functor.obj (CochainComplex.singleFunctor C i) P
h : IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q K) (CategoryTheory.Functor.map Q π)
g : K ⟶ L
hπ : IsSplitEpi π
rw :
  Eq.{w + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C i) P))
      (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C i) P)))
    (inv (CategoryTheory.Functor.map Q π) ≫ CategoryTheory.Functor.map Q π)
    (CategoryTheory.Functor.map Q (section_ π) ≫ CategoryTheory.Functor.map Q π)
rw₁ :
  Eq.{w + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C i) P))
      (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C i) P)))
    (𝟙 (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C i) P)))
    (CategoryTheory.Functor.map Q (section_ π) ≫ CategoryTheory.Functor.map Q π)
rw₂ :
  Eq.{w + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C i) P))
      (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C i) P)))
    (𝟙 (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C i) P)))
    (CategoryTheory.Functor.map Q (section_ π ≫ π))
⊢ Eq.{w + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C i) P))
      (Functor.obj Q K))
    (inv (CategoryTheory.Functor.map Q π)) (CategoryTheory.Functor.map Q (section_ π))
have rw₃ : Eq.{w + 1} (α :=
  Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C i) P))
    (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C i) P)))
  (𝟙 (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C i) P)))
  (CategoryTheory.Functor.map Q (𝟙 (Functor.obj (CochainComplex.singleFunctor C i) P)))
Tactic: rw [← cancel_mono (Q.map π), IsIso.inv_hom_id, ← Q.map_comp, IsSplitEpi.id, Q.map_id]
-- 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
inst_2 : HasDerivedCategory.{w, v, u} C
P : C
inst_3 : Projective.{v, u} P
L : CochainComplex.{v, u, 0} C ℤ
i n : ℤ
hn : n < i
inst_4 : L.IsStrictlyLE n
K : CochainComplex.{v, u, 0} C ℤ
w : K.IsStrictlyLE i
π : K ⟶ Functor.obj (CochainComplex.singleFunctor C i) P
h : IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q K) (CategoryTheory.Functor.map Q π)
g : K ⟶ L
hπ : IsSplitEpi π
rw :
  Eq.{w + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C i) P))
      (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C i) P)))
    (inv (CategoryTheory.Functor.map Q π) ≫ CategoryTheory.Functor.map Q π)
    (CategoryTheory.Functor.map Q (section_ π) ≫ CategoryTheory.Functor.map Q π)
rw₁ :
  Eq.{w + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C i) P))
      (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C i) P)))
    (𝟙 (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C i) P)))
    (CategoryTheory.Functor.map Q (section_ π) ≫ CategoryTheory.Functor.map Q π)
rw₂ :
  Eq.{w + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C i) P))
      (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C i) P)))
    (𝟙 (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C i) P)))
    (CategoryTheory.Functor.map Q (section_ π ≫ π))
rw₃ :
  Eq.{w + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C i) P))
      (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C i) P)))
    (𝟙 (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C i) P)))
    (CategoryTheory.Functor.map Q (𝟙 (Functor.obj (CochainComplex.singleFunctor C i) P)))
⊢ Eq.{w + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C i) P))
      (Functor.obj Q K))
    (inv (CategoryTheory.Functor.map Q π)) (CategoryTheory.Functor.map Q (section_ π))
have rw₄ : Eq.{w + 1} (α :=
  Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C i) P))
    (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C i) P)))
  (𝟙 (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C i) P)))
  (𝟙 (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C i) P)))
Tactic: rw [← cancel_mono (Q.map π), IsIso.inv_hom_id, ← Q.map_comp, IsSplitEpi.id, Q.map_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
P : C
inst_3 : Projective.{v, u} P
L : CochainComplex.{v, u, 0} C ℤ
i n : ℤ
hn : n < i
inst_4 : L.IsStrictlyLE n
K : CochainComplex.{v, u, 0} C ℤ
w : K.IsStrictlyLE i
π : K ⟶ Functor.obj (CochainComplex.singleFunctor C i) P
h : IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q K) (CategoryTheory.Functor.map Q π)
g : K ⟶ L
hπ : IsSplitEpi π
⊢ Eq.{w + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C i) P))
      (Functor.obj Q L))
    (inv (CategoryTheory.Functor.map Q π) ≫ CategoryTheory.Functor.map Q g) 0
have h₁ : Eq.{w + 1} (α :=
  Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C i) P))
    (Functor.obj Q K))
  (inv (CategoryTheory.Functor.map Q π)) (CategoryTheory.Functor.map Q (section_ π))
Tactic: have h₁ : inv (Q.map π) = Q.map (section_ π) := by
    rw [← cancel_mono (Q.map π), IsIso.inv_hom_id, ← Q.map_comp, IsSplitEpi.id, Q.map_id]
-- 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
inst_2 : HasDerivedCategory.{w, v, u} C
P : C
inst_3 : Projective.{v, u} P
L : CochainComplex.{v, u, 0} C ℤ
i n : ℤ
hn : n < i
inst_4 : L.IsStrictlyLE n
K : CochainComplex.{v, u, 0} C ℤ
w : K.IsStrictlyLE i
π : K ⟶ Functor.obj (CochainComplex.singleFunctor C i) P
h : IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q K) (CategoryTheory.Functor.map Q π)
g : K ⟶ L
hπ : IsSplitEpi π
h₁ :
  Eq.{w + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C i) P))
      (Functor.obj Q K))
    (inv (CategoryTheory.Functor.map Q π)) (CategoryTheory.Functor.map Q (section_ π))
⊢ section_ π ≫ g = 0
have hfg : (section_ π ≫ g).f i = HomologicalComplex.Hom.f 0 i
Tactic: apply HomologicalComplex.from_single_hom_ext
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
P : C
inst_3 : Projective.{v, u} P
L : CochainComplex.{v, u, 0} C ℤ
i n : ℤ
hn : n < i
inst_4 : L.IsStrictlyLE n
K : CochainComplex.{v, u, 0} C ℤ
w : K.IsStrictlyLE i
π : K ⟶ Functor.obj (CochainComplex.singleFunctor C i) P
h : IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q K) (CategoryTheory.Functor.map Q π)
g : K ⟶ L
hπ : IsSplitEpi π
h₁ :
  Eq.{w + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C i) P))
      (Functor.obj Q K))
    (inv (CategoryTheory.Functor.map Q π)) (CategoryTheory.Functor.map Q (section_ π))
⊢ Eq.{w + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C i) P))
      (Functor.obj Q L))
    (inv (CategoryTheory.Functor.map Q π) ≫ CategoryTheory.Functor.map Q g) 0
have h₂ : section_ π ≫ g = 0
Tactic: have h₂ : section_ π ≫ g = 0 := by
    apply HomologicalComplex.from_single_hom_ext
    apply (L.isZero_of_isStrictlyLE n i hn).eq_of_tgt
-- 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
inst_2 : HasDerivedCategory.{w, v, u} C
P : C
inst_3 : Projective.{v, u} P
L : CochainComplex.{v, u, 0} C ℤ
i n : ℤ
hn : n < i
inst_4 : L.IsStrictlyLE n
K : CochainComplex.{v, u, 0} C ℤ
w : K.IsStrictlyLE i
π : K ⟶ Functor.obj (CochainComplex.singleFunctor C i) P
h : IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q K) (CategoryTheory.Functor.map Q π)
g : K ⟶ L
hπ : IsSplitEpi π
h₁ :
  Eq.{w + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C i) P))
      (Functor.obj Q K))
    (inv (CategoryTheory.Functor.map Q π)) (CategoryTheory.Functor.map Q (section_ π))
h₂ : section_ π ≫ g = 0
⊢ Eq.{w + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C i) P))
      (Functor.obj Q L))
    (inv (CategoryTheory.Functor.map Q π) ≫ CategoryTheory.Functor.map Q g) 0
have rw : Eq.{w + 1} (α :=
  Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C i) P))
    (Functor.obj Q L))
  (CategoryTheory.Functor.map Q (section_ π) ≫ CategoryTheory.Functor.map Q g) 0
Tactic: rw [h₁, ← Q.map_comp, h₂, Q.map_zero]
-- 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
inst_2 : HasDerivedCategory.{w, v, u} C
P : C
inst_3 : Projective.{v, u} P
L : CochainComplex.{v, u, 0} C ℤ
i n : ℤ
hn : n < i
inst_4 : L.IsStrictlyLE n
K : CochainComplex.{v, u, 0} C ℤ
w : K.IsStrictlyLE i
π : K ⟶ Functor.obj (CochainComplex.singleFunctor C i) P
h : IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q K) (CategoryTheory.Functor.map Q π)
g : K ⟶ L
hπ : IsSplitEpi π
h₁ :
  Eq.{w + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C i) P))
      (Functor.obj Q K))
    (inv (CategoryTheory.Functor.map Q π)) (CategoryTheory.Functor.map Q (section_ π))
h₂ : section_ π ≫ g = 0
rw :
  Eq.{w + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C i) P))
      (Functor.obj Q L))
    (CategoryTheory.Functor.map Q (section_ π) ≫ CategoryTheory.Functor.map Q g) 0
⊢ Eq.{w + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C i) P))
      (Functor.obj Q L))
    (inv (CategoryTheory.Functor.map Q π) ≫ CategoryTheory.Functor.map Q g) 0
have rw₁ : Eq.{w + 1} (α :=
  Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C i) P))
    (Functor.obj Q L))
  (CategoryTheory.Functor.map Q (section_ π ≫ g)) 0
Tactic: rw [h₁, ← Q.map_comp, h₂, Q.map_zero]