awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
n : ℕ
X Y : C
f : X ⟶ Y
P : ProjectiveResolution.{v, u} X
Q : ProjectiveResolution.{v, u} Y
g : P.complex ⟶ Q.complex
w : g ≫ Q.π = P.π ≫ map (ChainComplex.single₀ C) f
rw :
  Eq (α := P.complex.X 0 ⟶ HomologicalComplex.X.{v, u, 0} (obj (ChainComplex.single₀ C) Y) 0) (g.f 0 ≫ Q.π.f 0)
    (P.π.f 0 ≫ f)
⊢ (F.leftDerived n).map f =
    Iso.hom (P.isoLeftDerivedObj F n) ≫
      map
          (comp (D := HomologicalComplex.{v_1, u_1, 0} D (ComplexShape.down ℕ))
            (F.mapHomologicalComplex (ComplexShape.down ℕ))
            (HomologicalComplex.homologyFunctor D (ComplexShape.down ℕ) n))
          g ≫
        Iso.inv (Q.isoLeftDerivedObj F n)

Tactic:
rw [← cancel_mono (Q.isoLeftDerivedObj F n).hom,
    ProjectiveResolution.isoLeftDerivedObj_hom_naturality f P Q g _ F n,
    assoc, assoc, Iso.inv_hom_id, comp_id]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.inv_hom_id, CategoryTheory.ProjectiveResolution.isoLeftDerivedObj, CategoryTheory.ProjectiveResolution.isoLeftDerivedObj_hom_naturality, CategoryTheory.cancel_mono, CategoryTheory.Category.comp_id, CategoryTheory.Iso.hom
-- 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
n : ℕ
X Y : C
f : X ⟶ Y
P : ProjectiveResolution.{v, u} X
Q : ProjectiveResolution.{v, u} Y
g : P.complex ⟶ Q.complex
w : g ≫ Q.π = P.π ≫ map (ChainComplex.single₀ C) f
rw :
  Eq (α := P.complex.X 0 ⟶ HomologicalComplex.X.{v, u, 0} (obj (ChainComplex.single₀ C) Y) 0) ((g ≫ Q.π).f 0)
    (P.π.f 0 ≫ f)
rw₁ :
  Eq (α := P.complex.X 0 ⟶ HomologicalComplex.X.{v, u, 0} (obj (ChainComplex.single₀ C) Y) 0)
    ((P.π ≫ map (ChainComplex.single₀ C) f).f 0) (P.π.f 0 ≫ f)
rw₂ :
  Eq (α := P.complex.X 0 ⟶ HomologicalComplex.X.{v, u, 0} (obj (ChainComplex.single₀ C) Y) 0)
    (P.π.f 0 ≫ HomologicalComplex.Hom.f (map (ChainComplex.single₀ C) f) 0) (P.π.f 0 ≫ f)
rw₃ rw₄ :
  Eq (α := P.complex.X 0 ⟶ HomologicalComplex.X.{v, u, 0} (obj (ChainComplex.single₀ C) Y) 0) (P.π.f 0 ≫ f)
    (P.π.f 0 ≫ f)
⊢ Eq (α := P.complex.X 0 ⟶ HomologicalComplex.X.{v, u, 0} (obj (ChainComplex.single₀ C) Y) 0) (g.f 0 ≫ Q.π.f 0)
    (P.π.f 0 ≫ f)

Tactic:
rw [← HomologicalComplex.comp_f, w, HomologicalComplex.comp_f,
    ChainComplex.single₀_map_f_zero]

