awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Preadditive.Projective.LiftingProperties
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
P Z : C
hZ : IsZero.{v, u} Z
mp : Projective.{v, u} P → MorphismProperty.llp.{v, u} (MorphismProperty.epimorphisms C) (X := Z) (Y := P) 0
mpr : MorphismProperty.llp.{v, u} (MorphismProperty.epimorphisms C) (X := Z) (Y := P) 0 → Projective.{v, u} P
⊢ Projective.{v, u} P ↔ MorphismProperty.llp.{v, u} (MorphismProperty.epimorphisms C) (X := Z) (Y := P) 0

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Preadditive.Projective.LiftingProperties
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
P Z : C
hZ : IsZero.{v, u} Z
h : Projective.{v, u} P
X Y : C
p : X ⟶ Y
mp : Epi p → HasLiftingProperty (A := Z) (B := P) 0 p
⊢ MorphismProperty.epimorphisms C p → HasLiftingProperty (A := Z) (B := P) 0 p

Tactic:
(_ : Epi p)
-- Module: Mathlib.CategoryTheory.Preadditive.Projective.LiftingProperties
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
P Z : C
hZ : IsZero.{v, u} Z
h : Projective.{v, u} P
X Y : C
p : X ⟶ Y
h_1 : Epi p
⊢ HasLiftingProperty (A := Z) (B := P) 0 p

Tactic:
Projective.hasLiftingProperty_of_isZero 0 p hZ

Premises used: CategoryTheory.Projective.hasLiftingProperty_of_isZero, OfNat.ofNat
-- Module: Mathlib.CategoryTheory.Preadditive.Projective.LiftingProperties
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
P Z : C
hZ : IsZero.{v, u} Z
h : Projective.{v, u} P
X Y : C
p : X ⟶ Y
h_1 : Epi p
⊢ HasLiftingProperty (A := Z) (B := P) 0 p

Tactic:
exact Projective.hasLiftingProperty_of_isZero 0 p hZ

