awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.RightDerived (goal)
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
⊢ 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))
have 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))
Tactic: rw [← isoRightDerivedToHomotopyCategoryObj_hom_naturality_assoc f I J φ comm F,
      Iso.hom_inv_id, comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.RightDerived (goal)
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))
⊢ 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))
have 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))
Tactic: rw [← isoRightDerivedToHomotopyCategoryObj_hom_naturality_assoc f I J φ comm F,
      Iso.hom_inv_id, comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.RightDerived (goal)
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))
⊢ 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))
have 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)
Tactic: rw [← isoRightDerivedToHomotopyCategoryObj_hom_naturality_assoc f I J φ comm F,
      Iso.hom_inv_id, comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.RightDerived (goal)
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 : ℕ
⊢ (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))
        φ
have 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)
Tactic: dsimp [isoRightDerivedObj, Functor.rightDerived]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.RightDerived (goal)
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)
        (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)
have rw : 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)) ≫
    Functor.map (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n)
        (Functor.map (F.mapHomologicalComplex (ComplexShape.up ℕ) ⋙ HomotopyCategory.quotient D (ComplexShape.up ℕ))
          φ) ≫
      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)
Tactic: rw [assoc, ← Functor.map_comp_assoc,
    InjectiveResolution.isoRightDerivedToHomotopyCategoryObj_hom_naturality f I J φ comm F,
    Functor.map_comp, assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.RightDerived (goal)
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)) ≫
      Functor.map (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n)
          (Functor.map (F.mapHomologicalComplex (ComplexShape.up ℕ) ⋙ HomotopyCategory.quotient D (ComplexShape.up ℕ))
            φ) ≫
        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)
have erw : 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: erw [(HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) n).hom.naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.RightDerived (goal)
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 : ℕ
⊢ Iso.inv (I.isoRightDerivedObj F n) ≫ (F.rightDerived n).map f =
    Functor.map
        (Functor.comp (D := HomologicalComplex.{v_1, u_1, 0} D (ComplexShape.up ℕ))
          (F.mapHomologicalComplex (ComplexShape.up ℕ)) (HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n))
        φ ≫
      Iso.inv (J.isoRightDerivedObj F n)
have rw : (Iso.inv (I.isoRightDerivedObj F n) ≫ (F.rightDerived n).map f) ≫ Iso.hom (J.isoRightDerivedObj F n) =
  CategoryStruct.comp (Y := (F.rightDerived n).obj Y)
    (Functor.map
        (Functor.comp (D := HomologicalComplex.{v_1, u_1, 0} D (ComplexShape.up ℕ))
          (F.mapHomologicalComplex (ComplexShape.up ℕ)) (HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n))
        φ ≫
      Iso.inv (J.isoRightDerivedObj F n))
    (Iso.hom (J.isoRightDerivedObj F n))
Tactic: rw [← cancel_mono (J.isoRightDerivedObj F n).hom, assoc, assoc,
    InjectiveResolution.isoRightDerivedObj_hom_naturality f I J φ comm F n,
    Iso.inv_hom_id_assoc, Iso.inv_hom_id, comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.RightDerived (goal)
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 : ℕ
rw :
  (Iso.inv (I.isoRightDerivedObj F n) ≫ (F.rightDerived n).map f) ≫ Iso.hom (J.isoRightDerivedObj F n) =
    CategoryStruct.comp (Y := (F.rightDerived n).obj Y)
      (Functor.map
          (Functor.comp (D := HomologicalComplex.{v_1, u_1, 0} D (ComplexShape.up ℕ))
            (F.mapHomologicalComplex (ComplexShape.up ℕ)) (HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n))
          φ ≫
        Iso.inv (J.isoRightDerivedObj F n))
      (Iso.hom (J.isoRightDerivedObj F n))
⊢ Iso.inv (I.isoRightDerivedObj F n) ≫ (F.rightDerived n).map f =
    Functor.map
        (Functor.comp (D := HomologicalComplex.{v_1, u_1, 0} D (ComplexShape.up ℕ))
          (F.mapHomologicalComplex (ComplexShape.up ℕ)) (HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n))
        φ ≫
      Iso.inv (J.isoRightDerivedObj F n)
have rw₁ : Iso.inv (I.isoRightDerivedObj F n) ≫ (F.rightDerived n).map f ≫ Iso.hom (J.isoRightDerivedObj F n) =
  CategoryStruct.comp (Y := (F.rightDerived n).obj Y)
    (Functor.map
        (Functor.comp (D := HomologicalComplex.{v_1, u_1, 0} D (ComplexShape.up ℕ))
          (F.mapHomologicalComplex (ComplexShape.up ℕ)) (HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n))
        φ ≫
      Iso.inv (J.isoRightDerivedObj F n))
    (Iso.hom (J.isoRightDerivedObj F n))
Tactic: rw [← cancel_mono (J.isoRightDerivedObj F n).hom, assoc, assoc,
    InjectiveResolution.isoRightDerivedObj_hom_naturality f I J φ comm F n,
    Iso.inv_hom_id_assoc, Iso.inv_hom_id, comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.RightDerived (goal)
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)
have 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))))
Tactic: refine IsZero.of_iso ?_ ((InjectiveResolution.self X).isoRightDerivedObj F (n + 1))
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.RightDerived (goal)
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}
    (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))))
have erw : HomologicalComplex.ExactAt
  (obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℕ)) (F.mapHomologicalComplex (ComplexShape.up ℕ))
    (InjectiveResolution.cocomplex (InjectiveResolution.self X)))
  (n + 1)
Tactic: erw [← HomologicalComplex.exactAt_iff_isZero_homology]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.RightDerived (goal)
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.ι
⊢ (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)
have 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)
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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.RightDerived (goal)
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.ι
⊢ 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)
have 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)
Tactic: rw [← HomologicalComplex.comp_f, w, HomologicalComplex.comp_f,
    CochainComplex.single₀_map_f_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.RightDerived (goal)
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)
⊢ 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)
have 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)
Tactic: rw [← HomologicalComplex.comp_f, w, HomologicalComplex.comp_f,
    CochainComplex.single₀_map_f_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.RightDerived (goal)
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)
⊢ 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)
have 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)
Tactic: rw [← HomologicalComplex.comp_f, w, HomologicalComplex.comp_f,
    CochainComplex.single₀_map_f_zero]