awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasProjectiveResolutions.{v, u} C
X Y : C
f : X ⟶ Y
P : ProjectiveResolution.{v, u} X
Q : ProjectiveResolution.{v, u} Y
φ : P.complex ⟶ Q.complex
comm :
  Eq (α := P.complex.X 0 ⟶ HomologicalComplex.X.{v, u, 0} (Functor.obj (ChainComplex.single₀ C) Y) 0) (φ.f 0 ≫ Q.π.f 0)
    (P.π.f 0 ≫ f)
rw :
  CategoryStruct.comp (Y := Functor.obj (projectiveResolutions C) X) (Iso.inv P.iso)
      (Functor.map (projectiveResolutions C) f ≫ Iso.hom Q.iso) =
    CategoryStruct.comp (Y := Functor.obj (projectiveResolutions C) X) (Iso.inv P.iso)
      (Iso.hom P.iso ≫ Functor.map (HomotopyCategory.quotient C (ComplexShape.down ℕ)) φ)
rw₁ :
  Functor.map (HomotopyCategory.quotient C (ComplexShape.down ℕ)) φ ≫
      CategoryStruct.comp (Y := Functor.obj (projectiveResolutions C) Y) (Iso.inv Q.iso) (Iso.hom Q.iso) =
    CategoryStruct.comp (Y := Functor.obj (projectiveResolutions C) X) (Iso.inv P.iso)
      (Iso.hom P.iso ≫ Functor.map (HomotopyCategory.quotient C (ComplexShape.down ℕ)) φ)
rw₂ :
  Functor.map (HomotopyCategory.quotient C (ComplexShape.down ℕ)) φ ≫
      CategoryStruct.comp (Y := Functor.obj (projectiveResolutions C) Y) (Iso.inv Q.iso) (Iso.hom Q.iso) =
    Functor.map (HomotopyCategory.quotient C (ComplexShape.down ℕ)) φ
rw₃ :
  Functor.map (HomotopyCategory.quotient C (ComplexShape.down ℕ)) φ ≫
      𝟙 (Functor.obj (HomotopyCategory.quotient C (ComplexShape.down ℕ)) Q.complex) =
    Functor.map (HomotopyCategory.quotient C (ComplexShape.down ℕ)) φ
rw₄ rw₅ :
  Eq (α :=
    Functor.obj (HomotopyCategory.quotient C (ComplexShape.down ℕ)) P.complex ⟶
      Functor.obj (HomotopyCategory.quotient C (ComplexShape.down ℕ)) Q.complex)
    (Functor.map (HomotopyCategory.quotient C (ComplexShape.down ℕ)) φ)
    (Functor.map (HomotopyCategory.quotient C (ComplexShape.down ℕ)) φ)
⊢ Eq (α :=
    Functor.obj (projectiveResolutions C) X ⟶ Functor.obj (HomotopyCategory.quotient C (ComplexShape.down ℕ)) Q.complex)
    (Functor.map (projectiveResolutions C) f ≫ Iso.hom Q.iso)
    (Iso.hom P.iso ≫ Functor.map (HomotopyCategory.quotient C (ComplexShape.down ℕ)) φ)

Tactic:
rw [← cancel_epi (P.iso).inv, iso_inv_naturality_assoc f P Q φ comm,
    Iso.inv_hom_id_assoc, Iso.inv_hom_id, comp_id]

Premises used: CategoryTheory.Iso.inv_hom_id, CategoryTheory.ProjectiveResolution.iso, CategoryTheory.Category.comp_id, CategoryTheory.Iso.inv_hom_id_assoc, CategoryTheory.cancel_epi, CategoryTheory.ProjectiveResolution.iso_inv_naturality_assoc, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : EnoughProjectives.{v, u} C
X Y : C
f : X ⟶ Y
⊢ Eq (α := syzygies f ⟶ Y) (d f ≫ f) 0

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : EnoughProjectives.{v, u} C
X Y : C
f : X ⟶ Y
⊢ Eq (α := kernel f ⟶ Y) (kernel.ι f ≫ f) 0

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : EnoughProjectives.{v, u} C
X Y : C
f : X ⟶ Y
α : ShortComplex.mk (X₁ := syzygies f) (d f) f ⋯ ⟶ ShortComplex.mk (X₁ := kernel f) (kernel.ι f) f ⋯ :=
  { τ₁ := π (kernel f), τ₂ := 𝟙 (ShortComplex.mk (X₁ := syzygies f) (d f) f ⋯).X₂,
    τ₃ := 𝟙 (ShortComplex.mk (X₁ := syzygies f) (d f) f ⋯).X₃, comm₁₂ := ⋯, comm₂₃ := ⋯ }
