awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Abelian.RightDerived
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 : HasInjectiveResolutions.{v, u} C
inst_4 : Abelian.{v_1, u_1} D
X Y : C
f : X ⟶ Y
I : InjectiveResolution.{v, u} X
J : InjectiveResolution.{v, u} Y
φ : I.cocomplex ⟶ J.cocomplex
comm :
  Eq (α := HomologicalComplex.X.{v, u, 0} (Functor.obj (CochainComplex.single₀ C) X) 0 ⟶ J.cocomplex.X 0)
    (I.ι.f 0 ≫ φ.f 0) (f ≫ J.ι.f 0)
F : Functor.{v, v_1, u, u_1} C D
inst_5 : F.Additive
rw :
  Eq (α :=
    Quiver.Hom (V := HomotopyCategory.{v_1, u_1, 0} D (ComplexShape.up ℕ))
      (Functor.obj F.rightDerivedToHomotopyCategory X) (Functor.obj F.rightDerivedToHomotopyCategory Y))
    (Functor.map F.rightDerivedToHomotopyCategory f)
    (Functor.map F.rightDerivedToHomotopyCategory f ≫
      Iso.hom (J.isoRightDerivedToHomotopyCategoryObj F) ≫ Iso.inv (J.isoRightDerivedToHomotopyCategoryObj F))
rw₁ :
  Eq (α :=
    Quiver.Hom (V := HomotopyCategory.{v_1, u_1, 0} D (ComplexShape.up ℕ))
      (Functor.obj F.rightDerivedToHomotopyCategory X) (Functor.obj F.rightDerivedToHomotopyCategory Y))
    (Functor.map F.rightDerivedToHomotopyCategory f)
    (Functor.map F.rightDerivedToHomotopyCategory f ≫ 𝟙 (Functor.obj F.rightDerivedToHomotopyCategory Y))
rw₂ rw₃ :
  Eq (α :=
    Quiver.Hom (V := HomotopyCategory.{v_1, u_1, 0} D (ComplexShape.up ℕ))
      (Functor.obj F.rightDerivedToHomotopyCategory X) (Functor.obj F.rightDerivedToHomotopyCategory Y))
    (Functor.map F.rightDerivedToHomotopyCategory f) (Functor.map F.rightDerivedToHomotopyCategory f)
⊢ Eq (α :=
    Quiver.Hom (V := HomotopyCategory.{v_1, u_1, 0} D (ComplexShape.up ℕ))
      (Functor.obj F.rightDerivedToHomotopyCategory X) (Functor.obj F.rightDerivedToHomotopyCategory Y))
    (Functor.map F.rightDerivedToHomotopyCategory f)
    (Iso.hom (I.isoRightDerivedToHomotopyCategoryObj F) ≫
      Functor.map (HomotopyCategory.quotient D (ComplexShape.up ℕ))
          (Functor.map (F.mapHomologicalComplex (ComplexShape.up ℕ)) φ) ≫
        Iso.inv (J.isoRightDerivedToHomotopyCategoryObj F))

Tactic:
rw [← isoRightDerivedToHomotopyCategoryObj_hom_naturality_assoc f I J φ comm F,
      Iso.hom_inv_id, comp_id]

Premises used: CategoryTheory.Iso.hom_inv_id, CategoryTheory.Category.comp_id, CategoryTheory.InjectiveResolution.isoRightDerivedToHomotopyCategoryObj_hom_naturality_assoc
-- Module: Mathlib.CategoryTheory.Abelian.RightDerived
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 : HasInjectiveResolutions.{v, u} C
inst_4 : Abelian.{v_1, u_1} D
X Y : C
f : X ⟶ Y
I : InjectiveResolution.{v, u} X
J : InjectiveResolution.{v, u} Y
φ : I.cocomplex ⟶ J.cocomplex
comm :
  Eq (α := HomologicalComplex.X.{v, u, 0} (Functor.obj (CochainComplex.single₀ C) X) 0 ⟶ J.cocomplex.X 0)
    (I.ι.f 0 ≫ φ.f 0) (f ≫ J.ι.f 0)
