awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Abelian.LeftDerived
Goal:
D : Type u_1
inst : Category.{v_1, u_1} D
inst_1 : Abelian.{v_1, u_1} D
C : Type u_2
inst_2 : Category.{v_2, u_2} C
inst_3 : Abelian.{v_2, u_2} C
X Y : C
f : X ⟶ Y
P : ProjectiveResolution.{v_2, u_2} X
Q : ProjectiveResolution.{v_2, u_2} Y
φ : P.complex ⟶ Q.complex
comm :
  Eq (α := P.complex.X 0 ⟶ HomologicalComplex.X.{v_2, u_2, 0} (Functor.obj (ChainComplex.single₀ C) Y) 0)
    (φ.f 0 ≫ Q.π.f 0) (P.π.f 0 ≫ f)
F : Functor.{v_2, v_1, u_2, u_1} C D
inst_4 : F.Additive
⊢ Eq (α :=
    HomologicalComplex.opcycles (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex) 0 ⟶ F.obj Y)
    (CategoryStruct.comp (Y :=
        HomologicalComplex.opcycles (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) Q.complex) 0)
        (HomologicalComplex.opcyclesMap (Functor.map (F.mapHomologicalComplex (ComplexShape.down ℕ)) φ) 0 :
          HomologicalComplex.opcycles (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex) 0 ⟶
            HomologicalComplex.opcycles (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) Q.complex) 0)
        (Q.fromLeftDerivedZero' F :
          HomologicalComplex.opcycles (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) Q.complex) 0 ⟶
            F.obj Y) :
      HomologicalComplex.opcycles (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex) 0 ⟶ F.obj Y)
    (P.fromLeftDerivedZero' F ≫ F.map f :
      HomologicalComplex.opcycles (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex) 0 ⟶ F.obj Y)

Tactic:
simp only [← cancel_epi (HomologicalComplex.pOpcycles _ _), ← F.map_comp, comm,
    HomologicalComplex.p_opcyclesMap_assoc, Functor.mapHomologicalComplex_map_f,
    pOpcycles_comp_fromLeftDerivedZero', pOpcycles_comp_fromLeftDerivedZero'_assoc]

Premises used: CategoryTheory.Functor.mapHomologicalComplex_map_f, CategoryTheory.ProjectiveResolution.pOpcycles_comp_fromLeftDerivedZero'_assoc, CategoryTheory.ProjectiveResolution.pOpcycles_comp_fromLeftDerivedZero', HomologicalComplex.pOpcycles, CategoryTheory.Functor.map_comp, CategoryTheory.cancel_epi, HomologicalComplex.p_opcyclesMap_assoc
-- Module: Mathlib.CategoryTheory.Abelian.LeftDerived
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
inst_2 : Abelian.{v, u} C
inst_3 : HasProjectiveResolutions.{v, u} C
inst_4 : Abelian.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
inst_5 : F.Additive
X : C
inst_6 : Projective.{v, u} X
dsimp :
  IsIso (X :=
    HomologicalComplex.opcycles
      (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.down ℕ))
        (F.mapHomologicalComplex (ComplexShape.down ℕ)) (Functor.obj (ChainComplex.single₀ C) X))
      0)
    (HomologicalComplex.descOpcycles
        (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.down ℕ))
          (F.mapHomologicalComplex (ComplexShape.down ℕ)) (Functor.obj (ChainComplex.single₀ C) X))
        (F.map (𝟙 X)) 1 fromLeftDerivedZero'._proof_1 ⋯ :
      HomologicalComplex.opcycles
          (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.down ℕ))
            (F.mapHomologicalComplex (ComplexShape.down ℕ)) (Functor.obj (ChainComplex.single₀ C) X))
          0 ⟶
        F.obj X)
⊢ IsIso (X :=
    HomologicalComplex.opcycles
      (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.down ℕ))
        (F.mapHomologicalComplex (ComplexShape.down ℕ)) (complex (self X)))
      0)
    (fromLeftDerivedZero' (self X) F :
      HomologicalComplex.opcycles
          (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.down ℕ))
            (F.mapHomologicalComplex (ComplexShape.down ℕ)) (complex (self X)))
          0 ⟶
        F.obj X)

