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
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)
⊢ 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) (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 : ℕ
⊢ Functor.whiskerRight (rightDerivedToHomotopyCategory (𝟙 F))
      (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n) =
    𝟙 (F.rightDerived n)
have simp : 𝟙
    (Functor.comp (D := HomotopyCategory.{v_1, u_1, 0} D (ComplexShape.up ℕ)) F.rightDerivedToHomotopyCategory
      (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n)) =
  𝟙 (F.rightDerived n)
Tactic: simp only [rightDerivedToHomotopyCategory_id, Functor.whiskerRight_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 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) (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))
have 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)))
Tactic: dsimp [NatTrans.rightDerived, isoRightDerivedObj]
-- 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 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)
      (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)))
have 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)))
Tactic: rw [InjectiveResolution.rightDerivedToHomotopyCategory_app_eq α P,
    Functor.map_comp, 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 : C
P : InjectiveResolution.{v, u} X
F : Functor.{v, v_1, u, u_1} C D
inst_5 : F.Additive
⊢ 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)
have 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)
Tactic: dsimp
-- 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 : C
P : InjectiveResolution.{v, u} X
F : Functor.{v, v_1, u, u_1} C D
inst_5 : F.Additive
⊢ 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)
have 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)
Tactic: rw [← F.map_comp, HomologicalComplex.Hom.comm, HomologicalComplex.single_obj_d,
      zero_comp, F.map_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
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)
⊢ 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)
have 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)
Tactic: rw [← F.map_comp, HomologicalComplex.Hom.comm, HomologicalComplex.single_obj_d,
      zero_comp, F.map_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
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)
⊢ 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)
have rw₂ : Eq (α := F.obj X ⟶ F.obj (P.cocomplex.X 1)) (F.map (0 ≫ P.ι.f 1)) 0
Tactic: rw [← F.map_comp, HomologicalComplex.Hom.comm, HomologicalComplex.single_obj_d,
      zero_comp, F.map_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
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
⊢ 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)
have rw₃ : Eq (α := F.obj X ⟶ F.obj (P.cocomplex.X 1)) (F.map 0) 0
Tactic: rw [← F.map_comp, HomologicalComplex.Hom.comm, HomologicalComplex.single_obj_d,
      zero_comp, F.map_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
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
⊢ 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)
have rw₄ : Eq.{v_1 + 1} (α := F.obj X ⟶ F.obj (P.cocomplex.X 1)) 0 0
Tactic: rw [← F.map_comp, HomologicalComplex.Hom.comm, HomologicalComplex.single_obj_d,
      zero_comp, F.map_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
X : C
inst_6 : Injective.{v, u} X
⊢ 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)
have 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 sorry)
Tactic: dsimp [InjectiveResolution.toRightDerivedZero']
-- 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
X : C
inst_6 : Injective.{v, u} 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 ⋯)
have 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)
      sorry) ∧
  Mono (F.map (𝟙 X))
Tactic: rw [CochainComplex.isIso_liftCycles_iff]
-- 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
X : C
inst_6 : Injective.{v, u} X
⊢ IsIso (Y := (F.rightDerived 0).obj X) (NatTrans.app F.toRightDerivedZero X)
have 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))
Tactic: rw [(InjectiveResolution.self X).toRightDerivedZero_eq F]
-- 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
inst_6 : PreservesFiniteLimits F
X : C
P : InjectiveResolution.{v, u} X
⊢ 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 ⋯)
have 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) sorry))
      (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) sorry))
      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) sorry))
      sorry))
Tactic: rw [CochainComplex.isIso_liftCycles_iff, ShortComplex.exact_and_mono_f_iff_f_is_kernel]
-- 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
inst_6 : PreservesFiniteLimits F
X : C
⊢ IsIso (Y := (F.rightDerived 0).obj X) (NatTrans.app F.toRightDerivedZero X)
have dsimp : 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 X)))
        0)
      (InjectiveResolution.toRightDerivedZero' (injectiveResolution X) F :
        F.obj X ⟶
          HomologicalComplex.cycles
            (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℕ))
              (F.mapHomologicalComplex (ComplexShape.up ℕ)) (InjectiveResolution.cocomplex (injectiveResolution X)))
            0)
      (HomologicalComplex.homologyπ
            (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℕ))
              (F.mapHomologicalComplex (ComplexShape.up ℕ)) (InjectiveResolution.cocomplex (injectiveResolution X)))
            0 ≫
          NatTrans.app (Iso.inv (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) 0))
            (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℕ))
              (F.mapHomologicalComplex (ComplexShape.up ℕ)) (InjectiveResolution.cocomplex (injectiveResolution X))) :
        HomologicalComplex.cycles
            (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℕ))
              (F.mapHomologicalComplex (ComplexShape.up ℕ)) (InjectiveResolution.cocomplex (injectiveResolution X)))
            0 ⟶
          (F.rightDerived 0).obj X) :
    F.obj X ⟶ (F.rightDerived 0).obj X)
Tactic: dsimp [Functor.toRightDerivedZero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.SerreClass.Basic (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P : ObjectProperty.{v, u} C
inst_2 : P.IsSerreClass
S : ShortComplex.{v, u} C
hS : S.Exact
h₁ : P S.X₁
h₃ : P S.X₃
d : S.HomologyData := S.homologyData
⊢ P S.X₂
have this : Epi d.left.f'
Tactic: have := hS.epi_f' d.left