Premises used: CategoryTheory.Projective.hasLiftingProperty_of_isZero, OfNat.ofNat
-- Module: Mathlib.CategoryTheory.Preadditive.Projective.LiftingProperties
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
P Z : C
hZ : IsZero.{v, u} Z
h : MorphismProperty.llp.{v, u} (MorphismProperty.epimorphisms C) (X := Z) (Y := P) 0
mpr : ∀ {E X : C} (f : P ⟶ X) (e : E ⟶ X) [Epi e], ∃ (f' : P ⟶ E), f' ≫ e = f
⊢ Projective.{v, u} P

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Preadditive.Projective.LiftingProperties
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
P Z : C
hZ : IsZero.{v, u} Z
h : MorphismProperty.llp.{v, u} (MorphismProperty.epimorphisms C) (X := Z) (Y := P) 0
X Y : C
f : P ⟶ Y
p : X ⟶ Y
hp : Epi p
⊢ HasLiftingProperty (A := Z) (B := P) 0 p

Tactic:
have := h _ hp
-- Module: Mathlib.CategoryTheory.Preadditive.Projective.LiftingProperties
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
P Z : C
hZ : IsZero.{v, u} Z
h : MorphismProperty.llp.{v, u} (MorphismProperty.epimorphisms C) (X := Z) (Y := P) 0
X Y : C
f : P ⟶ Y
p : X ⟶ Y
hp : Epi p
this : HasLiftingProperty (A := Z) (B := P) 0 p
⊢ Eq (α := Z ⟶ Y) (0 ≫ p) (0 ≫ f)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.Projective.LiftingProperties
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
P Z : C
hZ : IsZero.{v, u} Z
h : MorphismProperty.llp.{v, u} (MorphismProperty.epimorphisms C) (X := Z) (Y := P) 0
X Y : C
f : P ⟶ Y
p : X ⟶ Y
hp : Epi p
this : HasLiftingProperty (A := Z) (B := P) 0 p
⊢ CommSq (W := Z) 0 0 p f

Tactic:
have sq : CommSq 0 (0 : Z ⟶ P) p f := ⟨by simp⟩
-- Module: Mathlib.CategoryTheory.Preadditive.Projective.LiftingProperties
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
P Z : C
hZ : IsZero.{v, u} Z
h : MorphismProperty.llp.{v, u} (MorphismProperty.epimorphisms C) (X := Z) (Y := P) 0
X Y : C
f : P ⟶ Y
p : X ⟶ Y
hp : Epi p
this : HasLiftingProperty (A := Z) (B := P) 0 p
sq : CommSq (W := Z) 0 0 p f
⊢ sq.lift ≫ p = f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.Projective.LiftingProperties
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
P Z : C
hZ : IsZero.{v, u} Z
h : MorphismProperty.llp.{v, u} (MorphismProperty.epimorphisms C) (X := Z) (Y := P) 0
X Y : C
f : P ⟶ Y
p : X ⟶ Y
hp : Epi p
this : HasLiftingProperty (A := Z) (B := P) 0 p
sq : CommSq (W := Z) 0 0 p f
⊢ ∃ (f' : P ⟶ X), f' ≫ p = f

Tactic:
exact ⟨sq.lift, by simp⟩
-- Module: Mathlib.CategoryTheory.Preadditive.Projective.LiftingProperties
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasZeroObject.{v, u} C
P : C
⊢ Projective.{v, u} P ↔ MorphismProperty.llp.{v, u} (MorphismProperty.epimorphisms C) (X := 0) (Y := P) 0

Tactic:
projective_iff_llp_epimorphisms_of_isZero _ (isZero_zero C)

Premises used: CategoryTheory.projective_iff_llp_epimorphisms_of_isZero, CategoryTheory.Limits.isZero_zero
-- Module: Mathlib.CategoryTheory.Preadditive.Projective.Preserves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : F.PreservesProjectiveObjects
X : C
inst_4 : Projective.{v₁, u₁} X
⊢ Projective.{v₂, u₂} (F.obj X)

Tactic:
Functor.PreservesProjectiveObjects.projective_obj inferInstance

Premises used: inferInstance, CategoryTheory.Functor.PreservesProjectiveObjects.projective_obj
-- Module: Mathlib.CategoryTheory.Preadditive.Projective.Preserves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.PreservesProjectiveObjects
X : C
h : Projective.{v₁, u₁} X
⊢ Projective.{v₂, u₂} (F.obj X)

Tactic:
Functor.PreservesProjectiveObjects.projective_obj h

Premises used: CategoryTheory.Functor.PreservesProjectiveObjects.projective_obj
-- Module: Mathlib.CategoryTheory.Preadditive.Projective.Preserves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : F.IsEquivalence
⊢ F.PreservesProjectiveObjects

Tactic:
preservesProjectiveObjects_of_adjunction_of_preservesEpimorphisms F.asEquivalence.toAdjunction

Premises used: CategoryTheory.Functor.asEquivalence, CategoryTheory.Functor.preservesProjectiveObjects_of_adjunction_of_preservesEpimorphisms, CategoryTheory.Equivalence.toAdjunction
-- Module: Mathlib.CategoryTheory.Preadditive.Projective.Preserves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : EnoughProjectives.{v₁, u₁} C
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
inst_3 : F.PreservesProjectiveObjects
X Y : D
f : X ⟶ Y
h : Epi f
suffices : ∃ (h : Projective.over.{v₁, u₁} (G.obj Y) ⟶ G.obj X), h ≫ G.map f = Projective.π (G.obj Y)
⊢ Epi (G.map f)

Tactic:
suffices ∃ h, h ≫ G.map f = Projective.π (G.obj Y) from epi_of_epi_fac this.choose_spec
-- Module: Mathlib.CategoryTheory.Preadditive.Projective.Preserves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : EnoughProjectives.{v₁, u₁} C
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
inst_3 : F.PreservesProjectiveObjects
X Y : D
f : X ⟶ Y
h : Epi f
⊢ ∃ (h : Projective.over.{v₁, u₁} (G.obj Y) ⟶ G.obj X), h ≫ G.map f = Projective.π (G.obj Y)

Tactic:
⟨adj.unit.app (Projective.over (G.obj Y)) ≫
      G.map (Projective.factorThru (F.map (Projective.π _) ≫ adj.counit.app Y) f), ?_⟩

Premises used: CategoryTheory.Projective.over, CategoryTheory.Projective.factorThru, CategoryTheory.Projective.π, CategoryTheory.Adjunction.unit, CategoryTheory.Functor.map, CategoryTheory.Adjunction.counit, Exists.intro, CategoryTheory.CategoryStruct.comp, CategoryTheory.Functor.obj, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Preadditive.Projective.Preserves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : EnoughProjectives.{v₁, u₁} C
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
inst_3 : F.PreservesProjectiveObjects
X Y : D
f : X ⟶ Y
h : Epi f
refine :
  Eq (α := Projective.over.{v₁, u₁} (G.obj Y) ⟶ G.obj Y)
    ((adj.unit.app (Projective.over.{v₁, u₁} (G.obj Y)) ≫
          G.map (Projective.factorThru (F.map (Projective.π (G.obj Y)) ≫ adj.counit.app Y) f)) ≫
        G.map f :
      Projective.over.{v₁, u₁} (G.obj Y) ⟶ G.obj Y)
    (Projective.π (G.obj Y) : Projective.over.{v₁, u₁} (G.obj Y) ⟶ G.obj Y)
⊢ ∃ (h : Projective.over.{v₁, u₁} (G.obj Y) ⟶ G.obj X), h ≫ G.map f = Projective.π (G.obj Y)

Tactic:
refine ⟨adj.unit.app (Projective.over (G.obj Y)) ≫
      G.map (Projective.factorThru (F.map (Projective.π _) ≫ adj.counit.app Y) f), ?_⟩
-- Module: Mathlib.CategoryTheory.Preadditive.Projective.Preserves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : EnoughProjectives.{v₁, u₁} C
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
inst_3 : F.PreservesProjectiveObjects
X Y : D
f : X ⟶ Y
h : Epi f
rw :
  Eq (α := Projective.over.{v₁, u₁} (G.obj Y) ⟶ G.obj Y)
    (adj.unit.app (Projective.over.{v₁, u₁} (G.obj Y)) ≫
        G.map (Projective.factorThru (F.map (Projective.π (G.obj Y)) ≫ adj.counit.app Y) f ≫ f) :
      Projective.over.{v₁, u₁} (G.obj Y) ⟶ G.obj Y)
    (Projective.π (G.obj Y) : Projective.over.{v₁, u₁} (G.obj Y) ⟶ G.obj Y)
⊢ Eq (α := Projective.over.{v₁, u₁} (G.obj Y) ⟶ G.obj Y)
    ((adj.unit.app (Projective.over.{v₁, u₁} (G.obj Y)) ≫
          G.map (Projective.factorThru (F.map (Projective.π (G.obj Y)) ≫ adj.counit.app Y) f)) ≫
        G.map f :
      Projective.over.{v₁, u₁} (G.obj Y) ⟶ G.obj Y)
    (Projective.π (G.obj Y) : Projective.over.{v₁, u₁} (G.obj Y) ⟶ G.obj Y)

Tactic:
rw [Category.assoc, ← Functor.map_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Preadditive.Projective.Preserves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : EnoughProjectives.{v₁, u₁} C
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
inst_3 : F.PreservesProjectiveObjects
X Y : D
f : X ⟶ Y
h : Epi f
⊢ Eq (α := Projective.over.{v₁, u₁} (G.obj Y) ⟶ G.obj Y)
    (adj.unit.app (Projective.over.{v₁, u₁} (G.obj Y)) ≫
        G.map (Projective.factorThru (F.map (Projective.π (G.obj Y)) ≫ adj.counit.app Y) f ≫ f) :
      Projective.over.{v₁, u₁} (G.obj Y) ⟶ G.obj Y)
    (Projective.π (G.obj Y) : Projective.over.{v₁, u₁} (G.obj Y) ⟶ G.obj Y)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.Projective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
Z : C
P : ProjectiveResolution.{v, u} Z
n : ℕ
rw : QuasiIsoAt P.π (n + 1)
⊢ ExactAt P.complex (n + 1)

Tactic:
rw [← quasiIsoAt_iff_exactAt' P.π (n + 1) (exactAt_succ_single_obj _ _)]

Premises used: CategoryTheory.ProjectiveResolution.π, ChainComplex.exactAt_succ_single_obj, HAdd.hAdd, OfNat.ofNat, quasiIsoAt_iff_exactAt'
-- Module: Mathlib.CategoryTheory.Preadditive.Projective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
Z : C
P : ProjectiveResolution.{v, u} Z
n : ℕ
⊢ QuasiIsoAt P.π (n + 1)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Preadditive.Projective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
Z : C
P : ProjectiveResolution.{v, u} Z
n : ℕ
simp : n + 1 + 1 = n + 2
⊢ (ComplexShape.down ℕ).prev (n + 1) = n + 2

Tactic:
simp only [prev]

Premises used: ChainComplex.prev
-- Module: Mathlib.CategoryTheory.Preadditive.Projective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
Z : C
P : ProjectiveResolution.{v, u} Z
n : ℕ
⊢ n + 1 + 1 = n + 2

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Preadditive.Projective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
Z : C
P : ProjectiveResolution.{v, u} Z
n : ℕ
⊢ (ComplexShape.down ℕ).next (n + 1) = n

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.Projective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
Z : C
P : ProjectiveResolution.{v, u} Z
n : ℕ
⊢ n + 1 ≠ 0

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.Projective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
Z : C
P : ProjectiveResolution.{v, u} Z
rw :
  Eq (α := P.complex.X 1 ⟶ X.{v, u, 0} (Functor.obj (single₀ C) Z) 0)
    (P.π.f 1 ≫ HomologicalComplex.d (Functor.obj (single₀ C) Z) 1 0) 0
rw₁ : Eq (α := P.complex.X 1 ⟶ X.{v, u, 0} (Functor.obj (single₀ C) Z) 0) (P.π.f 1 ≫ 0) 0
rw₂ rw₃ : Eq.{v + 1} (α := P.complex.X 1 ⟶ X.{v, u, 0} (Functor.obj (single₀ C) Z) 0) 0 0
⊢ Eq (α := P.complex.X 1 ⟶ X.{v, u, 0} (Functor.obj (single₀ C) Z) 0) (P.complex.d 1 0 ≫ P.π.f 0) 0

Tactic:
rw [← P.π.comm 1 0, single_obj_d, comp_zero]

Premises used: CategoryTheory.ProjectiveResolution.π, HomologicalComplex.single_obj_d, CategoryTheory.Limits.comp_zero, OfNat.ofNat, HomologicalComplex.Hom.comm
-- Module: Mathlib.CategoryTheory.Preadditive.Projective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
Z : C
P : ProjectiveResolution.{v, u} Z
n : ℕ
⊢ Eq (α := P.complex.X n ⟶ P.complex.X (n + 2))
    (CategoryStruct.comp (Y := P.complex.X (n + 1)) (P.complex.d n (n + 1)) (P.complex.d (n + 1) (n + 2))) 0

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.Projective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
Z : C
P : ProjectiveResolution.{v, u} Z
⊢ (ComplexShape.down ℕ).prev 0 = 1

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.Projective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
Z : C
P : ProjectiveResolution.{v, u} Z
refine : CokernelCofork.ofπ (Z := opcycles P.complex 0) (pOpcycles P.complex 0) ⋯ ≅ P.cokernelCofork
⊢ IsColimit P.cokernelCofork

Tactic:
refine IsColimit.ofIsoColimit (P.complex.opcyclesIsCokernel 1 0 (by simp)) ?_

Premises used: CategoryTheory.Limits.IsColimit.ofIsoColimit, CategoryTheory.ProjectiveResolution.complex, HomologicalComplex.opcyclesIsCokernel, OfNat.ofNat
-- Module: Mathlib.CategoryTheory.Preadditive.Projective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
Z : C
P : ProjectiveResolution.{v, u} Z
refine :
  CategoryStruct.comp (Y :=
      Cocone.pt (F := parallelPair (X := P.complex.X 1) (Y := P.complex.X 0) (P.complex.d 1 0) 0)
        (CokernelCofork.ofπ (Z := opcycles P.complex 0) (pOpcycles P.complex 0) ⋯))
      (Cofork.π (CokernelCofork.ofπ (Z := opcycles P.complex 0) (pOpcycles P.complex 0) ⋯))
      (Iso.hom
        (Iso.trans (Y := homology P.complex 0) (Iso.symm P.complex.isoHomologyι₀)
          (isoOfQuasiIsoAt P.π 0 ≪≫ singleObjHomologySelfIso (ComplexShape.down ℕ) 0 Z))) =
    Cofork.π P.cokernelCofork
⊢ CokernelCofork.ofπ (Z := opcycles P.complex 0) (pOpcycles P.complex 0) ⋯ ≅ P.cokernelCofork

Tactic:
refine Cofork.ext (P.complex.isoHomologyι₀.symm ≪≫ isoOfQuasiIsoAt P.π 0 ≪≫
    singleObjHomologySelfIso _ _ _) ?_

Premises used: CategoryTheory.ProjectiveResolution.π, isoOfQuasiIsoAt, CategoryTheory.Iso.trans, CategoryTheory.Limits.Cofork.ext, OfNat.ofNat
-- Module: Mathlib.CategoryTheory.Preadditive.Projective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
Z : C
P : ProjectiveResolution.{v, u} Z
rw :
  Eq (α := P.complex.X 0 ⟶ opcycles.{v, u, 0} (Functor.obj (single C (ComplexShape.down ℕ) 0) P.cokernelCofork.pt) 0)
    ((CategoryStruct.comp (Y :=
          Cocone.pt (F := parallelPair (X := P.complex.X 1) (Y := P.complex.X 0) (P.complex.d 1 0) 0)
            (CokernelCofork.ofπ (Z := opcycles P.complex 0) (pOpcycles P.complex 0) ⋯))
          (Cofork.π (CokernelCofork.ofπ (Z := opcycles P.complex 0) (pOpcycles P.complex 0) ⋯))
          (Iso.hom
            (Iso.trans (Y := homology P.complex 0) (Iso.symm P.complex.isoHomologyι₀)
              (isoOfQuasiIsoAt P.π 0 ≪≫ singleObjHomologySelfIso (ComplexShape.down ℕ) 0 Z))) ≫
        Iso.inv (singleObjHomologySelfIso (ComplexShape.down ℕ) 0 P.cokernelCofork.pt)) ≫
      Iso.hom (isoHomologyι₀ (Functor.obj (single C (ComplexShape.down ℕ) 0) P.cokernelCofork.pt)))
    ((Cofork.π P.cokernelCofork ≫ Iso.inv (singleObjHomologySelfIso (ComplexShape.down ℕ) 0 P.cokernelCofork.pt)) ≫
      Iso.hom (isoHomologyι₀ (Functor.obj (single C (ComplexShape.down ℕ) 0) P.cokernelCofork.pt)))
⊢ CategoryStruct.comp (Y :=
      Cocone.pt (F := parallelPair (X := P.complex.X 1) (Y := P.complex.X 0) (P.complex.d 1 0) 0)
        (CokernelCofork.ofπ (Z := opcycles P.complex 0) (pOpcycles P.complex 0) ⋯))
      (Cofork.π (CokernelCofork.ofπ (Z := opcycles P.complex 0) (pOpcycles P.complex 0) ⋯))
      (Iso.hom
        (Iso.trans (Y := homology P.complex 0) (Iso.symm P.complex.isoHomologyι₀)
          (isoOfQuasiIsoAt P.π 0 ≪≫ singleObjHomologySelfIso (ComplexShape.down ℕ) 0 Z))) =
    Cofork.π P.cokernelCofork

Tactic:
rw [← cancel_mono (singleObjHomologySelfIso (ComplexShape.down ℕ) 0 _).inv,
    ← cancel_mono (isoHomologyι₀ _).hom]

Premises used: HomologicalComplex.singleObjHomologySelfIso, CategoryTheory.cancel_mono, ChainComplex.isoHomologyι₀, Nat, ComplexShape.down, OfNat.ofNat, CategoryTheory.Iso.hom, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.Preadditive.Projective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
Z : C
P : ProjectiveResolution.{v, u} Z
dsimp :
  Eq (α := P.complex.X 0 ⟶ opcycles.{v, u, 0} (Functor.obj (single C (ComplexShape.down ℕ) 0) Z) 0)
    ((CategoryStruct.comp (Y := opcycles P.complex 0) (pOpcycles P.complex 0)
          (Iso.inv P.complex.isoHomologyι₀ ≫
            homologyMap P.π 0 ≫ Iso.hom (singleObjHomologySelfIso (ComplexShape.down ℕ) 0 Z)) ≫
        Iso.inv (singleObjHomologySelfIso (ComplexShape.down ℕ) 0 Z)) ≫
      homologyι (Functor.obj (single C (ComplexShape.down ℕ) 0) Z) 0)
    ((P.π.f 0 ≫ Iso.inv (singleObjHomologySelfIso (ComplexShape.down ℕ) 0 Z)) ≫
      homologyι (Functor.obj (single C (ComplexShape.down ℕ) 0) Z) 0)
⊢ Eq (α := P.complex.X 0 ⟶ opcycles.{v, u, 0} (Functor.obj (single C (ComplexShape.down ℕ) 0) P.cokernelCofork.pt) 0)
    ((CategoryStruct.comp (Y :=
          Cocone.pt (F := parallelPair (X := P.complex.X 1) (Y := P.complex.X 0) (P.complex.d 1 0) 0)
            (CokernelCofork.ofπ (Z := opcycles P.complex 0) (pOpcycles P.complex 0) ⋯))
          (Cofork.π (CokernelCofork.ofπ (Z := opcycles P.complex 0) (pOpcycles P.complex 0) ⋯))
          (Iso.hom
            (Iso.trans (Y := homology P.complex 0) (Iso.symm P.complex.isoHomologyι₀)
              (isoOfQuasiIsoAt P.π 0 ≪≫ singleObjHomologySelfIso (ComplexShape.down ℕ) 0 Z))) ≫
        Iso.inv (singleObjHomologySelfIso (ComplexShape.down ℕ) 0 P.cokernelCofork.pt)) ≫
      Iso.hom (isoHomologyι₀ (Functor.obj (single C (ComplexShape.down ℕ) 0) P.cokernelCofork.pt)))
    ((Cofork.π P.cokernelCofork ≫ Iso.inv (singleObjHomologySelfIso (ComplexShape.down ℕ) 0 P.cokernelCofork.pt)) ≫
      Iso.hom (isoHomologyι₀ (Functor.obj (single C (ComplexShape.down ℕ) 0) P.cokernelCofork.pt)))

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Preadditive.Projective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
Z : C
P : ProjectiveResolution.{v, u} Z
⊢ Eq (α := P.complex.X 0 ⟶ opcycles.{v, u, 0} (Functor.obj (single C (ComplexShape.down ℕ) 0) Z) 0)
    ((CategoryStruct.comp (Y := opcycles P.complex 0) (pOpcycles P.complex 0)
          (Iso.inv P.complex.isoHomologyι₀ ≫
            homologyMap P.π 0 ≫ Iso.hom (singleObjHomologySelfIso (ComplexShape.down ℕ) 0 Z)) ≫
        Iso.inv (singleObjHomologySelfIso (ComplexShape.down ℕ) 0 Z)) ≫
      homologyι (Functor.obj (single C (ComplexShape.down ℕ) 0) Z) 0)
    ((P.π.f 0 ≫ Iso.inv (singleObjHomologySelfIso (ComplexShape.down ℕ) 0 Z)) ≫
      homologyι (Functor.obj (single C (ComplexShape.down ℕ) 0) Z) 0)

Tactic:
simp only [isoHomologyι₀_inv_naturality_assoc, p_opcyclesMap_assoc, single₀_obj_zero, assoc,
    Iso.hom_inv_id, comp_id, isoHomologyι_inv_hom_id, singleObjHomologySelfIso_inv_homologyι,
    singleObjOpcyclesSelfIso_hom, single₀ObjXSelf, Iso.refl_inv, id_comp]

Premises used: CategoryTheory.Category.assoc, HomologicalComplex.singleObjOpcyclesSelfIso_hom, ChainComplex.isoHomologyι₀_inv_naturality_assoc, HomologicalComplex.isoHomologyι_inv_hom_id, ChainComplex.single₀ObjXSelf, CategoryTheory.Iso.hom_inv_id, CategoryTheory.Category.comp_id, CategoryTheory.Iso.refl_inv, ChainComplex.single₀_obj_zero, HomologicalComplex.singleObjHomologySelfIso_inv_homologyι, CategoryTheory.Category.id_comp, HomologicalComplex.p_opcyclesMap_assoc
-- Module: Mathlib.CategoryTheory.Preadditive.Projective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
Z : C
P : ProjectiveResolution.{v, u} Z
n : ℕ
zero : Epi (X := P.complex.X 0) (P.π.f 0)
succ : ∀ (n : ℕ), Epi (X := P.complex.X (n + 1)) (P.π.f (n + 1))
⊢ Epi (P.π.f n)

Tactic:
cases n
-- Module: Mathlib.CategoryTheory.Preadditive.Projective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
Z : C
P : ProjectiveResolution.{v, u} Z
⊢ Epi (X := P.complex.X 0) (P.π.f 0)

Tactic:
epi_of_isColimit_cofork P.isColimitCokernelCofork

Premises used: CategoryTheory.ProjectiveResolution.isColimitCokernelCofork, CategoryTheory.Limits.Cofork.π, CategoryTheory.Limits.epi_of_isColimit_cofork, ite
-- Module: Mathlib.CategoryTheory.Preadditive.Projective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
Z : C
P : ProjectiveResolution.{v, u} Z
⊢ Epi (X := P.complex.X 0) (P.π.f 0)

Tactic:
exact epi_of_isColimit_cofork P.isColimitCokernelCofork

Premises used: CategoryTheory.ProjectiveResolution.isColimitCokernelCofork, CategoryTheory.Limits.epi_of_isColimit_cofork
-- Module: Mathlib.CategoryTheory.Preadditive.Projective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
Z : C
P : ProjectiveResolution.{v, u} Z
n : ℕ
succ : Epi.{v, u} (C := C) (X := P.complex.X (n + 1)) (Y := X.{v, u, 0} (Functor.obj (single₀ C) Z) (n + 1)) 0
⊢ Epi (X := P.complex.X (n + 1)) (P.π.f (n + 1))

Tactic:
rw [π_f_succ]

Premises used: CategoryTheory.ProjectiveResolution.π_f_succ
-- Module: Mathlib.CategoryTheory.Preadditive.Projective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
Z : C
P : ProjectiveResolution.{v, u} Z
n : ℕ
⊢ Epi.{v, u} (C := C) (X := P.complex.X (n + 1)) (Y := X.{v, u, 0} (Functor.obj (single₀ C) Z) (n + 1)) 0

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Preadditive.Projective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
Z : C
P : ProjectiveResolution.{v, u} Z
inst_3 : Projective.{v, u} Z
n : ℕ
zero : Projective.{v, u} (X.{v, u, 0} (Functor.obj (single₀ C) Z) 0)
succ : ∀ (n : ℕ), Projective.{v, u} (X.{v, u, 0} (Functor.obj (single₀ C) Z) (n + 1))
⊢ Projective.{v, u} (X.{v, u, 0} (Functor.obj (single₀ C) Z) n)

Tactic:
cases n
-- Module: Mathlib.CategoryTheory.Preadditive.Projective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
Z : C
P : ProjectiveResolution.{v, u} Z
inst_3 : Projective.{v, u} Z
⊢ Projective.{v, u} (X.{v, u, 0} (Functor.obj (single₀ C) Z) 0)

Tactic:
simpa