Tactic:
dsimp [ProjectiveResolution.fromLeftDerivedZero']

Premises used: CategoryTheory.ProjectiveResolution.fromLeftDerivedZero'
-- Module: Mathlib.CategoryTheory.Abelian.LeftDerived
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
inst_2 : Abelian.{v, u} C
inst_3 : HasProjectiveResolutions.{v, u} C
inst_4 : Abelian.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
inst_5 : F.Additive
X : C
inst_6 : Projective.{v, u} X
rw :
  ShortComplex.Exact
      (ShortComplex.mk (X₁ :=
        HomologicalComplex.X
          (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.down ℕ))
            (F.mapHomologicalComplex (ComplexShape.down ℕ)) (Functor.obj (ChainComplex.single₀ C) X))
          1)
        (HomologicalComplex.d
          (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.down ℕ))
            (F.mapHomologicalComplex (ComplexShape.down ℕ)) (Functor.obj (ChainComplex.single₀ C) X))
          1 0)
        (F.map (𝟙 X)) ⋯) ∧
    Epi (F.map (𝟙 X))
⊢ IsIso (X :=
    HomologicalComplex.opcycles
      (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.down ℕ))
        (F.mapHomologicalComplex (ComplexShape.down ℕ)) (Functor.obj (ChainComplex.single₀ C) X))
      0)
    (HomologicalComplex.descOpcycles
        (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.down ℕ))
          (F.mapHomologicalComplex (ComplexShape.down ℕ)) (Functor.obj (ChainComplex.single₀ C) X))
        (F.map (𝟙 X)) 1 fromLeftDerivedZero'._proof_1 ⋯ :
      HomologicalComplex.opcycles
          (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.down ℕ))
            (F.mapHomologicalComplex (ComplexShape.down ℕ)) (Functor.obj (ChainComplex.single₀ C) X))
          0 ⟶
        F.obj X)

Tactic:
rw [ChainComplex.isIso_descOpcycles_iff]

Premises used: ChainComplex.isIso_descOpcycles_iff
-- Module: Mathlib.CategoryTheory.Abelian.LeftDerived
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
inst_2 : Abelian.{v, u} C
inst_3 : HasProjectiveResolutions.{v, u} C
inst_4 : Abelian.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
inst_5 : F.Additive
X : C
inst_6 : Projective.{v, u} X
⊢ ShortComplex.Exact
      (ShortComplex.mk (X₁ :=
        HomologicalComplex.X
          (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.down ℕ))
            (F.mapHomologicalComplex (ComplexShape.down ℕ)) (Functor.obj (ChainComplex.single₀ C) X))
          1)
        (HomologicalComplex.d
          (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.down ℕ))
            (F.mapHomologicalComplex (ComplexShape.down ℕ)) (Functor.obj (ChainComplex.single₀ C) X))
          1 0)
        (F.map (𝟙 X)) ⋯) ∧
    Epi (F.map (𝟙 X))

Tactic:
⟨ShortComplex.Splitting.exact ?_, inferInstance⟩

Premises used: CategoryTheory.ShortComplex.Splitting.exact, inferInstance, And.intro
-- Module: Mathlib.CategoryTheory.Abelian.LeftDerived
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
inst_2 : Abelian.{v, u} C
inst_3 : HasProjectiveResolutions.{v, u} C
inst_4 : Abelian.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
inst_5 : F.Additive
X : C
inst_6 : Projective.{v, u} X
refine :
  ShortComplex.Splitting
    (ShortComplex.mk (X₁ :=
      HomologicalComplex.X
        (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.down ℕ))
          (F.mapHomologicalComplex (ComplexShape.down ℕ)) (Functor.obj (ChainComplex.single₀ C) X))
        1)
      (HomologicalComplex.d
        (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.down ℕ))
          (F.mapHomologicalComplex (ComplexShape.down ℕ)) (Functor.obj (ChainComplex.single₀ C) X))
        1 0)
      (F.map (𝟙 X)) ⋯)