Premises used: HomologicalComplex.comp_f, ChainComplex.single₀_map_f_zero
-- 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 G : Functor.{v, v_1, u, u_1} C D
inst_5 : F.Additive
inst_6 : G.Additive
α : F ⟶ G
X : C
P : ProjectiveResolution.{v, u} X
rw :
  Eq (α :=
    Quiver.Hom (V := HomotopyCategory.{v_1, u_1, 0} D (ComplexShape.down ℕ))
      (Functor.obj F.leftDerivedToHomotopyCategory X)
      (Functor.obj (G.mapHomologicalComplex (ComplexShape.down ℕ) ⋙ HomotopyCategory.quotient D (ComplexShape.down ℕ))
        P.complex))
    (CategoryStruct.comp (Y := Functor.obj G.leftDerivedToHomotopyCategory X)
        (NatTrans.app (NatTrans.leftDerivedToHomotopyCategory α) X)
        (Iso.hom (P.isoLeftDerivedToHomotopyCategoryObj G)) :
      Quiver.Hom (V := HomotopyCategory.{v_1, u_1, 0} D (ComplexShape.down ℕ))
        (Functor.obj F.leftDerivedToHomotopyCategory X)
        (Functor.obj (G.mapHomologicalComplex (ComplexShape.down ℕ) ⋙ HomotopyCategory.quotient D (ComplexShape.down ℕ))
          P.complex))
    (Iso.hom (P.isoLeftDerivedToHomotopyCategoryObj F) ≫
        Functor.map (HomotopyCategory.quotient D (ComplexShape.down ℕ))
          (NatTrans.app (NatTrans.mapHomologicalComplex α (ComplexShape.down ℕ)) P.complex) :
      Quiver.Hom (V := HomotopyCategory.{v_1, u_1, 0} D (ComplexShape.down ℕ))
        (Functor.obj F.leftDerivedToHomotopyCategory X)
        (Functor.obj (G.mapHomologicalComplex (ComplexShape.down ℕ) ⋙ HomotopyCategory.quotient D (ComplexShape.down ℕ))
          P.complex))
⊢ Eq (α :=
    Quiver.Hom (V := HomotopyCategory.{v_1, u_1, 0} D (ComplexShape.down ℕ))
      (Functor.obj F.leftDerivedToHomotopyCategory X) (Functor.obj G.leftDerivedToHomotopyCategory X))
    (NatTrans.app (NatTrans.leftDerivedToHomotopyCategory α) X)
    (Iso.hom (P.isoLeftDerivedToHomotopyCategoryObj F) ≫
      Functor.map (HomotopyCategory.quotient D (ComplexShape.down ℕ))
          (NatTrans.app (NatTrans.mapHomologicalComplex α (ComplexShape.down ℕ)) P.complex) ≫
        Iso.inv (P.isoLeftDerivedToHomotopyCategoryObj G))

Tactic:
rw [← cancel_mono (P.isoLeftDerivedToHomotopyCategoryObj G).hom, assoc, assoc,
      Iso.inv_hom_id, comp_id]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.inv_hom_id, CategoryTheory.ProjectiveResolution.isoLeftDerivedToHomotopyCategoryObj, CategoryTheory.cancel_mono, CategoryTheory.Category.comp_id, CategoryTheory.Iso.hom
-- 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 G : Functor.{v, v_1, u, u_1} C D
inst_5 : F.Additive
inst_6 : G.Additive
α : F ⟶ G
X : C
P : ProjectiveResolution.{v, u} X
β : complex (projectiveResolution X) ⟶ P.complex
hβ :
  Eq (α :=
    Functor.obj (HomotopyCategory.quotient C (ComplexShape.down ℕ)) (complex (projectiveResolution X)) ⟶
      Functor.obj (HomotopyCategory.quotient C (ComplexShape.down ℕ)) P.complex)
    (Functor.map (HomotopyCategory.quotient C (ComplexShape.down ℕ)) β) (Iso.hom P.iso)
⊢ Eq (α :=
    Quiver.Hom (V := HomotopyCategory.{v_1, u_1, 0} D (ComplexShape.down ℕ))
      (Functor.obj F.leftDerivedToHomotopyCategory X)
      (Functor.obj (HomotopyCategory.quotient D (ComplexShape.down ℕ))
        (Functor.obj (G.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex)))
    (Functor.map (HomotopyCategory.quotient D (ComplexShape.down ℕ))
        (NatTrans.app (NatTrans.mapHomologicalComplex α (ComplexShape.down ℕ))
            (Quotient.as (r := homotopic C (ComplexShape.down ℕ)) (Functor.obj (projectiveResolutions C) X)) ≫
          Functor.map (G.mapHomologicalComplex (ComplexShape.down ℕ)) β) :
      Quiver.Hom (V := HomotopyCategory.{v_1, u_1, 0} D (ComplexShape.down ℕ))
        (Functor.obj (HomotopyCategory.quotient D (ComplexShape.down ℕ))
          (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))))
        (Functor.obj (HomotopyCategory.quotient D (ComplexShape.down ℕ))
          (Functor.obj (G.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex)))
    (Functor.map (HomotopyCategory.quotient D (ComplexShape.down ℕ))
      (NatTrans.app (NatTrans.mapHomologicalComplex α (ComplexShape.down ℕ)) (complex (projectiveResolution X)) ≫
        Functor.map (G.mapHomologicalComplex (ComplexShape.down ℕ)) β))

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
F : Functor.{v, v_1, u, u_1} C D
inst_5 : F.Additive
⊢ Eq (α :=
    Quiver.Hom (V := C ⥤ HomotopyCategory.{v_1, u_1, 0} D (ComplexShape.down ℕ)) F.leftDerivedToHomotopyCategory
      F.leftDerivedToHomotopyCategory)
    (leftDerivedToHomotopyCategory (𝟙 F)) (𝟙 F.leftDerivedToHomotopyCategory)

