awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives
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)
⊢ Eq (α := P ⟶ K.X (i + 1)) (Projective.factorThru (𝟙 P) α ≫ K.d i (i + 1)) 0

Tactic:
apply (K.isZero_of_isStrictlyLE i (i + 1) (by simp)).eq_of_tgt

Premises used: CochainComplex.isZero_of_isStrictlyLE, HAdd.hAdd, CategoryTheory.Limits.IsZero.eq_of_tgt, OfNat.ofNat
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives
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)
hfg : Hom.f (mkHomFromSingle (Projective.factorThru (𝟙 P) α) ⋯ ≫ π) i = Hom.f (𝟙 (Functor.obj (singleFunctor C i) P)) i
⊢ mkHomFromSingle (Projective.factorThru (𝟙 P) α) ⋯ ≫ π = 𝟙 (Functor.obj (singleFunctor C i) P)

Tactic:
apply HomologicalComplex.from_single_hom_ext

Premises used: HomologicalComplex.from_single_hom_ext
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives
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)
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))
⊢ Hom.f (mkHomFromSingle (Projective.factorThru (𝟙 P) α) ⋯ ≫ π) i = Hom.f (𝟙 (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]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Projective.factorThru_comp_assoc, HomologicalComplex.id_f, CategoryTheory.Iso.hom_inv_id, HomologicalComplex.comp_f, HomologicalComplex.mkHomFromSingle_f, CategoryTheory.Category.id_comp
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives
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)
⊢ 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:
rfl
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives
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)
⊢ IsSplitEpi π

Tactic:
exact ⟨⟨{
    section_ := mkHomFromSingle (Projective.factorThru (𝟙 P) α) (by
      rintro _ rfl
      apply (K.isZero_of_isStrictlyLE i (i + 1) (by simp)).eq_of_tgt)
    id := by
      apply HomologicalComplex.from_single_hom_ext
      rw [comp_f, mkHomFromSingle_f, assoc, id_f, this, Projective.factorThru_comp_assoc,
        id_comp, Iso.hom_inv_id]
      rfl }⟩⟩
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives
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
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
⊢ φ = 0

Tactic:
obtain ⟨K, _, π, h, g, rfl⟩ := right_fac_of_isStrictlyLE φ i

Premises used: DerivedCategory.right_fac_of_isStrictlyLE, rfl
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives
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
rw : ∀ (h : QuasiIso π) (g : K ⟶ L), IsSplitEpi π
⊢ IsSplitEpi π

Tactic:
rw [isIso_Q_map_iff_quasiIso] at h

Premises used: DerivedCategory.isIso_Q_map_iff_quasiIso
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives
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 : QuasiIso π
g : K ⟶ L
⊢ IsSplitEpi π

Tactic:
CochainComplex.isSplitEpi_to_singleFunctor_obj_of_projective π

Premises used: CochainComplex.isSplitEpi_to_singleFunctor_obj_of_projective
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives
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 : QuasiIso π
g : K ⟶ L
⊢ IsSplitEpi π

Tactic:
exact CochainComplex.isSplitEpi_to_singleFunctor_obj_of_projective π

Premises used: CochainComplex.isSplitEpi_to_singleFunctor_obj_of_projective
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives
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 π

Tactic:
have hπ : IsSplitEpi π := by
    rw [isIso_Q_map_iff_quasiIso] at h
    exact CochainComplex.isSplitEpi_to_singleFunctor_obj_of_projective π
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives
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)))
rw₄ 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)))
⊢ 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:
rw [← cancel_mono (Q.map π), IsIso.inv_hom_id, ← Q.map_comp, IsSplitEpi.id, Q.map_id]

Premises used: DerivedCategory.Q, CategoryTheory.IsIso.inv_hom_id, CategoryTheory.IsSplitEpi.id, CategoryTheory.cancel_mono, CategoryTheory.Functor.map, CategoryTheory.Functor.map_id, CategoryTheory.Functor.map_comp
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives
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_ π))

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]
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives
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_ π))
hfg : (section_ π ≫ g).f i = HomologicalComplex.Hom.f 0 i
⊢ section_ π ≫ g = 0