⊢ ShortComplex.Exact
      (ShortComplex.mk (X₁ :=
        HomologicalComplex.X
          (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.down ℕ))
            (F.mapHomologicalComplex (ComplexShape.down ℕ)) (Functor.obj (ChainComplex.single₀ C) X))
          1)
        (HomologicalComplex.d
          (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.down ℕ))
            (F.mapHomologicalComplex (ComplexShape.down ℕ)) (Functor.obj (ChainComplex.single₀ C) X))
          1 0)
        (F.map (𝟙 X)) ⋯) ∧
    Epi (F.map (𝟙 X))

Tactic:
refine ⟨ShortComplex.Splitting.exact ?_, inferInstance⟩
-- Module: Mathlib.CategoryTheory.Abelian.LeftDerived
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
inst_2 : Abelian.{v, u} C
inst_3 : HasProjectiveResolutions.{v, u} C
inst_4 : Abelian.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
inst_5 : F.Additive
X : C
inst_6 : Projective.{v, u} X
⊢ ShortComplex.Splitting
    (ShortComplex.mk (X₁ :=
      HomologicalComplex.X
        (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.down ℕ))
          (F.mapHomologicalComplex (ComplexShape.down ℕ)) (Functor.obj (ChainComplex.single₀ C) X))
        1)
      (HomologicalComplex.d
        (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.down ℕ))
          (F.mapHomologicalComplex (ComplexShape.down ℕ)) (Functor.obj (ChainComplex.single₀ C) X))
        1 0)
      (F.map (𝟙 X)) ⋯)

Tactic:
exact
    { r := 0
      s := 𝟙 _
      f_r := (F.map_isZero (isZero_zero _)).eq_of_src _ _ }