Tactic:
rfl

Premises used: HomologicalComplex.id, CategoryTheory.Functor.whiskerLeft, CategoryTheory.Functor.leftDerivedToHomotopyCategory, CategoryTheory.NatTrans.id, CategoryTheory.NatTrans.leftDerivedToHomotopyCategory, 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
F G H : Functor.{v, v_1, u, u_1} C D
α : F ⟶ G
β : G ⟶ H
inst_5 : F.Additive
inst_6 : G.Additive
inst_7 : H.Additive
⊢ Eq (α :=
    Quiver.Hom (V := C ⥤ HomotopyCategory.{v_1, u_1, 0} D (ComplexShape.down ℕ)) F.leftDerivedToHomotopyCategory
      H.leftDerivedToHomotopyCategory)
    (leftDerivedToHomotopyCategory (α ≫ β))
    (CategoryStruct.comp (Y := G.leftDerivedToHomotopyCategory) (leftDerivedToHomotopyCategory α)
      (leftDerivedToHomotopyCategory β))

Tactic:
rfl

Premises used: CategoryTheory.NatTrans.vcomp, CategoryTheory.Functor.whiskerLeft, CategoryTheory.Functor.leftDerivedToHomotopyCategory, CategoryTheory.Quotient.comp, HomologicalComplex.comp, CategoryTheory.NatTrans.leftDerivedToHomotopyCategory, 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
F : Functor.{v, v_1, u, u_1} C D
inst_5 : F.Additive
n : ℕ
simp :
  𝟙
      (Functor.comp (D := HomotopyCategory.{v_1, u_1, 0} D (ComplexShape.down ℕ)) F.leftDerivedToHomotopyCategory
        (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n)) =
    𝟙 (F.leftDerived n)
⊢ Functor.whiskerRight (leftDerivedToHomotopyCategory (𝟙 F))
      (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n) =
    𝟙 (F.leftDerived n)

Tactic:
simp only [leftDerivedToHomotopyCategory_id, Functor.whiskerRight_id']

Premises used: CategoryTheory.Functor.whiskerRight_id', CategoryTheory.NatTrans.leftDerivedToHomotopyCategory_id
-- 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
n : ℕ
⊢ 𝟙
      (Functor.comp (D := HomotopyCategory.{v_1, u_1, 0} D (ComplexShape.down ℕ)) F.leftDerivedToHomotopyCategory
        (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n)) =
    𝟙 (F.leftDerived n)

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
F G H : Functor.{v, v_1, u, u_1} C D
inst_5 : F.Additive
inst_6 : G.Additive
inst_7 : H.Additive
α : F ⟶ G
β : G ⟶ H
n : ℕ
⊢ Eq (α := F.leftDerived n ⟶ H.leftDerived n) (leftDerived (α ≫ β) n)
    (CategoryStruct.comp (Y := G.leftDerived n) (leftDerived α n) (leftDerived β n))

Tactic:
simp [NatTrans.leftDerived]

Premises used: CategoryTheory.NatTrans.leftDerived
-- 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 G : Functor.{v, v_1, u, u_1} C D
inst_5 : F.Additive
inst_6 : G.Additive
α : F ⟶ G
X : C
P : ProjectiveResolution.{v, u} X
n : ℕ
dsimp :
  Eq (α := (F.leftDerived n).obj X ⟶ (G.leftDerived n).obj X)
    (Functor.map (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n)
      (NatTrans.app (NatTrans.leftDerivedToHomotopyCategory α) X))
    ((Functor.map (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n)
          (Iso.hom (P.isoLeftDerivedToHomotopyCategoryObj F)) ≫
        NatTrans.app (Iso.hom (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) n))
          (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex)) ≫
      HomologicalComplex.homologyMap (NatTrans.app (NatTrans.mapHomologicalComplex α (ComplexShape.down ℕ)) P.complex)
          n ≫
        NatTrans.app (Iso.inv (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) n))
            (Functor.obj (G.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex) ≫
          Functor.map (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n)
            (Iso.inv (P.isoLeftDerivedToHomotopyCategoryObj G)))