F : Functor.{v, v_1, u, u_1} C D
inst_5 : F.Additive
n : ℕ
dsimp :
  Eq (α :=
    Functor.obj (C := HomotopyCategory.{v_1, u_1, 0} D (ComplexShape.up ℕ))
        (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n) (Functor.obj F.rightDerivedToHomotopyCategory X) ⟶
      HomologicalComplex.homology (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) J.cocomplex) n)
    (Functor.map (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n)
        (Functor.map F.rightDerivedToHomotopyCategory f) ≫
      Functor.map (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n)
          (Iso.hom (J.isoRightDerivedToHomotopyCategoryObj F)) ≫
        NatTrans.app (Iso.hom (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) n))
          (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) J.cocomplex))
    ((Functor.map (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n)
          (Iso.hom (I.isoRightDerivedToHomotopyCategoryObj F)) ≫
        NatTrans.app (Iso.hom (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) n))
          (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) I.cocomplex)) ≫
      HomologicalComplex.homologyMap (Functor.map (F.mapHomologicalComplex (ComplexShape.up ℕ)) φ) n)
⊢ (F.rightDerived n).map f ≫ Iso.hom (J.isoRightDerivedObj F n) =
    Iso.hom (I.isoRightDerivedObj F n) ≫
      Functor.map
        (Functor.comp (D := HomologicalComplex.{v_1, u_1, 0} D (ComplexShape.up ℕ))
          (F.mapHomologicalComplex (ComplexShape.up ℕ)) (HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n))
        φ

Tactic:
dsimp [isoRightDerivedObj, Functor.rightDerived]

Premises used: CategoryTheory.InjectiveResolution.isoRightDerivedObj, CategoryTheory.Functor.rightDerived
-- Module: Mathlib.CategoryTheory.Abelian.RightDerived
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 : HasInjectiveResolutions.{v, u} C
inst_4 : Abelian.{v_1, u_1} D
X Y : C
f : X ⟶ Y
I : InjectiveResolution.{v, u} X
J : InjectiveResolution.{v, u} Y
φ : I.cocomplex ⟶ J.cocomplex
comm :
  Eq (α := HomologicalComplex.X.{v, u, 0} (Functor.obj (CochainComplex.single₀ C) X) 0 ⟶ J.cocomplex.X 0)
    (I.ι.f 0 ≫ φ.f 0) (f ≫ J.ι.f 0)
F : Functor.{v, v_1, u, u_1} C D
inst_5 : F.Additive
n : ℕ
⊢ Eq (α :=
    Functor.obj (C := HomotopyCategory.{v_1, u_1, 0} D (ComplexShape.up ℕ))
        (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n) (Functor.obj F.rightDerivedToHomotopyCategory X) ⟶
      HomologicalComplex.homology (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) J.cocomplex) n)
    (Functor.map (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n)
        (Iso.hom (I.isoRightDerivedToHomotopyCategoryObj F)) ≫
      NatTrans.app (Iso.hom (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) n))
          (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) I.cocomplex) ≫
        Functor.map (HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n)
          (Functor.map (F.mapHomologicalComplex (ComplexShape.up ℕ)) φ))
    (Functor.map (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n)
        (Iso.hom (I.isoRightDerivedToHomotopyCategoryObj F)) ≫
      NatTrans.app (Iso.hom (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) n))
          (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) I.cocomplex) ≫
        HomologicalComplex.homologyMap (Functor.map (F.mapHomologicalComplex (ComplexShape.up ℕ)) φ) n)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Abelian.RightDerived
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 : HasInjectiveResolutions.{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 : C
inst_6 : Injective.{v, u} X
⊢ IsZero.{v_1, u_1} ((F.rightDerived (n + 1)).obj X)

Tactic:
IsZero.of_iso ?_ ((InjectiveResolution.self X).isoRightDerivedObj F (n + 1))

Premises used: CategoryTheory.InjectiveResolution.isoRightDerivedObj, CategoryTheory.InjectiveResolution.self, CategoryTheory.Limits.IsZero.of_iso, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.CategoryTheory.Abelian.RightDerived
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 : HasInjectiveResolutions.{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 : C
inst_6 : Injective.{v, u} X
refine :
  IsZero.{v_1, u_1}
    (obj (C := HomologicalComplex.{v_1, u_1, 0} D (ComplexShape.up ℕ))
      (HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) (n + 1))
      (obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℕ)) (F.mapHomologicalComplex (ComplexShape.up ℕ))
        (InjectiveResolution.cocomplex (InjectiveResolution.self X))))