rw : ShortComplex.Exact (ShortComplex.mk (X₁ := kernel f) (kernel.ι f) f ⋯)
⊢ ShortComplex.Exact (ShortComplex.mk (X₁ := syzygies f) (d f) f ⋯)

Tactic:
rw [ShortComplex.exact_iff_of_epi_of_isIso_of_mono α]

Premises used: CategoryTheory.ShortComplex.exact_iff_of_epi_of_isIso_of_mono
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : EnoughProjectives.{v, u} C
X Y : C
f : X ⟶ Y
α : ShortComplex.mk (X₁ := syzygies f) (d f) f ⋯ ⟶ ShortComplex.mk (X₁ := kernel f) (kernel.ι f) f ⋯ :=
  { τ₁ := π (kernel f), τ₂ := 𝟙 (ShortComplex.mk (X₁ := syzygies f) (d f) f ⋯).X₂,
    τ₃ := 𝟙 (ShortComplex.mk (X₁ := syzygies f) (d f) f ⋯).X₃, comm₁₂ := ⋯, comm₂₃ := ⋯ }
hS :
  IsLimit (F :=
    parallelPair (X := ShortComplex.X₂ (ShortComplex.mk (X₁ := kernel f) (kernel.ι f) f ⋯))
      (ShortComplex.g (ShortComplex.mk (X₁ := kernel f) (kernel.ι f) f ⋯)) 0)
    (KernelFork.ofι (ShortComplex.f (ShortComplex.mk (X₁ := kernel f) (kernel.ι f) f ⋯)) ⋯)
⊢ ShortComplex.Exact (ShortComplex.mk (X₁ := kernel f) (kernel.ι f) f ⋯)

Tactic:
apply ShortComplex.exact_of_f_is_kernel

Premises used: CategoryTheory.ShortComplex.exact_of_f_is_kernel
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : EnoughProjectives.{v, u} C
X Y : C
f : X ⟶ Y
α : ShortComplex.mk (X₁ := syzygies f) (d f) f ⋯ ⟶ ShortComplex.mk (X₁ := kernel f) (kernel.ι f) f ⋯ :=
  { τ₁ := π (kernel f), τ₂ := 𝟙 (ShortComplex.mk (X₁ := syzygies f) (d f) f ⋯).X₂,
    τ₃ := 𝟙 (ShortComplex.mk (X₁ := syzygies f) (d f) f ⋯).X₃, comm₁₂ := ⋯, comm₂₃ := ⋯ }
⊢ IsLimit (F :=
    parallelPair (X := ShortComplex.X₂ (ShortComplex.mk (X₁ := kernel f) (kernel.ι f) f ⋯))
      (ShortComplex.g (ShortComplex.mk (X₁ := kernel f) (kernel.ι f) f ⋯)) 0)
    (KernelFork.ofι (ShortComplex.f (ShortComplex.mk (X₁ := kernel f) (kernel.ι f) f ⋯)) ⋯)

Tactic:
apply kernelIsKernel

Premises used: CategoryTheory.Limits.kernelIsKernel
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : EnoughProjectives.{v, u} C
Z X₀ X₁ : C
f : X₁ ⟶ X₀
⊢ Eq (α := syzygies f ⟶ X₀) (d f ≫ f) 0

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : EnoughProjectives.{v, u} C
Z : C
⊢ Eq.{v + 1} (α := HomologicalComplex.X.{v, u, 0} (ofComplex Z) 1 ⟶ HomologicalComplex.X.{v, u, 0} (ofComplex Z) 0)
    (HomologicalComplex.d (ofComplex Z) 1 0) (d (Projective.π Z))

Tactic:
simp [ofComplex]

