ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>i : CategoryTheory.Functor D C<VAR>CategoryTheory.Reflective i<VAR>X : C<GOAL>(CategoryTheory.reflectorAdjunction i).unit.app (i.obj ((CategoryTheory.reflector i).obj X)) = i.map ((CategoryTheory.reflector i).map ((CategoryTheory.reflectorAdjunction i).unit.app X))
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>i : CategoryTheory.Functor D C<VAR>CategoryTheory.Reflective i<VAR>A : C<VAR>h : A ∈ i.essImage<GOAL>CategoryTheory.IsIso ((CategoryTheory.reflectorAdjunction i).unit.app A)
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>i : CategoryTheory.Functor D C<VAR>CategoryTheory.Reflective i<VAR>A : C<VAR>CategoryTheory.IsSplitMono ((CategoryTheory.reflectorAdjunction i).unit.app A)<GOAL>A ∈ i.essImage
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>i : CategoryTheory.Functor D C<VAR>CategoryTheory.Reflective i<VAR>A : C<VAR>B : D<VAR>f : i.obj ((CategoryTheory.reflector i).obj A) ⟶ i.obj B<GOAL>(CategoryTheory.unitCompPartialBijectiveAux A B).symm f = CategoryTheory.CategoryStruct.comp ((CategoryTheory.reflectorAdjunction i).unit.app A) f
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>i : CategoryTheory.Functor D C<VAR>CategoryTheory.Reflective i<VAR>A : C<VAR>B : C<VAR>hB : B ∈ i.essImage<VAR>f : i.obj ((CategoryTheory.reflector i).obj A) ⟶ B<GOAL>(CategoryTheory.unitCompPartialBijective A hB).symm f = CategoryTheory.CategoryStruct.comp ((CategoryTheory.reflectorAdjunction i).unit.app A) f
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>i : CategoryTheory.Functor D C<VAR>CategoryTheory.Reflective i<VAR>A : C<VAR>B B' : C<VAR>h : B ⟶ B'<VAR>hB : B ∈ i.essImage<VAR>hB' : B' ∈ i.essImage<VAR>f : i.obj ((CategoryTheory.reflector i).obj A) ⟶ B<GOAL>(CategoryTheory.unitCompPartialBijective A hB').symm (CategoryTheory.CategoryStruct.comp f h) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.unitCompPartialBijective A hB).symm f) h
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>i : CategoryTheory.Functor D C<VAR>CategoryTheory.Reflective i<VAR>A : C<VAR>B B' : C<VAR>h : B ⟶ B'<VAR>hB : B ∈ i.essImage<VAR>hB' : B' ∈ i.essImage<VAR>f : A ⟶ B<GOAL>(CategoryTheory.unitCompPartialBijective A hB') (CategoryTheory.CategoryStruct.comp f h) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.unitCompPartialBijective A hB) f) h
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>i : CategoryTheory.Functor D C<VAR>CategoryTheory.Reflective i<VAR>X : i.EssImageSubcategory<GOAL>i.essImageInclusion.map (CategoryTheory.equivEssImageOfReflective_counitIso_app X).hom = CategoryTheory.inv ((CategoryTheory.reflectorAdjunction i).unit.app X.obj)
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>i : CategoryTheory.Functor D C<VAR>CategoryTheory.Reflective i<VAR>X : i.EssImageSubcategory<GOAL>i.essImageInclusion.map (CategoryTheory.equivEssImageOfReflective_counitIso_app X).inv = (CategoryTheory.reflectorAdjunction i).unit.app X.obj
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>i : CategoryTheory.Functor D C<VAR>CategoryTheory.Reflective i<GOAL>CategoryTheory.equivEssImageOfReflective.unitIso = CategoryTheory.NatIso.ofComponents (fun X => (CategoryTheory.asIso ((CategoryTheory.reflectorAdjunction i).counit.app X)).symm) ⋯
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>i : CategoryTheory.Functor D C<VAR>CategoryTheory.Reflective i<GOAL>CategoryTheory.equivEssImageOfReflective.inverse = i.essImageInclusion.comp (CategoryTheory.reflector i)
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>i : CategoryTheory.Functor D C<VAR>CategoryTheory.Reflective i<GOAL>CategoryTheory.equivEssImageOfReflective.counitIso = CategoryTheory.NatIso.ofComponents CategoryTheory.equivEssImageOfReflective_counitIso_app ⋯
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>i : CategoryTheory.Functor D C<VAR>CategoryTheory.Reflective i<GOAL>CategoryTheory.equivEssImageOfReflective.functor = i.toEssImage
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>j : CategoryTheory.Functor C D<VAR>CategoryTheory.Coreflective j<VAR>X : D<GOAL>(CategoryTheory.coreflectorAdjunction j).counit.app (j.obj ((CategoryTheory.coreflector j).obj X)) = j.map ((CategoryTheory.coreflector j).map ((CategoryTheory.coreflectorAdjunction j).counit.app X))
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>j : CategoryTheory.Functor C D<VAR>CategoryTheory.Coreflective j<VAR>A : D<VAR>h : A ∈ j.essImage<GOAL>CategoryTheory.IsIso ((CategoryTheory.coreflectorAdjunction j).counit.app A)
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>j : CategoryTheory.Functor C D<VAR>CategoryTheory.Coreflective j<VAR>A : D<VAR>CategoryTheory.IsSplitEpi ((CategoryTheory.coreflectorAdjunction j).counit.app A)<GOAL>A ∈ j.essImage
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>CategoryTheory.Category.{u_6, u_3} E<VAR>F : CategoryTheory.Functor D E<VAR>G : CategoryTheory.Functor E D<VAR>adj : F ⊣ G<VAR>X : CategoryTheory.Functor C D<GOAL>∀ (X_1 : C), ((CategoryTheory.Adjunction.whiskerRight C adj).unit.app X).app X_1 = adj.unit.app (X.obj X_1)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>CategoryTheory.Category.{u_6, u_3} E<VAR>F : CategoryTheory.Functor D E<VAR>G : CategoryTheory.Functor E D<VAR>adj : F ⊣ G<VAR>X : CategoryTheory.Functor C E<GOAL>∀ (X_1 : C), ((CategoryTheory.Adjunction.whiskerRight C adj).counit.app X).app X_1 = adj.counit.app (X.obj X_1)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>CategoryTheory.Category.{u_6, u_3} E<VAR>F : CategoryTheory.Functor D E<VAR>G : CategoryTheory.Functor E D<VAR>adj : F ⊣ G<VAR>X : CategoryTheory.Functor E C<GOAL>∀ (X_1 : E), ((CategoryTheory.Adjunction.whiskerLeft C adj).counit.app X).app X_1 = X.map (adj.counit.app X_1)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>CategoryTheory.Category.{u_6, u_3} E<VAR>F : CategoryTheory.Functor D E<VAR>G : CategoryTheory.Functor E D<VAR>adj : F ⊣ G<VAR>X : CategoryTheory.Functor D C<GOAL>∀ (X_1 : D), ((CategoryTheory.Adjunction.whiskerLeft C adj).unit.app X).app X_1 = X.map (adj.unit.app X_1)
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>G : CategoryTheory.Functor D C<VAR>∀ (A : C), CategoryTheory.Limits.HasInitial (CategoryTheory.StructuredArrow A G)<VAR>A : C<VAR>B : D<VAR>g : (⊥_ CategoryTheory.StructuredArrow A G).right ⟶ B<GOAL>(CategoryTheory.leftAdjointOfStructuredArrowInitialsAux G A B) g = CategoryTheory.CategoryStruct.comp (⊥_ CategoryTheory.StructuredArrow A G).hom (G.map g)
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>G : CategoryTheory.Functor D C<VAR>∀ (A : C), CategoryTheory.Limits.HasInitial (CategoryTheory.StructuredArrow A G)<VAR>A : C<VAR>B : D<VAR>f : A ⟶ G.obj B<GOAL>(CategoryTheory.leftAdjointOfStructuredArrowInitialsAux G A B).symm f = (CategoryTheory.Limits.initial.to (CategoryTheory.StructuredArrow.mk f)).right
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>G : CategoryTheory.Functor D C<VAR>∀ (A : C), CategoryTheory.Limits.HasInitial (CategoryTheory.StructuredArrow A G)<GOAL>G.IsRightAdjoint
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>G : CategoryTheory.Functor D C<VAR>∀ (A : C), CategoryTheory.Limits.HasTerminal (CategoryTheory.CostructuredArrow G A)<VAR>B : D<VAR>A : C<VAR>g : B ⟶ (⊤_ CategoryTheory.CostructuredArrow G A).left<GOAL>(CategoryTheory.rightAdjointOfCostructuredArrowTerminalsAux G B A).symm g = CategoryTheory.CategoryStruct.comp (G.map g) (⊤_ CategoryTheory.CostructuredArrow G A).hom
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>G : CategoryTheory.Functor D C<VAR>∀ (A : C), CategoryTheory.Limits.HasTerminal (CategoryTheory.CostructuredArrow G A)<VAR>B : D<VAR>A : C<VAR>g : G.obj B ⟶ A<GOAL>(CategoryTheory.rightAdjointOfCostructuredArrowTerminalsAux G B A) g = (CategoryTheory.Limits.terminal.from (CategoryTheory.CostructuredArrow.mk g)).left
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>G : CategoryTheory.Functor D C<VAR>∀ (A : C), CategoryTheory.Limits.HasTerminal (CategoryTheory.CostructuredArrow G A)<GOAL>G.IsLeftAdjoint
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>G : CategoryTheory.Functor D C<GOAL>G.IsRightAdjoint ↔ ∀ (A : C), CategoryTheory.Limits.HasInitial (CategoryTheory.StructuredArrow A G)
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : CategoryTheory.Functor C D<GOAL>F.IsLeftAdjoint ↔ ∀ (A : D), CategoryTheory.Limits.HasTerminal (CategoryTheory.CostructuredArrow F A)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>C' : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C'<VAR>D' : Type u₄<VAR>CategoryTheory.Category.{v₄, u₄} D'<VAR>iC : CategoryTheory.Functor C C'<VAR>iD : CategoryTheory.Functor D D'<VAR>L' : CategoryTheory.Functor C' D'<VAR>R' : CategoryTheory.Functor D' C'<VAR>adj : L' ⊣ R'<VAR>hiC : iC.FullyFaithful<VAR>hiD : iD.FullyFaithful<VAR>L : CategoryTheory.Functor C D<VAR>R : CategoryTheory.Functor D C<VAR>comm1 : iC.comp L' ≅ L.comp iD<VAR>comm2 : iD.comp R' ≅ R.comp iC<VAR>X : C<GOAL>iC.map ((adj.restrictFullyFaithful hiC hiD comm1 comm2).unit.app X) = CategoryTheory.CategoryStruct.comp (adj.unit.app (iC.obj X)) (CategoryTheory.CategoryStruct.comp (R'.map (comm1.hom.app X)) (comm2.hom.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>C' : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C'<VAR>D' : Type u₄<VAR>CategoryTheory.Category.{v₄, u₄} D'<VAR>iC : CategoryTheory.Functor C C'<VAR>iD : CategoryTheory.Functor D D'<VAR>L' : CategoryTheory.Functor C' D'<VAR>R' : CategoryTheory.Functor D' C'<VAR>adj : L' ⊣ R'<VAR>hiC : iC.FullyFaithful<VAR>hiD : iD.FullyFaithful<VAR>L : CategoryTheory.Functor C D<VAR>R : CategoryTheory.Functor D C<VAR>comm1 : iC.comp L' ≅ L.comp iD<VAR>comm2 : iD.comp R' ≅ R.comp iC<VAR>X : D<GOAL>iD.map ((adj.restrictFullyFaithful hiC hiD comm1 comm2).counit.app X) = CategoryTheory.CategoryStruct.comp (comm1.inv.app (R.obj X)) (CategoryTheory.CategoryStruct.comp (L'.map (comm2.inv.app X)) (adj.counit.app (iD.obj X)))
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>C' : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C'<VAR>D' : Type u₄<VAR>CategoryTheory.Category.{v₄, u₄} D'<VAR>iC : CategoryTheory.Functor C C'<VAR>iD : CategoryTheory.Functor D D'<VAR>L' : CategoryTheory.Functor C' D'<VAR>R' : CategoryTheory.Functor D' C'<VAR>adj : L' ⊣ R'<VAR>hiC : iC.FullyFaithful<VAR>hiD : iD.FullyFaithful<VAR>L : CategoryTheory.Functor C D<VAR>R : CategoryTheory.Functor D C<VAR>comm1 : iC.comp L' ≅ L.comp iD<VAR>comm2 : iD.comp R' ≅ R.comp iC<VAR>X : C<VAR>Y : D<VAR>f : L.obj X ⟶ Y<GOAL>((adj.restrictFullyFaithful hiC hiD comm1 comm2).homEquiv X Y) f = hiC.preimage (CategoryTheory.CategoryStruct.comp (adj.unit.app (iC.obj X)) (CategoryTheory.CategoryStruct.comp (R'.map (comm1.hom.app X)) (CategoryTheory.CategoryStruct.comp (R'.map (iD.map f)) (comm2.hom.app Y))))
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.FinitaryPreExtensive C<VAR>α : Type<VAR>Finite α<VAR>B : C<VAR>X : α → C<VAR>π : (a : α) → X a ⟶ B<GOAL>CategoryTheory.EffectiveEpi (CategoryTheory.Limits.Sigma.desc π) ↔ CategoryTheory.EffectiveEpiFamily 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>X Y : C<VAR>f : X ⟶ Y<VAR>P : CategoryTheory.ProjectiveResolution X<VAR>Q : CategoryTheory.ProjectiveResolution Y<VAR>φ : P.complex ⟶ Q.complex<VAR>comm : CategoryTheory.CategoryStruct.comp (φ.f 0) (Q.π.f 0) = CategoryTheory.CategoryStruct.comp (P.π.f 0) f<VAR>F : CategoryTheory.Functor C D<VAR>F.Additive<GOAL>CategoryTheory.CategoryStruct.comp (P.isoLeftDerivedToHomotopyCategoryObj F).inv (F.leftDerivedToHomotopyCategory.map f) = CategoryTheory.CategoryStruct.comp (((F.mapHomologicalComplex (ComplexShape.down ℕ)).comp (HomotopyCategory.quotient D (ComplexShape.down ℕ))).map φ) (Q.isoLeftDerivedToHomotopyCategoryObj 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.HasProjectiveResolutions C<VAR>CategoryTheory.Abelian D<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>P : CategoryTheory.ProjectiveResolution X<VAR>Q : CategoryTheory.ProjectiveResolution Y<VAR>φ : P.complex ⟶ Q.complex<VAR>comm : CategoryTheory.CategoryStruct.comp (φ.f 0) (Q.π.f 0) = CategoryTheory.CategoryStruct.comp (P.π.f 0) f<VAR>F : CategoryTheory.Functor C D<VAR>F.Additive<GOAL>CategoryTheory.CategoryStruct.comp (F.leftDerivedToHomotopyCategory.map f) (Q.isoLeftDerivedToHomotopyCategoryObj F).hom = CategoryTheory.CategoryStruct.comp (P.isoLeftDerivedToHomotopyCategoryObj F).hom (((F.mapHomologicalComplex (ComplexShape.down ℕ)).comp (HomotopyCategory.quotient D (ComplexShape.down ℕ))).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.HasProjectiveResolutions C<VAR>CategoryTheory.Abelian D<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>P : CategoryTheory.ProjectiveResolution X<VAR>Q : CategoryTheory.ProjectiveResolution Y<VAR>φ : P.complex ⟶ Q.complex<VAR>comm : CategoryTheory.CategoryStruct.comp (φ.f 0) (Q.π.f 0) = CategoryTheory.CategoryStruct.comp (P.π.f 0) f<VAR>F : CategoryTheory.Functor C D<VAR>F.Additive<VAR>n : ℕ<GOAL>CategoryTheory.CategoryStruct.comp ((F.leftDerived n).map f) (Q.isoLeftDerivedObj F n).hom = CategoryTheory.CategoryStruct.comp (P.isoLeftDerivedObj F n).hom (((F.mapHomologicalComplex (ComplexShape.down ℕ)).comp (HomologicalComplex.homologyFunctor D (ComplexShape.down ℕ) 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.HasProjectiveResolutions C<VAR>CategoryTheory.Abelian D<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>P : CategoryTheory.ProjectiveResolution X<VAR>Q : CategoryTheory.ProjectiveResolution Y<VAR>φ : P.complex ⟶ Q.complex<VAR>comm : CategoryTheory.CategoryStruct.comp (φ.f 0) (Q.π.f 0) = CategoryTheory.CategoryStruct.comp (P.π.f 0) f<VAR>F : CategoryTheory.Functor C D<VAR>F.Additive<VAR>n : ℕ<GOAL>CategoryTheory.CategoryStruct.comp (P.isoLeftDerivedObj F n).inv ((F.leftDerived n).map f) = CategoryTheory.CategoryStruct.comp (((F.mapHomologicalComplex (ComplexShape.down ℕ)).comp (HomologicalComplex.homologyFunctor D (ComplexShape.down ℕ) n)).map φ) (Q.isoLeftDerivedObj 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.HasProjectiveResolutions C<VAR>CategoryTheory.Abelian D<VAR>F : CategoryTheory.Functor C D<VAR>F.Additive<VAR>n : ℕ<VAR>X : C<VAR>CategoryTheory.Projective X<GOAL>CategoryTheory.Limits.IsZero ((F.leftDerived (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.HasProjectiveResolutions 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.ProjectiveResolution X<VAR>Q : CategoryTheory.ProjectiveResolution Y<VAR>g : P.complex ⟶ Q.complex<VAR>w : CategoryTheory.CategoryStruct.comp g Q.π = CategoryTheory.CategoryStruct.comp P.π ((ChainComplex.single₀ C).map f)<GOAL>(F.leftDerived n).map f = CategoryTheory.CategoryStruct.comp (P.isoLeftDerivedObj F n).hom (CategoryTheory.CategoryStruct.comp (((F.mapHomologicalComplex (ComplexShape.down ℕ)).comp (HomologicalComplex.homologyFunctor D (ComplexShape.down ℕ) n)).map g) (Q.isoLeftDerivedObj 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.HasProjectiveResolutions 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.ProjectiveResolution X<GOAL>(CategoryTheory.NatTrans.leftDerivedToHomotopyCategory α).app X = CategoryTheory.CategoryStruct.comp (P.isoLeftDerivedToHomotopyCategoryObj F).hom (CategoryTheory.CategoryStruct.comp ((HomotopyCategory.quotient D (ComplexShape.down ℕ)).map ((CategoryTheory.NatTrans.mapHomologicalComplex α (ComplexShape.down ℕ)).app P.complex)) (P.isoLeftDerivedToHomotopyCategoryObj 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.HasProjectiveResolutions C<VAR>CategoryTheory.Abelian D<VAR>F : CategoryTheory.Functor C D<VAR>F.Additive<GOAL>CategoryTheory.NatTrans.leftDerivedToHomotopyCategory (CategoryTheory.CategoryStruct.id F) = CategoryTheory.CategoryStruct.id F.leftDerivedToHomotopyCategory
<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 G H : CategoryTheory.Functor C D<VAR>α : F ⟶ G<VAR>β : G ⟶ H<VAR>F.Additive<VAR>G.Additive<VAR>H.Additive<GOAL>CategoryTheory.NatTrans.leftDerivedToHomotopyCategory (CategoryTheory.CategoryStruct.comp α β) = CategoryTheory.CategoryStruct.comp (CategoryTheory.NatTrans.leftDerivedToHomotopyCategory α) (CategoryTheory.NatTrans.leftDerivedToHomotopyCategory β)
<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>n : ℕ<GOAL>CategoryTheory.NatTrans.leftDerived (CategoryTheory.CategoryStruct.id F) n = CategoryTheory.CategoryStruct.id (F.leftDerived 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.HasProjectiveResolutions 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.leftDerived (CategoryTheory.CategoryStruct.comp α β) n = CategoryTheory.CategoryStruct.comp (CategoryTheory.NatTrans.leftDerived α n) (CategoryTheory.NatTrans.leftDerived β 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.HasProjectiveResolutions 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.ProjectiveResolution X<VAR>n : ℕ<GOAL>(CategoryTheory.NatTrans.leftDerived α n).app X = CategoryTheory.CategoryStruct.comp (P.isoLeftDerivedObj F n).hom (CategoryTheory.CategoryStruct.comp ((HomologicalComplex.homologyFunctor D (ComplexShape.down ℕ) n).map ((CategoryTheory.NatTrans.mapHomologicalComplex α (ComplexShape.down ℕ)).app P.complex)) (P.isoLeftDerivedObj 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.ProjectiveResolution X<VAR>F : CategoryTheory.Functor C D<VAR>F.Additive<GOAL>CategoryTheory.CategoryStruct.comp (((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj P.complex).pOpcycles 0) (P.fromLeftDerivedZero' F) = F.map (P.π.f 0)
<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 Y : C<VAR>f : X ⟶ Y<VAR>P : CategoryTheory.ProjectiveResolution X<VAR>Q : CategoryTheory.ProjectiveResolution Y<VAR>φ : P.complex ⟶ Q.complex<VAR>comm : CategoryTheory.CategoryStruct.comp (φ.f 0) (Q.π.f 0) = CategoryTheory.CategoryStruct.comp (P.π.f 0) f<VAR>F : CategoryTheory.Functor C D<VAR>F.Additive<GOAL>CategoryTheory.CategoryStruct.comp (HomologicalComplex.opcyclesMap ((F.mapHomologicalComplex (ComplexShape.down ℕ)).map φ) 0) (Q.fromLeftDerivedZero' F) = CategoryTheory.CategoryStruct.comp (P.fromLeftDerivedZero' F) (F.map f)
<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>X : C<VAR>P : CategoryTheory.ProjectiveResolution X<VAR>F : CategoryTheory.Functor C D<VAR>F.Additive<GOAL>F.fromLeftDerivedZero.app X = CategoryTheory.CategoryStruct.comp (P.isoLeftDerivedObj F 0).hom (CategoryTheory.CategoryStruct.comp (ChainComplex.isoHomologyι₀ ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj P.complex)).hom (P.fromLeftDerivedZero' F))
<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<GOAL>F.leftDerivedZeroIsoSelf.hom = F.fromLeftDerivedZero
<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<GOAL>CategoryTheory.CategoryStruct.comp F.fromLeftDerivedZero F.leftDerivedZeroIsoSelf.inv = CategoryTheory.CategoryStruct.id (F.leftDerived 0)
<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<GOAL>CategoryTheory.CategoryStruct.comp F.leftDerivedZeroIsoSelf.inv F.fromLeftDerivedZero = CategoryTheory.CategoryStruct.id F