-- Module: Mathlib.CategoryTheory.Abelian.LeftDerived
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
inst_2 : Abelian.{v, u} C
inst_3 : HasProjectiveResolutions.{v, u} C
inst_4 : Abelian.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
inst_5 : F.Additive
X Y : C
f : X ⟶ Y
⊢ Eq (α :=
    HomologicalComplex.X.{v, u, 0} (ProjectiveResolution.complex (projectiveResolution X)) 0 ⟶
      HomologicalComplex.X.{v, u, 0} (obj (ChainComplex.single₀ C) Y) 0)
    (CategoryStruct.comp (Y := HomologicalComplex.X.{v, u, 0} (ProjectiveResolution.complex (projectiveResolution Y)) 0)
      (HomologicalComplex.Hom.f (ProjectiveResolution.lift f (projectiveResolution X) (projectiveResolution Y)) 0)
      (HomologicalComplex.Hom.f (ProjectiveResolution.π (projectiveResolution Y)) 0))
    (HomologicalComplex.Hom.f (ProjectiveResolution.π (projectiveResolution X)) 0 ≫ f)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Abelian.LeftDerived
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
inst_2 : Abelian.{v, u} C
inst_3 : HasProjectiveResolutions.{v, u} C
inst_4 : Abelian.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
inst_5 : F.Additive
X Y : C
f : X ⟶ Y
⊢ Eq (α :=
    obj (C := HomotopyCategory.{v_1, u_1, 0} D (ComplexShape.down ℕ))
        (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) 0) (obj F.leftDerivedToHomotopyCategory X) ⟶
      F.obj Y)
    (map (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) 0) (map F.leftDerivedToHomotopyCategory f) ≫
      NatTrans.app (Iso.hom (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) 0))
          (obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.down ℕ))
            (F.mapHomologicalComplex (ComplexShape.down ℕ))
            (Quotient.as (r := homotopic C (ComplexShape.down ℕ)) (obj (projectiveResolutions C) Y))) ≫
        HomologicalComplex.homologyι
            (obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.down ℕ))
              (F.mapHomologicalComplex (ComplexShape.down ℕ))
              (Quotient.as (r := homotopic C (ComplexShape.down ℕ)) (obj (projectiveResolutions C) Y)))
            0 ≫
          ProjectiveResolution.fromLeftDerivedZero' (projectiveResolution Y) F)
    (CategoryStruct.comp (Y :=
      obj (C := HomologicalComplex.{v_1, u_1, 0} D (ComplexShape.down ℕ))
        (HomotopyCategory.quotient D (ComplexShape.down ℕ) ⋙ HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) 0)
        (obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.down ℕ)) (F.mapHomologicalComplex (ComplexShape.down ℕ))
          (ProjectiveResolution.complex (projectiveResolution Y))))
      (map
        (HomotopyCategory.quotient D (ComplexShape.down ℕ) ⋙ HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) 0)
        (map (F.mapHomologicalComplex (ComplexShape.down ℕ))
          (ProjectiveResolution.lift f (projectiveResolution X) (projectiveResolution Y))))
      (NatTrans.app (Iso.hom (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) 0))
          (obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.down ℕ))
            (F.mapHomologicalComplex (ComplexShape.down ℕ)) (ProjectiveResolution.complex (projectiveResolution Y))) ≫
        HomologicalComplex.homologyι
            (obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.down ℕ))
              (F.mapHomologicalComplex (ComplexShape.down ℕ)) (ProjectiveResolution.complex (projectiveResolution Y)))
            0 ≫
          ProjectiveResolution.fromLeftDerivedZero' (projectiveResolution Y) F))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Abelian.LeftDerived
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
inst_2 : Abelian.{v, u} C
inst_3 : HasProjectiveResolutions.{v, u} C
inst_4 : Abelian.{v_1, u_1} D
X : C
P : ProjectiveResolution.{v, u} X
F : Functor.{v, v_1, u, u_1} C D
inst_5 : F.Additive
dsimp :
  Eq (α := (F.leftDerived 0).obj X ⟶ F.obj X)
    (NatTrans.app (Iso.hom (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) 0))
          (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.down ℕ))
            (F.mapHomologicalComplex (ComplexShape.down ℕ))
            (Quotient.as (r := homotopic C (ComplexShape.down ℕ)) (Functor.obj (projectiveResolutions C) X))) ≫
        HomologicalComplex.homologyι
            (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.down ℕ))
              (F.mapHomologicalComplex (ComplexShape.down ℕ))
              (Quotient.as (r := homotopic C (ComplexShape.down ℕ)) (Functor.obj (projectiveResolutions C) X)))
            0 ≫
          fromLeftDerivedZero' (projectiveResolution X) F :
      (F.leftDerived 0).obj X ⟶ F.obj X)
    ((Functor.map (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) 0)
            (Iso.hom (P.isoLeftDerivedToHomotopyCategoryObj F)) ≫
          NatTrans.app (Iso.hom (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) 0))
            (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex)) ≫
        HomologicalComplex.homologyι (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex) 0 ≫
          P.fromLeftDerivedZero' F :
      (F.leftDerived 0).obj X ⟶ F.obj X)
