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 : C
P : InjectiveResolution.{v, u} X
F : Functor.{v, v_1, u, u_1} C D
inst_5 : F.Additive
dsimp :
  Eq (α := F.obj X ⟶ F.obj (P.cocomplex.X 1))
    (CategoryStruct.comp (Y := F.obj (P.cocomplex.X 0)) (F.map (P.ι.f 0)) (F.map (P.cocomplex.d 0 1)) :
      F.obj X ⟶ F.obj (P.cocomplex.X 1))
    (0 : F.obj X ⟶ HomologicalComplex.X (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) P.cocomplex) 1)
⊢ Eq (α := F.obj X ⟶ HomologicalComplex.X (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) P.cocomplex) 1)
    (CategoryStruct.comp (Y :=
        HomologicalComplex.X (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) P.cocomplex) 0)
        (F.map (P.ι.f 0))
        (HomologicalComplex.d (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) P.cocomplex) 0 1) :
      F.obj X ⟶ HomologicalComplex.X (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) P.cocomplex) 1)
    (0 : F.obj X ⟶ HomologicalComplex.X (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) P.cocomplex) 1)

Tactic:
dsimp
-- 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
rw :
  Eq (α := F.obj X ⟶ F.obj (P.cocomplex.X 1))
    (F.map (CategoryStruct.comp (Y := P.cocomplex.X 0) (P.ι.f 0) (P.cocomplex.d 0 1)) :
      F.obj X ⟶ F.obj (P.cocomplex.X 1))
    (0 : F.obj X ⟶ HomologicalComplex.X (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) P.cocomplex) 1)
rw₁ :
  Eq (α := F.obj X ⟶ F.obj (P.cocomplex.X 1))
    (F.map (HomologicalComplex.d (Functor.obj (CochainComplex.single₀ C) X) 0 1 ≫ P.ι.f 1) :
      F.obj X ⟶ F.obj (P.cocomplex.X 1))
    (0 : F.obj X ⟶ HomologicalComplex.X (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) P.cocomplex) 1)
rw₂ : Eq (α := F.obj X ⟶ F.obj (P.cocomplex.X 1)) (F.map (0 ≫ P.ι.f 1)) 0
rw₃ : Eq (α := F.obj X ⟶ F.obj (P.cocomplex.X 1)) (F.map 0) 0
rw₄ rw₅ : Eq.{v_1 + 1} (α := F.obj X ⟶ F.obj (P.cocomplex.X 1)) 0 0
⊢ Eq (α := F.obj X ⟶ F.obj (P.cocomplex.X 1))
    (CategoryStruct.comp (Y := F.obj (P.cocomplex.X 0)) (F.map (P.ι.f 0)) (F.map (P.cocomplex.d 0 1)) :
      F.obj X ⟶ F.obj (P.cocomplex.X 1))
    (0 : F.obj X ⟶ HomologicalComplex.X (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) P.cocomplex) 1)

Tactic:
rw [← F.map_comp, HomologicalComplex.Hom.comm, HomologicalComplex.single_obj_d,
      zero_comp, F.map_zero]

Premises used: HomologicalComplex.single_obj_d, CategoryTheory.Functor.map_zero, CategoryTheory.Functor.map_comp, CategoryTheory.Limits.zero_comp, HomologicalComplex.Hom.comm
-- Module: Mathlib.CategoryTheory.Abelian.RightDerived
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 : InjectiveResolution.{v_2, u_2} X
F : Functor.{v_2, v_1, u_2, u_1} C D
inst_4 : F.Additive
⊢ Eq (α := F.obj X ⟶ HomologicalComplex.X (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) P.cocomplex) 0)
    (CategoryStruct.comp (Y :=
        HomologicalComplex.cycles (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) P.cocomplex) 0)
        (P.toRightDerivedZero' F :
          F.obj X ⟶ HomologicalComplex.cycles (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) P.cocomplex) 0)
        (HomologicalComplex.iCycles (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) P.cocomplex) 0 :
          HomologicalComplex.cycles (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) P.cocomplex) 0 ⟶
            HomologicalComplex.X (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) P.cocomplex) 0) :
      F.obj X ⟶ HomologicalComplex.X (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) P.cocomplex) 0)
    (F.map (P.ι.f 0) :
      F.obj (HomologicalComplex.X.{v_2, u_2, 0} (Functor.obj (CochainComplex.single₀ C) X) 0) ⟶ F.obj (P.cocomplex.X 0))

