ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type uC<VAR>CategoryTheory.Category.{uC', uC} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>D : Type uD<VAR>CategoryTheory.Category.{uD', uD} D<VAR>G : CategoryTheory.Functor C D<VAR>hG : W.IsInvertedBy G<VAR>a b : CategoryTheory.Quotient (CategoryTheory.Localization.Construction.relations W)<VAR>hf : a ⟶ b<GOAL>(CategoryTheory.Localization.Construction.lift G hG).map hf = Quot.liftOn hf (fun f => CategoryTheory.composePath ({ obj := fun X => G.obj X.obj, map := fun {X Y} a => Sum.rec (fun val => G.map val) (fun val => CategoryTheory.inv (G.map ↑val)) a }.mapPath f)) ⋯
<VAR>C : Type uC<VAR>CategoryTheory.Category.{uC', uC} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>D : Type uD<VAR>CategoryTheory.Category.{uD', uD} D<VAR>G : CategoryTheory.Functor C D<VAR>hG : W.IsInvertedBy G<GOAL>W.Q.comp (CategoryTheory.Localization.Construction.lift G hG) = G
<VAR>C : Type uC<VAR>CategoryTheory.Category.{uC', uC} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>D : Type uD<VAR>CategoryTheory.Category.{uD', uD} D<VAR>G₁ G₂ : CategoryTheory.Functor W.Localization D<VAR>h : W.Q.comp G₁ = W.Q.comp G₂<GOAL>G₁ = G₂
<VAR>C : Type uC<VAR>CategoryTheory.Category.{uC', uC} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>X : W.Localization<GOAL>(CategoryTheory.Localization.Construction.objEquiv W).symm X = X.as.obj
<VAR>C : Type uC<VAR>CategoryTheory.Category.{uC', uC} C<VAR>W : CategoryTheory.MorphismProperty C<GOAL>∀ (a : C), (CategoryTheory.Localization.Construction.objEquiv W) a = W.Q.obj a
<VAR>C : Type uC<VAR>CategoryTheory.Category.{uC', uC} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>P : CategoryTheory.MorphismProperty W.Localization<VAR>P.IsStableUnderComposition<VAR>hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P (W.Q.map f)<VAR>hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (CategoryTheory.Localization.Construction.wInv w hw)<GOAL>P = ⊤
<VAR>C : Type uC<VAR>CategoryTheory.Category.{uC', uC} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>P : CategoryTheory.MorphismProperty W.Localization<VAR>P.IsStableUnderComposition<VAR>hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P (W.Q.map f)<VAR>hP₂ : ∀ ⦃X Y : W.Localization⦄ (e : X ≅ Y), P e.hom → P e.inv<GOAL>P = ⊤
<VAR>C : Type uC<VAR>CategoryTheory.Category.{uC', uC} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>D : Type uD<VAR>CategoryTheory.Category.{uD', uD} D<VAR>F₁ F₂ : CategoryTheory.Functor W.Localization D<VAR>τ : W.Q.comp F₁ ⟶ W.Q.comp F₂<VAR>X : C<GOAL>CategoryTheory.Localization.Construction.NatTransExtension.app τ (W.Q.obj X) = τ.app X
<VAR>C : Type uC<VAR>CategoryTheory.Category.{uC', uC} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>D : Type uD<VAR>CategoryTheory.Category.{uD', uD} D<VAR>F₁ F₂ : CategoryTheory.Functor W.Localization D<VAR>τ : W.Q.comp F₁ ⟶ W.Q.comp F₂<VAR>X : W.Localization<GOAL>(CategoryTheory.Localization.Construction.natTransExtension τ).app X = CategoryTheory.Localization.Construction.NatTransExtension.app τ X
<VAR>C : Type uC<VAR>CategoryTheory.Category.{uC', uC} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>D : Type uD<VAR>CategoryTheory.Category.{uD', uD} D<VAR>F G : CategoryTheory.Functor W.Localization D<VAR>τ : W.Q.comp F ⟶ W.Q.comp G<GOAL>CategoryTheory.CategoryStruct.id W.Q ◫ CategoryTheory.Localization.Construction.natTransExtension τ = τ
<VAR>C : Type uC<VAR>CategoryTheory.Category.{uC', uC} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>D : Type uD<VAR>CategoryTheory.Category.{uD', uD} D<VAR>F G : CategoryTheory.Functor W.Localization D<VAR>τ₁ τ₂ : F ⟶ G<VAR>h : CategoryTheory.CategoryStruct.id W.Q ◫ τ₁ = CategoryTheory.CategoryStruct.id W.Q ◫ τ₂<GOAL>τ₁ = τ₂
<VAR>C : Type uC<VAR>CategoryTheory.Category.{uC', uC} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>D : Type uD<VAR>CategoryTheory.Category.{uD', uD} D<VAR>X : CategoryTheory.Functor W.Localization D<GOAL>∀ (X_1 : C), ((CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.functor W D).obj X).obj.obj X_1 = X.obj (W.Q.obj X_1)
<VAR>C : Type uC<VAR>CategoryTheory.Category.{uC', uC} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>D : Type uD<VAR>CategoryTheory.Category.{uD', uD} D<VAR>X : CategoryTheory.Functor W.Localization D<GOAL>∀ {X_1 Y : C} (f : X_1 ⟶ Y), ((CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.functor W D).obj X).obj.map f = X.map (W.Q.map f)
<VAR>C : Type uC<VAR>CategoryTheory.Category.{uC', uC} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>D : Type uD<VAR>CategoryTheory.Category.{uD', uD} D<GOAL>∀ {X Y : CategoryTheory.Functor W.Localization D} (f : X ⟶ Y) (X_1 : C), ((CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.functor W D).map f).app X_1 = f.app (W.Q.obj X_1)
<VAR>C : Type uC<VAR>CategoryTheory.Category.{uC', uC} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>D : Type uD<VAR>CategoryTheory.Category.{uD', uD} D<VAR>G : W.FunctorsInverting D<VAR>a : CategoryTheory.Quotient (CategoryTheory.Localization.Construction.relations W)<GOAL>((CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.inverse W D).obj G).obj a = G.obj.obj a.as.obj
<VAR>C : Type uC<VAR>CategoryTheory.Category.{uC', uC} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>D : Type uD<VAR>CategoryTheory.Category.{uD', uD} D<GOAL>∀ {X Y : W.FunctorsInverting D} (τ : X ⟶ Y) (X_1 : W.Localization), ((CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.inverse W D).map τ).app X_1 = CategoryTheory.Localization.Construction.NatTransExtension.app (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp τ (CategoryTheory.eqToHom ⋯))) X_1
<VAR>C : Type uC<VAR>CategoryTheory.Category.{uC', uC} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>D : Type uD<VAR>CategoryTheory.Category.{uD', uD} D<VAR>G : W.FunctorsInverting D<VAR>a b : CategoryTheory.Quotient (CategoryTheory.Localization.Construction.relations W)<VAR>hf : a ⟶ b<GOAL>((CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.inverse W D).obj G).map hf = Quot.liftOn hf (fun f => CategoryTheory.composePath ({ obj := fun X => G.obj.obj X.obj, map := fun {X Y} a => Sum.rec (fun val => G.obj.map val) (fun val => CategoryTheory.inv (G.obj.map ↑val)) a }.mapPath f)) ⋯
<VAR>C : Type uC<VAR>CategoryTheory.Category.{uC', uC} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>D : Type uD<VAR>CategoryTheory.Category.{uD', uD} D<GOAL>(CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.unitIso W D).inv = CategoryTheory.eqToHom ⋯
<VAR>C : Type uC<VAR>CategoryTheory.Category.{uC', uC} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>D : Type uD<VAR>CategoryTheory.Category.{uD', uD} D<GOAL>(CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.unitIso W D).hom = CategoryTheory.eqToHom ⋯
<VAR>C : Type uC<VAR>CategoryTheory.Category.{uC', uC} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>D : Type uD<VAR>CategoryTheory.Category.{uD', uD} D<GOAL>(CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.counitIso W D).hom = CategoryTheory.eqToHom ⋯
<VAR>C : Type uC<VAR>CategoryTheory.Category.{uC', uC} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>D : Type uD<VAR>CategoryTheory.Category.{uD', uD} D<GOAL>(CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.counitIso W D).inv = CategoryTheory.eqToHom ⋯
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>A : Type u_2<VAR>B : Type u_3<VAR>AddMonoid A<VAR>AddMonoid B<VAR>φ : A →+ B<VAR>CategoryTheory.HasShift C B<VAR>X : CategoryTheory.PullbackShift C φ<GOAL>(CategoryTheory.shiftFunctorZero (CategoryTheory.PullbackShift C φ) A).inv.app X = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorZero C B).inv.app X) ((CategoryTheory.pullbackShiftIso C φ 0 0 ⋯).inv.app X)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>A : Type u_2<VAR>B : Type u_3<VAR>AddMonoid A<VAR>AddMonoid B<VAR>φ : A →+ B<VAR>CategoryTheory.HasShift C B<VAR>X : CategoryTheory.PullbackShift C φ<GOAL>(CategoryTheory.shiftFunctorZero (CategoryTheory.PullbackShift C φ) A).hom.app X = CategoryTheory.CategoryStruct.comp ((CategoryTheory.pullbackShiftIso C φ 0 0 ⋯).hom.app X) ((CategoryTheory.shiftFunctorZero C B).hom.app X)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>A : Type u_2<VAR>B : Type u_3<VAR>AddMonoid A<VAR>AddMonoid B<VAR>φ : A →+ B<VAR>CategoryTheory.HasShift C B<VAR>X : CategoryTheory.PullbackShift C φ<VAR>a₁ a₂ a₃ : A<VAR>h : a₁ + a₂ = a₃<VAR>b₁ b₂ b₃ : B<VAR>h₁ : b₁ = φ a₁<VAR>h₂ : b₂ = φ a₂<VAR>h₃ : b₃ = φ a₃<GOAL>(CategoryTheory.shiftFunctorAdd' (CategoryTheory.PullbackShift C φ) a₁ a₂ a₃ h).inv.app X = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor (CategoryTheory.PullbackShift C φ) a₂).map ((CategoryTheory.pullbackShiftIso C φ a₁ b₁ h₁).hom.app X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.pullbackShiftIso C φ a₂ b₂ h₂).hom.app ((CategoryTheory.shiftFunctor C b₁).obj X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd' C b₁ b₂ b₃ ⋯).inv.app X) ((CategoryTheory.pullbackShiftIso C φ a₃ b₃ h₃).inv.app X)))
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>A : Type u_2<VAR>B : Type u_3<VAR>AddMonoid A<VAR>AddMonoid B<VAR>φ : A →+ B<VAR>CategoryTheory.HasShift C B<VAR>X : CategoryTheory.PullbackShift C φ<VAR>a₁ a₂ a₃ : A<VAR>h : a₁ + a₂ = a₃<VAR>b₁ b₂ b₃ : B<VAR>h₁ : b₁ = φ a₁<VAR>h₂ : b₂ = φ a₂<VAR>h₃ : b₃ = φ a₃<GOAL>(CategoryTheory.shiftFunctorAdd' (CategoryTheory.PullbackShift C φ) a₁ a₂ a₃ h).hom.app X = CategoryTheory.CategoryStruct.comp ((CategoryTheory.pullbackShiftIso C φ a₃ b₃ h₃).hom.app X) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd' C b₁ b₂ b₃ ⋯).hom.app X) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.pullbackShiftIso C φ a₂ b₂ h₂).inv.app ((CategoryTheory.shiftFunctor C b₁).obj X)) ((CategoryTheory.shiftFunctor (CategoryTheory.PullbackShift C φ) a₂).map ((CategoryTheory.pullbackShiftIso C φ a₁ b₁ h₁).inv.app X))))
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>X Y : C<VAR>self : CategoryTheory.Localization.HasSmallLocalizedHom W X Y<GOAL>Small.{w, max u₁ v₁} (W.Q.obj X ⟶ W.Q.obj Y)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>L : CategoryTheory.Functor C D<VAR>L.IsLocalization W<VAR>X Y : C<GOAL>CategoryTheory.Localization.HasSmallLocalizedHom W X Y ↔ Small.{w, v₂} (L.obj X ⟶ L.obj Y)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>L : CategoryTheory.Functor C D<VAR>L.IsLocalization W<VAR>X Y : C<GOAL>CategoryTheory.Localization.HasSmallLocalizedHom W X Y
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>L : CategoryTheory.Functor C D<VAR>L.IsLocalization W<VAR>X Y : C<VAR>CategoryTheory.Localization.HasSmallLocalizedHom W X Y<GOAL>Small.{w, v₂} (L.obj X ⟶ L.obj Y)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>X Y X' Y' : C<VAR>e : X ≅ X'<VAR>e' : Y ≅ Y'<GOAL>CategoryTheory.Localization.HasSmallLocalizedHom W X Y ↔ CategoryTheory.Localization.HasSmallLocalizedHom W X' Y'
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>D' : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} D'<VAR>L : CategoryTheory.Functor C D<VAR>L.IsLocalization W<VAR>L' : CategoryTheory.Functor C D'<VAR>L'.IsLocalization W<VAR>G : CategoryTheory.Functor D D'<VAR>e : L.comp G ≅ L'<VAR>X Y : C<VAR>CategoryTheory.Localization.HasSmallLocalizedHom W X Y<VAR>f : L.obj X ⟶ L.obj Y<GOAL>(CategoryTheory.Localization.SmallHom.equiv W L') ((CategoryTheory.Localization.SmallHom.equiv W L).symm f) = CategoryTheory.CategoryStruct.comp (e.inv.app X) (CategoryTheory.CategoryStruct.comp (G.map f) (e.hom.app Y))
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>L : CategoryTheory.Functor C D<VAR>L.IsLocalization W<VAR>X Y : C<VAR>CategoryTheory.Localization.HasSmallLocalizedHom W X Y<VAR>f : X ⟶ Y<GOAL>(CategoryTheory.Localization.SmallHom.equiv W L) (CategoryTheory.Localization.SmallHom.mk W f) = L.map f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>L : CategoryTheory.Functor C D<VAR>L.IsLocalization W<VAR>X Y : C<VAR>f : Y ⟶ X<VAR>hf : W f<VAR>CategoryTheory.Localization.HasSmallLocalizedHom W X Y<GOAL>(CategoryTheory.Localization.SmallHom.equiv W L) (CategoryTheory.Localization.SmallHom.mkInv f hf) = (CategoryTheory.Localization.isoOfHom L W f hf).inv
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>L : CategoryTheory.Functor C D<VAR>L.IsLocalization W<VAR>X Y Z : C<VAR>CategoryTheory.Localization.HasSmallLocalizedHom W X Y<VAR>CategoryTheory.Localization.HasSmallLocalizedHom W Y Z<VAR>CategoryTheory.Localization.HasSmallLocalizedHom W X Z<VAR>α : CategoryTheory.Localization.SmallHom W X Y<VAR>β : CategoryTheory.Localization.SmallHom W Y Z<GOAL>(CategoryTheory.Localization.SmallHom.equiv W L) (α.comp β) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Localization.SmallHom.equiv W L) α) ((CategoryTheory.Localization.SmallHom.equiv W L) β)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>X Y Z : C<VAR>CategoryTheory.Localization.HasSmallLocalizedHom W X Y<VAR>CategoryTheory.Localization.HasSmallLocalizedHom W Y Z<VAR>CategoryTheory.Localization.HasSmallLocalizedHom W X Z<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>(CategoryTheory.Localization.SmallHom.mk W f).comp (CategoryTheory.Localization.SmallHom.mk W g) = CategoryTheory.Localization.SmallHom.mk W (CategoryTheory.CategoryStruct.comp f g)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>X Y : C<VAR>CategoryTheory.Localization.HasSmallLocalizedHom W X Y<VAR>CategoryTheory.Localization.HasSmallLocalizedHom W Y Y<VAR>α : CategoryTheory.Localization.SmallHom W X Y<GOAL>α.comp (CategoryTheory.Localization.SmallHom.mk W (CategoryTheory.CategoryStruct.id Y)) = α
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>X Y : C<VAR>CategoryTheory.Localization.HasSmallLocalizedHom W X Y<VAR>CategoryTheory.Localization.HasSmallLocalizedHom W X X<VAR>α : CategoryTheory.Localization.SmallHom W X Y<GOAL>(CategoryTheory.Localization.SmallHom.mk W (CategoryTheory.CategoryStruct.id X)).comp α = α
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>X Y Z T : C<VAR>CategoryTheory.Localization.HasSmallLocalizedHom W X Y<VAR>CategoryTheory.Localization.HasSmallLocalizedHom W X Z<VAR>CategoryTheory.Localization.HasSmallLocalizedHom W X T<VAR>CategoryTheory.Localization.HasSmallLocalizedHom W Y Z<VAR>CategoryTheory.Localization.HasSmallLocalizedHom W Y T<VAR>CategoryTheory.Localization.HasSmallLocalizedHom W Z T<VAR>α : CategoryTheory.Localization.SmallHom W X Y<VAR>β : CategoryTheory.Localization.SmallHom W Y Z<VAR>γ : CategoryTheory.Localization.SmallHom W Z T<GOAL>(α.comp β).comp γ = α.comp (β.comp γ)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>X Y : C<VAR>CategoryTheory.Localization.HasSmallLocalizedHom W X Y<VAR>CategoryTheory.Localization.HasSmallLocalizedHom W Y X<VAR>CategoryTheory.Localization.HasSmallLocalizedHom W Y Y<VAR>f : Y ⟶ X<VAR>hf : W f<GOAL>(CategoryTheory.Localization.SmallHom.mk W f).comp (CategoryTheory.Localization.SmallHom.mkInv f hf) = CategoryTheory.Localization.SmallHom.mk W (CategoryTheory.CategoryStruct.id Y)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>X Y : C<VAR>CategoryTheory.Localization.HasSmallLocalizedHom W X X<VAR>CategoryTheory.Localization.HasSmallLocalizedHom W X Y<VAR>CategoryTheory.Localization.HasSmallLocalizedHom W Y X<VAR>f : Y ⟶ X<VAR>hf : W f<GOAL>(CategoryTheory.Localization.SmallHom.mkInv f hf).comp (CategoryTheory.Localization.SmallHom.mk W f) = CategoryTheory.Localization.SmallHom.mk W (CategoryTheory.CategoryStruct.id X)
<VAR>C₁ : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C₁<VAR>W₁ : CategoryTheory.MorphismProperty C₁<VAR>C₂ : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} C₂<VAR>W₂ : CategoryTheory.MorphismProperty C₂<VAR>D₁ : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} D₁<VAR>D₂ : Type u₄<VAR>CategoryTheory.Category.{v₄, u₄} D₂<VAR>Φ : CategoryTheory.LocalizerMorphism W₁ W₂<VAR>L₁ : CategoryTheory.Functor C₁ D₁<VAR>L₁.IsLocalization W₁<VAR>L₂ : CategoryTheory.Functor C₂ D₂<VAR>L₂.IsLocalization W₂<VAR>X Y : C₁<VAR>CategoryTheory.Localization.HasSmallLocalizedHom W₁ X Y<VAR>CategoryTheory.Localization.HasSmallLocalizedHom W₂ (Φ.functor.obj X) (Φ.functor.obj Y)<VAR>G : CategoryTheory.Functor D₁ D₂<VAR>e : Φ.functor.comp L₂ ≅ L₁.comp G<VAR>f : CategoryTheory.Localization.SmallHom W₁ X Y<GOAL>(CategoryTheory.Localization.SmallHom.equiv W₂ L₂) (Φ.smallHomMap f) = CategoryTheory.CategoryStruct.comp (e.hom.app X) (CategoryTheory.CategoryStruct.comp (G.map ((CategoryTheory.Localization.SmallHom.equiv W₁ L₁) f)) (e.inv.app Y))
<VAR>C₁ : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C₁<VAR>W₁ : CategoryTheory.MorphismProperty C₁<VAR>C₂ : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} C₂<VAR>W₂ : CategoryTheory.MorphismProperty C₂<VAR>Φ : CategoryTheory.LocalizerMorphism W₁ W₂<VAR>X Y Z : C₁<VAR>CategoryTheory.Localization.HasSmallLocalizedHom W₁ X Y<VAR>CategoryTheory.Localization.HasSmallLocalizedHom W₁ Y Z<VAR>CategoryTheory.Localization.HasSmallLocalizedHom W₁ X Z<VAR>CategoryTheory.Localization.HasSmallLocalizedHom W₂ (Φ.functor.obj X) (Φ.functor.obj Y)<VAR>CategoryTheory.Localization.HasSmallLocalizedHom W₂ (Φ.functor.obj Y) (Φ.functor.obj Z)<VAR>CategoryTheory.Localization.HasSmallLocalizedHom W₂ (Φ.functor.obj X) (Φ.functor.obj Z)<VAR>f : CategoryTheory.Localization.SmallHom W₁ X Y<VAR>g : CategoryTheory.Localization.SmallHom W₁ Y Z<GOAL>Φ.smallHomMap (f.comp g) = (Φ.smallHomMap f).comp (Φ.smallHomMap g)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>P : C → Prop<VAR>A : Type u_2<VAR>AddMonoid A<VAR>CategoryTheory.HasShift C A<VAR>a : A<VAR>X : C<GOAL>CategoryTheory.PredicateShift P a X ↔ P ((CategoryTheory.shiftFunctor C a).obj X)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>P : C → Prop<VAR>A : Type u_2<VAR>AddMonoid A<VAR>CategoryTheory.HasShift C A<VAR>CategoryTheory.ClosedUnderIsomorphisms P<GOAL>CategoryTheory.PredicateShift P 0 = P
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>P : C → Prop<VAR>A : Type u_2<VAR>AddMonoid A<VAR>CategoryTheory.HasShift C A<VAR>a b c : A<VAR>h : a + b = c<VAR>CategoryTheory.ClosedUnderIsomorphisms P<GOAL>CategoryTheory.PredicateShift (CategoryTheory.PredicateShift P b) a = CategoryTheory.PredicateShift P c
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Preadditive C<VAR>M N : CategoryTheory.Mat_ C<VAR>f g : M ⟶ N<VAR>H : ∀ (i : M.ι) (j : N.ι), f i j = g i j<GOAL>f = g
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Preadditive C<VAR>M : CategoryTheory.Mat_ C<GOAL>𝟙 M = fun i j => if h : i = j then CategoryTheory.eqToHom ⋯ else 0
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Preadditive C<VAR>M : CategoryTheory.Mat_ C<VAR>i j : M.ι<GOAL>𝟙 M i j = if h : i = j then CategoryTheory.eqToHom ⋯ else 0
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Preadditive C<VAR>M : CategoryTheory.Mat_ C<VAR>i : M.ι<GOAL>𝟙 M i i = 𝟙 (M.X i)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Preadditive C<VAR>M : CategoryTheory.Mat_ C<VAR>i j : M.ι<VAR>h : i ≠ j<GOAL>𝟙 M i j = 0
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Preadditive C<VAR>M N K : CategoryTheory.Mat_ C<VAR>f : M ⟶ N<VAR>g : N ⟶ K<GOAL>f ≫ g = fun i k => ∑ j : N.ι, f i j ≫ g j k
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Preadditive C<VAR>M N K : CategoryTheory.Mat_ C<VAR>f : M ⟶ N<VAR>g : N ⟶ K<VAR>i : M.ι<VAR>k : K.ι<GOAL>(f ≫ g) i k = ∑ j : N.ι, f i j ≫ g j k
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Preadditive C<VAR>M N : CategoryTheory.Mat_ C<VAR>f g : M ⟶ N<VAR>i : M.ι<VAR>j : N.ι<GOAL>(f + g) i j = f i j + g i j
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Preadditive C<VAR>D : Type u_1<VAR>CategoryTheory.Category.{v₁, u_1} D<VAR>CategoryTheory.Preadditive D<VAR>F : C ⥤ D<VAR>F.Additive<VAR>M : CategoryTheory.Mat_ C<GOAL>(F.mapMat_.obj M).ι = M.ι
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Preadditive C<VAR>D : Type u_1<VAR>CategoryTheory.Category.{v₁, u_1} D<VAR>CategoryTheory.Preadditive D<VAR>F : C ⥤ D<VAR>F.Additive<GOAL>∀ {X Y : CategoryTheory.Mat_ C} (f : X ⟶ Y) (i : ((fun M => CategoryTheory.Mat_.mk M.ι fun i => F.obj (M.X i)) X).ι) (j : ((fun M => CategoryTheory.Mat_.mk M.ι fun i => F.obj (M.X i)) Y).ι), F.mapMat_.map f i j = F.map (f i j)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Preadditive C<VAR>D : Type u_1<VAR>CategoryTheory.Category.{v₁, u_1} D<VAR>CategoryTheory.Preadditive D<VAR>F : C ⥤ D<VAR>F.Additive<VAR>M : CategoryTheory.Mat_ C<GOAL>(F.mapMat_.obj M).fintype = M.fintype
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Preadditive C<VAR>D : Type u_1<VAR>CategoryTheory.Category.{v₁, u_1} D<VAR>CategoryTheory.Preadditive D<VAR>F : C ⥤ D<VAR>F.Additive<VAR>M : CategoryTheory.Mat_ C<VAR>i : M.ι<GOAL>(F.mapMat_.obj M).X i = F.obj (M.X i)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Preadditive C<VAR>X : CategoryTheory.Mat_ C<GOAL>CategoryTheory.Functor.mapMatId.inv.app X = 𝟙 ((𝟭 C).mapMat_.obj X)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Preadditive C<VAR>X : CategoryTheory.Mat_ C<GOAL>CategoryTheory.Functor.mapMatId.hom.app X = 𝟙 ((𝟭 C).mapMat_.obj X)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Preadditive C<VAR>D : Type u_1<VAR>CategoryTheory.Category.{v₁, u_1} D<VAR>CategoryTheory.Preadditive D<VAR>E : Type u_2<VAR>CategoryTheory.Category.{v₁, u_2} E<VAR>CategoryTheory.Preadditive E<VAR>F : C ⥤ D<VAR>F.Additive<VAR>G : D ⥤ E<VAR>G.Additive<VAR>X : CategoryTheory.Mat_ C<GOAL>(F.mapMatComp G).inv.app X = 𝟙 ((F ⋙ G).mapMat_.obj X)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Preadditive C<VAR>D : Type u_1<VAR>CategoryTheory.Category.{v₁, u_1} D<VAR>CategoryTheory.Preadditive D<VAR>E : Type u_2<VAR>CategoryTheory.Category.{v₁, u_2} E<VAR>CategoryTheory.Preadditive E<VAR>F : C ⥤ D<VAR>F.Additive<VAR>G : D ⥤ E<VAR>G.Additive<VAR>X : CategoryTheory.Mat_ C<GOAL>(F.mapMatComp G).hom.app X = 𝟙 ((F ⋙ G).mapMat_.obj X)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Preadditive C<VAR>X : C<GOAL>((CategoryTheory.Mat_.embedding C).obj X).fintype = PUnit.fintype
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Preadditive C<GOAL>∀ {X Y : C} (f : X ⟶ Y) (x : ((fun X => CategoryTheory.Mat_.mk PUnit.{1} fun x => X) X).ι) (x_1 : ((fun X => CategoryTheory.Mat_.mk PUnit.{1} fun x => X) Y).ι), (CategoryTheory.Mat_.embedding C).map f x x_1 = f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Preadditive C<VAR>X : C<GOAL>∀ (x : PUnit.{1}), ((CategoryTheory.Mat_.embedding C).obj X).X x = X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Preadditive C<VAR>X : C<GOAL>((CategoryTheory.Mat_.embedding C).obj X).ι = PUnit.{1}
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Preadditive C<VAR>M : CategoryTheory.Mat_ C<GOAL>M.isoBiproductEmbedding.hom = CategoryTheory.Limits.biproduct.lift fun i j k => if h : j = i then CategoryTheory.eqToHom ⋯ else 0