⊢ IsZero.{v_1, u_1} ((F.rightDerived (n + 1)).obj X)

Tactic:
refine IsZero.of_iso ?_ ((InjectiveResolution.self X).isoRightDerivedObj F (n + 1))

Premises used: CategoryTheory.InjectiveResolution.isoRightDerivedObj, CategoryTheory.InjectiveResolution.self, CategoryTheory.Limits.IsZero.of_iso, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.CategoryTheory.Abelian.RightDerived
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 : HasInjectiveResolutions.{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 : C
inst_6 : Injective.{v, u} X
erw :
  HomologicalComplex.ExactAt
    (obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℕ)) (F.mapHomologicalComplex (ComplexShape.up ℕ))
      (InjectiveResolution.cocomplex (InjectiveResolution.self X)))
    (n + 1)
⊢ IsZero.{v_1, u_1}
    (obj (C := HomologicalComplex.{v_1, u_1, 0} D (ComplexShape.up ℕ))
      (HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) (n + 1))
      (obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℕ)) (F.mapHomologicalComplex (ComplexShape.up ℕ))
        (InjectiveResolution.cocomplex (InjectiveResolution.self X))))

Tactic:
erw [← HomologicalComplex.exactAt_iff_isZero_homology]

Premises used: HomologicalComplex.exactAt_iff_isZero_homology
-- Module: Mathlib.CategoryTheory.Abelian.RightDerived
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 : HasInjectiveResolutions.{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 : C
inst_6 : Injective.{v, u} X
⊢ IsZero.{v, u} (HomologicalComplex.X.{v, u, 0} (InjectiveResolution.cocomplex (InjectiveResolution.self X)) (n + 1))

Tactic:
apply isZero_zero

Premises used: CategoryTheory.Limits.isZero_zero
-- Module: Mathlib.CategoryTheory.Abelian.RightDerived
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 : HasInjectiveResolutions.{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 : C
inst_6 : Injective.{v, u} X
⊢ HomologicalComplex.ExactAt
    (obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℕ)) (F.mapHomologicalComplex (ComplexShape.up ℕ))
      (InjectiveResolution.cocomplex (InjectiveResolution.self X)))
    (n + 1)

Tactic:
exact ShortComplex.exact_of_isZero_X₂ _ (F.map_isZero (by apply isZero_zero))