Tactic:
simp [toRightDerivedZero']

Premises used: CategoryTheory.InjectiveResolution.toRightDerivedZero'
-- Module: Mathlib.CategoryTheory.Abelian.RightDerived
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 : InjectiveResolution.{v_2, u_2} X
Q : InjectiveResolution.{v_2, u_2} Y
φ : P.cocomplex ⟶ Q.cocomplex
comm :
  Eq (α := HomologicalComplex.X.{v_2, u_2, 0} (Functor.obj (CochainComplex.single₀ C) X) 0 ⟶ Q.cocomplex.X 0)
    (P.ι.f 0 ≫ φ.f 0) (f ≫ Q.ι.f 0)
F : Functor.{v_2, v_1, u_2, u_1} C D
inst_4 : F.Additive
⊢ Eq (α :=
    F.obj X ⟶ HomologicalComplex.cycles (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) Q.cocomplex) 0)
    (F.map f ≫ Q.toRightDerivedZero' F :
      F.obj X ⟶ HomologicalComplex.cycles (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) Q.cocomplex) 0)
    (CategoryStruct.comp (Y :=
        HomologicalComplex.cycles (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) P.cocomplex) 0)
        (P.toRightDerivedZero' F :
          F.obj X ⟶ HomologicalComplex.cycles (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) P.cocomplex) 0)
        (HomologicalComplex.cyclesMap (Functor.map (F.mapHomologicalComplex (ComplexShape.up ℕ)) φ) 0 :
          HomologicalComplex.cycles (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) P.cocomplex) 0 ⟶
            HomologicalComplex.cycles (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) Q.cocomplex) 0) :
      F.obj X ⟶ HomologicalComplex.cycles (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) Q.cocomplex) 0)

Tactic:
simp only [← cancel_mono (HomologicalComplex.iCycles _ _),
    Functor.mapHomologicalComplex_obj_X, assoc, toRightDerivedZero'_comp_iCycles,
    CochainComplex.single₀_obj_zero, HomologicalComplex.cyclesMap_i,
    Functor.mapHomologicalComplex_map_f, toRightDerivedZero'_comp_iCycles_assoc,
    ← F.map_comp, comm]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Functor.mapHomologicalComplex_map_f, CategoryTheory.InjectiveResolution.toRightDerivedZero'_comp_iCycles, HomologicalComplex.iCycles, CategoryTheory.Functor.mapHomologicalComplex_obj_X, CategoryTheory.cancel_mono, CategoryTheory.Functor.map_comp, CategoryTheory.InjectiveResolution.toRightDerivedZero'_comp_iCycles_assoc, HomologicalComplex.cyclesMap_i, CochainComplex.single₀_obj_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
X : C
inst_6 : Injective.{v, u} X
dsimp :
  IsIso (X := F.obj X) (Y :=
    HomologicalComplex.cycles
      (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℕ))
        (F.mapHomologicalComplex (ComplexShape.up ℕ)) (Functor.obj (CochainComplex.single₀ C) X))
      0)
    (HomologicalComplex.liftCycles
      (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℕ))
        (F.mapHomologicalComplex (ComplexShape.up ℕ)) (Functor.obj (CochainComplex.single₀ C) X))
      (F.map (𝟙 X)) 1 toRightDerivedZero'._proof_1 ⋯)
⊢ IsIso (Y :=
    HomologicalComplex.cycles
      (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℕ))
        (F.mapHomologicalComplex (ComplexShape.up ℕ)) (cocomplex (self X)))
      0)
    (toRightDerivedZero' (self X) F :
      F.obj X ⟶
        HomologicalComplex.cycles
          (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℕ))
            (F.mapHomologicalComplex (ComplexShape.up ℕ)) (cocomplex (self X)))
          0)

