ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} D<VAR>CategoryTheory.Abelian C<VAR>CategoryTheory.HasProjectiveResolutions C<VAR>CategoryTheory.Abelian D<VAR>F : CategoryTheory.Functor C D<VAR>F.Additive<VAR>CategoryTheory.Limits.PreservesFiniteColimits F<VAR>X : C<GOAL>CategoryTheory.CategoryStruct.comp (F.fromLeftDerivedZero.app X) (F.leftDerivedZeroIsoSelf.inv.app X) = CategoryTheory.CategoryStruct.id ((F.leftDerived 0).obj X)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} D<VAR>CategoryTheory.Abelian C<VAR>CategoryTheory.HasProjectiveResolutions C<VAR>CategoryTheory.Abelian D<VAR>F : CategoryTheory.Functor C D<VAR>F.Additive<VAR>CategoryTheory.Limits.PreservesFiniteColimits F<VAR>X : C<GOAL>CategoryTheory.CategoryStruct.comp (F.leftDerivedZeroIsoSelf.inv.app X) (F.fromLeftDerivedZero.app X) = CategoryTheory.CategoryStruct.id (F.obj X)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>self : CategoryTheory.NonPreadditiveAbelian C<GOAL>CategoryTheory.Limits.HasCokernels C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>self : CategoryTheory.NonPreadditiveAbelian C<GOAL>CategoryTheory.Limits.HasFiniteCoproducts C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>self : CategoryTheory.NonPreadditiveAbelian C<GOAL>CategoryTheory.Limits.HasZeroObject C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>self : CategoryTheory.NonPreadditiveAbelian C<GOAL>CategoryTheory.Limits.HasKernels C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>self : CategoryTheory.NonPreadditiveAbelian C<GOAL>CategoryTheory.Limits.HasFiniteProducts C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.NonPreadditiveAbelian C<VAR>X : C<GOAL>CategoryTheory.Limits.diag X ≫ CategoryTheory.NonPreadditiveAbelian.σ = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.NonPreadditiveAbelian C<VAR>X : C<GOAL>CategoryTheory.Limits.prod.lift (𝟙 X) 0 ≫ CategoryTheory.NonPreadditiveAbelian.σ = 𝟙 X
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.NonPreadditiveAbelian C<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>CategoryTheory.Limits.prod.lift (𝟙 X) 0 ≫ CategoryTheory.Limits.prod.map f f = f ≫ CategoryTheory.Limits.prod.lift (𝟙 Y) 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.NonPreadditiveAbelian C<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>CategoryTheory.NonPreadditiveAbelian.σ ≫ f = CategoryTheory.Limits.prod.map f f ≫ CategoryTheory.NonPreadditiveAbelian.σ
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.NonPreadditiveAbelian C<VAR>X Y : C<VAR>a b : X ⟶ Y<GOAL>a - b = CategoryTheory.Limits.prod.lift a b ≫ CategoryTheory.NonPreadditiveAbelian.σ
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.NonPreadditiveAbelian C<VAR>X Y : C<VAR>a b : X ⟶ Y<GOAL>a + b = a - -b
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.NonPreadditiveAbelian C<VAR>X Y : C<VAR>a : X ⟶ Y<GOAL>-a = 0 - a
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.NonPreadditiveAbelian C<VAR>X Y : C<VAR>a : X ⟶ Y<GOAL>a - 0 = a
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.NonPreadditiveAbelian C<VAR>X Y : C<VAR>a : X ⟶ Y<GOAL>a - a = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.NonPreadditiveAbelian C<VAR>X Y : C<VAR>a b c d : X ⟶ Y<GOAL>CategoryTheory.Limits.prod.lift a b - CategoryTheory.Limits.prod.lift c d = CategoryTheory.Limits.prod.lift (a - c) (b - d)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.NonPreadditiveAbelian C<VAR>X Y : C<VAR>a b c d : X ⟶ Y<GOAL>a - c - (b - d) = a - b - (c - d)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.NonPreadditiveAbelian C<VAR>X Y : C<VAR>a b : X ⟶ Y<GOAL>-a - b = -b - a
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.NonPreadditiveAbelian C<VAR>X Y : C<VAR>a : X ⟶ Y<GOAL>- -a = a
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.NonPreadditiveAbelian C<VAR>X Y : C<VAR>a b : X ⟶ Y<GOAL>a + b = b + a
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.NonPreadditiveAbelian C<VAR>X Y : C<VAR>a b : X ⟶ Y<GOAL>a + -b = a - b
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.NonPreadditiveAbelian C<VAR>X Y : C<VAR>a : X ⟶ Y<GOAL>a + -a = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.NonPreadditiveAbelian C<VAR>X Y : C<VAR>a : X ⟶ Y<GOAL>-a + a = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.NonPreadditiveAbelian C<VAR>X Y : C<VAR>a b : X ⟶ Y<GOAL>-(a - b) = -a + b
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.NonPreadditiveAbelian C<VAR>X Y : C<VAR>a b : X ⟶ Y<GOAL>-(a + b) = -a - b
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.NonPreadditiveAbelian C<VAR>X Y : C<VAR>a b c : X ⟶ Y<GOAL>a - b + c = a - (b - c)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.NonPreadditiveAbelian C<VAR>X Y : C<VAR>a b c : X ⟶ Y<GOAL>a + b + c = a + (b + c)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.NonPreadditiveAbelian C<VAR>X Y : C<VAR>a : X ⟶ Y<GOAL>a + 0 = a
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.NonPreadditiveAbelian C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g h : Y ⟶ Z<GOAL>f ≫ (g - h) = f ≫ g - f ≫ h
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.NonPreadditiveAbelian C<VAR>X Y Z : C<VAR>f g : X ⟶ Y<VAR>h : Y ⟶ Z<GOAL>(f - g) ≫ h = f ≫ h - g ≫ h
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.NonPreadditiveAbelian C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g h : Y ⟶ Z<GOAL>f ≫ (g + h) = f ≫ g + f ≫ h
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.NonPreadditiveAbelian C<VAR>X Y Z : C<VAR>f g : X ⟶ Y<VAR>h : Y ⟶ Z<GOAL>(f + g) ≫ h = f ≫ h + g ≫ h
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X Y : C<VAR>f : Y ⟶ X<VAR>self : CategoryTheory.EffectiveEpiStruct f<VAR>W : C<VAR>e : Y ⟶ W<VAR>h : ∀ {Z : C} (g₁ g₂ : Z ⟶ Y), CategoryTheory.CategoryStruct.comp g₁ f = CategoryTheory.CategoryStruct.comp g₂ f → CategoryTheory.CategoryStruct.comp g₁ e = CategoryTheory.CategoryStruct.comp g₂ e<VAR>m : X ⟶ W<GOAL>CategoryTheory.CategoryStruct.comp f m = e → m = self.desc e ⋯
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X Y : C<VAR>f : Y ⟶ X<VAR>self : CategoryTheory.EffectiveEpiStruct f<VAR>W : C<VAR>e : Y ⟶ W<VAR>h : ∀ {Z : C} (g₁ g₂ : Z ⟶ Y), CategoryTheory.CategoryStruct.comp g₁ f = CategoryTheory.CategoryStruct.comp g₂ f → CategoryTheory.CategoryStruct.comp g₁ e = CategoryTheory.CategoryStruct.comp g₂ e<GOAL>CategoryTheory.CategoryStruct.comp f (self.desc e ⋯) = e
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X Y : C<VAR>f : Y ⟶ X<VAR>self : CategoryTheory.EffectiveEpi f<GOAL>Nonempty (CategoryTheory.EffectiveEpiStruct f)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X Y W : C<VAR>f : Y ⟶ X<VAR>CategoryTheory.EffectiveEpi f<VAR>e : Y ⟶ W<VAR>h : ∀ {Z : C} (g₁ g₂ : Z ⟶ Y), CategoryTheory.CategoryStruct.comp g₁ f = CategoryTheory.CategoryStruct.comp g₂ f → CategoryTheory.CategoryStruct.comp g₁ e = CategoryTheory.CategoryStruct.comp g₂ e<GOAL>CategoryTheory.CategoryStruct.comp f (CategoryTheory.EffectiveEpi.desc f e ⋯) = e
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X Y W : C<VAR>f : Y ⟶ X<VAR>CategoryTheory.EffectiveEpi f<VAR>e : Y ⟶ W<VAR>h : ∀ {Z : C} (g₁ g₂ : Z ⟶ Y), CategoryTheory.CategoryStruct.comp g₁ f = CategoryTheory.CategoryStruct.comp g₂ f → CategoryTheory.CategoryStruct.comp g₁ e = CategoryTheory.CategoryStruct.comp g₂ e<VAR>m : X ⟶ W<VAR>hm : CategoryTheory.CategoryStruct.comp f m = e<GOAL>m = CategoryTheory.EffectiveEpi.desc f e ⋯
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>B : C<VAR>α : Type u_2<VAR>X : α → C<VAR>π : (a : α) → X a ⟶ B<VAR>self : CategoryTheory.EffectiveEpiFamilyStruct X π<VAR>W : C<VAR>e : (a : α) → X a ⟶ W<VAR>h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), CategoryTheory.CategoryStruct.comp g₁ (π a₁) = CategoryTheory.CategoryStruct.comp g₂ (π a₂) → CategoryTheory.CategoryStruct.comp g₁ (e a₁) = CategoryTheory.CategoryStruct.comp g₂ (e a₂)<VAR>m : B ⟶ W<GOAL>(∀ (a : α), CategoryTheory.CategoryStruct.comp (π a) m = e a) → m = self.desc e ⋯
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>B : C<VAR>α : Type u_2<VAR>X : α → C<VAR>π : (a : α) → X a ⟶ B<VAR>self : CategoryTheory.EffectiveEpiFamilyStruct X π<VAR>W : C<VAR>e : (a : α) → X a ⟶ W<VAR>h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), CategoryTheory.CategoryStruct.comp g₁ (π a₁) = CategoryTheory.CategoryStruct.comp g₂ (π a₂) → CategoryTheory.CategoryStruct.comp g₁ (e a₁) = CategoryTheory.CategoryStruct.comp g₂ (e a₂)<VAR>a : α<GOAL>CategoryTheory.CategoryStruct.comp (π a) (self.desc e ⋯) = e a
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>B : C<VAR>α : Type u_2<VAR>X : α → C<VAR>π : (a : α) → X a ⟶ B<VAR>self : CategoryTheory.EffectiveEpiFamily X π<GOAL>Nonempty (CategoryTheory.EffectiveEpiFamilyStruct X π)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>B W : C<VAR>α : Type u_2<VAR>X : α → C<VAR>π : (a : α) → X a ⟶ B<VAR>CategoryTheory.EffectiveEpiFamily X π<VAR>e : (a : α) → X a ⟶ W<VAR>h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), CategoryTheory.CategoryStruct.comp g₁ (π a₁) = CategoryTheory.CategoryStruct.comp g₂ (π a₂) → CategoryTheory.CategoryStruct.comp g₁ (e a₁) = CategoryTheory.CategoryStruct.comp g₂ (e a₂)<VAR>a : α<GOAL>CategoryTheory.CategoryStruct.comp (π a) (CategoryTheory.EffectiveEpiFamily.desc X π e ⋯) = e a
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>B W : C<VAR>α : Type u_2<VAR>X : α → C<VAR>π : (a : α) → X a ⟶ B<VAR>CategoryTheory.EffectiveEpiFamily X π<VAR>e : (a : α) → X a ⟶ W<VAR>h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), CategoryTheory.CategoryStruct.comp g₁ (π a₁) = CategoryTheory.CategoryStruct.comp g₂ (π a₂) → CategoryTheory.CategoryStruct.comp g₁ (e a₁) = CategoryTheory.CategoryStruct.comp g₂ (e a₂)<VAR>m : B ⟶ W<VAR>hm : ∀ (a : α), CategoryTheory.CategoryStruct.comp (π a) m = e a<GOAL>m = CategoryTheory.EffectiveEpiFamily.desc X π e ⋯
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>B W : C<VAR>α : Type u_2<VAR>X : α → C<VAR>π : (a : α) → X a ⟶ B<VAR>CategoryTheory.EffectiveEpiFamily X π<VAR>m₁ m₂ : B ⟶ W<VAR>h : ∀ (a : α), CategoryTheory.CategoryStruct.comp (π a) m₁ = CategoryTheory.CategoryStruct.comp (π a) m₂<GOAL>m₁ = m₂
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>B X : C<VAR>f : X ⟶ B<GOAL>CategoryTheory.EffectiveEpi f ↔ CategoryTheory.EffectiveEpiFamily (fun x => X) fun x => match x with | PUnit.unit => f
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>B : C<VAR>α : Type u_2<VAR>α' : Type u_3<VAR>X : α → C<VAR>π : (a : α) → X a ⟶ B<VAR>e : α' ≃ α<VAR>h : CategoryTheory.EffectiveEpiFamily (fun a => X (e a)) fun a => π (e a)<GOAL>CategoryTheory.EffectiveEpiFamily X π
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>L : C ⥤ D<VAR>R : D ⥤ C<VAR>h : L ⊣ R<VAR>X : C<VAR>CategoryTheory.IsIso (h.unit.app X)<GOAL>CategoryTheory.inv (L.map (h.unit.app X)) = h.counit.app (L.obj X)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>L : C ⥤ D<VAR>R : D ⥤ C<VAR>h : L ⊣ R<VAR>CategoryTheory.IsIso h.unit<VAR>X : C<GOAL>h.whiskerLeftLCounitIsoOfIsIsoUnit.inv.app X = L.map (h.unit.app X)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>L : C ⥤ D<VAR>R : D ⥤ C<VAR>h : L ⊣ R<VAR>CategoryTheory.IsIso h.unit<VAR>X : C<GOAL>h.whiskerLeftLCounitIsoOfIsIsoUnit.hom.app X = h.counit.app (L.obj X)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>L : C ⥤ D<VAR>R : D ⥤ C<VAR>h : L ⊣ R<VAR>X : D<VAR>CategoryTheory.IsIso (h.counit.app X)<GOAL>CategoryTheory.inv (R.map (h.counit.app X)) = h.unit.app (R.obj X)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>L : C ⥤ D<VAR>R : D ⥤ C<VAR>h : L ⊣ R<VAR>CategoryTheory.IsIso h.counit<VAR>X : D<GOAL>h.whiskerLeftRUnitIsoOfIsIsoCounit.inv.app X = h.unit.app (R.obj X)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>L : C ⥤ D<VAR>R : D ⥤ C<VAR>h : L ⊣ R<VAR>CategoryTheory.IsIso h.counit<VAR>X : D<GOAL>h.whiskerLeftRUnitIsoOfIsIsoCounit.hom.app X = R.map (h.counit.app X)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>L : C ⥤ D<VAR>R : D ⥤ C<VAR>h : L ⊣ R<VAR>∀ (X : C), CategoryTheory.Mono (h.unit.app X)<GOAL>L.Faithful
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>L : C ⥤ D<VAR>R : D ⥤ C<VAR>h : L ⊣ R<VAR>∀ (X : C), CategoryTheory.IsSplitEpi (h.unit.app X)<GOAL>L.Full
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>L : C ⥤ D<VAR>R : D ⥤ C<VAR>h : L ⊣ R<VAR>∀ (X : D), CategoryTheory.Epi (h.counit.app X)<GOAL>R.Faithful
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>L : C ⥤ D<VAR>R : D ⥤ C<VAR>h : L ⊣ R<VAR>∀ (X : D), CategoryTheory.IsSplitMono (h.counit.app X)<GOAL>R.Full
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>L : C ⥤ D<VAR>R : D ⥤ C<VAR>h : L ⊣ R<VAR>L.Faithful<VAR>L.Full<VAR>X : D<GOAL>CategoryTheory.IsIso (h.counit.app X) ↔ X ∈ L.essImage
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>L : C ⥤ D<VAR>R : D ⥤ C<VAR>h : L ⊣ R<VAR>A : D<VAR>CategoryTheory.IsIso (h.counit.app A)<GOAL>A ∈ L.essImage
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>L : C ⥤ D<VAR>R : D ⥤ C<VAR>h : L ⊣ R<VAR>L.Faithful<VAR>L.Full<VAR>X : D<VAR>Y : C<VAR>e : X ≅ L.obj Y<GOAL>CategoryTheory.IsIso (h.counit.app X)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>L : C ⥤ D<VAR>R : D ⥤ C<VAR>h : L ⊣ R<VAR>R.Faithful<VAR>R.Full<VAR>Y : C<GOAL>CategoryTheory.IsIso (h.unit.app Y) ↔ Y ∈ R.essImage
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>L : C ⥤ D<VAR>R : D ⥤ C<VAR>h : L ⊣ R<VAR>A : C<VAR>CategoryTheory.IsIso (h.unit.app A)<GOAL>A ∈ R.essImage
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>L : C ⥤ D<VAR>R : D ⥤ C<VAR>h : L ⊣ R<VAR>R.Faithful<VAR>R.Full<VAR>X : D<VAR>Y : C<VAR>e : Y ≅ R.obj X<GOAL>CategoryTheory.IsIso (h.unit.app Y)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>L : C ⥤ D<VAR>R : D ⥤ C<VAR>h : L ⊣ R<VAR>R.IsEquivalence<GOAL>L.IsEquivalence
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>L : C ⥤ D<VAR>R : D ⥤ C<VAR>h : L ⊣ R<VAR>L.IsEquivalence<GOAL>R.IsEquivalence
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} D<VAR>CategoryTheory.Abelian C<VAR>CategoryTheory.HasInjectiveResolutions C<VAR>CategoryTheory.Abelian D<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>I : CategoryTheory.InjectiveResolution X<VAR>J : CategoryTheory.InjectiveResolution Y<VAR>φ : I.cocomplex ⟶ J.cocomplex<VAR>comm : CategoryTheory.CategoryStruct.comp (I.ι.f 0) (φ.f 0) = CategoryTheory.CategoryStruct.comp f (J.ι.f 0)<VAR>F : CategoryTheory.Functor C D<VAR>F.Additive<GOAL>CategoryTheory.CategoryStruct.comp (F.rightDerivedToHomotopyCategory.map f) (J.isoRightDerivedToHomotopyCategoryObj F).hom = CategoryTheory.CategoryStruct.comp (I.isoRightDerivedToHomotopyCategoryObj F).hom (((F.mapHomologicalComplex (ComplexShape.up ℕ)).comp (HomotopyCategory.quotient D (ComplexShape.up ℕ))).map φ)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} D<VAR>CategoryTheory.Abelian C<VAR>CategoryTheory.HasInjectiveResolutions C<VAR>CategoryTheory.Abelian D<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>I : CategoryTheory.InjectiveResolution X<VAR>J : CategoryTheory.InjectiveResolution Y<VAR>φ : I.cocomplex ⟶ J.cocomplex<VAR>comm : CategoryTheory.CategoryStruct.comp (I.ι.f 0) (φ.f 0) = CategoryTheory.CategoryStruct.comp f (J.ι.f 0)<VAR>F : CategoryTheory.Functor C D<VAR>F.Additive<GOAL>CategoryTheory.CategoryStruct.comp (I.isoRightDerivedToHomotopyCategoryObj F).inv (F.rightDerivedToHomotopyCategory.map f) = CategoryTheory.CategoryStruct.comp (((F.mapHomologicalComplex (ComplexShape.up ℕ)).comp (HomotopyCategory.quotient D (ComplexShape.up ℕ))).map φ) (J.isoRightDerivedToHomotopyCategoryObj F).inv
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} D<VAR>CategoryTheory.Abelian C<VAR>CategoryTheory.HasInjectiveResolutions C<VAR>CategoryTheory.Abelian D<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>I : CategoryTheory.InjectiveResolution X<VAR>J : CategoryTheory.InjectiveResolution Y<VAR>φ : I.cocomplex ⟶ J.cocomplex<VAR>comm : CategoryTheory.CategoryStruct.comp (I.ι.f 0) (φ.f 0) = CategoryTheory.CategoryStruct.comp f (J.ι.f 0)<VAR>F : CategoryTheory.Functor C D<VAR>F.Additive<VAR>n : ℕ<GOAL>CategoryTheory.CategoryStruct.comp ((F.rightDerived n).map f) (J.isoRightDerivedObj F n).hom = CategoryTheory.CategoryStruct.comp (I.isoRightDerivedObj F n).hom (((F.mapHomologicalComplex (ComplexShape.up ℕ)).comp (HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n)).map φ)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} D<VAR>CategoryTheory.Abelian C<VAR>CategoryTheory.HasInjectiveResolutions C<VAR>CategoryTheory.Abelian D<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>I : CategoryTheory.InjectiveResolution X<VAR>J : CategoryTheory.InjectiveResolution Y<VAR>φ : I.cocomplex ⟶ J.cocomplex<VAR>comm : CategoryTheory.CategoryStruct.comp (I.ι.f 0) (φ.f 0) = CategoryTheory.CategoryStruct.comp f (J.ι.f 0)<VAR>F : CategoryTheory.Functor C D<VAR>F.Additive<VAR>n : ℕ<GOAL>CategoryTheory.CategoryStruct.comp (I.isoRightDerivedObj F n).inv ((F.rightDerived n).map f) = CategoryTheory.CategoryStruct.comp (((F.mapHomologicalComplex (ComplexShape.up ℕ)).comp (HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n)).map φ) (J.isoRightDerivedObj F n).inv
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} D<VAR>CategoryTheory.Abelian C<VAR>CategoryTheory.HasInjectiveResolutions C<VAR>CategoryTheory.Abelian D<VAR>F : CategoryTheory.Functor C D<VAR>F.Additive<VAR>n : ℕ<VAR>X : C<VAR>CategoryTheory.Injective X<GOAL>CategoryTheory.Limits.IsZero ((F.rightDerived (n + 1)).obj X)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} D<VAR>CategoryTheory.Abelian C<VAR>CategoryTheory.HasInjectiveResolutions C<VAR>CategoryTheory.Abelian D<VAR>F : CategoryTheory.Functor C D<VAR>F.Additive<VAR>n : ℕ<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>P : CategoryTheory.InjectiveResolution X<VAR>Q : CategoryTheory.InjectiveResolution Y<VAR>g : P.cocomplex ⟶ Q.cocomplex<VAR>w : CategoryTheory.CategoryStruct.comp P.ι g = CategoryTheory.CategoryStruct.comp ((CochainComplex.single₀ C).map f) Q.ι<GOAL>(F.rightDerived n).map f = CategoryTheory.CategoryStruct.comp (P.isoRightDerivedObj F n).hom (CategoryTheory.CategoryStruct.comp (((F.mapHomologicalComplex (ComplexShape.up ℕ)).comp (HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n)).map g) (Q.isoRightDerivedObj F n).inv)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} D<VAR>CategoryTheory.Abelian C<VAR>CategoryTheory.HasInjectiveResolutions C<VAR>CategoryTheory.Abelian D<VAR>F G : CategoryTheory.Functor C D<VAR>F.Additive<VAR>G.Additive<VAR>α : F ⟶ G<VAR>X : C<VAR>P : CategoryTheory.InjectiveResolution X<GOAL>(CategoryTheory.NatTrans.rightDerivedToHomotopyCategory α).app X = CategoryTheory.CategoryStruct.comp (P.isoRightDerivedToHomotopyCategoryObj F).hom (CategoryTheory.CategoryStruct.comp ((HomotopyCategory.quotient D (ComplexShape.up ℕ)).map ((CategoryTheory.NatTrans.mapHomologicalComplex α (ComplexShape.up ℕ)).app P.cocomplex)) (P.isoRightDerivedToHomotopyCategoryObj G).inv)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} D<VAR>CategoryTheory.Abelian C<VAR>CategoryTheory.HasInjectiveResolutions C<VAR>CategoryTheory.Abelian D<VAR>F : CategoryTheory.Functor C D<VAR>F.Additive<GOAL>CategoryTheory.NatTrans.rightDerivedToHomotopyCategory (CategoryTheory.CategoryStruct.id F) = CategoryTheory.CategoryStruct.id F.rightDerivedToHomotopyCategory
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} D<VAR>CategoryTheory.Abelian C<VAR>CategoryTheory.HasInjectiveResolutions C<VAR>CategoryTheory.Abelian D<VAR>F G H : CategoryTheory.Functor C D<VAR>α : F ⟶ G<VAR>β : G ⟶ H<VAR>F.Additive<VAR>G.Additive<VAR>H.Additive<GOAL>CategoryTheory.NatTrans.rightDerivedToHomotopyCategory (CategoryTheory.CategoryStruct.comp α β) = CategoryTheory.CategoryStruct.comp (CategoryTheory.NatTrans.rightDerivedToHomotopyCategory α) (CategoryTheory.NatTrans.rightDerivedToHomotopyCategory β)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} D<VAR>CategoryTheory.Abelian C<VAR>CategoryTheory.HasInjectiveResolutions C<VAR>CategoryTheory.Abelian D<VAR>F : CategoryTheory.Functor C D<VAR>F.Additive<VAR>n : ℕ<GOAL>CategoryTheory.NatTrans.rightDerived (CategoryTheory.CategoryStruct.id F) n = CategoryTheory.CategoryStruct.id (F.rightDerived n)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} D<VAR>CategoryTheory.Abelian C<VAR>CategoryTheory.HasInjectiveResolutions C<VAR>CategoryTheory.Abelian D<VAR>F G H : CategoryTheory.Functor C D<VAR>F.Additive<VAR>G.Additive<VAR>H.Additive<VAR>α : F ⟶ G<VAR>β : G ⟶ H<VAR>n : ℕ<GOAL>CategoryTheory.NatTrans.rightDerived (CategoryTheory.CategoryStruct.comp α β) n = CategoryTheory.CategoryStruct.comp (CategoryTheory.NatTrans.rightDerived α n) (CategoryTheory.NatTrans.rightDerived β n)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} D<VAR>CategoryTheory.Abelian C<VAR>CategoryTheory.HasInjectiveResolutions C<VAR>CategoryTheory.Abelian D<VAR>F G : CategoryTheory.Functor C D<VAR>F.Additive<VAR>G.Additive<VAR>α : F ⟶ G<VAR>X : C<VAR>P : CategoryTheory.InjectiveResolution X<VAR>n : ℕ<GOAL>(CategoryTheory.NatTrans.rightDerived α n).app X = CategoryTheory.CategoryStruct.comp (P.isoRightDerivedObj F n).hom (CategoryTheory.CategoryStruct.comp ((HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n).map ((CategoryTheory.NatTrans.mapHomologicalComplex α (ComplexShape.up ℕ)).app P.cocomplex)) (P.isoRightDerivedObj G n).inv)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} D<VAR>CategoryTheory.Abelian C<VAR>CategoryTheory.Abelian D<VAR>X : C<VAR>P : CategoryTheory.InjectiveResolution X<VAR>F : CategoryTheory.Functor C D<VAR>F.Additive<GOAL>CategoryTheory.CategoryStruct.comp (P.toRightDerivedZero' F) (((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj P.cocomplex).iCycles 0) = F.map (P.ι.f 0)