⊢ Eq (α := (F.leftDerived 0).obj X ⟶ F.obj X) (NatTrans.app F.fromLeftDerivedZero X)
    (Iso.hom (P.isoLeftDerivedObj F 0) ≫
      Iso.hom (ChainComplex.isoHomologyι₀ (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex)) ≫
        P.fromLeftDerivedZero' F)

Tactic:
dsimp [Functor.fromLeftDerivedZero, isoLeftDerivedObj]

Premises used: CategoryTheory.ProjectiveResolution.isoLeftDerivedObj, CategoryTheory.Functor.fromLeftDerivedZero
-- Module: Mathlib.CategoryTheory.Abelian.LeftDerived
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
inst_2 : Abelian.{v, u} C
inst_3 : HasProjectiveResolutions.{v, u} C
inst_4 : Abelian.{v_1, u_1} D
X : C
P : ProjectiveResolution.{v, u} X
F : Functor.{v, v_1, u, u_1} C D
inst_5 : F.Additive
⊢ Eq (α := P.complex.X 0 ⟶ HomologicalComplex.X.{v, u, 0} (Functor.obj (ChainComplex.single₀ C) X) 0)
    (CategoryStruct.comp (Y := HomologicalComplex.X.{v, u, 0} (complex (projectiveResolution X)) 0)
      (HomologicalComplex.Hom.f (lift (𝟙 X) P (projectiveResolution X)) 0)
      (HomologicalComplex.Hom.f (π (projectiveResolution X)) 0))
    (P.π.f 0 ≫ 𝟙 X)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Abelian.LeftDerived
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
inst_2 : Abelian.{v, u} C
inst_3 : HasProjectiveResolutions.{v, u} C
inst_4 : Abelian.{v_1, u_1} D
X : C
P : ProjectiveResolution.{v, u} X
F : Functor.{v, v_1, u, u_1} C D
inst_5 : F.Additive
⊢ Eq (α :=
    HomologicalComplex.opcycles (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex) 0 ⟶ F.obj X)
    (CategoryStruct.comp (Y :=
        HomologicalComplex.opcycles
          (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.down ℕ))
            (F.mapHomologicalComplex (ComplexShape.down ℕ)) (complex (projectiveResolution X)))
          0)
        (HomologicalComplex.opcyclesMap
            (Functor.map (F.mapHomologicalComplex (ComplexShape.down ℕ)) (lift (𝟙 X) P (projectiveResolution X))) 0 :
          HomologicalComplex.opcycles (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex) 0 ⟶
            HomologicalComplex.opcycles
              (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.down ℕ))
                (F.mapHomologicalComplex (ComplexShape.down ℕ)) (complex (projectiveResolution X)))
              0)
        (fromLeftDerivedZero' (projectiveResolution X) F :
          HomologicalComplex.opcycles
              (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.down ℕ))
                (F.mapHomologicalComplex (ComplexShape.down ℕ)) (complex (projectiveResolution X)))
              0 ⟶
            F.obj X) :
      HomologicalComplex.opcycles (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex) 0 ⟶ F.obj X)
    (P.fromLeftDerivedZero' F ≫ F.map (𝟙 X) :
      HomologicalComplex.opcycles (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex) 0 ⟶ F.obj X)

Tactic:
have h₁ := ProjectiveResolution.fromLeftDerivedZero'_naturality
    (𝟙 X) P (projectiveResolution X) (lift (𝟙 X) _ _) (by simp) F
-- Module: Mathlib.CategoryTheory.Abelian.LeftDerived
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
inst_2 : Abelian.{v, u} C
inst_3 : HasProjectiveResolutions.{v, u} C
inst_4 : Abelian.{v_1, u_1} D
X : C
P : ProjectiveResolution.{v, u} X
F : Functor.{v, v_1, u, u_1} C D
inst_5 : F.Additive
h₁ :
  Eq (α :=
    HomologicalComplex.opcycles (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex) 0 ⟶ F.obj X)
    (CategoryStruct.comp (Y :=
        HomologicalComplex.opcycles
          (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.down ℕ))
            (F.mapHomologicalComplex (ComplexShape.down ℕ)) (complex (projectiveResolution X)))
          0)
        (HomologicalComplex.opcyclesMap
            (Functor.map (F.mapHomologicalComplex (ComplexShape.down ℕ)) (lift (𝟙 X) P (projectiveResolution X))) 0 :
          HomologicalComplex.opcycles (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex) 0 ⟶
            HomologicalComplex.opcycles
              (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.down ℕ))
                (F.mapHomologicalComplex (ComplexShape.down ℕ)) (complex (projectiveResolution X)))
              0)
        (fromLeftDerivedZero' (projectiveResolution X) F :
          HomologicalComplex.opcycles
              (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.down ℕ))
                (F.mapHomologicalComplex (ComplexShape.down ℕ)) (complex (projectiveResolution X)))
              0 ⟶
            F.obj X) :
      HomologicalComplex.opcycles (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex) 0 ⟶ F.obj X)
    (P.fromLeftDerivedZero' F ≫ F.map (𝟙 X) :
      HomologicalComplex.opcycles (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex) 0 ⟶ F.obj X)