Tactic:
dsimp [InjectiveResolution.toRightDerivedZero']

Premises used: CategoryTheory.InjectiveResolution.toRightDerivedZero'
-- 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
X : C
inst_6 : Injective.{v, u} X
rw :
  ShortComplex.Exact
      (ShortComplex.mk (X₃ :=
        HomologicalComplex.X
          (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℕ))
            (F.mapHomologicalComplex (ComplexShape.up ℕ)) (Functor.obj (CochainComplex.single₀ C) X))
          1)
        (F.map (𝟙 X))
        (HomologicalComplex.d
          (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℕ))
            (F.mapHomologicalComplex (ComplexShape.up ℕ)) (Functor.obj (CochainComplex.single₀ C) X))
          0 1)
        ⋯) ∧
    Mono (F.map (𝟙 X))
⊢ IsIso (X := F.obj X) (Y :=
    HomologicalComplex.cycles
      (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℕ))
        (F.mapHomologicalComplex (ComplexShape.up ℕ)) (Functor.obj (CochainComplex.single₀ C) X))
      0)
    (HomologicalComplex.liftCycles
      (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℕ))
        (F.mapHomologicalComplex (ComplexShape.up ℕ)) (Functor.obj (CochainComplex.single₀ C) X))
      (F.map (𝟙 X)) 1 toRightDerivedZero'._proof_1 ⋯)

Tactic:
rw [CochainComplex.isIso_liftCycles_iff]

Premises used: CochainComplex.isIso_liftCycles_iff
-- 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
X : C
inst_6 : Injective.{v, u} X
⊢ ShortComplex.Exact
      (ShortComplex.mk (X₃ :=
        HomologicalComplex.X
          (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℕ))
            (F.mapHomologicalComplex (ComplexShape.up ℕ)) (Functor.obj (CochainComplex.single₀ C) X))
          1)
        (F.map (𝟙 X))
        (HomologicalComplex.d
          (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℕ))
            (F.mapHomologicalComplex (ComplexShape.up ℕ)) (Functor.obj (CochainComplex.single₀ C) X))
          0 1)
        ⋯) ∧
    Mono (F.map (𝟙 X))

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

Premises used: CategoryTheory.ShortComplex.Splitting.exact, inferInstance, And.intro
-- 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
X : C
inst_6 : Injective.{v, u} X
⊢ ShortComplex.Splitting
    (ShortComplex.mk (X₃ :=
      HomologicalComplex.X
        (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℕ))
          (F.mapHomologicalComplex (ComplexShape.up ℕ)) (Functor.obj (CochainComplex.single₀ C) X))
        1)
      (F.map (𝟙 X))
      (HomologicalComplex.d
        (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℕ))
          (F.mapHomologicalComplex (ComplexShape.up ℕ)) (Functor.obj (CochainComplex.single₀ C) X))
        0 1)
      ⋯)

Tactic:
exact
    { r := 𝟙 _
      s := 0
      s_g := (F.map_isZero (isZero_zero _)).eq_of_src _ _ }
-- 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
I : InjectiveResolution.{v, u} X
F : Functor.{v, v_1, u, u_1} C D
inst_5 : F.Additive
⊢ Eq (α := HomologicalComplex.X.{v, u, 0} (Functor.obj (CochainComplex.single₀ C) X) 0 ⟶ I.cocomplex.X 0)
    (CategoryStruct.comp (Y := HomologicalComplex.X.{v, u, 0} (cocomplex (injectiveResolution X)) 0)
      (HomologicalComplex.Hom.f (ι (injectiveResolution X)) 0)
      (HomologicalComplex.Hom.f (desc (𝟙 X) I (injectiveResolution X)) 0))
    (𝟙 X ≫ I.ι.f 0)

Tactic:
simp
-- 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
I : InjectiveResolution.{v, u} X
F : Functor.{v, v_1, u, u_1} C D
inst_5 : F.Additive
⊢ Eq (α :=
    F.obj X ⟶ HomologicalComplex.cycles (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) I.cocomplex) 0)
    (F.map (𝟙 X) ≫ I.toRightDerivedZero' F :
      F.obj X ⟶ HomologicalComplex.cycles (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) I.cocomplex) 0)
    (CategoryStruct.comp (Y :=
        HomologicalComplex.cycles
          (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℕ))
            (F.mapHomologicalComplex (ComplexShape.up ℕ)) (cocomplex (injectiveResolution X)))
          0)
        (toRightDerivedZero' (injectiveResolution X) F :
          F.obj X ⟶
            HomologicalComplex.cycles
              (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℕ))
                (F.mapHomologicalComplex (ComplexShape.up ℕ)) (cocomplex (injectiveResolution X)))
              0)
        (HomologicalComplex.cyclesMap
            (Functor.map (F.mapHomologicalComplex (ComplexShape.up ℕ)) (desc (𝟙 X) I (injectiveResolution X))) 0 :
          HomologicalComplex.cycles
              (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℕ))
                (F.mapHomologicalComplex (ComplexShape.up ℕ)) (cocomplex (injectiveResolution X)))
              0 ⟶
            HomologicalComplex.cycles (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) I.cocomplex) 0) :
      F.obj X ⟶ HomologicalComplex.cycles (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) I.cocomplex) 0)

