ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>self : CategoryTheory.Functor C D<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>self.map (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (self.map f) (self.map g)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>self : CategoryTheory.Functor C D<VAR>X : C<GOAL>self.map (CategoryTheory.CategoryStruct.id X) = CategoryTheory.CategoryStruct.id (self.obj X)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{u_1, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{u_2, u₂} D<VAR>F : CategoryTheory.Functor C D<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>W : D<VAR>h : F.obj Z ⟶ W<GOAL>CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.CategoryStruct.comp f g)) h = CategoryTheory.CategoryStruct.comp (F.map f) (CategoryTheory.CategoryStruct.comp (F.map g) h)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : C<GOAL>(CategoryTheory.Functor.id C).obj X = X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>(CategoryTheory.Functor.id C).map f = f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>F : CategoryTheory.Functor C D<VAR>G : CategoryTheory.Functor D E<VAR>X : C<GOAL>(F.comp G).obj X = G.obj (F.obj X)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>F : CategoryTheory.Functor C D<VAR>G : CategoryTheory.Functor D E<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>(F.comp G).map f = G.map (F.map f)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : CategoryTheory.Functor C D<GOAL>F.comp (CategoryTheory.Functor.id D) = F
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : CategoryTheory.Functor C D<GOAL>(CategoryTheory.Functor.id C).comp F = F
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : CategoryTheory.Functor C D<VAR>X Y : C<VAR>P : Prop<VAR>Decidable P<VAR>f : P → (X ⟶ Y)<VAR>g : ¬P → (X ⟶ Y)<GOAL>F.map (if h : P then f h else g h) = if h : P then F.map (f h) else F.map (g h)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>F : CategoryTheory.Functor C D<VAR>G : CategoryTheory.Functor D E<GOAL>F.toPrefunctor ⋙q G.toPrefunctor = (F.comp G).toPrefunctor
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : C → D<VAR>self : CategoryTheory.Functorial F<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>CategoryTheory.Functorial.map' (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functorial.map' f) (CategoryTheory.Functorial.map' g)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : C → D<VAR>self : CategoryTheory.Functorial F<VAR>X : C<GOAL>CategoryTheory.Functorial.map' (CategoryTheory.CategoryStruct.id X) = CategoryTheory.CategoryStruct.id (F X)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : C → D<VAR>CategoryTheory.Functorial F<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>CategoryTheory.Functorial.map' f = CategoryTheory.map F f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : C → D<VAR>CategoryTheory.Functorial F<VAR>X : C<GOAL>CategoryTheory.map F (CategoryTheory.CategoryStruct.id X) = CategoryTheory.CategoryStruct.id (F X)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : C → D<VAR>CategoryTheory.Functorial F<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>CategoryTheory.map F (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (CategoryTheory.map F f) (CategoryTheory.map F g)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : CategoryTheory.Functor C D<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>CategoryTheory.map F.obj f = F.map f
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} C<VAR>X : C<GOAL>∀ (x : J), ((CategoryTheory.Functor.const J).obj X).obj x = X
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} C<GOAL>∀ {X Y : C} (f : X ⟶ Y) (x : J), ((CategoryTheory.Functor.const J).map f).app x = f
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} C<VAR>X : C<GOAL>∀ {X_1 Y : J} (x : X_1 ⟶ Y), ((CategoryTheory.Functor.const J).obj X).map x = 𝟙 X
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} C<VAR>X : C<VAR>j : Jᵒᵖ<GOAL>(CategoryTheory.Functor.const.opObjOp X).inv.app j = 𝟙 (((CategoryTheory.Functor.const J).obj X).op.obj j)
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} C<VAR>X : C<VAR>j : Jᵒᵖ<GOAL>(CategoryTheory.Functor.const.opObjOp X).hom.app j = 𝟙 (((CategoryTheory.Functor.const Jᵒᵖ).obj (Opposite.op X)).obj j)
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} C<VAR>X : Cᵒᵖ<VAR>j : Jᵒᵖ<GOAL>(CategoryTheory.Functor.const.opObjUnop X).hom.app j = 𝟙 (((CategoryTheory.Functor.const Jᵒᵖ).obj (Opposite.unop X)).obj j)
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} C<VAR>X : Cᵒᵖ<VAR>j : Jᵒᵖ<GOAL>(CategoryTheory.Functor.const.opObjUnop X).inv.app j = 𝟙 (((CategoryTheory.Functor.const J).obj X).leftOp.obj j)
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} C<VAR>X : Cᵒᵖ<VAR>j₁ j₂ : J<VAR>f : j₁ ⟶ j₂<GOAL>(Opposite.unop ((CategoryTheory.Functor.const J).op.obj X)).map f = 𝟙 (Opposite.unop X)
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} C<VAR>D : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} D<VAR>X : C<VAR>F : C ⥤ D<GOAL>∀ (x : J), (CategoryTheory.Functor.constComp J X F).inv.app x = 𝟙 (((CategoryTheory.Functor.const J).obj (F.obj X)).obj x)
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} C<VAR>D : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} D<VAR>X : C<VAR>F : C ⥤ D<GOAL>∀ (x : J), (CategoryTheory.Functor.constComp J X F).hom.app x = 𝟙 (((CategoryTheory.Functor.const J).obj X ⋙ F).obj x)
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} C<VAR>D : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} D<VAR>F : C ⥤ D<VAR>X : C<GOAL>∀ (X_1 : J), ((CategoryTheory.Functor.compConstIso J F).inv.app X).app X_1 = 𝟙 (F.obj X)
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} C<VAR>D : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} D<VAR>F : C ⥤ D<VAR>X : C<GOAL>∀ (X_1 : J), ((CategoryTheory.Functor.compConstIso J F).hom.app X).app X_1 = 𝟙 (F.obj X)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<GOAL>∀ {X Y : Cᵒᵖ × C} (f : X ⟶ Y) (h : Opposite.unop X.1 ⟶ X.2), (CategoryTheory.Functor.hom C).map f h = f.1.unop ≫ h ≫ f.2
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>p : Cᵒᵖ × C<GOAL>(CategoryTheory.Functor.hom C).obj p = (Opposite.unop p.1 ⟶ p.2)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X : ℕ → C<VAR>f : (n : ℕ) → X n ⟶ X (n + 1)<VAR>i j : ℕ<VAR>h : i = j<GOAL>f i = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (f j) (CategoryTheory.eqToHom ⋯))
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X : ℕ → C<VAR>f : (n : ℕ) → X n ⟶ X (n + 1)<VAR>i : ℕ<GOAL>CategoryTheory.Functor.OfSequence.map f i i ⋯ = CategoryTheory.CategoryStruct.id (X i)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X : ℕ → C<VAR>f : (n : ℕ) → X n ⟶ X (n + 1)<VAR>i : ℕ<GOAL>CategoryTheory.Functor.OfSequence.map f i (i + 1) ⋯ = f i
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X : ℕ → C<VAR>f : (n : ℕ) → X n ⟶ X (n + 1)<VAR>i j k : ℕ<VAR>hij : i ≤ j<VAR>hjk : j ≤ k<GOAL>CategoryTheory.Functor.OfSequence.map f i k ⋯ = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OfSequence.map f i j hij) (CategoryTheory.Functor.OfSequence.map f j k hjk)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X : ℕ → C<VAR>f : (n : ℕ) → X n ⟶ X (n + 1)<GOAL>∀ (a : ℕ), (CategoryTheory.Functor.ofSequence f).obj a = X a
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X : ℕ → C<VAR>f : (n : ℕ) → X n ⟶ X (n + 1)<VAR>n : ℕ<GOAL>(CategoryTheory.Functor.ofSequence f).map (CategoryTheory.homOfLE ⋯) = f n
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>F G : CategoryTheory.Functor ℕ C<VAR>app : (n : ℕ) → F.obj n ⟶ G.obj n<VAR>naturality : ∀ (n : ℕ), CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.homOfLE ⋯)) (app (n + 1)) = CategoryTheory.CategoryStruct.comp (app n) (G.map (CategoryTheory.homOfLE ⋯))<VAR>n : ℕ<GOAL>(CategoryTheory.NatTrans.ofSequence app naturality).app n = app n
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>self : F.PreservesMonomorphisms<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Mono f<GOAL>CategoryTheory.Mono (F.map f)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>self : F.PreservesEpimorphisms<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Epi f<GOAL>CategoryTheory.Epi (F.map f)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>self : F.ReflectsMonomorphisms<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>CategoryTheory.Mono (F.map f) → CategoryTheory.Mono f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>F.ReflectsMonomorphisms<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>h : CategoryTheory.Mono (F.map f)<GOAL>CategoryTheory.Mono f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>self : F.ReflectsEpimorphisms<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>CategoryTheory.Epi (F.map f) → CategoryTheory.Epi f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>F.ReflectsEpimorphisms<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>h : CategoryTheory.Epi (F.map f)<GOAL>CategoryTheory.Epi f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>F : C ⥤ D<VAR>G : D ⥤ E<VAR>(F ⋙ G).PreservesEpimorphisms<VAR>G.ReflectsEpimorphisms<GOAL>F.PreservesEpimorphisms
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>F : C ⥤ D<VAR>G : D ⥤ E<VAR>(F ⋙ G).PreservesMonomorphisms<VAR>G.ReflectsMonomorphisms<GOAL>F.PreservesMonomorphisms
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>F : C ⥤ D<VAR>G : D ⥤ E<VAR>G.PreservesEpimorphisms<VAR>(F ⋙ G).ReflectsEpimorphisms<GOAL>F.ReflectsEpimorphisms
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>F : C ⥤ D<VAR>G : D ⥤ E<VAR>G.PreservesMonomorphisms<VAR>(F ⋙ G).ReflectsMonomorphisms<GOAL>F.ReflectsMonomorphisms
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F G : C ⥤ D<VAR>F.PreservesMonomorphisms<VAR>α : F ≅ G<GOAL>G.PreservesMonomorphisms
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F G : C ⥤ D<VAR>α : F ≅ G<GOAL>F.PreservesMonomorphisms ↔ G.PreservesMonomorphisms
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F G : C ⥤ D<VAR>F.PreservesEpimorphisms<VAR>α : F ≅ G<GOAL>G.PreservesEpimorphisms
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F G : C ⥤ D<VAR>α : F ≅ G<GOAL>F.PreservesEpimorphisms ↔ G.PreservesEpimorphisms
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F G : C ⥤ D<VAR>F.ReflectsMonomorphisms<VAR>α : F ≅ G<GOAL>G.ReflectsMonomorphisms
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F G : C ⥤ D<VAR>α : F ≅ G<GOAL>F.ReflectsMonomorphisms ↔ G.ReflectsMonomorphisms
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F G : C ⥤ D<VAR>F.ReflectsEpimorphisms<VAR>α : F ≅ G<GOAL>G.ReflectsEpimorphisms
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F G : C ⥤ D<VAR>α : F ≅ G<GOAL>F.ReflectsEpimorphisms ↔ G.ReflectsEpimorphisms
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>G : D ⥤ C<VAR>adj : F ⊣ G<GOAL>F.PreservesEpimorphisms
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>G : D ⥤ C<VAR>adj : F ⊣ G<GOAL>G.PreservesMonomorphisms
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>F.Full<VAR>F.Faithful<GOAL>CategoryTheory.IsSplitEpi (F.map f) ↔ CategoryTheory.IsSplitEpi f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>F.Full<VAR>F.Faithful<GOAL>CategoryTheory.IsSplitMono (F.map f) ↔ CategoryTheory.IsSplitMono f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>hF₁ : F.PreservesEpimorphisms<VAR>hF₂ : F.ReflectsEpimorphisms<GOAL>CategoryTheory.Epi (F.map f) ↔ CategoryTheory.Epi f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>hF₁ : F.PreservesMonomorphisms<VAR>hF₂ : F.ReflectsMonomorphisms<GOAL>CategoryTheory.Mono (F.map f) ↔ CategoryTheory.Mono f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>F.IsEquivalence<VAR>CategoryTheory.SplitEpiCategory C<GOAL>CategoryTheory.SplitEpiCategory D
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>F : C ⥤ D<VAR>F' : D ⥤ C<VAR>A B : C<VAR>adj : F ⊣ F'<VAR>f : A ⟶ B<VAR>h₁ : F'.PreservesMonomorphisms<VAR>h₂ : F.PreservesEpimorphisms<VAR>CategoryTheory.StrongEpi f<GOAL>CategoryTheory.StrongEpi (F.map f)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>F : C ⥤ D<VAR>A B : C<VAR>f : A ⟶ B<VAR>F.IsEquivalence<GOAL>CategoryTheory.StrongEpi (F.map f) ↔ CategoryTheory.StrongEpi f
<VAR>R : Type u<VAR>CommRing R<VAR>A : Mon_ (ModuleCat R)<VAR>r : R<GOAL>(algebraMap R ↑A.X) r = A.one r
<VAR>R : Type u<VAR>CommRing R<VAR>A : Mon_ (ModuleCat R)<GOAL>↑(ModuleCat.MonModuleEquivalenceAlgebra.functor.obj A) = ↑A.X
<VAR>R : Type u<VAR>CommRing R<VAR>A B : Mon_ (ModuleCat R)<VAR>f : A ⟶ B<VAR>a : ↑A.X<GOAL>(ModuleCat.MonModuleEquivalenceAlgebra.functor.map f) a = f.hom a
<VAR>R : Type u<VAR>CommRing R<VAR>A : AlgebraCat R<GOAL>(ModuleCat.MonModuleEquivalenceAlgebra.inverseObj A).one = Algebra.linearMap R ↑A
<VAR>R : Type u<VAR>CommRing R<VAR>A : AlgebraCat R<GOAL>(ModuleCat.MonModuleEquivalenceAlgebra.inverseObj A).mul = LinearMap.mul' R ↑A
<VAR>R : Type u<VAR>CommRing R<VAR>A : AlgebraCat R<GOAL>(ModuleCat.MonModuleEquivalenceAlgebra.inverseObj A).X = ModuleCat.of R ↑A
<VAR>R : Type u<VAR>CommRing R<GOAL>∀ {X Y : AlgebraCat R} (f : X ⟶ Y), (ModuleCat.MonModuleEquivalenceAlgebra.inverse.map f).hom = AlgHom.toLinearMap f
<VAR>R : Type u<VAR>CommRing R<VAR>A : AlgebraCat R<GOAL>ModuleCat.MonModuleEquivalenceAlgebra.inverse.obj A = ModuleCat.MonModuleEquivalenceAlgebra.inverseObj A
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>self : F.ReflectsIsomorphisms<VAR>A B : C<VAR>f : A ⟶ B<VAR>CategoryTheory.IsIso (F.map f)<GOAL>CategoryTheory.IsIso f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>A B : C<VAR>f : A ⟶ B<VAR>F : C ⥤ D<VAR>CategoryTheory.IsIso (F.map f)<VAR>F.ReflectsIsomorphisms<GOAL>CategoryTheory.IsIso f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>A B : C<VAR>f : A ⟶ B<VAR>F : C ⥤ D<VAR>F.ReflectsIsomorphisms<GOAL>CategoryTheory.IsIso (F.map f) ↔ CategoryTheory.IsIso f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>hF : F.FullyFaithful<GOAL>F.ReflectsIsomorphisms
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>F : C ⥤ D<VAR>G : D ⥤ E<VAR>(F ⋙ G).ReflectsIsomorphisms<GOAL>F.ReflectsIsomorphisms
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>F.ReflectsIsomorphisms<VAR>F.PreservesEpimorphisms<VAR>F.PreservesMonomorphisms<VAR>CategoryTheory.Balanced D<GOAL>CategoryTheory.Balanced C
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>F G : CategoryTheory.OplaxFunctor B C<VAR>self : CategoryTheory.OplaxNatTrans F G<VAR>a b : B<VAR>f g : a ⟶ b<VAR>η : f ⟶ g<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.map₂ η) (self.app b)) (self.naturality g) = CategoryTheory.CategoryStruct.comp (self.naturality f) (CategoryTheory.Bicategory.whiskerLeft (self.app a) (G.map₂ η))
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>F G : CategoryTheory.OplaxFunctor B C<VAR>self : CategoryTheory.OplaxNatTrans F G<VAR>a : B<GOAL>CategoryTheory.CategoryStruct.comp (self.naturality (CategoryTheory.CategoryStruct.id a)) (CategoryTheory.Bicategory.whiskerLeft (self.app a) (G.mapId a)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapId a) (self.app a)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor (self.app a)).hom (CategoryTheory.Bicategory.rightUnitor (self.app a)).inv)
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>F G : CategoryTheory.OplaxFunctor B C<VAR>self : CategoryTheory.OplaxNatTrans F G<VAR>a b c : B<VAR>f : a ⟶ b<VAR>g : b ⟶ c<GOAL>CategoryTheory.CategoryStruct.comp (self.naturality (CategoryTheory.CategoryStruct.comp f g)) (CategoryTheory.Bicategory.whiskerLeft (self.app a) (G.mapComp f g)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapComp f g) (self.app c)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f) (F.map g) (self.app c)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (self.naturality g)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f) (self.app b) (G.map g)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (self.naturality f) (G.map g)) (CategoryTheory.Bicategory.associator (self.app a) (G.map f) (G.map g)).hom))))
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>F : CategoryTheory.OplaxFunctor B C<VAR>a : B<GOAL>(CategoryTheory.OplaxNatTrans.id F).app a = CategoryTheory.CategoryStruct.id (F.obj a)
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>F : CategoryTheory.OplaxFunctor B C<VAR>a b : B<VAR>f : a ⟶ b<GOAL>(CategoryTheory.OplaxNatTrans.id F).naturality f = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor (F.map f)).hom (CategoryTheory.Bicategory.leftUnitor (F.map f)).inv
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>G H : CategoryTheory.OplaxFunctor B C<VAR>θ : CategoryTheory.OplaxNatTrans G H<VAR>a b : B<VAR>a' : C<VAR>f : a' ⟶ G.obj a<VAR>g h : a ⟶ b<VAR>β : g ⟶ h<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerRight (G.map₂ β) (θ.app b))) (CategoryTheory.Bicategory.whiskerLeft f (θ.naturality h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (θ.naturality g)) (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerLeft (θ.app a) (H.map₂ β)))
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>F G : CategoryTheory.OplaxFunctor B C<VAR>η : CategoryTheory.OplaxNatTrans F G<VAR>a b : B<VAR>a' : C<VAR>f g : a ⟶ b<VAR>β : f ⟶ g<VAR>h : G.obj b ⟶ a'<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.whiskerRight (F.map₂ β) (η.app b)) h) (CategoryTheory.Bicategory.whiskerRight (η.naturality g) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (η.naturality f) h) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (η.app a) (G.map f) h).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (η.app a) (CategoryTheory.Bicategory.whiskerRight (G.map₂ β) h)) (CategoryTheory.Bicategory.associator (η.app a) (G.map g) h).inv))
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>G H : CategoryTheory.OplaxFunctor B C<VAR>θ : CategoryTheory.OplaxNatTrans G H<VAR>a b c : B<VAR>a' : C<VAR>f : a' ⟶ G.obj a<VAR>g : a ⟶ b<VAR>h : b ⟶ c<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (θ.naturality (CategoryTheory.CategoryStruct.comp g h))) (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerLeft (θ.app a) (H.mapComp g h))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerRight (G.mapComp g h) (θ.app c))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.associator (G.map g) (G.map h) (θ.app c)).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerLeft (G.map g) (θ.naturality h))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.associator (G.map g) (θ.app b) (H.map h)).inv) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerRight (θ.naturality g) (H.map h))) (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.associator (θ.app a) (H.map g) (H.map h)).hom)))))