awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Resolution (goal)
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)
h :
  CategoryStruct.comp (Y := complex (projectiveResolution Y))
      (CategoryStruct.comp (Y :=
        Quotient.as (r := homotopic C (ComplexShape.down ℕ)) (Functor.obj (projectiveResolutions C) X))
        (HomotopyEquiv.inv (homotopyEquiv (projectiveResolution X) P))
        (lift f (projectiveResolution X) (projectiveResolution Y)))
      (π (projectiveResolution Y)) =
    P.π ≫ Functor.map (ChainComplex.single₀ C) f
⊢ Homotopy (D := complex (projectiveResolution Y))
    (CategoryStruct.comp (Y :=
      Quotient.as (r := homotopic C (ComplexShape.down ℕ)) (Functor.obj (projectiveResolutions C) X))
      (HomotopyEquiv.inv (homotopyEquiv (projectiveResolution X) P))
      (lift f (projectiveResolution X) (projectiveResolution Y)))
    (φ ≫ HomotopyEquiv.inv (homotopyEquiv (projectiveResolution Y) Q))
have h₁ : CategoryStruct.comp (Y := complex (projectiveResolution Y))
    (φ ≫ HomotopyEquiv.inv (homotopyEquiv (projectiveResolution Y) Q)) (π (projectiveResolution Y)) =
  P.π ≫ Functor.map (ChainComplex.single₀ C) f
Tactic: apply liftHomotopy f
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Resolution (goal)
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)
⊢ 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 ℕ)) φ)
have 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 ℕ)) φ)
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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Resolution (goal)
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 ℕ)) φ)
⊢ 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 ℕ)) φ)
have 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 ℕ)) φ)
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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Resolution (goal)
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 ℕ)) φ)
⊢ 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 ℕ)) φ)
have 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 ℕ)) φ
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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Resolution (goal)
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 ℕ)) φ
⊢ 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 ℕ)) φ)
have rw₃ : Functor.map (HomotopyCategory.quotient C (ComplexShape.down ℕ)) φ ≫
    𝟙 (Functor.obj (HomotopyCategory.quotient C (ComplexShape.down ℕ)) Q.complex) =
  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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Resolution (goal)
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 ℕ)) φ
⊢ 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 ℕ)) φ)
have 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 ℕ)) φ)
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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Resolution (goal)
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₂₃ := ⋯ }
⊢ ShortComplex.Exact (ShortComplex.mk (X₁ := syzygies f) (d f) f ⋯)
have rw : ShortComplex.Exact (ShortComplex.mk (X₁ := kernel f) (kernel.ι f) f sorry)
Tactic: rw [ShortComplex.exact_iff_of_epi_of_isIso_of_mono α]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Resolution (goal)
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₂₃ := ⋯ }
⊢ ShortComplex.Exact (ShortComplex.mk (X₁ := kernel f) (kernel.ι f) f ⋯)
have hS : IsLimit (F :=
  parallelPair (X := ShortComplex.X₂ (ShortComplex.mk (X₁ := kernel f) (kernel.ι f) f sorry))
    (ShortComplex.g (ShortComplex.mk (X₁ := kernel f) (kernel.ι f) f sorry)) 0)
  (KernelFork.ofι (ShortComplex.f (ShortComplex.mk (X₁ := kernel f) (kernel.ι f) f sorry)) sorry)
Tactic: apply ShortComplex.exact_of_f_is_kernel
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Resolution (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : EnoughProjectives.{v, u} C
Z : C
n : ℕ
⊢ HomologicalComplex.ExactAt.{v, u, 0} (ofComplex Z) (n + 1)
have rw : ShortComplex.Exact.{v, u} (HomologicalComplex.sc' (ofComplex Z) (n + 1 + 1) (n + 1) n)
Tactic: rw [HomologicalComplex.exactAt_iff' _ (n + 1 + 1) (n + 1) n (by simp) (by simp)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Resolution (goal)
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.{v, u} (HomologicalComplex.sc' (ofComplex Z) (n + 1 + 1) (n + 1) n)
have 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))) sorry
        (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) sorry))
        (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))) sorry
        (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) sorry))
        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))) sorry
        (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) sorry))
        (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))) sorry
        (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) sorry))
        n))
    sorry)
Tactic: simp only [HomologicalComplex.sc', HomologicalComplex.shortComplexFunctor', ofComplex,
    ChainComplex.mk', ChainComplex.mk, ChainComplex.of_d]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Resolution (goal)
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)
have zero : Projective.{v, u} (HomologicalComplex.X.{v, u, 0} (ofComplex Z) 0)
Tactic: obtain (_ | _ | _ | n) := n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Resolution (goal)
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)
⊢ Projective.{v, u} (HomologicalComplex.X.{v, u, 0} (ofComplex Z) n)
have succ : Projective.{v, u} (HomologicalComplex.X.{v, u, 0} (ofComplex Z) (HAdd.hAdd (α := ℕ) 0 1))
Tactic: obtain (_ | _ | _ | n) := n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Resolution (goal)
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))
⊢ Projective.{v, u} (HomologicalComplex.X.{v, u, 0} (ofComplex Z) n)
have succ₁ : Projective.{v, u} (HomologicalComplex.X.{v, u, 0} (ofComplex Z) (HAdd.hAdd (α := ℕ) 0 1 + 1))
Tactic: obtain (_ | _ | _ | n) := n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Resolution (goal)
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))
⊢ Projective.{v, u} (HomologicalComplex.X.{v, u, 0} (ofComplex Z) n)
have succ₂ : ∀ (n : ℕ), Projective.{v, u} (HomologicalComplex.X.{v, u, 0} (ofComplex Z) (n + 1 + 1 + 1))
Tactic: obtain (_ | _ | _ | n) := n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Resolution (goal)
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 ⟶ Z)
    (CategoryStruct.comp (Y := HomologicalComplex.X.{v, u, 0} (ofComplex Z) 0) (HomologicalComplex.d (ofComplex Z) 1 0)
      (Projective.π Z))
    0
have 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)
Tactic: rw [ofComplex_d_1_0, assoc, kernel.condition, comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Resolution (goal)
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)
⊢ 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
have 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)
Tactic: rw [ofComplex_d_1_0, assoc, kernel.condition, comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Resolution (goal)
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)
⊢ 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
have 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)
Tactic: rw [ofComplex_d_1_0, assoc, kernel.condition, comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Resolution (goal)
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)
⊢ 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
have rw₃ : Eq.{v + 1} (α := HomologicalComplex.X.{v, u, 0} (ofComplex Z) 1 ⟶ Z) 0 0
Tactic: rw [ofComplex_d_1_0, assoc, kernel.condition, comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Resolution (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : EnoughProjectives.{v, u} C
Z : C
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
have 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) sorry :
      { 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
Tactic: cases n
Cleared hypotheses: n