Tactic:
have h₁ := InjectiveResolution.toRightDerivedZero'_naturality
    (𝟙 X) (injectiveResolution X) I (desc (𝟙 X) _ _) (by simp) 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
X : C
I : InjectiveResolution.{v, u} X
F : Functor.{v, v_1, u, u_1} C D
inst_5 : F.Additive
h₁ :
  Eq (α :=
    F.obj X ⟶ HomologicalComplex.cycles (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) I.cocomplex) 0)
    (I.toRightDerivedZero' F :
      F.obj X ⟶ HomologicalComplex.cycles (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) I.cocomplex) 0)
    (CategoryStruct.comp (Y :=
        HomologicalComplex.cycles
          (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℕ))
            (F.mapHomologicalComplex (ComplexShape.up ℕ)) (cocomplex (injectiveResolution X)))
          0)
        (toRightDerivedZero' (injectiveResolution X) F :
          F.obj X ⟶
            HomologicalComplex.cycles
              (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℕ))
                (F.mapHomologicalComplex (ComplexShape.up ℕ)) (cocomplex (injectiveResolution X)))
              0)
        (HomologicalComplex.cyclesMap
            (Functor.map (F.mapHomologicalComplex (ComplexShape.up ℕ)) (desc (𝟙 X) I (injectiveResolution X))) 0 :
          HomologicalComplex.cycles
              (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℕ))
                (F.mapHomologicalComplex (ComplexShape.up ℕ)) (cocomplex (injectiveResolution X)))
              0 ⟶
            HomologicalComplex.cycles (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) I.cocomplex) 0) :
      F.obj X ⟶ HomologicalComplex.cycles (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) I.cocomplex) 0)
⊢ Eq (α :=
    Quiver.Hom (V := HomotopyCategory.{v_1, u_1, 0} D (ComplexShape.up ℕ))
      (Functor.obj F.rightDerivedToHomotopyCategory X)
      (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ) ⋙ HomotopyCategory.quotient D (ComplexShape.up ℕ))
        I.cocomplex))
    (Iso.hom (I.isoRightDerivedToHomotopyCategoryObj F))
    (Functor.map (F.mapHomologicalComplex (ComplexShape.up ℕ) ⋙ HomotopyCategory.quotient D (ComplexShape.up ℕ))
      (desc (𝟙 X) I (injectiveResolution X)))

Tactic:
have h₂ : (I.isoRightDerivedToHomotopyCategoryObj F).hom =
    (F.mapHomologicalComplex _ ⋙ HomotopyCategory.quotient _ _).map (desc (𝟙 X) _ _) :=
    comp_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
X : C
inst_6 : Injective.{v, u} X
rw :
  IsIso (Y := (F.rightDerived 0).obj X)
    (CategoryStruct.comp (Y :=
      HomologicalComplex.cycles
        (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℕ))
          (F.mapHomologicalComplex (ComplexShape.up ℕ)) (InjectiveResolution.cocomplex (InjectiveResolution.self X)))
        0)
      (InjectiveResolution.toRightDerivedZero' (InjectiveResolution.self X) F :
        F.obj X ⟶
          HomologicalComplex.cycles
            (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℕ))
              (F.mapHomologicalComplex (ComplexShape.up ℕ))
              (InjectiveResolution.cocomplex (InjectiveResolution.self X)))
            0)
      (Iso.hom
            (CochainComplex.isoHomologyπ₀
              (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℕ))
                (F.mapHomologicalComplex (ComplexShape.up ℕ))
                (InjectiveResolution.cocomplex (InjectiveResolution.self X)))) ≫
          Iso.inv (InjectiveResolution.isoRightDerivedObj (InjectiveResolution.self X) F 0) :
        HomologicalComplex.cycles
            (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℕ))
              (F.mapHomologicalComplex (ComplexShape.up ℕ))
              (InjectiveResolution.cocomplex (InjectiveResolution.self X)))
            0 ⟶
          (F.rightDerived 0).obj X))
