ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<VAR>F : CategoryTheory.MonoidalFunctor C D<VAR>G : CategoryTheory.Functor D C<VAR>adj : F.toFunctor ⊣ G<VAR>F.IsEquivalence<VAR>CategoryTheory.MonoidalClosed D<VAR>X Y Z : C<VAR>f : CategoryTheory.MonoidalCategory.tensorObj X Y ⟶ Z<GOAL>CategoryTheory.MonoidalClosed.curry f = (adj.homEquiv Y ((CategoryTheory.ihom (F.obj X)).obj (F.obj Z))) (CategoryTheory.MonoidalClosed.curry ((adj.toEquivalence.symm.toAdjunction.homEquiv (CategoryTheory.MonoidalCategory.tensorObj (F.obj X) (F.obj Y)) Z) (CategoryTheory.CategoryStruct.comp ((F.commTensorLeft X).compInverseIso.hom.app Y) f)))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<VAR>F : CategoryTheory.MonoidalFunctor C D<VAR>G : CategoryTheory.Functor D C<VAR>adj : F.toFunctor ⊣ G<VAR>F.IsEquivalence<VAR>CategoryTheory.MonoidalClosed D<VAR>X Y Z : C<VAR>f : Y ⟶ (CategoryTheory.ihom X).obj Z<GOAL>CategoryTheory.MonoidalClosed.uncurry f = CategoryTheory.CategoryStruct.comp ((F.commTensorLeft X).compInverseIso.inv.app Y) ((adj.toEquivalence.symm.toAdjunction.homEquiv ((F.comp (CategoryTheory.MonoidalCategory.tensorLeft (F.obj X))).obj Y) Z).symm (CategoryTheory.MonoidalClosed.uncurry ((adj.homEquiv Y ((CategoryTheory.ihom (F.obj X)).obj (adj.toEquivalence.symm.inverse.obj Z))).symm f)))
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : C<VAR>p : CategoryTheory.Subobject X → Prop<VAR>h : ∀ ⦃A : C⦄ (f : A ⟶ X) [inst : CategoryTheory.Mono f], p (CategoryTheory.Subobject.mk f)<VAR>P : CategoryTheory.Subobject X<GOAL>p P
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : C<VAR>p : CategoryTheory.Subobject X → CategoryTheory.Subobject X → Prop<VAR>h : ∀ ⦃A B : C⦄ (f : A ⟶ X) (g : B ⟶ X) [inst : CategoryTheory.Mono f] [inst_1 : CategoryTheory.Mono g], p (CategoryTheory.Subobject.mk f) (CategoryTheory.Subobject.mk g)<VAR>P Q : CategoryTheory.Subobject X<GOAL>p P Q
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>α : Sort u_1<VAR>X : C<VAR>F : ⦃A : C⦄ → (f : A ⟶ X) → [inst : CategoryTheory.Mono f] → α<VAR>h : ∀ ⦃A B : C⦄ (f : A ⟶ X) (g : B ⟶ X) [inst : CategoryTheory.Mono f] [inst_1 : CategoryTheory.Mono g] (i : A ≅ B), CategoryTheory.CategoryStruct.comp i.hom g = f → F f = F g<VAR>A : C<VAR>f : A ⟶ X<VAR>CategoryTheory.Mono f<GOAL>CategoryTheory.Subobject.lift F h (CategoryTheory.Subobject.mk f) = F f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>A : C<VAR>X Y : CategoryTheory.Subobject A<VAR>h : X = Y<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) Y.arrow = X.arrow
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : C<VAR>Y : CategoryTheory.Subobject X<GOAL>(CategoryTheory.Subobject.representative.obj Y).obj.left = CategoryTheory.Subobject.underlying.obj Y
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : C<VAR>Y : CategoryTheory.Subobject X<GOAL>(CategoryTheory.Subobject.representative.obj Y).arrow = Y.arrow
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : C<VAR>Y Z : CategoryTheory.Subobject X<VAR>f : Y ⟶ Z<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Subobject.underlying.map f) Z.arrow = Y.arrow
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Mono f<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Subobject.underlyingIso f).inv (CategoryTheory.Subobject.mk f).arrow = f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Mono f<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Subobject.underlyingIso f).hom f = (CategoryTheory.Subobject.mk f).arrow
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<VAR>P : CategoryTheory.Subobject Y<VAR>f g : X ⟶ CategoryTheory.Subobject.underlying.obj P<VAR>h : CategoryTheory.CategoryStruct.comp f P.arrow = CategoryTheory.CategoryStruct.comp g P.arrow<GOAL>f = g
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>B A₁ A₂ : C<VAR>f₁ : A₁ ⟶ B<VAR>f₂ : A₂ ⟶ B<VAR>CategoryTheory.Mono f₁<VAR>CategoryTheory.Mono f₂<VAR>g : A₁ ⟶ A₂<VAR>w : CategoryTheory.CategoryStruct.comp g f₂ = f₁<GOAL>CategoryTheory.Subobject.mk f₁ ≤ CategoryTheory.Subobject.mk f₂
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : C<VAR>P : CategoryTheory.Subobject X<GOAL>CategoryTheory.Subobject.mk P.arrow = P
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>B : C<VAR>X Y : CategoryTheory.Subobject B<VAR>f : CategoryTheory.Subobject.underlying.obj X ⟶ CategoryTheory.Subobject.underlying.obj Y<VAR>w : CategoryTheory.CategoryStruct.comp f Y.arrow = X.arrow<GOAL>X ≤ Y
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>B A : C<VAR>X : CategoryTheory.Subobject B<VAR>f : A ⟶ B<VAR>CategoryTheory.Mono f<VAR>g : CategoryTheory.Subobject.underlying.obj X ⟶ A<VAR>w : CategoryTheory.CategoryStruct.comp g f = X.arrow<GOAL>X ≤ CategoryTheory.Subobject.mk f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>B A : C<VAR>X : CategoryTheory.Subobject B<VAR>f : A ⟶ B<VAR>CategoryTheory.Mono f<VAR>g : A ⟶ CategoryTheory.Subobject.underlying.obj X<VAR>w : CategoryTheory.CategoryStruct.comp g X.arrow = f<GOAL>CategoryTheory.Subobject.mk f ≤ X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>B : C<VAR>X Y : CategoryTheory.Subobject B<VAR>f : CategoryTheory.Subobject.underlying.obj X ≅ CategoryTheory.Subobject.underlying.obj Y<VAR>w : CategoryTheory.CategoryStruct.comp f.hom Y.arrow = X.arrow<GOAL>X = Y
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>B A : C<VAR>X : CategoryTheory.Subobject B<VAR>f : A ⟶ B<VAR>CategoryTheory.Mono f<VAR>i : CategoryTheory.Subobject.underlying.obj X ≅ A<VAR>w : CategoryTheory.CategoryStruct.comp i.hom f = X.arrow<GOAL>X = CategoryTheory.Subobject.mk f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>B A : C<VAR>X : CategoryTheory.Subobject B<VAR>f : A ⟶ B<VAR>CategoryTheory.Mono f<VAR>i : A ≅ CategoryTheory.Subobject.underlying.obj X<VAR>w : CategoryTheory.CategoryStruct.comp i.hom X.arrow = f<GOAL>CategoryTheory.Subobject.mk f = X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>B A₁ A₂ : C<VAR>f : A₁ ⟶ B<VAR>g : A₂ ⟶ B<VAR>CategoryTheory.Mono f<VAR>CategoryTheory.Mono g<VAR>i : A₁ ≅ A₂<VAR>w : CategoryTheory.CategoryStruct.comp i.hom g = f<GOAL>CategoryTheory.Subobject.mk f = CategoryTheory.Subobject.mk g
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>B : C<VAR>X Y : CategoryTheory.Subobject B<VAR>h : X ≤ Y<GOAL>CategoryTheory.CategoryStruct.comp (X.ofLE Y h) Y.arrow = X.arrow
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>B A₁ A₂ : C<VAR>f₁ : A₁ ⟶ B<VAR>f₂ : A₂ ⟶ B<VAR>CategoryTheory.Mono f₁<VAR>CategoryTheory.Mono f₂<VAR>g : A₁ ⟶ A₂<VAR>w : CategoryTheory.CategoryStruct.comp g f₂ = f₁<GOAL>(CategoryTheory.Subobject.mk f₁).ofLE (CategoryTheory.Subobject.mk f₂) ⋯ = CategoryTheory.CategoryStruct.comp (CategoryTheory.Subobject.underlyingIso f₁).hom (CategoryTheory.CategoryStruct.comp g (CategoryTheory.Subobject.underlyingIso f₂).inv)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>B A : C<VAR>X : CategoryTheory.Subobject B<VAR>f : A ⟶ B<VAR>CategoryTheory.Mono f<VAR>h : X ≤ CategoryTheory.Subobject.mk f<GOAL>CategoryTheory.CategoryStruct.comp (X.ofLEMk f h) f = X.arrow
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>B A : C<VAR>f : A ⟶ B<VAR>CategoryTheory.Mono f<VAR>X : CategoryTheory.Subobject B<VAR>h : CategoryTheory.Subobject.mk f ≤ X<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Subobject.ofMkLE f X h) X.arrow = f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>B A₁ A₂ : C<VAR>f : A₁ ⟶ B<VAR>g : A₂ ⟶ B<VAR>CategoryTheory.Mono f<VAR>CategoryTheory.Mono g<VAR>h : CategoryTheory.Subobject.mk f ≤ CategoryTheory.Subobject.mk g<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Subobject.ofMkLEMk f g h) g = f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>B : C<VAR>X Y Z : CategoryTheory.Subobject B<VAR>h₁ : X ≤ Y<VAR>h₂ : Y ≤ Z<GOAL>CategoryTheory.CategoryStruct.comp (X.ofLE Y h₁) (Y.ofLE Z h₂) = X.ofLE Z ⋯
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>B A : C<VAR>X Y : CategoryTheory.Subobject B<VAR>f : A ⟶ B<VAR>CategoryTheory.Mono f<VAR>h₁ : X ≤ Y<VAR>h₂ : Y ≤ CategoryTheory.Subobject.mk f<GOAL>CategoryTheory.CategoryStruct.comp (X.ofLE Y h₁) (Y.ofLEMk f h₂) = X.ofLEMk f ⋯
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>B A : C<VAR>X : CategoryTheory.Subobject B<VAR>f : A ⟶ B<VAR>CategoryTheory.Mono f<VAR>Y : CategoryTheory.Subobject B<VAR>h₁ : X ≤ CategoryTheory.Subobject.mk f<VAR>h₂ : CategoryTheory.Subobject.mk f ≤ Y<GOAL>CategoryTheory.CategoryStruct.comp (X.ofLEMk f h₁) (CategoryTheory.Subobject.ofMkLE f Y h₂) = X.ofLE Y ⋯
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>B A₁ A₂ : C<VAR>X : CategoryTheory.Subobject B<VAR>f : A₁ ⟶ B<VAR>CategoryTheory.Mono f<VAR>g : A₂ ⟶ B<VAR>CategoryTheory.Mono g<VAR>h₁ : X ≤ CategoryTheory.Subobject.mk f<VAR>h₂ : CategoryTheory.Subobject.mk f ≤ CategoryTheory.Subobject.mk g<GOAL>CategoryTheory.CategoryStruct.comp (X.ofLEMk f h₁) (CategoryTheory.Subobject.ofMkLEMk f g h₂) = X.ofLEMk g ⋯
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>B A₁ : C<VAR>f : A₁ ⟶ B<VAR>CategoryTheory.Mono f<VAR>X Y : CategoryTheory.Subobject B<VAR>h₁ : CategoryTheory.Subobject.mk f ≤ X<VAR>h₂ : X ≤ Y<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Subobject.ofMkLE f X h₁) (X.ofLE Y h₂) = CategoryTheory.Subobject.ofMkLE f Y ⋯
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>B A₁ A₂ : C<VAR>f : A₁ ⟶ B<VAR>CategoryTheory.Mono f<VAR>X : CategoryTheory.Subobject B<VAR>g : A₂ ⟶ B<VAR>CategoryTheory.Mono g<VAR>h₁ : CategoryTheory.Subobject.mk f ≤ X<VAR>h₂ : X ≤ CategoryTheory.Subobject.mk g<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Subobject.ofMkLE f X h₁) (X.ofLEMk g h₂) = CategoryTheory.Subobject.ofMkLEMk f g ⋯
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>B A₁ A₂ : C<VAR>f : A₁ ⟶ B<VAR>CategoryTheory.Mono f<VAR>g : A₂ ⟶ B<VAR>CategoryTheory.Mono g<VAR>X : CategoryTheory.Subobject B<VAR>h₁ : CategoryTheory.Subobject.mk f ≤ CategoryTheory.Subobject.mk g<VAR>h₂ : CategoryTheory.Subobject.mk g ≤ X<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Subobject.ofMkLEMk f g h₁) (CategoryTheory.Subobject.ofMkLE g X h₂) = CategoryTheory.Subobject.ofMkLE f X ⋯
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>B A₁ A₂ A₃ : C<VAR>f : A₁ ⟶ B<VAR>CategoryTheory.Mono f<VAR>g : A₂ ⟶ B<VAR>CategoryTheory.Mono g<VAR>h : A₃ ⟶ B<VAR>CategoryTheory.Mono h<VAR>h₁ : CategoryTheory.Subobject.mk f ≤ CategoryTheory.Subobject.mk g<VAR>h₂ : CategoryTheory.Subobject.mk g ≤ CategoryTheory.Subobject.mk h<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Subobject.ofMkLEMk f g h₁) (CategoryTheory.Subobject.ofMkLEMk g h h₂) = CategoryTheory.Subobject.ofMkLEMk f h ⋯
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>B : C<VAR>X : CategoryTheory.Subobject B<GOAL>X.ofLE X ⋯ = CategoryTheory.CategoryStruct.id (CategoryTheory.Subobject.underlying.obj X)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>B A₁ : C<VAR>f : A₁ ⟶ B<VAR>CategoryTheory.Mono f<GOAL>CategoryTheory.Subobject.ofMkLEMk f f ⋯ = CategoryTheory.CategoryStruct.id A₁
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>B : C<VAR>X Y : CategoryTheory.Subobject B<VAR>h : X = Y<GOAL>(X.isoOfEq Y h).hom = X.ofLE Y ⋯
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>B : C<VAR>X Y : CategoryTheory.Subobject B<VAR>h : X = Y<GOAL>(X.isoOfEq Y h).inv = Y.ofLE X ⋯
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>B A : C<VAR>X : CategoryTheory.Subobject B<VAR>f : A ⟶ B<VAR>CategoryTheory.Mono f<VAR>h : X = CategoryTheory.Subobject.mk f<GOAL>(X.isoOfEqMk f h).inv = CategoryTheory.Subobject.ofMkLE f X ⋯
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>B A : C<VAR>X : CategoryTheory.Subobject B<VAR>f : A ⟶ B<VAR>CategoryTheory.Mono f<VAR>h : X = CategoryTheory.Subobject.mk f<GOAL>(X.isoOfEqMk f h).hom = X.ofLEMk f ⋯
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>B A : C<VAR>f : A ⟶ B<VAR>CategoryTheory.Mono f<VAR>X : CategoryTheory.Subobject B<VAR>h : CategoryTheory.Subobject.mk f = X<GOAL>(CategoryTheory.Subobject.isoOfMkEq f X h).hom = CategoryTheory.Subobject.ofMkLE f X ⋯
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>B A : C<VAR>f : A ⟶ B<VAR>CategoryTheory.Mono f<VAR>X : CategoryTheory.Subobject B<VAR>h : CategoryTheory.Subobject.mk f = X<GOAL>(CategoryTheory.Subobject.isoOfMkEq f X h).inv = X.ofLEMk f ⋯
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>B A₁ A₂ : C<VAR>f : A₁ ⟶ B<VAR>g : A₂ ⟶ B<VAR>CategoryTheory.Mono f<VAR>CategoryTheory.Mono g<VAR>h : CategoryTheory.Subobject.mk f = CategoryTheory.Subobject.mk g<GOAL>(CategoryTheory.Subobject.isoOfMkEqMk f g h).inv = CategoryTheory.Subobject.ofMkLEMk g f ⋯
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>B A₁ A₂ : C<VAR>f : A₁ ⟶ B<VAR>g : A₂ ⟶ B<VAR>CategoryTheory.Mono f<VAR>CategoryTheory.Mono g<VAR>h : CategoryTheory.Subobject.mk f = CategoryTheory.Subobject.mk g<GOAL>(CategoryTheory.Subobject.isoOfMkEqMk f g h).hom = CategoryTheory.Subobject.ofMkLEMk f g ⋯
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<VAR>F₁ F₂ : CategoryTheory.Functor (CategoryTheory.MonoOver X) (CategoryTheory.MonoOver Y)<VAR>h : F₁ ≅ F₂<GOAL>CategoryTheory.Subobject.lower F₁ = CategoryTheory.Subobject.lower F₂
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<VAR>F : CategoryTheory.Functor (CategoryTheory.MonoOver Y) (CategoryTheory.MonoOver X)<GOAL>(CategoryTheory.toThinSkeleton (CategoryTheory.MonoOver Y)).comp (CategoryTheory.Subobject.lower F) = F.comp (CategoryTheory.toThinSkeleton (CategoryTheory.MonoOver X))
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>A : C<VAR>B : D<VAR>e : CategoryTheory.MonoOver A ≌ CategoryTheory.MonoOver B<GOAL>(CategoryTheory.Subobject.lowerEquivalence e).inverse = CategoryTheory.Subobject.lower e.inverse
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>A : C<VAR>B : D<VAR>e : CategoryTheory.MonoOver A ≌ CategoryTheory.MonoOver B<GOAL>(CategoryTheory.Subobject.lowerEquivalence e).unitIso = CategoryTheory.eqToIso ⋯
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>A : C<VAR>B : D<VAR>e : CategoryTheory.MonoOver A ≌ CategoryTheory.MonoOver B<GOAL>(CategoryTheory.Subobject.lowerEquivalence e).counitIso = CategoryTheory.eqToIso ⋯
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>A : C<VAR>B : D<VAR>e : CategoryTheory.MonoOver A ≌ CategoryTheory.MonoOver B<GOAL>(CategoryTheory.Subobject.lowerEquivalence e).functor = CategoryTheory.Subobject.lower e.functor
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>x : CategoryTheory.Subobject X<GOAL>(CategoryTheory.Subobject.pullback (CategoryTheory.CategoryStruct.id X)).obj x = x
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y Z : C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>x : CategoryTheory.Subobject Z<GOAL>(CategoryTheory.Subobject.pullback (CategoryTheory.CategoryStruct.comp f g)).obj x = (CategoryTheory.Subobject.pullback f).obj ((CategoryTheory.Subobject.pullback g).obj x)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : C<VAR>x : CategoryTheory.Subobject X<GOAL>(CategoryTheory.Subobject.map (CategoryTheory.CategoryStruct.id X)).obj x = x
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>CategoryTheory.Mono f<VAR>CategoryTheory.Mono g<VAR>x : CategoryTheory.Subobject X<GOAL>(CategoryTheory.Subobject.map (CategoryTheory.CategoryStruct.comp f g)).obj x = (CategoryTheory.Subobject.map g).obj ((CategoryTheory.Subobject.map f).obj x)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<VAR>e : X ≅ Y<VAR>P : CategoryTheory.Subobject X<GOAL>(CategoryTheory.Subobject.mapIsoToOrderIso e) P = (CategoryTheory.Subobject.map e.hom).obj P
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<VAR>e : X ≅ Y<VAR>Q : CategoryTheory.Subobject Y<GOAL>(CategoryTheory.Subobject.mapIsoToOrderIso e).symm Q = (CategoryTheory.Subobject.map e.inv).obj Q
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Mono f<VAR>g : CategoryTheory.Subobject X<GOAL>(CategoryTheory.Subobject.pullback f).obj ((CategoryTheory.Subobject.map f).obj g) = g
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>X Y Z W : C<VAR>f : X ⟶ Y<VAR>g : X ⟶ Z<VAR>h : Y ⟶ W<VAR>k : Z ⟶ W<VAR>CategoryTheory.Mono h<VAR>CategoryTheory.Mono g<VAR>comm : CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g k<VAR>t : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.PullbackCone.mk f g comm)<VAR>p : CategoryTheory.Subobject Y<GOAL>(CategoryTheory.Subobject.map g).obj ((CategoryTheory.Subobject.pullback f).obj p) = (CategoryTheory.Subobject.pullback k).obj ((CategoryTheory.Subobject.map h).obj p)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasImages C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Mono f<GOAL>CategoryTheory.Subobject.exists f = CategoryTheory.Subobject.map f
<VAR>α : Type u<VAR>s : Set α<GOAL>CategoryTheory.Mono (↾Subtype.val)
<VAR>α : Type u<VAR>s : Set α<GOAL>(Types.monoOverEquivalenceSet α).inverse.obj s = CategoryTheory.MonoOver.mk' Subtype.val
<VAR>α : Type u<VAR>f g : CategoryTheory.MonoOver α<VAR>t : f ⟶ g<GOAL>(Types.monoOverEquivalenceSet α).functor.map t = CategoryTheory.homOfLE ⋯
<VAR>α : Type u<VAR>s t : Set α<VAR>b : s ⟶ t<GOAL>(Types.monoOverEquivalenceSet α).inverse.map b = CategoryTheory.MonoOver.homMk (fun w => ⟨↑w, ⋯⟩) ⋯
<VAR>α : Type u<GOAL>(Types.monoOverEquivalenceSet α).counitIso = CategoryTheory.NatIso.ofComponents (fun s => CategoryTheory.eqToIso ⋯) ⋯
<VAR>α : Type u<GOAL>(Types.monoOverEquivalenceSet α).unitIso = CategoryTheory.NatIso.ofComponents (fun f => CategoryTheory.MonoOver.isoMk (Equiv.ofInjective f.obj.hom ⋯).toIso ⋯) ⋯
<VAR>α : Type u<VAR>f : CategoryTheory.MonoOver α<GOAL>(Types.monoOverEquivalenceSet α).functor.obj f = Set.range f.obj.hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>CategoryTheory.Limits.HasEqualizer f g<GOAL>(CategoryTheory.Limits.equalizerSubobjectIso f g).hom ≫ CategoryTheory.Limits.equalizer.ι f g = (CategoryTheory.Limits.equalizerSubobject f g).arrow
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>CategoryTheory.Limits.HasEqualizer f g<GOAL>(CategoryTheory.Limits.equalizerSubobjectIso f g).inv ≫ (CategoryTheory.Limits.equalizerSubobject f g).arrow = CategoryTheory.Limits.equalizer.ι f g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>CategoryTheory.Limits.HasEqualizer f g<GOAL>(CategoryTheory.Limits.equalizerSubobject f g).arrow ≫ f = (CategoryTheory.Limits.equalizerSubobject f g).arrow ≫ g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>CategoryTheory.Limits.HasEqualizer f g<VAR>W : C<VAR>h : W ⟶ X<VAR>w : h ≫ f = h ≫ g<GOAL>(CategoryTheory.Limits.equalizerSubobject f g).Factors h
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>CategoryTheory.Limits.HasEqualizer f g<VAR>W : C<VAR>h : W ⟶ X<GOAL>(CategoryTheory.Limits.equalizerSubobject f g).Factors h ↔ h ≫ f = h ≫ g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Limits.HasKernel f<GOAL>(CategoryTheory.Limits.kernelSubobjectIso f).hom ≫ CategoryTheory.Limits.kernel.ι f = (CategoryTheory.Limits.kernelSubobject f).arrow
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Limits.HasKernel f<GOAL>(CategoryTheory.Limits.kernelSubobjectIso f).inv ≫ (CategoryTheory.Limits.kernelSubobject f).arrow = CategoryTheory.Limits.kernel.ι f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Limits.HasKernel f<GOAL>(CategoryTheory.Limits.kernelSubobject f).arrow ≫ f = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Limits.HasKernel f<VAR>W : C<VAR>h : W ⟶ X<VAR>w : h ≫ f = 0<GOAL>(CategoryTheory.Limits.kernelSubobject f).Factors h
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Limits.HasKernel f<VAR>W : C<VAR>h : W ⟶ X<GOAL>(CategoryTheory.Limits.kernelSubobject f).Factors h ↔ h ≫ f = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Limits.HasKernel f<VAR>W : C<VAR>h : W ⟶ X<VAR>w : h ≫ f = 0<GOAL>CategoryTheory.Limits.factorThruKernelSubobject f h w ≫ (CategoryTheory.Limits.kernelSubobject f).arrow = h
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Limits.HasKernel f<VAR>W : C<VAR>h : W ⟶ X<VAR>w : h ≫ f = 0<GOAL>CategoryTheory.Limits.factorThruKernelSubobject f h w ≫ (CategoryTheory.Limits.kernelSubobjectIso f).hom = CategoryTheory.Limits.kernel.lift f h w
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Limits.HasKernel f<VAR>X' Y' : C<VAR>f' : X' ⟶ Y'<VAR>CategoryTheory.Limits.HasKernel f'<VAR>sq : CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk f'<GOAL>CategoryTheory.Limits.kernelSubobjectMap sq ≫ (CategoryTheory.Limits.kernelSubobject f').arrow = (CategoryTheory.Limits.kernelSubobject f).arrow ≫ sq.left
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Limits.HasKernel f<GOAL>CategoryTheory.Limits.kernelSubobjectMap (𝟙 (CategoryTheory.Arrow.mk f)) = 𝟙 (CategoryTheory.Subobject.underlying.obj (CategoryTheory.Limits.kernelSubobject f))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Limits.HasKernel f<VAR>X' Y' : C<VAR>f' : X' ⟶ Y'<VAR>CategoryTheory.Limits.HasKernel f'<VAR>X'' Y'' : C<VAR>f'' : X'' ⟶ Y''<VAR>CategoryTheory.Limits.HasKernel f''<VAR>sq : CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk f'<VAR>sq' : CategoryTheory.Arrow.mk f' ⟶ CategoryTheory.Arrow.mk f''<GOAL>CategoryTheory.Limits.kernelSubobjectMap (sq ≫ sq') = CategoryTheory.Limits.kernelSubobjectMap sq ≫ CategoryTheory.Limits.kernelSubobjectMap sq'
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Limits.HasKernel f<VAR>X' Y' : C<VAR>f' : X' ⟶ Y'<VAR>CategoryTheory.Limits.HasKernel f'<VAR>sq : CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk f'<GOAL>CategoryTheory.Limits.kernel.map f f' sq.left sq.right ⋯ ≫ (CategoryTheory.Limits.kernelSubobjectIso f').inv = (CategoryTheory.Limits.kernelSubobjectIso f).inv ≫ CategoryTheory.Limits.kernelSubobjectMap sq