⊢ Eq (α := (F.leftDerived n).obj X ⟶ (G.leftDerived n).obj X) (NatTrans.app (NatTrans.leftDerived α n) X)
    (Iso.hom (P.isoLeftDerivedObj F n) ≫
      Functor.map (HomologicalComplex.homologyFunctor D (ComplexShape.down ℕ) n)
          (NatTrans.app (NatTrans.mapHomologicalComplex α (ComplexShape.down ℕ)) P.complex) ≫
        Iso.inv (P.isoLeftDerivedObj G n))

Tactic:
dsimp [NatTrans.leftDerived, isoLeftDerivedObj]

Premises used: CategoryTheory.ProjectiveResolution.isoLeftDerivedObj, CategoryTheory.NatTrans.leftDerived
-- 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 G : Functor.{v, v_1, u, u_1} C D
inst_5 : F.Additive
inst_6 : G.Additive
α : F ⟶ G
X : C
P : ProjectiveResolution.{v, u} X
n : ℕ
rw :
  Eq (α := (F.leftDerived n).obj X ⟶ (G.leftDerived n).obj X)
    (Functor.map (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n)
        (Iso.hom (P.isoLeftDerivedToHomotopyCategoryObj F)) ≫
      Functor.map (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n)
          (Functor.map (HomotopyCategory.quotient D (ComplexShape.down ℕ))
            (NatTrans.app (NatTrans.mapHomologicalComplex α (ComplexShape.down ℕ)) P.complex)) ≫
        Functor.map (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n)
          (Iso.inv (P.isoLeftDerivedToHomotopyCategoryObj G)))
    (Functor.map (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n)
        (Iso.hom (P.isoLeftDerivedToHomotopyCategoryObj F)) ≫
      NatTrans.app (Iso.hom (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) n))
          (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex) ≫
        HomologicalComplex.homologyMap (NatTrans.app (NatTrans.mapHomologicalComplex α (ComplexShape.down ℕ)) P.complex)
            n ≫
          NatTrans.app (Iso.inv (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) n))
              (Functor.obj (G.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex) ≫
            Functor.map (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n)
              (Iso.inv (P.isoLeftDerivedToHomotopyCategoryObj G)))
⊢ Eq (α := (F.leftDerived n).obj X ⟶ (G.leftDerived n).obj X)
    (Functor.map (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n)
      (NatTrans.app (NatTrans.leftDerivedToHomotopyCategory α) X))
    ((Functor.map (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n)
          (Iso.hom (P.isoLeftDerivedToHomotopyCategoryObj F)) ≫
        NatTrans.app (Iso.hom (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) n))
          (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex)) ≫
      HomologicalComplex.homologyMap (NatTrans.app (NatTrans.mapHomologicalComplex α (ComplexShape.down ℕ)) P.complex)
          n ≫
        NatTrans.app (Iso.inv (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) n))
            (Functor.obj (G.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex) ≫
          Functor.map (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n)
            (Iso.inv (P.isoLeftDerivedToHomotopyCategoryObj G)))