⊢ Eq (α :=
    Quiver.Hom (V := HomotopyCategory.{v_1, u_1, 0} D (ComplexShape.down ℕ))
      (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ) ⋙ HomotopyCategory.quotient D (ComplexShape.down ℕ))
        P.complex)
      (Functor.obj F.leftDerivedToHomotopyCategory X))
    (Iso.inv (P.isoLeftDerivedToHomotopyCategoryObj F))
    (Functor.map (F.mapHomologicalComplex (ComplexShape.down ℕ) ⋙ HomotopyCategory.quotient D (ComplexShape.down ℕ))
      (lift (𝟙 X) P (projectiveResolution X)))

Tactic:
have h₂ : (P.isoLeftDerivedToHomotopyCategoryObj F).inv =
    (F.mapHomologicalComplex _ ⋙ HomotopyCategory.quotient _ _).map (lift (𝟙 X) _ _) :=
      id_comp _
-- Module: Mathlib.CategoryTheory.Abelian.LeftDerived
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
inst_2 : Abelian.{v, u} C
inst_3 : HasProjectiveResolutions.{v, u} C
inst_4 : Abelian.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
inst_5 : F.Additive
X : C
inst_6 : Projective.{v, u} X
rw :
  IsIso (X := (F.leftDerived 0).obj X)
    (CategoryStruct.comp (Y :=
      Functor.obj (C := HomologicalComplex.{v_1, u_1, 0} D (ComplexShape.down ℕ))
        (HomologicalComplex.homologyFunctor D (ComplexShape.down ℕ) 0)
        (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.down ℕ))
          (F.mapHomologicalComplex (ComplexShape.down ℕ)) (ProjectiveResolution.complex (ProjectiveResolution.self X))))
      (Iso.hom (ProjectiveResolution.isoLeftDerivedObj (ProjectiveResolution.self X) F 0))
      (Iso.hom
          (ChainComplex.isoHomologyι₀
            (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.down ℕ))
              (F.mapHomologicalComplex (ComplexShape.down ℕ))
              (ProjectiveResolution.complex (ProjectiveResolution.self X)))) ≫
        ProjectiveResolution.fromLeftDerivedZero' (ProjectiveResolution.self X) F))
⊢ IsIso (X := (F.leftDerived 0).obj X) (NatTrans.app F.fromLeftDerivedZero X)

Tactic:
rw [(ProjectiveResolution.self X).fromLeftDerivedZero_eq F]

Premises used: CategoryTheory.ProjectiveResolution.self, CategoryTheory.ProjectiveResolution.fromLeftDerivedZero_eq
-- Module: Mathlib.CategoryTheory.Abelian.LeftDerived
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
inst_2 : Abelian.{v, u} C
inst_3 : HasProjectiveResolutions.{v, u} C
inst_4 : Abelian.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
inst_5 : F.Additive
X : C
inst_6 : Projective.{v, u} X
⊢ IsIso (X := (F.leftDerived 0).obj X)
    (CategoryStruct.comp (Y :=
      Functor.obj (C := HomologicalComplex.{v_1, u_1, 0} D (ComplexShape.down ℕ))
        (HomologicalComplex.homologyFunctor D (ComplexShape.down ℕ) 0)
        (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.down ℕ))
          (F.mapHomologicalComplex (ComplexShape.down ℕ)) (ProjectiveResolution.complex (ProjectiveResolution.self X))))
      (Iso.hom (ProjectiveResolution.isoLeftDerivedObj (ProjectiveResolution.self X) F 0))
      (Iso.hom
          (ChainComplex.isoHomologyι₀
            (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.down ℕ))
              (F.mapHomologicalComplex (ComplexShape.down ℕ))
              (ProjectiveResolution.complex (ProjectiveResolution.self X)))) ≫
        ProjectiveResolution.fromLeftDerivedZero' (ProjectiveResolution.self X) F))

Tactic:
infer_instance