awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Ext (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X Y : C
R : ProjectiveResolution.{v, u} X
n : ℕ
f : R.complex.X n ⟶ Y
m : ℕ
hm : n + 1 = m
hf : R.complex.d m n ≫ f = 0
X' : C
R' : ProjectiveResolution.{v, u} X'
g : X' ⟶ X
φ : R'.Hom R g
this_1 : HasDerivedCategory C
this :
  (R'.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom ≫ φ.hom.f n =
    φ.hom'.f (-(↑n : ℤ)) ≫ (R.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom
⊢ Eq (α :=
    ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (DerivedCategory.singleFunctor C 0) X')
      (Functor.obj (DerivedCategory.singleFunctor C 0) Y) (↑n : ℤ))
    (ShiftedHom.comp (a := (↑n : ℤ))
      (ShiftedHom.comp
        (ShiftedHom.mk₀ (↑0 : ℤ) ⋯
          (Functor.map (DerivedCategory.singleFunctor C 0) g ≫
            NatTrans.app (Iso.hom (DerivedCategory.singleFunctorIsoCompQ C 0)) X ≫
              inv (Functor.map DerivedCategory.Q R.π')))
        (ShiftedHom.map
          ((AddEquiv.symm Cocycle.equivHomShift :
              (a : Cocycle R.cochainComplex ((singleFunctor C 0).obj Y) (↑n : ℤ)) →
                R.cochainComplex ⟶ (shiftFunctor (CochainComplex C ℤ) (↑n : ℤ)).obj ((singleFunctor C 0).obj Y))
            (Cocycle.toSingleMk ((R.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom ≫ f) ⋯ (-(↑m : ℤ)) ⋯ ⋯))
          DerivedCategory.Q)
        ⋯)
      (ShiftedHom.mk₀ 0 ⋯ (NatTrans.app (Iso.inv (DerivedCategory.singleFunctorIsoCompQ C 0)) Y)) ⋯)
    (ShiftedHom.comp (a := (↑n : ℤ))
      (ShiftedHom.comp (a := 0) (b := (↑n : ℤ))
        (ShiftedHom.mk₀ 0 ⋯
          ((NatTrans.app (Iso.hom (DerivedCategory.singleFunctorIsoCompQ C 0)) X' ≫
              inv (Functor.map DerivedCategory.Q R'.π')) ≫
            Functor.map DerivedCategory.Q φ.hom'))
        (ShiftedHom.map
          ((AddEquiv.symm Cocycle.equivHomShift :
              (a : Cocycle R.cochainComplex ((singleFunctor C 0).obj Y) (↑n : ℤ)) →
                R.cochainComplex ⟶ (shiftFunctor (CochainComplex C ℤ) (↑n : ℤ)).obj ((singleFunctor C 0).obj Y))
            (Cocycle.toSingleMk ((R.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom ≫ f) ⋯ (-(↑m : ℤ)) ⋯ ⋯))
          DerivedCategory.Q)
        ⋯)
      (ShiftedHom.mk₀ 0 ⋯ (NatTrans.app (Iso.inv (DerivedCategory.singleFunctorIsoCompQ C 0)) Y)) ⋯)
have h : Eq (α :=
  Quiver.Hom (V := DerivedCategory C) (Functor.obj (DerivedCategory.singleFunctor C 0) X')
    (Functor.obj DerivedCategory.Q R.cochainComplex))
  (Functor.map (DerivedCategory.singleFunctor C 0) g ≫
    NatTrans.app (Iso.hom (DerivedCategory.singleFunctorIsoCompQ C 0)) X ≫ inv (Functor.map DerivedCategory.Q R.π'))
  ((NatTrans.app (Iso.hom (DerivedCategory.singleFunctorIsoCompQ C 0)) X' ≫ inv (Functor.map DerivedCategory.Q R'.π')) ≫
    Functor.map DerivedCategory.Q φ.hom')
Tactic: congr 3
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Extend (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : Preadditive.{v, u} C
X : C
R : ProjectiveResolution.{v, u} X
n : ℤ
⊢ Projective.{v, u} (R.cochainComplex.X n)
have pos : ∀ (hn : n ≤ 0), Projective.{v, u} (R.cochainComplex.X n)
Tactic: by_cases hn : n ≤ 0
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Extend (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : Preadditive.{v, u} C
X : C
R : ProjectiveResolution.{v, u} X
n : ℤ
pos : ∀ (hn : n ≤ 0), Projective.{v, u} (R.cochainComplex.X n)
⊢ Projective.{v, u} (R.cochainComplex.X n)
have neg : ∀ (hn : ¬n ≤ 0), Projective.{v, u} (R.cochainComplex.X n)
Tactic: by_cases hn : n ≤ 0
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Extend (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : Preadditive.{v, u} C
X : C
R : ProjectiveResolution.{v, u} X
n : ℤ
hn : n ≤ 0
⊢ Projective.{v, u} (R.cochainComplex.X n)
have pos : ∀ (k : ℕ) (hn : LE.le (α := ℤ) (-(↑k : ℤ)) 0), Projective.{v, u} (R.cochainComplex.X (-(↑k : ℤ)))
Tactic: obtain ⟨k, rfl⟩ := Int.exists_eq_neg_ofNat hn
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Extend (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : Preadditive.{v, u} C
X : C
R : ProjectiveResolution.{v, u} X
⊢ R.π'.f 0 =
    (R.cochainComplexXIso 0 0 π'_f_zero._proof_2).hom ≫
      R.π.f 0 ≫ Iso.inv (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) 0 X)
have dsimp : Eq (α := R.cochainComplex.X 0 ⟶ HomologicalComplex.X.{v, u, 0} (Functor.obj (CochainComplex.singleFunctor C 0) X) 0)
  (HomologicalComplex.Hom.f (HomologicalComplex.extendMap R.π ComplexShape.embeddingDownNat) 0 ≫
    HomologicalComplex.Hom.f
      (Iso.hom (HomologicalComplex.extendSingleIso ComplexShape.embeddingDownNat X 0 0 π'._proof_1)) 0)
  ((R.cochainComplexXIso 0 0 π'_f_zero._proof_2).hom ≫
    R.π.f 0 ≫ Iso.inv (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) 0 X))
Tactic: dsimp [π']
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Extend (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : Preadditive.{v, u} C
X : C
R : ProjectiveResolution.{v, u} X
⊢ Eq (α := R.cochainComplex.X 0 ⟶ HomologicalComplex.X.{v, u, 0} (Functor.obj (CochainComplex.singleFunctor C 0) X) 0)
    (HomologicalComplex.Hom.f (HomologicalComplex.extendMap R.π ComplexShape.embeddingDownNat) 0 ≫
      HomologicalComplex.Hom.f
        (Iso.hom (HomologicalComplex.extendSingleIso ComplexShape.embeddingDownNat X 0 0 π'._proof_1)) 0)
    ((R.cochainComplexXIso 0 0 π'_f_zero._proof_2).hom ≫
      R.π.f 0 ≫ Iso.inv (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) 0 X))
have rw : Eq (α := R.cochainComplex.X 0 ⟶ HomologicalComplex.X.{v, u, 0} (Functor.obj (CochainComplex.singleFunctor C 0) X) 0)
  (CategoryStruct.comp (Y :=
    HomologicalComplex.X.{v, u, 0}
      (HomologicalComplex.extend (Functor.obj (ChainComplex.single₀ C) X) ComplexShape.embeddingDownNat) 0)
    (Iso.hom (HomologicalComplex.extendXIso R.complex ComplexShape.embeddingDownNat sorry) ≫
      R.π.f 0 ≫
        Iso.inv
          (HomologicalComplex.extendXIso (Functor.obj (ChainComplex.single₀ C) X) ComplexShape.embeddingDownNat sorry))
    (Iso.hom
        (HomologicalComplex.extendXIso (Functor.obj (HomologicalComplex.single C (ComplexShape.down ℕ) 0) X)
          ComplexShape.embeddingDownNat π'._proof_1) ≫
      Iso.hom (HomologicalComplex.singleObjXSelf (ComplexShape.down ℕ) 0 X) ≫
        Iso.inv (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) 0 X)))
  ((R.cochainComplexXIso 0 0 π'_f_zero._proof_2).hom ≫
    R.π.f 0 ≫ Iso.inv (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) 0 X))
Tactic: rw [HomologicalComplex.extendMap_f _ _ (i := 0) (by simp),
    HomologicalComplex.extendSingleIso_hom_f]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Extend (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
R : ProjectiveResolution.{v, u} X
⊢ R.cochainComplex.IsGE 0
have simp : HomologicalComplex.IsSupported.{0, 0, v, u} (Functor.obj (CochainComplex.singleFunctor C 0) X)
  (ComplexShape.embeddingUpIntGE 0)
Tactic: simp only [HomologicalComplex.isSupported_iff_of_quasiIso R.π']
-- 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
Y Z : C
f : Y ⟶ Z
P : ProjectiveResolution.{v, u} Y
Q : ProjectiveResolution.{v, u} Z
⊢ lift f P Q ≫ Q.π = P.π ≫ Functor.map (ChainComplex.single₀ C) f
have hfg : Eq (α :=
  P.complex.X 0 ⟶
    HomologicalComplex.X.{v, u, 0} (Functor.obj (HomologicalComplex.single C (ComplexShape.down ℕ) 0) Z) 0)
  ((lift f P Q ≫ Q.π).f 0) ((P.π ≫ Functor.map (ChainComplex.single₀ C) f).f 0)
Tactic: ext
-- 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
Y Z : C
P : ProjectiveResolution.{v, u} Y
Q : ProjectiveResolution.{v, u} Z
f : P.complex ⟶ Q.complex
comm : f ≫ Q.π = 0
⊢ (f.f 1 - P.complex.d 1 0 ≫ liftHomotopyZeroZero f comm) ≫
      (ShortComplex.mk (X₁ := Q.complex.X (HAdd.hAdd (α := ℕ) 0 2)) (X₂ := Q.complex.X (HAdd.hAdd (α := ℕ) 0 1)) (X₃ :=
          Q.complex.X 0) (Q.complex.d (HAdd.hAdd (α := ℕ) 0 2) (HAdd.hAdd (α := ℕ) 0 1))
          (Q.complex.d (HAdd.hAdd (α := ℕ) 0 1) 0) ⋯).g =
    0
have rw : f.f 1 ≫
      (ShortComplex.mk (X₁ := Q.complex.X (HAdd.hAdd (α := ℕ) 0 2)) (X₂ := Q.complex.X (HAdd.hAdd (α := ℕ) 0 1)) (X₃ :=
          Q.complex.X 0) (Q.complex.d (HAdd.hAdd (α := ℕ) 0 2) (HAdd.hAdd (α := ℕ) 0 1))
          (Q.complex.d (HAdd.hAdd (α := ℕ) 0 1) 0) sorry).g -
    (P.complex.d 1 0 ≫ liftHomotopyZeroZero f comm) ≫
      (ShortComplex.mk (X₁ := Q.complex.X (HAdd.hAdd (α := ℕ) 0 2)) (X₂ := Q.complex.X (HAdd.hAdd (α := ℕ) 0 1)) (X₃ :=
          Q.complex.X 0) (Q.complex.d (HAdd.hAdd (α := ℕ) 0 2) (HAdd.hAdd (α := ℕ) 0 1))
          (Q.complex.d (HAdd.hAdd (α := ℕ) 0 1) 0) sorry).g =
  0
Tactic: rw [Preadditive.sub_comp, assoc, HomologicalComplex.Hom.comm,
              liftHomotopyZeroZero_comp, sub_self]
-- 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
Y Z : C
P : ProjectiveResolution.{v, u} Y
Q : ProjectiveResolution.{v, u} Z
f : P.complex ⟶ Q.complex
comm : f ≫ Q.π = 0
rw :
  f.f 1 ≫
        (ShortComplex.mk (X₁ := Q.complex.X (HAdd.hAdd (α := ℕ) 0 2)) (X₂ := Q.complex.X (HAdd.hAdd (α := ℕ) 0 1))
            (X₃ := Q.complex.X 0) (Q.complex.d (HAdd.hAdd (α := ℕ) 0 2) (HAdd.hAdd (α := ℕ) 0 1))
            (Q.complex.d (HAdd.hAdd (α := ℕ) 0 1) 0) ⋯).g -
      (P.complex.d 1 0 ≫ liftHomotopyZeroZero f comm) ≫
        (ShortComplex.mk (X₁ := Q.complex.X (HAdd.hAdd (α := ℕ) 0 2)) (X₂ := Q.complex.X (HAdd.hAdd (α := ℕ) 0 1))
            (X₃ := Q.complex.X 0) (Q.complex.d (HAdd.hAdd (α := ℕ) 0 2) (HAdd.hAdd (α := ℕ) 0 1))
            (Q.complex.d (HAdd.hAdd (α := ℕ) 0 1) 0) ⋯).g =
    0
⊢ (f.f 1 - P.complex.d 1 0 ≫ liftHomotopyZeroZero f comm) ≫
      (ShortComplex.mk (X₁ := Q.complex.X (HAdd.hAdd (α := ℕ) 0 2)) (X₂ := Q.complex.X (HAdd.hAdd (α := ℕ) 0 1)) (X₃ :=
          Q.complex.X 0) (Q.complex.d (HAdd.hAdd (α := ℕ) 0 2) (HAdd.hAdd (α := ℕ) 0 1))
          (Q.complex.d (HAdd.hAdd (α := ℕ) 0 1) 0) ⋯).g =
    0
have rw₁ : f.f 1 ≫
      (ShortComplex.mk (X₁ := Q.complex.X (HAdd.hAdd (α := ℕ) 0 2)) (X₂ := Q.complex.X (HAdd.hAdd (α := ℕ) 0 1)) (X₃ :=
          Q.complex.X 0) (Q.complex.d (HAdd.hAdd (α := ℕ) 0 2) (HAdd.hAdd (α := ℕ) 0 1))
          (Q.complex.d (HAdd.hAdd (α := ℕ) 0 1) 0) sorry).g -
    P.complex.d 1 0 ≫
      liftHomotopyZeroZero f comm ≫
        (ShortComplex.mk (X₁ := Q.complex.X (HAdd.hAdd (α := ℕ) 0 2)) (X₂ := Q.complex.X (HAdd.hAdd (α := ℕ) 0 1))
            (X₃ := Q.complex.X 0) (Q.complex.d (HAdd.hAdd (α := ℕ) 0 2) (HAdd.hAdd (α := ℕ) 0 1))
            (Q.complex.d (HAdd.hAdd (α := ℕ) 0 1) 0) sorry).g =
  0
Tactic: rw [Preadditive.sub_comp, assoc, HomologicalComplex.Hom.comm,
              liftHomotopyZeroZero_comp, sub_self]
-- 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
Y Z : C
P : ProjectiveResolution.{v, u} Y
Q : ProjectiveResolution.{v, u} Z
f : P.complex ⟶ Q.complex
comm : f ≫ Q.π = 0
rw :
  f.f 1 ≫
        (ShortComplex.mk (X₁ := Q.complex.X (HAdd.hAdd (α := ℕ) 0 2)) (X₂ := Q.complex.X (HAdd.hAdd (α := ℕ) 0 1))
            (X₃ := Q.complex.X 0) (Q.complex.d (HAdd.hAdd (α := ℕ) 0 2) (HAdd.hAdd (α := ℕ) 0 1))
            (Q.complex.d (HAdd.hAdd (α := ℕ) 0 1) 0) ⋯).g -
      (P.complex.d 1 0 ≫ liftHomotopyZeroZero f comm) ≫
        (ShortComplex.mk (X₁ := Q.complex.X (HAdd.hAdd (α := ℕ) 0 2)) (X₂ := Q.complex.X (HAdd.hAdd (α := ℕ) 0 1))
            (X₃ := Q.complex.X 0) (Q.complex.d (HAdd.hAdd (α := ℕ) 0 2) (HAdd.hAdd (α := ℕ) 0 1))
            (Q.complex.d (HAdd.hAdd (α := ℕ) 0 1) 0) ⋯).g =
    0
rw₁ :
  f.f 1 ≫
        (ShortComplex.mk (X₁ := Q.complex.X (HAdd.hAdd (α := ℕ) 0 2)) (X₂ := Q.complex.X (HAdd.hAdd (α := ℕ) 0 1))
            (X₃ := Q.complex.X 0) (Q.complex.d (HAdd.hAdd (α := ℕ) 0 2) (HAdd.hAdd (α := ℕ) 0 1))
            (Q.complex.d (HAdd.hAdd (α := ℕ) 0 1) 0) ⋯).g -
      P.complex.d 1 0 ≫
        liftHomotopyZeroZero f comm ≫
          (ShortComplex.mk (X₁ := Q.complex.X (HAdd.hAdd (α := ℕ) 0 2)) (X₂ := Q.complex.X (HAdd.hAdd (α := ℕ) 0 1))
              (X₃ := Q.complex.X 0) (Q.complex.d (HAdd.hAdd (α := ℕ) 0 2) (HAdd.hAdd (α := ℕ) 0 1))
              (Q.complex.d (HAdd.hAdd (α := ℕ) 0 1) 0) ⋯).g =
    0
⊢ (f.f 1 - P.complex.d 1 0 ≫ liftHomotopyZeroZero f comm) ≫
      (ShortComplex.mk (X₁ := Q.complex.X (HAdd.hAdd (α := ℕ) 0 2)) (X₂ := Q.complex.X (HAdd.hAdd (α := ℕ) 0 1)) (X₃ :=
          Q.complex.X 0) (Q.complex.d (HAdd.hAdd (α := ℕ) 0 2) (HAdd.hAdd (α := ℕ) 0 1))
          (Q.complex.d (HAdd.hAdd (α := ℕ) 0 1) 0) ⋯).g =
    0
have rw₂ : HSub.hSub (α :=
    P.complex.X 1 ⟶
      (ShortComplex.mk (X₁ := Q.complex.X (HAdd.hAdd (α := ℕ) 0 2)) (X₂ := Q.complex.X (HAdd.hAdd (α := ℕ) 0 1)) (X₃ :=
          Q.complex.X 0) (Q.complex.d (HAdd.hAdd (α := ℕ) 0 2) (HAdd.hAdd (α := ℕ) 0 1))
          (Q.complex.d (HAdd.hAdd (α := ℕ) 0 1) 0) sorry).X₃)
    (P.complex.d 1 0 ≫ f.f 0)
    (P.complex.d 1 0 ≫
      liftHomotopyZeroZero f comm ≫
        (ShortComplex.mk (X₁ := Q.complex.X (HAdd.hAdd (α := ℕ) 0 2)) (X₂ := Q.complex.X (HAdd.hAdd (α := ℕ) 0 1))
            (X₃ := Q.complex.X 0) (Q.complex.d (HAdd.hAdd (α := ℕ) 0 2) (HAdd.hAdd (α := ℕ) 0 1))
            (Q.complex.d (HAdd.hAdd (α := ℕ) 0 1) 0) sorry).g) =
  0
Tactic: rw [Preadditive.sub_comp, assoc, HomologicalComplex.Hom.comm,
              liftHomotopyZeroZero_comp, sub_self]
-- 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
Y Z : C
P : ProjectiveResolution.{v, u} Y
Q : ProjectiveResolution.{v, u} Z
f : P.complex ⟶ Q.complex
comm : f ≫ Q.π = 0
rw :
  f.f 1 ≫
        (ShortComplex.mk (X₁ := Q.complex.X (HAdd.hAdd (α := ℕ) 0 2)) (X₂ := Q.complex.X (HAdd.hAdd (α := ℕ) 0 1))
            (X₃ := Q.complex.X 0) (Q.complex.d (HAdd.hAdd (α := ℕ) 0 2) (HAdd.hAdd (α := ℕ) 0 1))
            (Q.complex.d (HAdd.hAdd (α := ℕ) 0 1) 0) ⋯).g -
      (P.complex.d 1 0 ≫ liftHomotopyZeroZero f comm) ≫
        (ShortComplex.mk (X₁ := Q.complex.X (HAdd.hAdd (α := ℕ) 0 2)) (X₂ := Q.complex.X (HAdd.hAdd (α := ℕ) 0 1))
            (X₃ := Q.complex.X 0) (Q.complex.d (HAdd.hAdd (α := ℕ) 0 2) (HAdd.hAdd (α := ℕ) 0 1))
            (Q.complex.d (HAdd.hAdd (α := ℕ) 0 1) 0) ⋯).g =
    0
rw₁ :
  f.f 1 ≫
        (ShortComplex.mk (X₁ := Q.complex.X (HAdd.hAdd (α := ℕ) 0 2)) (X₂ := Q.complex.X (HAdd.hAdd (α := ℕ) 0 1))
            (X₃ := Q.complex.X 0) (Q.complex.d (HAdd.hAdd (α := ℕ) 0 2) (HAdd.hAdd (α := ℕ) 0 1))
            (Q.complex.d (HAdd.hAdd (α := ℕ) 0 1) 0) ⋯).g -
      P.complex.d 1 0 ≫
        liftHomotopyZeroZero f comm ≫
          (ShortComplex.mk (X₁ := Q.complex.X (HAdd.hAdd (α := ℕ) 0 2)) (X₂ := Q.complex.X (HAdd.hAdd (α := ℕ) 0 1))
              (X₃ := Q.complex.X 0) (Q.complex.d (HAdd.hAdd (α := ℕ) 0 2) (HAdd.hAdd (α := ℕ) 0 1))
              (Q.complex.d (HAdd.hAdd (α := ℕ) 0 1) 0) ⋯).g =
    0
rw₂ :
  HSub.hSub (α :=
      P.complex.X 1 ⟶
        (ShortComplex.mk (X₁ := Q.complex.X (HAdd.hAdd (α := ℕ) 0 2)) (X₂ := Q.complex.X (HAdd.hAdd (α := ℕ) 0 1))
            (X₃ := Q.complex.X 0) (Q.complex.d (HAdd.hAdd (α := ℕ) 0 2) (HAdd.hAdd (α := ℕ) 0 1))
            (Q.complex.d (HAdd.hAdd (α := ℕ) 0 1) 0) ⋯).X₃)
      (P.complex.d 1 0 ≫ f.f 0)
      (P.complex.d 1 0 ≫
        liftHomotopyZeroZero f comm ≫
          (ShortComplex.mk (X₁ := Q.complex.X (HAdd.hAdd (α := ℕ) 0 2)) (X₂ := Q.complex.X (HAdd.hAdd (α := ℕ) 0 1))
              (X₃ := Q.complex.X 0) (Q.complex.d (HAdd.hAdd (α := ℕ) 0 2) (HAdd.hAdd (α := ℕ) 0 1))
              (Q.complex.d (HAdd.hAdd (α := ℕ) 0 1) 0) ⋯).g) =
    0
⊢ (f.f 1 - P.complex.d 1 0 ≫ liftHomotopyZeroZero f comm) ≫
      (ShortComplex.mk (X₁ := Q.complex.X (HAdd.hAdd (α := ℕ) 0 2)) (X₂ := Q.complex.X (HAdd.hAdd (α := ℕ) 0 1)) (X₃ :=
          Q.complex.X 0) (Q.complex.d (HAdd.hAdd (α := ℕ) 0 2) (HAdd.hAdd (α := ℕ) 0 1))
          (Q.complex.d (HAdd.hAdd (α := ℕ) 0 1) 0) ⋯).g =
    0
have rw₃ : HSub.hSub (α :=
    P.complex.X 1 ⟶
      (ShortComplex.mk (X₁ := Q.complex.X (HAdd.hAdd (α := ℕ) 0 2)) (X₂ := Q.complex.X (HAdd.hAdd (α := ℕ) 0 1)) (X₃ :=
          Q.complex.X 0) (Q.complex.d (HAdd.hAdd (α := ℕ) 0 2) (HAdd.hAdd (α := ℕ) 0 1))
          (Q.complex.d (HAdd.hAdd (α := ℕ) 0 1) 0) sorry).X₃)
    (P.complex.d 1 0 ≫ f.f 0) (P.complex.d 1 0 ≫ f.f 0) =
  0
Tactic: rw [Preadditive.sub_comp, assoc, HomologicalComplex.Hom.comm,
              liftHomotopyZeroZero_comp, sub_self]
-- 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
X : C
P : ProjectiveResolution.{v, u} X
⊢ Homotopy (lift (𝟙 X) P P) (𝟙 P.complex)
have g_comm : lift (𝟙 X) P P ≫ P.π = P.π ≫ Functor.map (ChainComplex.single₀ C) (𝟙 X)
Tactic: apply liftHomotopy (𝟙 X)
-- 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
X : C
P : ProjectiveResolution.{v, u} X
g_comm : lift (𝟙 X) P P ≫ P.π = P.π ≫ Functor.map (ChainComplex.single₀ C) (𝟙 X)
⊢ Homotopy (lift (𝟙 X) P P) (𝟙 P.complex)
have h_comm : 𝟙 P.complex ≫ P.π = P.π ≫ Functor.map (ChainComplex.single₀ C) (𝟙 X)
Tactic: apply liftHomotopy (𝟙 X)
-- 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
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
P : ProjectiveResolution.{v, u} X
Q : ProjectiveResolution.{v, u} Y
R : ProjectiveResolution.{v, u} Z
⊢ Homotopy (lift (f ≫ g) P R) (lift f P Q ≫ lift g Q R)
have g_comm : lift (f ≫ g) P R ≫ R.π = P.π ≫ Functor.map (ChainComplex.single₀ C) (f ≫ g)
Tactic: apply liftHomotopy (f ≫ g)
-- 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
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
P : ProjectiveResolution.{v, u} X
Q : ProjectiveResolution.{v, u} Y
R : ProjectiveResolution.{v, u} Z
g_comm : lift (f ≫ g) P R ≫ R.π = P.π ≫ Functor.map (ChainComplex.single₀ C) (f ≫ g)
⊢ Homotopy (lift (f ≫ g) P R) (lift f P Q ≫ lift g Q R)
have h_comm : (lift f P Q ≫ lift g Q R) ≫ R.π = P.π ≫ Functor.map (ChainComplex.single₀ C) (f ≫ g)
Tactic: apply liftHomotopy (f ≫ g)
-- 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 : C
⊢ Eq.{v + 1} (α :=
    Quiver.Hom (V := HomotopyCategory.{v, u, 0} C (ComplexShape.down ℕ))
      (Functor.obj (HomotopyCategory.quotient C (ComplexShape.down ℕ))
        (ProjectiveResolution.complex (projectiveResolution X)))
      (Functor.obj (HomotopyCategory.quotient C (ComplexShape.down ℕ))
        (ProjectiveResolution.complex (projectiveResolution X))))
    (Functor.map (HomotopyCategory.quotient C (ComplexShape.down ℕ))
      (ProjectiveResolution.lift (𝟙 X) (projectiveResolution X) (projectiveResolution X)))
    (Functor.map (HomotopyCategory.quotient C (ComplexShape.down ℕ))
      (𝟙 (ProjectiveResolution.complex (projectiveResolution X))))
have h : Homotopy (C := ProjectiveResolution.complex (projectiveResolution X))
  (ProjectiveResolution.lift (𝟙 X) (projectiveResolution X) (projectiveResolution X))
  (𝟙 (ProjectiveResolution.complex (projectiveResolution X)))
Tactic: apply HomotopyCategory.eq_of_homotopy
-- 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 Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq (α :=
    Quiver.Hom (V := HomotopyCategory.{v, u, 0} C (ComplexShape.down ℕ))
      (Functor.obj (HomotopyCategory.quotient C (ComplexShape.down ℕ))
        (ProjectiveResolution.complex (projectiveResolution X)))
      (Functor.obj (HomotopyCategory.quotient C (ComplexShape.down ℕ))
        (ProjectiveResolution.complex (projectiveResolution Z))))
    (Functor.map (HomotopyCategory.quotient C (ComplexShape.down ℕ))
      (ProjectiveResolution.lift (f ≫ g) (projectiveResolution X) (projectiveResolution Z)))
    (Functor.map (HomotopyCategory.quotient C (ComplexShape.down ℕ))
      (CategoryStruct.comp (Y := ProjectiveResolution.complex (projectiveResolution Y))
        (ProjectiveResolution.lift f (projectiveResolution X) (projectiveResolution Y))
        (ProjectiveResolution.lift g (projectiveResolution Y) (projectiveResolution Z))))
have h : Homotopy (C := ProjectiveResolution.complex (projectiveResolution X)) (D :=
  ProjectiveResolution.complex (projectiveResolution Z))
  (ProjectiveResolution.lift (f ≫ g) (projectiveResolution X) (projectiveResolution Z))
  (CategoryStruct.comp (Y := ProjectiveResolution.complex (projectiveResolution Y))
    (ProjectiveResolution.lift f (projectiveResolution X) (projectiveResolution Y))
    (ProjectiveResolution.lift g (projectiveResolution Y) (projectiveResolution Z)))
Tactic: apply HomotopyCategory.eq_of_homotopy
-- 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 (HomotopyCategory.quotient C (ComplexShape.down ℕ)) P.complex ⟶ Functor.obj (projectiveResolutions C) Y)
    (Iso.inv P.iso ≫ Functor.map (projectiveResolutions C) f)
    (Functor.map (HomotopyCategory.quotient C (ComplexShape.down ℕ)) φ ≫ Iso.inv Q.iso)
have h : 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))
Tactic: apply HomotopyCategory.eq_of_homotopy
-- 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)
⊢ 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))
    (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
Tactic: apply liftHomotopy f