Tactic:
apply HomologicalComplex.from_single_hom_ext

Premises used: HomologicalComplex.from_single_hom_ext
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives
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).f i = HomologicalComplex.Hom.f 0 i

Tactic:
apply (L.isZero_of_isStrictlyLE n i hn).eq_of_tgt

Premises used: CochainComplex.isZero_of_isStrictlyLE, CategoryTheory.Limits.IsZero.eq_of_tgt
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives
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

Tactic:
have h₂ : section_ π ≫ g = 0 := by
    apply HomologicalComplex.from_single_hom_ext
    apply (L.isZero_of_isStrictlyLE n i hn).eq_of_tgt
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives
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
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
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 0) 0
rw₃ 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))
    0 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

Tactic:
rw [h₁, ← Q.map_comp, h₂, Q.map_zero]

Premises used: DerivedCategory.Q, CategoryTheory.Functor.map_zero, CategoryTheory.Functor.map_comp
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
P Y : C
n : ℕ
inst_3 : Projective.{v, u} P
e : Ext.{w, v, u} P Y (n + 1)
this : HasDerivedCategory C := HasDerivedCategory.standard C
a :
  Eq (α :=
    ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (singleFunctor C 0) P) (Functor.obj (singleFunctor C 0) Y)
      (↑(n + 1) : ℤ))
    ((homEquiv :
          (a : Ext P Y (n + 1)) → ShiftedHom ((singleFunctor C 0).obj P) ((singleFunctor C 0).obj Y) (↑(n + 1) : ℤ))
        e :
      ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (singleFunctor C 0) P)
        (Functor.obj (singleFunctor C 0) Y) (↑(n + 1) : ℤ))
    ((homEquiv :
          (a : Ext P Y (n + 1)) → ShiftedHom ((singleFunctor C 0).obj P) ((singleFunctor C 0).obj Y) (↑(n + 1) : ℤ))
        0 :
      ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (singleFunctor C 0) P)
        (Functor.obj (singleFunctor C 0) Y) (↑(n + 1) : ℤ))
⊢ e = 0

Tactic:
apply homEquiv.injective

Premises used: CategoryTheory.Abelian.Ext.homEquiv, Equiv.injective
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
P Y : C
n : ℕ
inst_3 : Projective.{v, u} P
e : Ext.{w, v, u} P Y (n + 1)
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + -HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 = 0

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
P Y : C
n : ℕ
inst_3 : Projective.{v, u} P
e : Ext.{w, v, u} P Y (n + 1)
this : HasDerivedCategory C := HasDerivedCategory.standard C
a :
  Eq (α :=
    Quiver.Hom (V := DerivedCategory C) (Functor.obj (singleFunctor C 0) P)
      (Functor.obj (SingleFunctors.functor (singleFunctors C) (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) Y))
    ((homEquiv :
            (a : Ext P Y (n + 1)) → ShiftedHom ((singleFunctor C 0).obj P) ((singleFunctor C 0).obj Y) (↑(n + 1) : ℤ))
          e ≫
        NatTrans.app
          (Iso.hom
            (SingleFunctors.shiftIso (singleFunctors C) (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)
              0 ⋯))
          Y :
      Quiver.Hom (V := DerivedCategory C) (Functor.obj (singleFunctor C 0) P)
        (Functor.obj (SingleFunctors.functor (singleFunctors C) (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) Y))
    (0 :
      Quiver.Hom (V := DerivedCategory C) (Functor.obj (singleFunctor C 0) P)
        (Functor.obj (SingleFunctors.functor (singleFunctors C) (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) Y))
⊢ Eq (α :=
    ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (singleFunctor C 0) P) (Functor.obj (singleFunctor C 0) Y)
      (↑(n + 1) : ℤ))
    ((homEquiv :
          (a : Ext P Y (n + 1)) → ShiftedHom ((singleFunctor C 0).obj P) ((singleFunctor C 0).obj Y) (↑(n + 1) : ℤ))
        e :
      ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (singleFunctor C 0) P)
        (Functor.obj (singleFunctor C 0) Y) (↑(n + 1) : ℤ))
    ((homEquiv :
          (a : Ext P Y (n + 1)) → ShiftedHom ((singleFunctor C 0).obj P) ((singleFunctor C 0).obj Y) (↑(n + 1) : ℤ))
        0 :
      ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (singleFunctor C 0) P)
        (Functor.obj (singleFunctor C 0) Y) (↑(n + 1) : ℤ))

