awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Extend
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
R : ProjectiveResolution.{v, u} X
X' : C
R' : ProjectiveResolution.{v, u} X'
f : X ⟶ X'
φ : R.Hom R' f
n : ℤ
m : ℕ
h : -(↑m : ℤ) = n
⊢ -(↑m : ℤ) = n

Tactic:
lia
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Extend
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
R : ProjectiveResolution.{v, u} X
X' : C
R' : ProjectiveResolution.{v, u} X'
f : X ⟶ X'
φ : R.Hom R' f
n : ℤ
m : ℕ
h : -(↑m : ℤ) = n
⊢ φ.hom'.f n = (R.cochainComplexXIso n m h).hom ≫ φ.hom.f m ≫ (R'.cochainComplexXIso n m h).inv

Tactic:
simp [hom', HomologicalComplex.extendMap_f _
    ComplexShape.embeddingDownNat (i := m) (i' := n) (by dsimp; lia),
    cochainComplexXIso]

Premises used: HomologicalComplex.extendMap_f, ComplexShape.embeddingDownNat, CategoryTheory.ProjectiveResolution.cochainComplexXIso, CategoryTheory.ProjectiveResolution.Hom.hom'
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Extend
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
R : ProjectiveResolution.{v, u} X
X' : C
R' : ProjectiveResolution.{v, u} X'
f : X ⟶ X'
φ : R.Hom R' f
⊢ Eq (α :=
    R.cochainComplex.X 0 ⟶
      HomologicalComplex.X.{v, u, 0} (Functor.obj (HomologicalComplex.single C (ComplexShape.up ℤ) 0) X') 0)
    ((φ.hom' ≫ R'.π').f 0) ((R.π' ≫ Functor.map (CochainComplex.singleFunctor C 0) f).f 0)

Tactic:
simp [hom'_f _ 0 0 rfl, π'_f_zero, CochainComplex.singleFunctor,
      CochainComplex.singleFunctors,
      HomologicalComplex.single, HomologicalComplex.singleObjXSelf,
      HomologicalComplex.singleObjXIsoOfEq]

Premises used: CochainComplex.singleFunctor, CategoryTheory.ProjectiveResolution.Hom.hom'_f, HomologicalComplex.singleObjXIsoOfEq, CochainComplex.singleFunctors, CategoryTheory.ProjectiveResolution.π'_f_zero, HomologicalComplex.singleObjXSelf, OfNat.ofNat, rfl, HomologicalComplex.single
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
Z : C
P : ProjectiveResolution.{v, u} Z
⊢ { X₁ := P.complex.X 1, X₂ := P.complex.X 0, X₃ := ((ChainComplex.single₀ C).obj Z).X 0, f := P.complex.d 1 0,
      g := P.π.f 0, zero := ⋯ : ShortComplex.{v, u} C }.Exact

Tactic:
ShortComplex.exact_of_g_is_cokernel _ P.isColimitCokernelCofork

Premises used: CategoryTheory.ShortComplex.exact_of_g_is_cokernel, CategoryTheory.ProjectiveResolution.isColimitCokernelCofork
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Resolution
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
⊢ Eq (α :=
    P.complex.X 1 ⟶
      { X₁ := Q.complex.X 1, X₂ := Q.complex.X 0, X₃ := ((ChainComplex.single₀ C).obj Z).X 0, f := Q.complex.d 1 0,
          g := Q.π.f 0, zero := ⋯ : ShortComplex.{v, u} C }.X₃)
    ((P.complex.d 1 0 ≫ liftFZero f P Q) ≫
      { X₁ := Q.complex.X 1, X₂ := Q.complex.X 0, X₃ := ((ChainComplex.single₀ C).obj Z).X 0, f := Q.complex.d 1 0,
          g := Q.π.f 0, zero := ⋯ : ShortComplex.{v, u} C }.g)
    0

Tactic:
simp [liftFZero]

Premises used: CategoryTheory.ProjectiveResolution.liftFZero
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Resolution
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
⊢ liftFOne f P Q ≫ Q.complex.d 1 0 = P.complex.d 1 0 ≫ liftFZero f P Q

Tactic:
apply Q.exact₀.liftFromProjective_comp

Premises used: CategoryTheory.ShortComplex.Exact.liftFromProjective_comp, CategoryTheory.ProjectiveResolution.exact₀
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Resolution
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
n : ℕ
g : P.complex.X n ⟶ Q.complex.X n
g' : P.complex.X (n + 1) ⟶ Q.complex.X (n + 1)
w : g' ≫ Q.complex.d (n + 1) n = P.complex.d (n + 1) n ≫ g
⊢ Eq (α :=
    P.complex.X (n + 2) ⟶
      (ShortComplex.mk (X₁ := Q.complex.X (n + 2)) (X₂ := Q.complex.X (n + 1)) (Q.complex.d (n + 2) (n + 1))
          (Q.complex.d (n + 1) n) ⋯).X₃)
    ((P.complex.d (n + 2) (n + 1) ≫ g') ≫
      (ShortComplex.mk (X₁ := Q.complex.X (n + 2)) (X₂ := Q.complex.X (n + 1)) (Q.complex.d (n + 2) (n + 1))
          (Q.complex.d (n + 1) n) ⋯).g)
    0

Tactic:
simp [w]
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Resolution
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
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)
⊢ lift f P Q ≫ Q.π = P.π ≫ Functor.map (ChainComplex.single₀ C) f

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Resolution
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
⊢ 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:
simp [lift, liftFZero, liftFOne]

Premises used: CategoryTheory.ProjectiveResolution.liftFZero, CategoryTheory.ProjectiveResolution.lift, CategoryTheory.ProjectiveResolution.liftFOne
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Resolution
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
⊢ Eq (α := P.complex.X 0 ⟶ HomologicalComplex.X.{v, u, 0} (Functor.obj (ChainComplex.single₀ C) Z) 0)
    ((P.π ≫ Functor.map (ChainComplex.single₀ C) f).f 0) (P.π.f 0 ≫ f)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Resolution
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
⊢ liftHomotopyZeroZero f comm ≫ Q.complex.d 1 0 = f.f 0

Tactic:
Q.exact₀.liftFromProjective_comp _ _

Premises used: CategoryTheory.ShortComplex.Exact.liftFromProjective_comp, CategoryTheory.ProjectiveResolution.exact₀, CategoryTheory.ProjectiveResolution.liftHomotopyZeroZero
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Resolution
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
⊢ liftHomotopyZeroOne f comm ≫ Q.complex.d 2 1 = f.f 1 - P.complex.d 1 0 ≫ liftHomotopyZeroZero f comm

Tactic:
(Q.exact_succ 0).liftFromProjective_comp _ _

Premises used: CategoryTheory.ShortComplex.Exact.liftFromProjective_comp, CategoryTheory.ProjectiveResolution.exact_succ, CategoryTheory.ProjectiveResolution.liftHomotopyZeroOne, OfNat.ofNat
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Resolution
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
n : ℕ
g : P.complex.X n ⟶ Q.complex.X (n + 1)
g' : P.complex.X (n + 1) ⟶ Q.complex.X (n + 2)
w : f.f (n + 1) = P.complex.d (n + 1) n ≫ g + g' ≫ Q.complex.d (n + 2) (n + 1)
⊢ (f.f (n + 2) - P.complex.d (n + 2) (n + 1) ≫ g') ≫
      (ShortComplex.mk (X₁ := Q.complex.X (n + 1 + 2)) (X₂ := Q.complex.X (n + 1 + 1)) (X₃ := Q.complex.X (n + 1))
          (Q.complex.d (n + 1 + 2) (n + 1 + 1)) (Q.complex.d (n + 1 + 1) (n + 1)) ⋯).g =
    0

Tactic:
simp [w]
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Resolution
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
n : ℕ
g : P.complex.X n ⟶ Q.complex.X (n + 1)
g' : P.complex.X (n + 1) ⟶ Q.complex.X (n + 2)
w : f.f (n + 1) = P.complex.d (n + 1) n ≫ g + g' ≫ Q.complex.d (n + 2) (n + 1)
⊢ liftHomotopyZeroSucc f n g g' w ≫ Q.complex.d (n + 3) (n + 2) = f.f (n + 2) - P.complex.d (n + 2) (n + 1) ≫ g'

Tactic:
(Q.exact_succ (n + 1)).liftFromProjective_comp _ _

Premises used: CategoryTheory.ProjectiveResolution.liftHomotopyZeroSucc, CategoryTheory.ShortComplex.Exact.liftFromProjective_comp, CategoryTheory.ProjectiveResolution.exact_succ, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Resolution
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 0 = liftHomotopyZeroZero f comm ≫ Q.complex.d 1 0

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Resolution
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 + liftHomotopyZeroOne f comm ≫ Q.complex.d 2 1

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Resolution
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
n : ℕ
x :
  (f_1 : P.complex.X n ⟶ Q.complex.X (n + 1)) ×'
    (f' : P.complex.X (n + 1) ⟶ Q.complex.X (n + 2)) ×'
      f.f (n + 1) = P.complex.d (n + 1) n ≫ f_1 + f' ≫ Q.complex.d (n + 2) (n + 1)
g : P.complex.X n ⟶ Q.complex.X (n + 1)
g' : P.complex.X (n + 1) ⟶ Q.complex.X (n + 2)
w : f.f (n + 1) = P.complex.d (n + 1) n ≫ g + g' ≫ Q.complex.d (n + 2) (n + 1)
⊢ f.f (n + 2) =
    HAdd.hAdd (α := P.complex.X (n + 2) ⟶ Q.complex.X (n + 2))
      (CategoryStruct.comp (Y := P.complex.X (n + 1)) (P.complex.d (n + 2) (n + 1))
        (PSigma.fst (β := fun (f' : P.complex.X (n + 1) ⟶ Q.complex.X (n + 2)) ↦
          f.f (n + 1) =
            P.complex.d (n + 1) n ≫
                PSigma.fst (β := fun (f_1 : P.complex.X n ⟶ Q.complex.X (n + 1)) ↦
                  (f' : P.complex.X (n + 1) ⟶ Q.complex.X (n + 2)) ×'
                    f.f (n + 1) = P.complex.d (n + 1) n ≫ f_1 + f' ≫ Q.complex.d (n + 2) (n + 1))
                  (PSigma.mk (β := fun (f_1 : P.complex.X n ⟶ Q.complex.X (n + 1)) ↦
                    (f' : P.complex.X (n + 1) ⟶ Q.complex.X (n + 2)) ×'
                      f.f (n + 1) = P.complex.d (n + 1) n ≫ f_1 + f' ≫ Q.complex.d (n + 2) (n + 1))
                    g
                    (PSigma.mk (β := fun (f' : P.complex.X (n + 1) ⟶ Q.complex.X (n + 2)) ↦
                      f.f (n + 1) = P.complex.d (n + 1) n ≫ g + f' ≫ Q.complex.d (n + 2) (n + 1)) g' w)) +
              f' ≫ Q.complex.d (n + 2) (n + 1))
          (PSigma.snd (β := fun (f_1 : P.complex.X n ⟶ Q.complex.X (n + 1)) ↦
            (f' : P.complex.X (n + 1) ⟶ Q.complex.X (n + 2)) ×'
              f.f (n + 1) = P.complex.d (n + 1) n ≫ f_1 + f' ≫ Q.complex.d (n + 2) (n + 1))
            (PSigma.mk (β := fun (f_1 : P.complex.X n ⟶ Q.complex.X (n + 1)) ↦
              (f' : P.complex.X (n + 1) ⟶ Q.complex.X (n + 2)) ×'
                f.f (n + 1) = P.complex.d (n + 1) n ≫ f_1 + f' ≫ Q.complex.d (n + 2) (n + 1))
              g
              (PSigma.mk (β := fun (f' : P.complex.X (n + 1) ⟶ Q.complex.X (n + 2)) ↦
                f.f (n + 1) = P.complex.d (n + 1) n ≫ g + f' ≫ Q.complex.d (n + 2) (n + 1)) g' w)))))
      (liftHomotopyZeroSucc f n g g' w ≫ Q.complex.d (n + 3) (n + 2))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Resolution
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
g h : P.complex ⟶ Q.complex
g_comm : g ≫ Q.π = P.π ≫ Functor.map (ChainComplex.single₀ C) f
h_comm : h ≫ Q.π = P.π ≫ Functor.map (ChainComplex.single₀ C) f
⊢ (g - h) ≫ Q.π = 0

Tactic:
simp [g_comm, h_comm]
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Resolution
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)
h_comm : 𝟙 P.complex ≫ P.π = P.π ≫ Functor.map (ChainComplex.single₀ C) (𝟙 X)
⊢ Homotopy (lift (𝟙 X) P P) (𝟙 P.complex)

Tactic:
apply liftHomotopy (𝟙 X)

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.ProjectiveResolution.liftHomotopy
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
P : ProjectiveResolution.{v, u} X
⊢ lift (𝟙 X) P P ≫ P.π = P.π ≫ Functor.map (ChainComplex.single₀ C) (𝟙 X)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
P : ProjectiveResolution.{v, u} X
⊢ 𝟙 P.complex ≫ P.π = P.π ≫ Functor.map (ChainComplex.single₀ C) (𝟙 X)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Resolution
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)
h_comm : (lift f P Q ≫ lift g Q R) ≫ R.π = P.π ≫ Functor.map (ChainComplex.single₀ C) (f ≫ g)
⊢ Homotopy (lift (f ≫ g) P R) (lift f P Q ≫ lift g Q R)

Tactic:
apply liftHomotopy (f ≫ g)

Premises used: CategoryTheory.CategoryStruct.comp, CategoryTheory.ProjectiveResolution.liftHomotopy
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Resolution
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
⊢ lift (f ≫ g) P R ≫ R.π = P.π ≫ Functor.map (ChainComplex.single₀ C) (f ≫ g)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Resolution
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
⊢ (lift f P Q ≫ lift g Q R) ≫ R.π = P.π ≫ Functor.map (ChainComplex.single₀ C) (f ≫ g)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
P Q : ProjectiveResolution.{v, u} X
⊢ Homotopy (lift (𝟙 X ≫ 𝟙 X) P P) (𝟙 P.complex)

Tactic:
simpa [id_comp] using liftIdHomotopy _ _

Premises used: CategoryTheory.ProjectiveResolution.liftIdHomotopy, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
P Q : ProjectiveResolution.{v, u} X
⊢ Homotopy (lift (𝟙 X ≫ 𝟙 X) Q Q) (𝟙 Q.complex)

Tactic:
simpa [id_comp] using liftIdHomotopy _ _

Premises used: CategoryTheory.ProjectiveResolution.liftIdHomotopy, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
P Q : ProjectiveResolution.{v, u} X
⊢ (P.homotopyEquiv Q).hom ≫ Q.π = P.π

Tactic:
simp [homotopyEquiv]

Premises used: CategoryTheory.ProjectiveResolution.homotopyEquiv
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
P Q : ProjectiveResolution.{v, u} X
⊢ (P.homotopyEquiv Q).inv ≫ P.π = Q.π

Tactic:
simp [homotopyEquiv]

Premises used: CategoryTheory.ProjectiveResolution.homotopyEquiv
-- 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 : C
h :
  Homotopy (C := ProjectiveResolution.complex (projectiveResolution X))
    (ProjectiveResolution.lift (𝟙 X) (projectiveResolution X) (projectiveResolution X))
    (𝟙 (ProjectiveResolution.complex (projectiveResolution X)))
⊢ 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))))

Tactic:
apply HomotopyCategory.eq_of_homotopy

Premises used: HomotopyCategory.eq_of_homotopy
-- 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 : C
⊢ Homotopy (C := ProjectiveResolution.complex (projectiveResolution X))
    (ProjectiveResolution.lift (𝟙 X) (projectiveResolution X) (projectiveResolution X))
    (𝟙 (ProjectiveResolution.complex (projectiveResolution X)))

Tactic:
apply ProjectiveResolution.liftIdHomotopy

Premises used: CategoryTheory.ProjectiveResolution.liftIdHomotopy
-- 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 Z : C
f : X ⟶ Y
g : Y ⟶ Z
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)))
⊢ 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))))

Tactic:
apply HomotopyCategory.eq_of_homotopy

Premises used: HomotopyCategory.eq_of_homotopy
-- 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 Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ 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 ProjectiveResolution.liftCompHomotopy

Premises used: CategoryTheory.ProjectiveResolution.liftCompHomotopy
-- 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)
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))
⊢ 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)

Tactic:
apply HomotopyCategory.eq_of_homotopy

Premises used: HomotopyCategory.eq_of_homotopy
-- 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)
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
h₁ :
  CategoryStruct.comp (Y := complex (projectiveResolution Y))
      (φ ≫ HomotopyEquiv.inv (homotopyEquiv (projectiveResolution Y) Q)) (π (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))

Tactic:
apply liftHomotopy f

Premises used: CategoryTheory.ProjectiveResolution.liftHomotopy