Premises used: CategoryTheory.ProjectiveResolution.ofComplex
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : EnoughProjectives.{v, u} C
Z : C
n : ℕ
⊢ (ComplexShape.down ℕ).prev (n + 1) = n + 1 + 1

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : EnoughProjectives.{v, u} C
Z : C
n : ℕ
⊢ (ComplexShape.down ℕ).next (n + 1) = n

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : EnoughProjectives.{v, u} C
Z : C
n : ℕ
rw : ShortComplex.Exact.{v, u} (HomologicalComplex.sc' (ofComplex Z) (n + 1 + 1) (n + 1) n)
⊢ HomologicalComplex.ExactAt.{v, u, 0} (ofComplex Z) (n + 1)

Tactic:
rw [HomologicalComplex.exactAt_iff' _ (n + 1 + 1) (n + 1) n (by simp) (by simp)]

Premises used: HAdd.hAdd, OfNat.ofNat, HomologicalComplex.exactAt_iff'
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : EnoughProjectives.{v, u} C
Z : C
n : ℕ
simp :
  ShortComplex.Exact
    (ShortComplex.mk (X₁ :=
      ShortComplex.X₃
        (ChainComplex.mkAux (over.{v, u} Z) (syzygies.{v, u} (X := over.{v, u} Z) (Projective.π Z))
          (syzygies.{v, u} (X := syzygies.{v, u} (X := over.{v, u} Z) (Projective.π Z)) (d (Projective.π Z)))
          (d (Projective.π Z)) (d (d (Projective.π Z))) ⋯
          (fun (S : ShortComplex.{v, u} C) ↦
            PSigma.mk (β := fun (X₂ : C) ↦ (d : X₂ ⟶ S.X₁) ×' d ≫ S.f = 0) (syzygies S.f)
              (PSigma.mk (β := fun (d : syzygies S.f ⟶ S.X₁) ↦ d ≫ S.f = 0) (d S.f) ⋯))
          (n + 1 + 1)))
      (X₃ :=
      ShortComplex.X₃
        (ChainComplex.mkAux (over.{v, u} Z) (syzygies.{v, u} (X := over.{v, u} Z) (Projective.π Z))
          (syzygies.{v, u} (X := syzygies.{v, u} (X := over.{v, u} Z) (Projective.π Z)) (d (Projective.π Z)))
          (d (Projective.π Z)) (d (d (Projective.π Z))) ⋯
          (fun (S : ShortComplex.{v, u} C) ↦
            PSigma.mk (β := fun (X₂ : C) ↦ (d : X₂ ⟶ S.X₁) ×' d ≫ S.f = 0) (syzygies S.f)
              (PSigma.mk (β := fun (d : syzygies S.f ⟶ S.X₁) ↦ d ≫ S.f = 0) (d S.f) ⋯))
          n))
      (ShortComplex.g
        (ChainComplex.mkAux (over.{v, u} Z) (syzygies.{v, u} (X := over.{v, u} Z) (Projective.π Z))
          (syzygies.{v, u} (X := syzygies.{v, u} (X := over.{v, u} Z) (Projective.π Z)) (d (Projective.π Z)))
          (d (Projective.π Z)) (d (d (Projective.π Z))) ⋯
          (fun (S : ShortComplex.{v, u} C) ↦
            PSigma.mk (β := fun (X₂ : C) ↦ (d : X₂ ⟶ S.X₁) ×' d ≫ S.f = 0) (syzygies S.f)
              (PSigma.mk (β := fun (d : syzygies S.f ⟶ S.X₁) ↦ d ≫ S.f = 0) (d S.f) ⋯))
          (n + 1)))
      (ShortComplex.g
        (ChainComplex.mkAux (over.{v, u} Z) (syzygies.{v, u} (X := over.{v, u} Z) (Projective.π Z))
          (syzygies.{v, u} (X := syzygies.{v, u} (X := over.{v, u} Z) (Projective.π Z)) (d (Projective.π Z)))
          (d (Projective.π Z)) (d (d (Projective.π Z))) ⋯
          (fun (S : ShortComplex.{v, u} C) ↦
            PSigma.mk (β := fun (X₂ : C) ↦ (d : X₂ ⟶ S.X₁) ×' d ≫ S.f = 0) (syzygies S.f)
              (PSigma.mk (β := fun (d : syzygies S.f ⟶ S.X₁) ↦ d ≫ S.f = 0) (d S.f) ⋯))
          n))
      ⋯)
⊢ ShortComplex.Exact.{v, u} (HomologicalComplex.sc' (ofComplex Z) (n + 1 + 1) (n + 1) n)

Tactic:
simp only [HomologicalComplex.sc', HomologicalComplex.shortComplexFunctor', ofComplex,
    ChainComplex.mk', ChainComplex.mk, ChainComplex.of_d]

Premises used: CategoryTheory.ProjectiveResolution.ofComplex, HomologicalComplex.shortComplexFunctor', ChainComplex.mk', ChainComplex.mk, HomologicalComplex.sc', ChainComplex.of_d
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : EnoughProjectives.{v, u} C
Z : C
n : ℕ
⊢ ShortComplex.Exact
    (ShortComplex.mk (X₁ :=
      ShortComplex.X₃
        (ChainComplex.mkAux (over.{v, u} Z) (syzygies.{v, u} (X := over.{v, u} Z) (Projective.π Z))
          (syzygies.{v, u} (X := syzygies.{v, u} (X := over.{v, u} Z) (Projective.π Z)) (d (Projective.π Z)))
          (d (Projective.π Z)) (d (d (Projective.π Z))) ⋯
          (fun (S : ShortComplex.{v, u} C) ↦
            PSigma.mk (β := fun (X₂ : C) ↦ (d : X₂ ⟶ S.X₁) ×' d ≫ S.f = 0) (syzygies S.f)
              (PSigma.mk (β := fun (d : syzygies S.f ⟶ S.X₁) ↦ d ≫ S.f = 0) (d S.f) ⋯))
          (HAdd.hAdd (α := ℕ) 0 1 + 1)))
      (X₃ :=
      ShortComplex.X₃
        (ChainComplex.mkAux (over.{v, u} Z) (syzygies.{v, u} (X := over.{v, u} Z) (Projective.π Z))
          (syzygies.{v, u} (X := syzygies.{v, u} (X := over.{v, u} Z) (Projective.π Z)) (d (Projective.π Z)))
          (d (Projective.π Z)) (d (d (Projective.π Z))) ⋯
          (fun (S : ShortComplex.{v, u} C) ↦
            PSigma.mk (β := fun (X₂ : C) ↦ (d : X₂ ⟶ S.X₁) ×' d ≫ S.f = 0) (syzygies S.f)
              (PSigma.mk (β := fun (d : syzygies S.f ⟶ S.X₁) ↦ d ≫ S.f = 0) (d S.f) ⋯))
          0))
      (ShortComplex.g
        (ChainComplex.mkAux (over.{v, u} Z) (syzygies.{v, u} (X := over.{v, u} Z) (Projective.π Z))
          (syzygies.{v, u} (X := syzygies.{v, u} (X := over.{v, u} Z) (Projective.π Z)) (d (Projective.π Z)))
          (d (Projective.π Z)) (d (d (Projective.π Z))) ⋯
          (fun (S : ShortComplex.{v, u} C) ↦
            PSigma.mk (β := fun (X₂ : C) ↦ (d : X₂ ⟶ S.X₁) ×' d ≫ S.f = 0) (syzygies S.f)
              (PSigma.mk (β := fun (d : syzygies S.f ⟶ S.X₁) ↦ d ≫ S.f = 0) (d S.f) ⋯))
          (HAdd.hAdd (α := ℕ) 0 1)))
      (ShortComplex.g
        (ChainComplex.mkAux (over.{v, u} Z) (syzygies.{v, u} (X := over.{v, u} Z) (Projective.π Z))
          (syzygies.{v, u} (X := syzygies.{v, u} (X := over.{v, u} Z) (Projective.π Z)) (d (Projective.π Z)))
          (d (Projective.π Z)) (d (d (Projective.π Z))) ⋯
          (fun (S : ShortComplex.{v, u} C) ↦
            PSigma.mk (β := fun (X₂ : C) ↦ (d : X₂ ⟶ S.X₁) ×' d ≫ S.f = 0) (syzygies S.f)
              (PSigma.mk (β := fun (d : syzygies S.f ⟶ S.X₁) ↦ d ≫ S.f = 0) (d S.f) ⋯))
          0))
      ⋯)

Tactic:
apply exact_d_f

Premises used: CategoryTheory.exact_d_f
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : EnoughProjectives.{v, u} C
Z : C
n_1 n : ℕ
⊢ ShortComplex.Exact
    (ShortComplex.mk (X₁ :=
      ShortComplex.X₃
        (ChainComplex.mkAux (over.{v, u} Z) (syzygies.{v, u} (X := over.{v, u} Z) (Projective.π Z))
          (syzygies.{v, u} (X := syzygies.{v, u} (X := over.{v, u} Z) (Projective.π Z)) (d (Projective.π Z)))
          (d (Projective.π Z)) (d (d (Projective.π Z))) ⋯
          (fun (S : ShortComplex.{v, u} C) ↦
            PSigma.mk (β := fun (X₂ : C) ↦ (d : X₂ ⟶ S.X₁) ×' d ≫ S.f = 0) (syzygies S.f)
              (PSigma.mk (β := fun (d : syzygies S.f ⟶ S.X₁) ↦ d ≫ S.f = 0) (d S.f) ⋯))
          (n + 1 + 1 + 1)))
      (X₃ :=
      ShortComplex.X₃
        (ChainComplex.mkAux (over.{v, u} Z) (syzygies.{v, u} (X := over.{v, u} Z) (Projective.π Z))
          (syzygies.{v, u} (X := syzygies.{v, u} (X := over.{v, u} Z) (Projective.π Z)) (d (Projective.π Z)))
          (d (Projective.π Z)) (d (d (Projective.π Z))) ⋯
          (fun (S : ShortComplex.{v, u} C) ↦
            PSigma.mk (β := fun (X₂ : C) ↦ (d : X₂ ⟶ S.X₁) ×' d ≫ S.f = 0) (syzygies S.f)
              (PSigma.mk (β := fun (d : syzygies S.f ⟶ S.X₁) ↦ d ≫ S.f = 0) (d S.f) ⋯))
          (n + 1)))
      (ShortComplex.g
        (ChainComplex.mkAux (over.{v, u} Z) (syzygies.{v, u} (X := over.{v, u} Z) (Projective.π Z))
          (syzygies.{v, u} (X := syzygies.{v, u} (X := over.{v, u} Z) (Projective.π Z)) (d (Projective.π Z)))
          (d (Projective.π Z)) (d (d (Projective.π Z))) ⋯
          (fun (S : ShortComplex.{v, u} C) ↦
            PSigma.mk (β := fun (X₂ : C) ↦ (d : X₂ ⟶ S.X₁) ×' d ≫ S.f = 0) (syzygies S.f)
              (PSigma.mk (β := fun (d : syzygies S.f ⟶ S.X₁) ↦ d ≫ S.f = 0) (d S.f) ⋯))
          (n + 1 + 1)))
      (ShortComplex.g
        (ChainComplex.mkAux (over.{v, u} Z) (syzygies.{v, u} (X := over.{v, u} Z) (Projective.π Z))
          (syzygies.{v, u} (X := syzygies.{v, u} (X := over.{v, u} Z) (Projective.π Z)) (d (Projective.π Z)))
          (d (Projective.π Z)) (d (d (Projective.π Z))) ⋯
          (fun (S : ShortComplex.{v, u} C) ↦
            PSigma.mk (β := fun (X₂ : C) ↦ (d : X₂ ⟶ S.X₁) ×' d ≫ S.f = 0) (syzygies S.f)
              (PSigma.mk (β := fun (d : syzygies S.f ⟶ S.X₁) ↦ d ≫ S.f = 0) (d S.f) ⋯))
          (n + 1)))
      ⋯)

Tactic:
apply exact_d_f

Premises used: CategoryTheory.exact_d_f
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : EnoughProjectives.{v, u} C
Z : C
n : ℕ
⊢ ShortComplex.Exact
    (ShortComplex.mk (X₁ :=
      ShortComplex.X₃
        (ChainComplex.mkAux (over.{v, u} Z) (syzygies.{v, u} (X := over.{v, u} Z) (Projective.π Z))
          (syzygies.{v, u} (X := syzygies.{v, u} (X := over.{v, u} Z) (Projective.π Z)) (d (Projective.π Z)))
          (d (Projective.π Z)) (d (d (Projective.π Z))) ⋯
          (fun (S : ShortComplex.{v, u} C) ↦
            PSigma.mk (β := fun (X₂ : C) ↦ (d : X₂ ⟶ S.X₁) ×' d ≫ S.f = 0) (syzygies S.f)
              (PSigma.mk (β := fun (d : syzygies S.f ⟶ S.X₁) ↦ d ≫ S.f = 0) (d S.f) ⋯))
          (n + 1 + 1)))
      (X₃ :=
      ShortComplex.X₃
        (ChainComplex.mkAux (over.{v, u} Z) (syzygies.{v, u} (X := over.{v, u} Z) (Projective.π Z))
          (syzygies.{v, u} (X := syzygies.{v, u} (X := over.{v, u} Z) (Projective.π Z)) (d (Projective.π Z)))
          (d (Projective.π Z)) (d (d (Projective.π Z))) ⋯
          (fun (S : ShortComplex.{v, u} C) ↦
            PSigma.mk (β := fun (X₂ : C) ↦ (d : X₂ ⟶ S.X₁) ×' d ≫ S.f = 0) (syzygies S.f)
              (PSigma.mk (β := fun (d : syzygies S.f ⟶ S.X₁) ↦ d ≫ S.f = 0) (d S.f) ⋯))
          n))
      (ShortComplex.g
        (ChainComplex.mkAux (over.{v, u} Z) (syzygies.{v, u} (X := over.{v, u} Z) (Projective.π Z))
          (syzygies.{v, u} (X := syzygies.{v, u} (X := over.{v, u} Z) (Projective.π Z)) (d (Projective.π Z)))
          (d (Projective.π Z)) (d (d (Projective.π Z))) ⋯
          (fun (S : ShortComplex.{v, u} C) ↦
            PSigma.mk (β := fun (X₂ : C) ↦ (d : X₂ ⟶ S.X₁) ×' d ≫ S.f = 0) (syzygies S.f)
              (PSigma.mk (β := fun (d : syzygies S.f ⟶ S.X₁) ↦ d ≫ S.f = 0) (d S.f) ⋯))
          (n + 1)))
      (ShortComplex.g
        (ChainComplex.mkAux (over.{v, u} Z) (syzygies.{v, u} (X := over.{v, u} Z) (Projective.π Z))
          (syzygies.{v, u} (X := syzygies.{v, u} (X := over.{v, u} Z) (Projective.π Z)) (d (Projective.π Z)))
          (d (Projective.π Z)) (d (d (Projective.π Z))) ⋯
          (fun (S : ShortComplex.{v, u} C) ↦
            PSigma.mk (β := fun (X₂ : C) ↦ (d : X₂ ⟶ S.X₁) ×' d ≫ S.f = 0) (syzygies S.f)
              (PSigma.mk (β := fun (d : syzygies S.f ⟶ S.X₁) ↦ d ≫ S.f = 0) (d S.f) ⋯))
          n))
      ⋯)

Tactic:
match n with
  | 0 => apply exact_d_f
  | n + 1 => apply exact_d_f
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : EnoughProjectives.{v, u} C
Z : C
n : ℕ
zero : Projective.{v, u} (HomologicalComplex.X.{v, u, 0} (ofComplex Z) 0)
succ : Projective.{v, u} (HomologicalComplex.X.{v, u, 0} (ofComplex Z) (HAdd.hAdd (α := ℕ) 0 1))
succ₁ : Projective.{v, u} (HomologicalComplex.X.{v, u, 0} (ofComplex Z) (HAdd.hAdd (α := ℕ) 0 1 + 1))
succ₂ : ∀ (n : ℕ), Projective.{v, u} (HomologicalComplex.X.{v, u, 0} (ofComplex Z) (n + 1 + 1 + 1))
⊢ Projective.{v, u} (HomologicalComplex.X.{v, u, 0} (ofComplex Z) n)

Tactic:
obtain (_ | _ | _ | n) := n
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : EnoughProjectives.{v, u} C
Z : C
⊢ Projective.{v, u} (HomologicalComplex.X.{v, u, 0} (ofComplex Z) 0)

Tactic:
apply Projective.projective_over

Premises used: CategoryTheory.Projective.projective_over
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : EnoughProjectives.{v, u} C
Z : C
⊢ Projective.{v, u} (HomologicalComplex.X.{v, u, 0} (ofComplex Z) (HAdd.hAdd (α := ℕ) 0 1))

Tactic:
apply Projective.projective_over

Premises used: CategoryTheory.Projective.projective_over
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : EnoughProjectives.{v, u} C
Z : C
⊢ Projective.{v, u} (HomologicalComplex.X.{v, u, 0} (ofComplex Z) (HAdd.hAdd (α := ℕ) 0 1 + 1))

Tactic:
apply Projective.projective_over

Premises used: CategoryTheory.Projective.projective_over
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : EnoughProjectives.{v, u} C
Z : C
n : ℕ
⊢ Projective.{v, u} (HomologicalComplex.X.{v, u, 0} (ofComplex Z) (n + 1 + 1 + 1))

Tactic:
apply Projective.projective_over

Premises used: CategoryTheory.Projective.projective_over
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : EnoughProjectives.{v, u} C
Z : C
rw :
  Eq.{v + 1} (α := HomologicalComplex.X.{v, u, 0} (ofComplex Z) 1 ⟶ Z)
    (d (Projective.π Z) ≫ Projective.π Z : HomologicalComplex.X.{v, u, 0} (ofComplex Z) 1 ⟶ Z)
    (0 : HomologicalComplex.X.{v, u, 0} (ofComplex Z) 1 ⟶ Z)
rw₁ :
  Eq (α := HomologicalComplex.X.{v, u, 0} (ofComplex Z) 1 ⟶ Z)
    (Projective.π (kernel.{v, u} (X := over.{v, u} Z) (Projective.π Z)) ≫ kernel.ι (Projective.π Z) ≫ Projective.π Z :
      HomologicalComplex.X.{v, u, 0} (ofComplex Z) 1 ⟶ Z)
    (0 : HomologicalComplex.X.{v, u, 0} (ofComplex Z) 1 ⟶ Z)
rw₂ :
  Eq.{v + 1} (α := HomologicalComplex.X.{v, u, 0} (ofComplex Z) 1 ⟶ Z)
    (Projective.π (kernel.{v, u} (X := over.{v, u} Z) (Projective.π Z)) ≫ 0 :
      HomologicalComplex.X.{v, u, 0} (ofComplex Z) 1 ⟶ Z)
    (0 : HomologicalComplex.X.{v, u, 0} (ofComplex Z) 1 ⟶ Z)
rw₃ rw₄ : Eq.{v + 1} (α := HomologicalComplex.X.{v, u, 0} (ofComplex Z) 1 ⟶ Z) 0 0
⊢ Eq.{v + 1} (α := HomologicalComplex.X.{v, u, 0} (ofComplex Z) 1 ⟶ Z)
    (CategoryStruct.comp (Y := HomologicalComplex.X.{v, u, 0} (ofComplex Z) 0) (HomologicalComplex.d (ofComplex Z) 1 0)
      (Projective.π Z))
    0

Tactic:
rw [ofComplex_d_1_0, assoc, kernel.condition, comp_zero]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.ProjectiveResolution.ofComplex_d_1_0, CategoryTheory.Limits.comp_zero, CategoryTheory.Limits.kernel.condition
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : EnoughProjectives.{v, u} C
Z : C
n : ℕ
zero :
  QuasiIsoAt.{v, u, 0} (ι := ℕ) (C := C) (c := ComplexShape.down ℕ) (K := ofComplex Z) (L :=
    Functor.obj (ChainComplex.single₀ C) Z)
    ((Equiv.symm (ChainComplex.toSingle₀Equiv (ofComplex Z) Z) :
        (a : { f : (ofComplex Z).X 0 ⟶ Z // (ofComplex Z).d 1 0 ≫ f = 0 }) →
          ofComplex Z ⟶ (ChainComplex.single₀ C).obj Z)
      (Subtype.mk (p := fun (f : HomologicalComplex.X.{v, u, 0} (ofComplex Z) 0 ⟶ Z) ↦
          Eq (α := HomologicalComplex.X.{v, u, 0} (ofComplex Z) 1 ⟶ Z) (HomologicalComplex.d (ofComplex Z) 1 0 ≫ f) 0)
          (Projective.π Z) ⋯ :
        { f : HomologicalComplex.X.{v, u, 0} (ofComplex Z) 0 ⟶ Z //
          Eq (α := HomologicalComplex.X.{v, u, 0} (ofComplex Z) 1 ⟶ Z) (HomologicalComplex.d (ofComplex Z) 1 0 ≫ f)
            0 }))
    0
succ :
  ∀ (n : ℕ),
    QuasiIsoAt.{v, u, 0} (C := C) (c := ComplexShape.down ℕ) (K := ofComplex Z) (L :=
      Functor.obj (ChainComplex.single₀ C) Z)
      ((Equiv.symm (ChainComplex.toSingle₀Equiv (ofComplex Z) Z) :
          (a : { f : (ofComplex Z).X 0 ⟶ Z // (ofComplex Z).d 1 0 ≫ f = 0 }) →
            ofComplex Z ⟶ (ChainComplex.single₀ C).obj Z)
        (Subtype.mk (p := fun (f : HomologicalComplex.X.{v, u, 0} (ofComplex Z) 0 ⟶ Z) ↦
            Eq (α := HomologicalComplex.X.{v, u, 0} (ofComplex Z) 1 ⟶ Z) (HomologicalComplex.d (ofComplex Z) 1 0 ≫ f) 0)
            (Projective.π Z) ⋯ :
          { f : HomologicalComplex.X.{v, u, 0} (ofComplex Z) 0 ⟶ Z //
            Eq (α := HomologicalComplex.X.{v, u, 0} (ofComplex Z) 1 ⟶ Z) (HomologicalComplex.d (ofComplex Z) 1 0 ≫ f)
              0 }))
      (n + 1)
⊢ QuasiIsoAt.{v, u, 0} (C := C) (c := ComplexShape.down ℕ) (K := ofComplex Z) (L :=
    Functor.obj (ChainComplex.single₀ C) Z)
    ((Equiv.symm (ChainComplex.toSingle₀Equiv (ofComplex Z) Z) :
        (a : { f : (ofComplex Z).X 0 ⟶ Z // (ofComplex Z).d 1 0 ≫ f = 0 }) →
          ofComplex Z ⟶ (ChainComplex.single₀ C).obj Z)
      (Subtype.mk (p := fun (f : HomologicalComplex.X.{v, u, 0} (ofComplex Z) 0 ⟶ Z) ↦
          Eq (α := HomologicalComplex.X.{v, u, 0} (ofComplex Z) 1 ⟶ Z) (HomologicalComplex.d (ofComplex Z) 1 0 ≫ f) 0)
          (Projective.π Z) ⋯ :
        { f : HomologicalComplex.X.{v, u, 0} (ofComplex Z) 0 ⟶ Z //
          Eq (α := HomologicalComplex.X.{v, u, 0} (ofComplex Z) 1 ⟶ Z) (HomologicalComplex.d (ofComplex Z) 1 0 ≫ f)
            0 }))
    n

Tactic:
cases n
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : EnoughProjectives.{v, u} C
Z : C
dsimp : Epi.{v, u} (X := over.{v, u} Z) (Projective.π Z)
⊢ Epi.{v, u} (X :=
    ShortComplex.X₂.{v, u}
      (ShortComplex.mk (X₁ := syzygies.{v, u} (X := over.{v, u} Z) (Projective.π Z)) (d (Projective.π Z))
        (Projective.π Z) ⋯))
    (ShortComplex.g
      (ShortComplex.mk (X₁ := syzygies.{v, u} (X := over.{v, u} Z) (Projective.π Z)) (d (Projective.π Z))
        (Projective.π Z) ⋯))

Tactic:
dsimp