⊢ IsIso (Y := (F.rightDerived 0).obj X) (NatTrans.app F.toRightDerivedZero X)

Tactic:
rw [(InjectiveResolution.self X).toRightDerivedZero_eq F]

Premises used: CategoryTheory.InjectiveResolution.toRightDerivedZero_eq, CategoryTheory.InjectiveResolution.self
-- 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
X : C
inst_6 : Injective.{v, u} X
⊢ IsIso (Y := (F.rightDerived 0).obj X)
    (CategoryStruct.comp (Y :=
      HomologicalComplex.cycles
        (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℕ))
          (F.mapHomologicalComplex (ComplexShape.up ℕ)) (InjectiveResolution.cocomplex (InjectiveResolution.self X)))
        0)
      (InjectiveResolution.toRightDerivedZero' (InjectiveResolution.self X) F :
        F.obj X ⟶
          HomologicalComplex.cycles
            (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℕ))
              (F.mapHomologicalComplex (ComplexShape.up ℕ))
              (InjectiveResolution.cocomplex (InjectiveResolution.self X)))
            0)
      (Iso.hom
            (CochainComplex.isoHomologyπ₀
              (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℕ))
                (F.mapHomologicalComplex (ComplexShape.up ℕ))
                (InjectiveResolution.cocomplex (InjectiveResolution.self X)))) ≫
          Iso.inv (InjectiveResolution.isoRightDerivedObj (InjectiveResolution.self X) F 0) :
        HomologicalComplex.cycles
            (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℕ))
              (F.mapHomologicalComplex (ComplexShape.up ℕ))
              (InjectiveResolution.cocomplex (InjectiveResolution.self X)))
            0 ⟶
          (F.rightDerived 0).obj X))

Tactic:
infer_instance
-- 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
inst_6 : PreservesFiniteLimits F
X : C
P : InjectiveResolution.{v, u} X
rw :
  Nonempty
    (IsLimit (F :=
      parallelPair (X :=
        ShortComplex.X₂
          (ShortComplex.mk (X₁ := F.obj X) (X₂ :=
            HomologicalComplex.X (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) P.cocomplex) 0) (X₃ :=
            HomologicalComplex.X (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) P.cocomplex) 1)
            (F.map (P.ι.f 0))
            (HomologicalComplex.d (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) P.cocomplex) 0 1) ⋯))
        (ShortComplex.g
          (ShortComplex.mk (X₁ := F.obj X) (X₂ :=
            HomologicalComplex.X (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) P.cocomplex) 0) (X₃ :=
            HomologicalComplex.X (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) P.cocomplex) 1)
            (F.map (P.ι.f 0))
            (HomologicalComplex.d (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) P.cocomplex) 0 1) ⋯))
        0)
      (KernelFork.ofι
        (ShortComplex.f
          (ShortComplex.mk (X₁ := F.obj X) (X₂ :=
            HomologicalComplex.X (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) P.cocomplex) 0) (X₃ :=
            HomologicalComplex.X (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) P.cocomplex) 1)
            (F.map (P.ι.f 0))
            (HomologicalComplex.d (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) P.cocomplex) 0 1) ⋯))
        ⋯))
⊢ IsIso (X := F.obj X) (Y :=
    HomologicalComplex.cycles (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) P.cocomplex) 0)
    (HomologicalComplex.liftCycles (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) P.cocomplex)
      (F.map (P.ι.f 0)) 1 InjectiveResolution.toRightDerivedZero'._proof_1 ⋯)

Tactic:
rw [CochainComplex.isIso_liftCycles_iff, ShortComplex.exact_and_mono_f_iff_f_is_kernel]

Premises used: CochainComplex.isIso_liftCycles_iff, CategoryTheory.ShortComplex.exact_and_mono_f_iff_f_is_kernel