Premises used: CategoryTheory.ShortComplex.exact_of_isZero_X₂
-- Module: Mathlib.CategoryTheory.Abelian.RightDerived
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 : HasInjectiveResolutions.{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 : InjectiveResolution.{v, u} X
Q : InjectiveResolution.{v, u} Y
g : P.cocomplex ⟶ Q.cocomplex
w : P.ι ≫ g = map (CochainComplex.single₀ C) f ≫ Q.ι
rw :
  Eq (α := HomologicalComplex.X.{v, u, 0} (obj (CochainComplex.single₀ C) X) 0 ⟶ Q.cocomplex.X 0) (P.ι.f 0 ≫ g.f 0)
    (f ≫ Q.ι.f 0)
⊢ (F.rightDerived n).map f =
    Iso.hom (P.isoRightDerivedObj F n) ≫
      map
          (comp (D := HomologicalComplex.{v_1, u_1, 0} D (ComplexShape.up ℕ))
            (F.mapHomologicalComplex (ComplexShape.up ℕ)) (HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n))
          g ≫
        Iso.inv (Q.isoRightDerivedObj F n)

Tactic:
rw [← cancel_mono (Q.isoRightDerivedObj F n).hom,
    InjectiveResolution.isoRightDerivedObj_hom_naturality f P Q g _ F n,
    assoc, assoc, Iso.inv_hom_id, comp_id]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.InjectiveResolution.isoRightDerivedObj, CategoryTheory.Iso.inv_hom_id, CategoryTheory.InjectiveResolution.isoRightDerivedObj_hom_naturality, CategoryTheory.cancel_mono, CategoryTheory.Category.comp_id, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Abelian.RightDerived
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 : HasInjectiveResolutions.{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 : InjectiveResolution.{v, u} X
Q : InjectiveResolution.{v, u} Y
g : P.cocomplex ⟶ Q.cocomplex
w : P.ι ≫ g = map (CochainComplex.single₀ C) f ≫ Q.ι
rw :
  Eq (α := HomologicalComplex.X.{v, u, 0} (obj (CochainComplex.single₀ C) X) 0 ⟶ Q.cocomplex.X 0) ((P.ι ≫ g).f 0)
    (f ≫ Q.ι.f 0)
rw₁ :
  Eq (α := HomologicalComplex.X.{v, u, 0} (obj (CochainComplex.single₀ C) X) 0 ⟶ Q.cocomplex.X 0)
    ((map (CochainComplex.single₀ C) f ≫ Q.ι).f 0) (f ≫ Q.ι.f 0)
rw₂ :
  Eq (α := HomologicalComplex.X.{v, u, 0} (obj (CochainComplex.single₀ C) X) 0 ⟶ Q.cocomplex.X 0)
    (HomologicalComplex.Hom.f (map (CochainComplex.single₀ C) f) 0 ≫ Q.ι.f 0) (f ≫ Q.ι.f 0)
rw₃ rw₄ :
  Eq (α := HomologicalComplex.X.{v, u, 0} (obj (CochainComplex.single₀ C) X) 0 ⟶ Q.cocomplex.X 0) (f ≫ Q.ι.f 0)
    (f ≫ Q.ι.f 0)
⊢ Eq (α := HomologicalComplex.X.{v, u, 0} (obj (CochainComplex.single₀ C) X) 0 ⟶ Q.cocomplex.X 0) (P.ι.f 0 ≫ g.f 0)
    (f ≫ Q.ι.f 0)

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

Premises used: CochainComplex.single₀_map_f_zero, HomologicalComplex.comp_f
-- Module: Mathlib.CategoryTheory.Abelian.RightDerived
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 : HasInjectiveResolutions.{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.up ℕ)) F.rightDerivedToHomotopyCategory
      F.rightDerivedToHomotopyCategory)
    (rightDerivedToHomotopyCategory (𝟙 F)) (𝟙 F.rightDerivedToHomotopyCategory)

Tactic:
rfl

Premises used: CategoryTheory.NatTrans.rightDerivedToHomotopyCategory, HomologicalComplex.id, CategoryTheory.Functor.whiskerLeft, CategoryTheory.Functor.rightDerivedToHomotopyCategory, CategoryTheory.NatTrans.id, rfl
-- Module: Mathlib.CategoryTheory.Abelian.RightDerived
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 : HasInjectiveResolutions.{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.up ℕ)) F.rightDerivedToHomotopyCategory
      H.rightDerivedToHomotopyCategory)
    (rightDerivedToHomotopyCategory (α ≫ β))
    (CategoryStruct.comp (Y := G.rightDerivedToHomotopyCategory) (rightDerivedToHomotopyCategory α)
      (rightDerivedToHomotopyCategory β))

Tactic:
rfl