Tactic:
simp only [← cancel_mono (((singleFunctors C).shiftIso (n + 1) (-(n + 1)) 0
    (by lia)).hom.app _), zero_hom, Limits.zero_comp]

Premises used: DerivedCategory.singleFunctors, CategoryTheory.cancel_mono, Nat.cast, CategoryTheory.Abelian.Ext.zero_hom, HAdd.hAdd, CategoryTheory.SingleFunctors.shiftIso, CategoryTheory.Limits.zero_comp, OfNat.ofNat, CategoryTheory.Iso.hom, CategoryTheory.NatTrans.app, Neg.neg
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
P Y : C
n : ℕ
inst_3 : Projective.{v, u} P
e : Ext.{w, v, u} P Y (n + 1)
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ -HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 < 0

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
P Y : C
n : ℕ
inst_3 : Projective.{v, u} P
e : Ext.{w, v, u} P Y (n + 1)
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ Eq (α :=
    Quiver.Hom (V := DerivedCategory C) (Functor.obj (singleFunctor C 0) P)
      (Functor.obj (SingleFunctors.functor (singleFunctors C) (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) Y))
    ((homEquiv :
            (a : Ext P Y (n + 1)) → ShiftedHom ((singleFunctor C 0).obj P) ((singleFunctor C 0).obj Y) (↑(n + 1) : ℤ))
          e ≫
        NatTrans.app
          (Iso.hom
            (SingleFunctors.shiftIso (singleFunctors C) (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)
              0 ⋯))
          Y :
      Quiver.Hom (V := DerivedCategory C) (Functor.obj (singleFunctor C 0) P)
        (Functor.obj (SingleFunctors.functor (singleFunctors C) (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) Y))
    (0 :
      Quiver.Hom (V := DerivedCategory C) (Functor.obj (singleFunctor C 0) P)
        (Functor.obj (SingleFunctors.functor (singleFunctors C) (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) Y))

Tactic:
apply from_singleFunctor_obj_eq_zero_of_projective
    (L := (CochainComplex.singleFunctor C (-(n + 1))).obj Y) (n := -(n + 1)) _ (by lia)

Premises used: Nat.cast, HAdd.hAdd, DerivedCategory.from_singleFunctor_obj_eq_zero_of_projective, OfNat.ofNat, Neg.neg
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
P Y : C
inst_3 : Projective.{v, u} P
n : ℕ
⊢ Subsingleton.{w + 1} (Ext.{w, v, u} P Y (n + 1))

Tactic:
subsingleton_of_forall_eq 0 Ext.eq_zero_of_projective

Premises used: subsingleton_of_forall_eq, CategoryTheory.Abelian.Ext.eq_zero_of_projective, OfNat.ofNat
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : LocallySmall.{w, v, u} C
inst_3 : EnoughProjectives.{v, u} C
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ HasExt C

Tactic:
have := hasExt_of_hasDerivedCategory C
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : LocallySmall.{w, v, u} C
inst_3 : EnoughProjectives.{v, u} C
this_1 : HasDerivedCategory C := HasDerivedCategory.standard C
this : HasExt C
X Y : C
zero : Small.{w, v} (X ⟶ Y)
⊢ Small.{w, max u v} (Ext X Y 0)

Tactic:
rw [small_congr Ext.homEquiv₀]

Premises used: small_congr, CategoryTheory.Abelian.Ext.homEquiv₀