Tactic:
rw [ProjectiveResolution.leftDerivedToHomotopyCategory_app_eq α P,
    Functor.map_comp, Functor.map_comp, assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.ProjectiveResolution.leftDerivedToHomotopyCategory_app_eq, CategoryTheory.Functor.map_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 G : Functor.{v, v_1, u, u_1} C D
inst_5 : F.Additive
inst_6 : G.Additive
α : F ⟶ G
X : C
P : ProjectiveResolution.{v, u} X
n : ℕ
⊢ Eq (α := (F.leftDerived n).obj X ⟶ (G.leftDerived n).obj X)
    (Functor.map (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n)
        (Iso.hom (P.isoLeftDerivedToHomotopyCategoryObj F)) ≫
      Functor.map (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n)
          (Functor.map (HomotopyCategory.quotient D (ComplexShape.down ℕ))
            (NatTrans.app (NatTrans.mapHomologicalComplex α (ComplexShape.down ℕ)) P.complex)) ≫
        Functor.map (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n)
          (Iso.inv (P.isoLeftDerivedToHomotopyCategoryObj G)))
    (Functor.map (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n)
        (Iso.hom (P.isoLeftDerivedToHomotopyCategoryObj F)) ≫
      Functor.map
          (HomotopyCategory.quotient D (ComplexShape.down ℕ) ⋙
            HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n)
          (NatTrans.app (NatTrans.mapHomologicalComplex α (ComplexShape.down ℕ)) P.complex) ≫
        NatTrans.app (Iso.hom (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) n))
            (Functor.obj (G.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex) ≫
          NatTrans.app (Iso.inv (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) n))
              (Functor.obj (G.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex) ≫
            Functor.map (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n)
              (Iso.inv (P.isoLeftDerivedToHomotopyCategoryObj G)))

Tactic:
simp only [Functor.comp_map, Iso.hom_inv_id_app_assoc]

Premises used: CategoryTheory.Iso.hom_inv_id_app_assoc, CategoryTheory.Functor.comp_map
-- 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
⊢ (ComplexShape.down ℕ).prev 0 = 1

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
dsimp :
  Eq (α := F.obj (P.complex.X 1) ⟶ F.obj X)
    (CategoryStruct.comp (Y := F.obj (P.complex.X 0)) (F.map (P.complex.d 1 0)) (F.map (P.π.f 0)) :
      F.obj (P.complex.X 1) ⟶ F.obj X)
    (0 : HomologicalComplex.X (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex) 1 ⟶ F.obj X)
⊢ Eq (α := HomologicalComplex.X (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex) 1 ⟶ F.obj X)
    (CategoryStruct.comp (Y :=
      HomologicalComplex.X (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex) 0)
      (HomologicalComplex.d (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex) 1 0)
      (F.map (P.π.f 0)))
    0

Tactic:
dsimp
-- 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
rw :
  Eq (α := F.obj (P.complex.X 1) ⟶ F.obj X)
    (F.map (CategoryStruct.comp (Y := P.complex.X 0) (P.complex.d 1 0) (P.π.f 0)) : F.obj (P.complex.X 1) ⟶ F.obj X)
    (0 : HomologicalComplex.X (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex) 1 ⟶ F.obj X)
rw₁ : Eq (α := F.obj (P.complex.X 1) ⟶ F.obj X) (F.map 0) 0
rw₂ rw₃ : Eq.{v_1 + 1} (α := F.obj (P.complex.X 1) ⟶ F.obj X) 0 0
⊢ Eq (α := F.obj (P.complex.X 1) ⟶ F.obj X)
    (CategoryStruct.comp (Y := F.obj (P.complex.X 0)) (F.map (P.complex.d 1 0)) (F.map (P.π.f 0)) :
      F.obj (P.complex.X 1) ⟶ F.obj X)
    (0 : HomologicalComplex.X (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex) 1 ⟶ F.obj X)

Tactic:
rw [← F.map_comp, complex_d_comp_π_f_zero, F.map_zero]

Premises used: CategoryTheory.Functor.map_zero, CategoryTheory.ProjectiveResolution.complex_d_comp_π_f_zero, CategoryTheory.Functor.map_comp
-- 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 : C
P : ProjectiveResolution.{v_2, u_2} X
F : Functor.{v_2, v_1, u_2, u_1} C D
inst_4 : F.Additive
⊢ Eq (α := HomologicalComplex.X (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex) 0 ⟶ F.obj X)
    (CategoryStruct.comp (Y :=
        HomologicalComplex.opcycles (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex) 0)
        (HomologicalComplex.pOpcycles (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex) 0 :
          HomologicalComplex.X (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex) 0 ⟶
            HomologicalComplex.opcycles (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex) 0)
        (P.fromLeftDerivedZero' F :
          HomologicalComplex.opcycles (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex) 0 ⟶
            F.obj X) :
      HomologicalComplex.X (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex) 0 ⟶ F.obj X)
    (F.map (P.π.f 0) :
      F.obj (P.complex.X 0) ⟶ F.obj (HomologicalComplex.X.{v_2, u_2, 0} (Functor.obj (ChainComplex.single₀ C) X) 0))

Tactic:
simp [fromLeftDerivedZero']

Premises used: CategoryTheory.ProjectiveResolution.fromLeftDerivedZero'