Premises used: CategoryTheory.NatTrans.vcomp, CategoryTheory.NatTrans.rightDerivedToHomotopyCategory, CategoryTheory.Functor.whiskerLeft, CategoryTheory.Quotient.comp, HomologicalComplex.comp, CategoryTheory.Functor.rightDerivedToHomotopyCategory, rfl
-- Module: Mathlib.CategoryTheory.Abelian.RightDerived
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 : HasInjectiveResolutions.{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.up ℕ)) F.rightDerivedToHomotopyCategory
        (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n)) =
    𝟙 (F.rightDerived n)
⊢ Functor.whiskerRight (rightDerivedToHomotopyCategory (𝟙 F))
      (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n) =
    𝟙 (F.rightDerived n)

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

Premises used: CategoryTheory.NatTrans.rightDerivedToHomotopyCategory_id, CategoryTheory.Functor.whiskerRight_id'
-- Module: Mathlib.CategoryTheory.Abelian.RightDerived
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 : HasInjectiveResolutions.{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.up ℕ)) F.rightDerivedToHomotopyCategory
        (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n)) =
    𝟙 (F.rightDerived n)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Abelian.RightDerived
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 : HasInjectiveResolutions.{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.rightDerived n ⟶ H.rightDerived n) (rightDerived (α ≫ β) n)
    (CategoryStruct.comp (Y := G.rightDerived n) (rightDerived α n) (rightDerived β n))

Tactic:
simp [NatTrans.rightDerived]

Premises used: CategoryTheory.NatTrans.rightDerived
-- Module: Mathlib.CategoryTheory.Abelian.RightDerived
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 : HasInjectiveResolutions.{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 : InjectiveResolution.{v, u} X
n : ℕ
dsimp :
  Eq (α := (F.rightDerived n).obj X ⟶ (G.rightDerived n).obj X)
    (Functor.map (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n)
      (NatTrans.app (NatTrans.rightDerivedToHomotopyCategory α) X))
    ((Functor.map (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n)
          (Iso.hom (P.isoRightDerivedToHomotopyCategoryObj F)) ≫
        NatTrans.app (Iso.hom (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) n))
          (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) P.cocomplex)) ≫
      HomologicalComplex.homologyMap (NatTrans.app (NatTrans.mapHomologicalComplex α (ComplexShape.up ℕ)) P.cocomplex)
          n ≫
        NatTrans.app (Iso.inv (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) n))
            (Functor.obj (G.mapHomologicalComplex (ComplexShape.up ℕ)) P.cocomplex) ≫
          Functor.map (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n)
            (Iso.inv (P.isoRightDerivedToHomotopyCategoryObj G)))
⊢ Eq (α := (F.rightDerived n).obj X ⟶ (G.rightDerived n).obj X) (NatTrans.app (NatTrans.rightDerived α n) X)
    (Iso.hom (P.isoRightDerivedObj F n) ≫
      Functor.map (HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n)
          (NatTrans.app (NatTrans.mapHomologicalComplex α (ComplexShape.up ℕ)) P.cocomplex) ≫
        Iso.inv (P.isoRightDerivedObj G n))

Tactic:
dsimp [NatTrans.rightDerived, isoRightDerivedObj]

Premises used: CategoryTheory.InjectiveResolution.isoRightDerivedObj, CategoryTheory.NatTrans.rightDerived
-- Module: Mathlib.CategoryTheory.Abelian.RightDerived
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 : HasInjectiveResolutions.{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 : InjectiveResolution.{v, u} X
n : ℕ
rw :
  Eq (α := (F.rightDerived n).obj X ⟶ (G.rightDerived n).obj X)
    (Functor.map (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n)
        (Iso.hom (P.isoRightDerivedToHomotopyCategoryObj F)) ≫
      Functor.map (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n)
          (Functor.map (HomotopyCategory.quotient D (ComplexShape.up ℕ))
            (NatTrans.app (NatTrans.mapHomologicalComplex α (ComplexShape.up ℕ)) P.cocomplex)) ≫
        Functor.map (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n)
          (Iso.inv (P.isoRightDerivedToHomotopyCategoryObj G)))
    (Functor.map (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n)
        (Iso.hom (P.isoRightDerivedToHomotopyCategoryObj F)) ≫
      NatTrans.app (Iso.hom (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) n))
          (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) P.cocomplex) ≫
        HomologicalComplex.homologyMap (NatTrans.app (NatTrans.mapHomologicalComplex α (ComplexShape.up ℕ)) P.cocomplex)
            n ≫
          NatTrans.app (Iso.inv (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) n))
              (Functor.obj (G.mapHomologicalComplex (ComplexShape.up ℕ)) P.cocomplex) ≫
            Functor.map (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n)
              (Iso.inv (P.isoRightDerivedToHomotopyCategoryObj G)))
⊢ Eq (α := (F.rightDerived n).obj X ⟶ (G.rightDerived n).obj X)
    (Functor.map (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n)
      (NatTrans.app (NatTrans.rightDerivedToHomotopyCategory α) X))
    ((Functor.map (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n)
          (Iso.hom (P.isoRightDerivedToHomotopyCategoryObj F)) ≫
        NatTrans.app (Iso.hom (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) n))
          (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) P.cocomplex)) ≫
      HomologicalComplex.homologyMap (NatTrans.app (NatTrans.mapHomologicalComplex α (ComplexShape.up ℕ)) P.cocomplex)
          n ≫
        NatTrans.app (Iso.inv (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) n))
            (Functor.obj (G.mapHomologicalComplex (ComplexShape.up ℕ)) P.cocomplex) ≫
          Functor.map (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n)
            (Iso.inv (P.isoRightDerivedToHomotopyCategoryObj G)))

Tactic:
rw [InjectiveResolution.rightDerivedToHomotopyCategory_app_eq α P,
    Functor.map_comp, Functor.map_comp, assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Functor.map_comp, CategoryTheory.InjectiveResolution.rightDerivedToHomotopyCategory_app_eq
-- Module: Mathlib.CategoryTheory.Abelian.RightDerived
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 : HasInjectiveResolutions.{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 : InjectiveResolution.{v, u} X
n : ℕ
⊢ Eq (α := (F.rightDerived n).obj X ⟶ (G.rightDerived n).obj X)
    (Functor.map (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n)
        (Iso.hom (P.isoRightDerivedToHomotopyCategoryObj F)) ≫
      Functor.map (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n)
          (Functor.map (HomotopyCategory.quotient D (ComplexShape.up ℕ))
            (NatTrans.app (NatTrans.mapHomologicalComplex α (ComplexShape.up ℕ)) P.cocomplex)) ≫
        Functor.map (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n)
          (Iso.inv (P.isoRightDerivedToHomotopyCategoryObj G)))
    (Functor.map (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n)
        (Iso.hom (P.isoRightDerivedToHomotopyCategoryObj F)) ≫
      Functor.map
          (HomotopyCategory.quotient D (ComplexShape.up ℕ) ⋙ HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n)
          (NatTrans.app (NatTrans.mapHomologicalComplex α (ComplexShape.up ℕ)) P.cocomplex) ≫
        NatTrans.app (Iso.hom (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) n))
            (Functor.obj (G.mapHomologicalComplex (ComplexShape.up ℕ)) P.cocomplex) ≫
          NatTrans.app (Iso.inv (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) n))
              (Functor.obj (G.mapHomologicalComplex (ComplexShape.up ℕ)) P.cocomplex) ≫
            Functor.map (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n)
              (Iso.inv (P.isoRightDerivedToHomotopyCategoryObj 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.RightDerived
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 : HasInjectiveResolutions.{v, u} C
inst_4 : Abelian.{v_1, u_1} D
X : C
P : InjectiveResolution.{v, u} X
F : Functor.{v, v_1, u, u_1} C D
inst_5 : F.Additive
⊢ (ComplexShape.up ℕ).next 0 = 1

Tactic:
simp