Loogle!

Result

Found 611 declarations mentioning CategoryTheory.eqToHom. Of these, only the first 200 are shown.

• CategoryTheory.eqToHom 📋 Mathlib.CategoryTheory.EqToHom
  {C : Type u₁} [CategoryTheory.CategoryStruct.{v₁, u₁} C] {X Y : C} (p : X = Y) : X ⟶ Y
• CategoryTheory.instIsIsoEqToHom 📋 Mathlib.CategoryTheory.EqToHom
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (h : X = Y) : CategoryTheory.IsIso (CategoryTheory.eqToHom h)
• CategoryTheory.eqToHom_refl 📋 Mathlib.CategoryTheory.EqToHom
  {C : Type u₁} [CategoryTheory.CategoryStruct.{v₁, u₁} C] (X : C) (p : X = X) : CategoryTheory.eqToHom p = CategoryTheory.CategoryStruct.id X
• CategoryTheory.eqToIso.hom 📋 Mathlib.CategoryTheory.EqToHom
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (p : X = Y) : (CategoryTheory.eqToIso p).hom = CategoryTheory.eqToHom p
• CategoryTheory.eqToHom_heq_id_cod 📋 Mathlib.CategoryTheory.EqToHom
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (X Y : C) (h : X = Y) : CategoryTheory.eqToHom h ≍ CategoryTheory.CategoryStruct.id Y
• CategoryTheory.eqToHom_heq_id_dom 📋 Mathlib.CategoryTheory.EqToHom
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (X Y : C) (h : X = Y) : CategoryTheory.eqToHom h ≍ CategoryTheory.CategoryStruct.id X
• CategoryTheory.eqToIso.inv 📋 Mathlib.CategoryTheory.EqToHom
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (p : X = Y) : (CategoryTheory.eqToIso p).inv = CategoryTheory.eqToHom ⋯
• CategoryTheory.inv_eqToHom 📋 Mathlib.CategoryTheory.EqToHom
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (h : X = Y) : CategoryTheory.inv (CategoryTheory.eqToHom h) = CategoryTheory.eqToHom ⋯
• CategoryTheory.comp_eqToHom_heq 📋 Mathlib.CategoryTheory.EqToHom
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {X Y Z : C} (f : X ⟶ Y) (h : Y = Z) : CategoryTheory.CategoryStruct.comp f (CategoryTheory.eqToHom h) ≍ f
• CategoryTheory.eqToHom_comp_heq 📋 Mathlib.CategoryTheory.EqToHom
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {W X Y : C} (f : Y ⟶ X) (h : W = Y) : CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h) f ≍ f
• CategoryTheory.eqToHom_trans 📋 Mathlib.CategoryTheory.EqToHom
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} (p : X = Y) (q : Y = Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom p) (CategoryTheory.eqToHom q) = CategoryTheory.eqToHom ⋯
• CategoryTheory.eq_conj_eqToHom 📋 Mathlib.CategoryTheory.EqToHom
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) : f = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp f (CategoryTheory.eqToHom ⋯))
• CategoryTheory.eqToHom_op 📋 Mathlib.CategoryTheory.EqToHom
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (h : X = Y) : (CategoryTheory.eqToHom h).op = CategoryTheory.eqToHom ⋯
• CategoryTheory.eqToHom_unop 📋 Mathlib.CategoryTheory.EqToHom
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : Cᵒᵖ} (h : X = Y) : (CategoryTheory.eqToHom h).unop = CategoryTheory.eqToHom ⋯
• CategoryTheory.InducedCategory.eqToHom_hom 📋 Mathlib.CategoryTheory.EqToHom
  {C : Type u_2} {D : Type u_3} [CategoryTheory.Category.{u_4, u_3} D] {F : C → D} {X Y : CategoryTheory.InducedCategory D F} (h : X = Y) : (CategoryTheory.eqToHom h).hom = CategoryTheory.eqToHom ⋯
• CategoryTheory.congrArg_mpr_hom_left 📋 Mathlib.CategoryTheory.EqToHom
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} (p : X = Y) (q : Y ⟶ Z) : ⋯.mpr q = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom p) q
• CategoryTheory.congrArg_cast_hom_left 📋 Mathlib.CategoryTheory.EqToHom
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} (p : X = Y) (q : Y ⟶ Z) : cast ⋯ q = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom p) q
• CategoryTheory.congrArg_mpr_hom_right 📋 Mathlib.CategoryTheory.EqToHom
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} (p : X ⟶ Y) (q : Z = Y) : ⋯.mpr p = CategoryTheory.CategoryStruct.comp p (CategoryTheory.eqToHom ⋯)
• CategoryTheory.eqToHom_map 📋 Mathlib.CategoryTheory.EqToHom
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) {X Y : C} (p : X = Y) : F.map (CategoryTheory.eqToHom p) = CategoryTheory.eqToHom ⋯
• CategoryTheory.comp_eqToHom_heq_iff 📋 Mathlib.CategoryTheory.EqToHom
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {W X Y Z Z' : C} (f : X ⟶ Y) (g : Z ⟶ Z') (h : Y = W) : CategoryTheory.CategoryStruct.comp f (CategoryTheory.eqToHom h) ≍ g ↔ f ≍ g
• CategoryTheory.comp_eqToHom_iff 📋 Mathlib.CategoryTheory.EqToHom
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y Y' : C} (p : Y = Y') (f : X ⟶ Y) (g : X ⟶ Y') : CategoryTheory.CategoryStruct.comp f (CategoryTheory.eqToHom p) = g ↔ f = CategoryTheory.CategoryStruct.comp g (CategoryTheory.eqToHom ⋯)
• CategoryTheory.eqToHom_comp_heq_iff 📋 Mathlib.CategoryTheory.EqToHom
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {W X Y Z Z' : C} (f : Y ⟶ X) (g : Z ⟶ Z') (h : W = Y) : CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h) f ≍ g ↔ f ≍ g
• CategoryTheory.eqToHom_comp_iff 📋 Mathlib.CategoryTheory.EqToHom
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X X' Y : C} (p : X = X') (f : X ⟶ Y) (g : X' ⟶ Y) : CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom p) g = f ↔ g = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) f
• CategoryTheory.heq_comp_eqToHom_iff 📋 Mathlib.CategoryTheory.EqToHom
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {W X Y Z Z' : C} (f : X ⟶ Y) (g : Z ⟶ Z') (h : Y = W) : g ≍ CategoryTheory.CategoryStruct.comp f (CategoryTheory.eqToHom h) ↔ g ≍ f
• CategoryTheory.heq_eqToHom_comp_iff 📋 Mathlib.CategoryTheory.EqToHom
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {W X Y Z Z' : C} (f : Y ⟶ X) (g : Z ⟶ Z') (h : W = Y) : g ≍ CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h) f ↔ g ≍ f
• CategoryTheory.congrArg_cast_hom_right 📋 Mathlib.CategoryTheory.EqToHom
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} (p : X ⟶ Y) (q : Z = Y) : cast ⋯ p = CategoryTheory.CategoryStruct.comp p (CategoryTheory.eqToHom ⋯)
• CategoryTheory.eqToHom_trans_assoc 📋 Mathlib.CategoryTheory.EqToHom
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} (p : X = Y) (q : Y = Z) {Z✝ : C} (h : Z ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom p) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom q) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) h
• CategoryTheory.ObjectProperty.eqToHom_hom 📋 Mathlib.CategoryTheory.EqToHom
  {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] {P : CategoryTheory.ObjectProperty C} {X Y : P.FullSubcategory} (h : X = Y) : (CategoryTheory.eqToHom h).hom = CategoryTheory.eqToHom ⋯
• CategoryTheory.eqToHom_naturality 📋 Mathlib.CategoryTheory.EqToHom
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {β : Sort u_1} {f g : β → C} (z : (b : β) → f b ⟶ g b) {j j' : β} (w : j = j') : CategoryTheory.CategoryStruct.comp (z j) (CategoryTheory.eqToHom ⋯) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (z j')
• CategoryTheory.conj_eqToHom_iff_heq' 📋 Mathlib.CategoryTheory.EqToHom
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {W X Y Z : C} (f : W ⟶ X) (g : Y ⟶ Z) (h : W = Y) (h' : Z = X) : f = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h) (CategoryTheory.CategoryStruct.comp g (CategoryTheory.eqToHom h')) ↔ f ≍ g
• CategoryTheory.dcongr_arg 📋 Mathlib.CategoryTheory.EqToHom
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {ι : Type u_2} {F G : ι → C} (α : (i : ι) → F i ⟶ G i) {i j : ι} (h : i = j) : α i = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (α j) (CategoryTheory.eqToHom ⋯))
• CategoryTheory.conj_eqToHom_iff_heq 📋 Mathlib.CategoryTheory.EqToHom
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {W X Y Z : C} (f : W ⟶ X) (g : Y ⟶ Z) (h : W = Y) (h' : X = Z) : f = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h) (CategoryTheory.CategoryStruct.comp g (CategoryTheory.eqToHom ⋯)) ↔ f ≍ g
• CategoryTheory.eqToHom_app 📋 Mathlib.CategoryTheory.EqToHom
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F G : CategoryTheory.Functor C D} (h : F = G) (X : C) : (CategoryTheory.eqToHom h).app X = CategoryTheory.eqToHom ⋯
• CategoryTheory.eqToHom_iso_hom_naturality 📋 Mathlib.CategoryTheory.EqToHom
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {β : Sort u_1} {f g : β → C} (z : (b : β) → f b ≅ g b) {j j' : β} (w : j = j') : CategoryTheory.CategoryStruct.comp (z j).hom (CategoryTheory.eqToHom ⋯) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (z j').hom
• CategoryTheory.eqToHom_iso_inv_naturality 📋 Mathlib.CategoryTheory.EqToHom
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {β : Sort u_1} {f g : β → C} (z : (b : β) → f b ≅ g b) {j j' : β} (w : j = j') : CategoryTheory.CategoryStruct.comp (z j).inv (CategoryTheory.eqToHom ⋯) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (z j').inv
• CategoryTheory.Functor.ext_of_iso 📋 Mathlib.CategoryTheory.EqToHom
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F G : CategoryTheory.Functor C D} (e : F ≅ G) (hobj : ∀ (X : C), F.obj X = G.obj X) (happ : ∀ (X : C), e.hom.app X = CategoryTheory.eqToHom ⋯ := by cat_disch) : F = G
• CategoryTheory.eqToHom_map_comp 📋 Mathlib.CategoryTheory.EqToHom
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) {X Y Z : C} (p : X = Y) (q : Y = Z) : CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.eqToHom p)) (F.map (CategoryTheory.eqToHom q)) = F.map (CategoryTheory.eqToHom ⋯)
• CategoryTheory.eqToHom_naturality_assoc 📋 Mathlib.CategoryTheory.EqToHom
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {β : Sort u_1} {f g : β → C} (z : (b : β) → f b ⟶ g b) {j j' : β} (w : j = j') {Z : C} (h : g j' ⟶ Z) : CategoryTheory.CategoryStruct.comp (z j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (z j') h)
• CategoryTheory.eqToHom_iso_hom_naturality_assoc 📋 Mathlib.CategoryTheory.EqToHom
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {β : Sort u_1} {f g : β → C} (z : (b : β) → f b ≅ g b) {j j' : β} (w : j = j') {Z : C} (h : g j' ⟶ Z) : CategoryTheory.CategoryStruct.comp (z j).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (z j').hom h)
• CategoryTheory.eqToHom_iso_inv_naturality_assoc 📋 Mathlib.CategoryTheory.EqToHom
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {β : Sort u_1} {f g : β → C} (z : (b : β) → f b ≅ g b) {j j' : β} (w : j = j') {Z : C} (h : f j' ⟶ Z) : CategoryTheory.CategoryStruct.comp (z j).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (z j').inv h)
• CategoryTheory.eqToHom_map_comp_assoc 📋 Mathlib.CategoryTheory.EqToHom
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) {X Y Z : C} (p : X = Y) (q : Y = Z) {Z✝ : D} (h : F.obj Z ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.eqToHom p)) (CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.eqToHom q)) h) = CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.eqToHom ⋯)) h
• CategoryTheory.NatTrans.congr 📋 Mathlib.CategoryTheory.EqToHom
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F G : CategoryTheory.Functor C D} (α : F ⟶ G) {X Y : C} (h : X = Y) : α.app X = CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.eqToHom h)) (CategoryTheory.CategoryStruct.comp (α.app Y) (G.map (CategoryTheory.eqToHom ⋯)))
• CategoryTheory.Functor.congr_hom 📋 Mathlib.CategoryTheory.EqToHom
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F G : CategoryTheory.Functor C D} (h : F = G) {X Y : C} (f : X ⟶ Y) : F.map f = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (G.map f) (CategoryTheory.eqToHom ⋯))
• CategoryTheory.Functor.ext 📋 Mathlib.CategoryTheory.EqToHom
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F G : CategoryTheory.Functor C D} (h_obj : ∀ (X : C), F.obj X = G.obj X) (h_map : ∀ (X Y : C) (f : X ⟶ Y), F.map f = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (G.map f) (CategoryTheory.eqToHom ⋯)) := by cat_disch) : F = G
• CategoryTheory.Functor.congr_hom_assoc 📋 Mathlib.CategoryTheory.EqToHom
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F G : CategoryTheory.Functor C D} (h : F = G) {X Y : C} (f : X ⟶ Y) {Z : D} (h✝ : F.obj Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (F.map f) h✝ = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (G.map f) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) h✝))
• CategoryTheory.Functor.congr_inv_of_congr_hom 📋 Mathlib.CategoryTheory.EqToHom
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F G : CategoryTheory.Functor C D) {X Y : C} (e : X ≅ Y) (hX : F.obj X = G.obj X) (hY : F.obj Y = G.obj Y) (h₂ : F.map e.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (G.map e.hom) (CategoryTheory.eqToHom ⋯))) : F.map e.inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (G.map e.inv) (CategoryTheory.eqToHom ⋯))
• CategoryTheory.Equivalence.induced_inverse_map 📋 Mathlib.CategoryTheory.EqToHom
  {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T : Type u_2} (e : T ≃ D) {X✝ Y✝ : D} (f : X✝ ⟶ Y✝) : (CategoryTheory.Equivalence.induced e).inverse.map f = CategoryTheory.InducedCategory.homMk (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp f (CategoryTheory.eqToHom ⋯)))
• CategoryTheory.Equivalence.induced_counitIso 📋 Mathlib.CategoryTheory.EqToHom
  {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T : Type u_2} (e : T ≃ D) : (CategoryTheory.Equivalence.induced e).counitIso = CategoryTheory.NatIso.ofComponents (fun x => CategoryTheory.eqToIso ⋯) ⋯
• CategoryTheory.Equivalence.induced_unitIso 📋 Mathlib.CategoryTheory.EqToHom
  {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T : Type u_2} (e : T ≃ D) : (CategoryTheory.Equivalence.induced e).unitIso = CategoryTheory.NatIso.ofComponents (fun x => CategoryTheory.eqToIso ⋯) ⋯
• CategoryTheory.eqToHom_fst 📋 Mathlib.CategoryTheory.Products.Basic
  {C : Type u₁} [CategoryTheory.CategoryStruct.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.CategoryStruct.{v₂, u₂} D] {X Y : C × D} (h : X = Y) : (CategoryTheory.eqToHom h).1 = CategoryTheory.eqToHom ⋯
• CategoryTheory.eqToHom_snd 📋 Mathlib.CategoryTheory.Products.Basic
  {C : Type u₁} [CategoryTheory.CategoryStruct.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.CategoryStruct.{v₂, u₂} D] {X Y : C × D} (h : X = Y) : (CategoryTheory.eqToHom h).2 = CategoryTheory.eqToHom ⋯
• CategoryTheory.Functor.eqToHom_proj 📋 Mathlib.CategoryTheory.Pi.Basic
  {I : Type w₀} {C : I → Type u₁} [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {x x' : (i : I) → C i} (h : x = x') (i : I) : CategoryTheory.eqToHom h i = CategoryTheory.eqToHom ⋯
• CategoryTheory.Pi.evalCompEqToEquivalenceFunctor_hom 📋 Mathlib.CategoryTheory.Pi.Basic
  {I : Type w₀} (C : I → Type u₁) [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {i j : I} (h : i = j) : (CategoryTheory.Pi.evalCompEqToEquivalenceFunctor C h).hom = CategoryTheory.eqToHom ⋯
• CategoryTheory.Pi.eqToEquivalenceFunctorIso_hom 📋 Mathlib.CategoryTheory.Pi.Basic
  {I : Type w₀} {J : Type w₁} (C : I → Type u₁) [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] (f : J → I) {i' j' : J} (h : i' = j') : (CategoryTheory.Pi.eqToEquivalenceFunctorIso C f h).hom = CategoryTheory.eqToHom ⋯
• CategoryTheory.Pi.evalCompEqToEquivalenceFunctor_inv 📋 Mathlib.CategoryTheory.Pi.Basic
  {I : Type w₀} (C : I → Type u₁) [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {i j : I} (h : i = j) : (CategoryTheory.Pi.evalCompEqToEquivalenceFunctor C h).inv = CategoryTheory.eqToHom ⋯
• CategoryTheory.Pi.eqToEquivalenceFunctorIso_inv 📋 Mathlib.CategoryTheory.Pi.Basic
  {I : Type w₀} {J : Type w₁} (C : I → Type u₁) [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] (f : J → I) {i' j' : J} (h : i' = j') : (CategoryTheory.Pi.eqToEquivalenceFunctorIso C f h).inv = CategoryTheory.eqToHom ⋯
• CategoryTheory.Comma.eqToHom_left 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T) (X Y : CategoryTheory.Comma L R) (H : X = Y) : (CategoryTheory.eqToHom H).left = CategoryTheory.eqToHom ⋯
• CategoryTheory.Comma.eqToHom_right 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T) (X Y : CategoryTheory.Comma L R) (H : X = Y) : (CategoryTheory.eqToHom H).right = CategoryTheory.eqToHom ⋯
• CategoryTheory.Arrow.arrow_mk_comp_eqToHom 📋 Mathlib.CategoryTheory.Comma.Arrow
  {T : Type u} [CategoryTheory.Category.{v, u} T] {X Y Y' : T} (f : X ⟶ Y) (h : Y = Y') : CategoryTheory.Arrow.mk (CategoryTheory.CategoryStruct.comp f (CategoryTheory.eqToHom h)) = CategoryTheory.Arrow.mk f
• CategoryTheory.Arrow.arrow_mk_eqToHom_comp 📋 Mathlib.CategoryTheory.Comma.Arrow
  {T : Type u} [CategoryTheory.Category.{v, u} T] {X' X Y : T} (f : X ⟶ Y) (h : X' = X) : CategoryTheory.Arrow.mk (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h) f) = CategoryTheory.Arrow.mk f
• CategoryTheory.Arrow.eqToHom_left 📋 Mathlib.CategoryTheory.Comma.Arrow
  {T : Type u} [CategoryTheory.Category.{v, u} T] {X Y : CategoryTheory.Arrow T} (h : X = Y) : CategoryTheory.Arrow.Hom.left (CategoryTheory.eqToHom h) = CategoryTheory.eqToHom ⋯
• CategoryTheory.Arrow.eqToHom_right 📋 Mathlib.CategoryTheory.Comma.Arrow
  {T : Type u} [CategoryTheory.Category.{v, u} T] {X Y : CategoryTheory.Arrow T} (h : X = Y) : CategoryTheory.Arrow.Hom.right (CategoryTheory.eqToHom h) = CategoryTheory.eqToHom ⋯
• CategoryTheory.Arrow.mk_eq_mk_iff 📋 Mathlib.CategoryTheory.Comma.Arrow
  {T : Type u} [CategoryTheory.Category.{v, u} T] {X Y X' Y' : T} (f : X ⟶ Y) (f' : X' ⟶ Y') : CategoryTheory.Arrow.mk f = CategoryTheory.Arrow.mk f' ↔ ∃ (hX : X = X') (hY : Y = Y'), f = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom hX) (CategoryTheory.CategoryStruct.comp f' (CategoryTheory.eqToHom ⋯))
• CategoryTheory.Arrow.ext 📋 Mathlib.CategoryTheory.Comma.Arrow
  {T : Type u} [CategoryTheory.Category.{v, u} T] {f g : CategoryTheory.Arrow T} (h₁ : f.left = g.left) (h₂ : f.right = g.right) (h₃ : f.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h₁) (CategoryTheory.CategoryStruct.comp g.hom (CategoryTheory.eqToHom ⋯))) : f = g
• CategoryTheory.MorphismProperty.of_eq 📋 Mathlib.CategoryTheory.MorphismProperty.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C) {X Y : C} {f : X ⟶ Y} (hf : P f) {X' Y' : C} {f' : X' ⟶ Y'} (hX : X = X') (hY : Y = Y') (h : f' = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp f (CategoryTheory.eqToHom hY))) : P f'
• CategoryTheory.eqToHom_map_comp_apply 📋 Mathlib.CategoryTheory.Types.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) {X Y Z : C} (p : X = Y) (q : Y = Z) {F✝ : D → D → Type uF} {carrier : D → Type w} {instFunLike : (X Y : D) → FunLike (F✝ X Y) (carrier X) (carrier Y)} [inst : CategoryTheory.ConcreteCategory D F✝] (x : carrier (F.obj X)) : (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.eqToHom q))) ((CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.eqToHom p))) x) = (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.eqToHom ⋯))) x
• CategoryTheory.eqToHom_down 📋 Mathlib.CategoryTheory.Category.ULift
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : CategoryTheory.AsSmall C} (h : X = Y) : (CategoryTheory.eqToHom h).down = CategoryTheory.eqToHom ⋯
• CategoryTheory.eqToHom_comp_homOfLE 📋 Mathlib.CategoryTheory.Category.Preorder
  {X : Type u} [Preorder X] {a b c : X} (hab : a = b) (hbc : b ≤ c) : CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom hab) (CategoryTheory.homOfLE hbc) = CategoryTheory.homOfLE ⋯
• CategoryTheory.homOfLE_comp_eqToHom 📋 Mathlib.CategoryTheory.Category.Preorder
  {X : Type u} [Preorder X] {a b c : X} (hab : a ≤ b) (hbc : b = c) : CategoryTheory.CategoryStruct.comp (CategoryTheory.homOfLE hab) (CategoryTheory.eqToHom hbc) = CategoryTheory.homOfLE ⋯
• CategoryTheory.eqToHom_comp_homOfLE_assoc 📋 Mathlib.CategoryTheory.Category.Preorder
  {X : Type u} [Preorder X] {a b c : X} (hab : a = b) (hbc : b ≤ c) {Z : X} (h : c ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom hab) (CategoryTheory.CategoryStruct.comp (CategoryTheory.homOfLE hbc) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.homOfLE ⋯) h
• CategoryTheory.homOfLE_comp_eqToHom_assoc 📋 Mathlib.CategoryTheory.Category.Preorder
  {X : Type u} [Preorder X] {a b c : X} (hab : a ≤ b) (hbc : b = c) {Z : X} (h : c ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.homOfLE hab) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom hbc) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.homOfLE ⋯) h
• CategoryTheory.eqToHom_comp_homOfLE_op 📋 Mathlib.CategoryTheory.Category.Preorder
  {X : Type u} [Preorder X] {a b c : X} (hab : Opposite.op a = Opposite.op b) (hbc : c ≤ b) : CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom hab) (CategoryTheory.homOfLE hbc).op = (CategoryTheory.homOfLE ⋯).op
• CategoryTheory.homOfLE_op_comp_eqToHom 📋 Mathlib.CategoryTheory.Category.Preorder
  {X : Type u} [Preorder X] {a b c : X} (hab : b ≤ a) (hbc : Opposite.op b = Opposite.op c) : CategoryTheory.CategoryStruct.comp (CategoryTheory.homOfLE hab).op (CategoryTheory.eqToHom hbc) = (CategoryTheory.homOfLE ⋯).op
• CategoryTheory.eqToHom_comp_homOfLE_op_assoc 📋 Mathlib.CategoryTheory.Category.Preorder
  {X : Type u} [Preorder X] {a b c : X} (hab : Opposite.op a = Opposite.op b) (hbc : c ≤ b) {Z : Xᵒᵖ} (h : Opposite.op c ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom hab) (CategoryTheory.CategoryStruct.comp (CategoryTheory.homOfLE hbc).op h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.homOfLE ⋯).op h
• CategoryTheory.homOfLE_op_comp_eqToHom_assoc 📋 Mathlib.CategoryTheory.Category.Preorder
  {X : Type u} [Preorder X] {a b c : X} (hab : b ≤ a) (hbc : Opposite.op b = Opposite.op c) {Z : Xᵒᵖ} (h : Opposite.op c ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.homOfLE hab).op (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom hbc) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.homOfLE ⋯).op h
• CategoryTheory.Bicategory.eqToHom_whiskerRight 📋 Mathlib.CategoryTheory.Bicategory.Strict.Basic
  {B : Type u} [CategoryTheory.Bicategory B] {a b c : B} {f g : a ⟶ b} (η : f = g) (h : b ⟶ c) : CategoryTheory.Bicategory.whiskerRight (CategoryTheory.eqToHom η) h = CategoryTheory.eqToHom ⋯
• CategoryTheory.Bicategory.whiskerLeft_eqToHom 📋 Mathlib.CategoryTheory.Bicategory.Strict.Basic
  {B : Type u} [CategoryTheory.Bicategory B] {a b c : B} (f : a ⟶ b) {g h : b ⟶ c} (η : g = h) : CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.eqToHom η) = CategoryTheory.eqToHom ⋯
• CategoryTheory.Cat.leftUnitor_hom_app 📋 Mathlib.CategoryTheory.Category.Cat
  {B C : CategoryTheory.Cat} (F : B ⟶ C) (X : ↑B) : (CategoryTheory.Bicategory.leftUnitor F).hom.toNatTrans.app X = CategoryTheory.eqToHom ⋯
• CategoryTheory.Cat.leftUnitor_inv_app 📋 Mathlib.CategoryTheory.Category.Cat
  {B C : CategoryTheory.Cat} (F : B ⟶ C) (X : ↑B) : (CategoryTheory.Bicategory.leftUnitor F).inv.toNatTrans.app X = CategoryTheory.eqToHom ⋯
• CategoryTheory.Cat.rightUnitor_hom_app 📋 Mathlib.CategoryTheory.Category.Cat
  {B C : CategoryTheory.Cat} (F : B ⟶ C) (X : ↑B) : (CategoryTheory.Bicategory.rightUnitor F).hom.toNatTrans.app X = CategoryTheory.eqToHom ⋯
• CategoryTheory.Cat.rightUnitor_inv_app 📋 Mathlib.CategoryTheory.Category.Cat
  {B C : CategoryTheory.Cat} (F : B ⟶ C) (X : ↑B) : (CategoryTheory.Bicategory.rightUnitor F).inv.toNatTrans.app X = CategoryTheory.eqToHom ⋯
• CategoryTheory.Cat.Hom₂.eqToHom_toNatTrans 📋 Mathlib.CategoryTheory.Category.Cat
  {C D : CategoryTheory.Cat} {F G : C ⟶ D} (h : F = G) : (CategoryTheory.eqToHom h).toNatTrans = CategoryTheory.eqToHom ⋯
• CategoryTheory.Cat.eqToHom_app 📋 Mathlib.CategoryTheory.Category.Cat
  {C D : CategoryTheory.Cat} (F G : C ⟶ D) (h : F = G) (X : ↑C) : (CategoryTheory.eqToHom h).toNatTrans.app X = CategoryTheory.eqToHom ⋯
• CategoryTheory.Cat.associator_hom_app 📋 Mathlib.CategoryTheory.Category.Cat
  {B C D E : CategoryTheory.Cat} (F : B ⟶ C) (G : C ⟶ D) (H : D ⟶ E) (X : ↑B) : (CategoryTheory.Bicategory.associator F G H).hom.toNatTrans.app X = CategoryTheory.eqToHom ⋯
• CategoryTheory.Cat.associator_inv_app 📋 Mathlib.CategoryTheory.Category.Cat
  {B C D E : CategoryTheory.Cat} (F : B ⟶ C) (G : C ⟶ D) (H : D ⟶ E) (X : ↑B) : (CategoryTheory.Bicategory.associator F G H).inv.toNatTrans.app X = CategoryTheory.eqToHom ⋯
• CategoryTheory.Cat.isoOfEquiv 📋 Mathlib.CategoryTheory.Category.Cat
  {C D : CategoryTheory.Cat} (e : ↑C ≌ ↑D) (h₁ : ∀ (X : ↑C), e.inverse.obj (e.functor.obj X) = X) (h₂ : ∀ (Y : ↑D), e.functor.obj (e.inverse.obj Y) = Y) (h₃ : ∀ (X : ↑C), e.unitIso.hom.app X = CategoryTheory.eqToHom ⋯ := by cat_disch) (h₄ : ∀ (Y : ↑D), e.counitIso.hom.app Y = CategoryTheory.eqToHom ⋯ := by cat_disch) : C ≅ D
• CategoryTheory.Cat.isoOfEquiv_hom 📋 Mathlib.CategoryTheory.Category.Cat
  {C D : CategoryTheory.Cat} (e : ↑C ≌ ↑D) (h₁ : ∀ (X : ↑C), e.inverse.obj (e.functor.obj X) = X) (h₂ : ∀ (Y : ↑D), e.functor.obj (e.inverse.obj Y) = Y) (h₃ : ∀ (X : ↑C), e.unitIso.hom.app X = CategoryTheory.eqToHom ⋯ := by cat_disch) (h₄ : ∀ (Y : ↑D), e.counitIso.hom.app Y = CategoryTheory.eqToHom ⋯ := by cat_disch) : (CategoryTheory.Cat.isoOfEquiv e h₁ h₂ h₃ h₄).hom = e.functor.toCatHom
• CategoryTheory.Cat.isoOfEquiv_inv 📋 Mathlib.CategoryTheory.Category.Cat
  {C D : CategoryTheory.Cat} (e : ↑C ≌ ↑D) (h₁ : ∀ (X : ↑C), e.inverse.obj (e.functor.obj X) = X) (h₂ : ∀ (Y : ↑D), e.functor.obj (e.inverse.obj Y) = Y) (h₃ : ∀ (X : ↑C), e.unitIso.hom.app X = CategoryTheory.eqToHom ⋯ := by cat_disch) (h₄ : ∀ (Y : ↑D), e.counitIso.hom.app Y = CategoryTheory.eqToHom ⋯ := by cat_disch) : (CategoryTheory.Cat.isoOfEquiv e h₁ h₂ h₃ h₄).inv = e.inverse.toCatHom
• CategoryTheory.Limits.colimit.eqToHom_comp_ι 📋 Mathlib.CategoryTheory.Limits.HasLimits
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor J C) [CategoryTheory.Limits.HasColimit F] {j j' : J} (hj : j = j') : CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.Limits.colimit.ι F j) = CategoryTheory.Limits.colimit.ι F j'
• CategoryTheory.Limits.limit.π_comp_eqToHom 📋 Mathlib.CategoryTheory.Limits.HasLimits
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor J C) [CategoryTheory.Limits.HasLimit F] {j j' : J} (hj : j = j') : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π F j) (CategoryTheory.eqToHom ⋯) = CategoryTheory.Limits.limit.π F j'
• CategoryTheory.Limits.colimit.eqToHom_comp_ι_assoc 📋 Mathlib.CategoryTheory.Limits.HasLimits
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor J C) [CategoryTheory.Limits.HasColimit F] {j j' : J} (hj : j = j') {Z : C} (h : CategoryTheory.Limits.colimit F ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι F j) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι F j') h
• CategoryTheory.Limits.limit.π_comp_eqToHom_assoc 📋 Mathlib.CategoryTheory.Limits.HasLimits
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor J C) [CategoryTheory.Limits.HasLimit F] {j j' : J} (hj : j = j') {Z : C} (h : F.obj j' ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π F j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π F j') h
• CategoryTheory.Limits.Pi.π_comp_eqToHom 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type u_1} (f : J → C) [CategoryTheory.Limits.HasProduct f] {j j' : J} (w : j = j') : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π f j) (CategoryTheory.eqToHom ⋯) = CategoryTheory.Limits.Pi.π f j'
• CategoryTheory.Limits.Sigma.eqToHom_comp_ι 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type u_1} (f : J → C) [CategoryTheory.Limits.HasCoproduct f] {j j' : J} (w : j = j') : CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.Limits.Sigma.ι f j') = CategoryTheory.Limits.Sigma.ι f j
• CategoryTheory.Limits.Pi.π_comp_eqToHom_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type u_1} (f : J → C) [CategoryTheory.Limits.HasProduct f] {j j' : J} (w : j = j') {Z : C} (h : f j' ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π f j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π f j') h
• CategoryTheory.Limits.Sigma.eqToHom_comp_ι_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type u_1} (f : J → C) [CategoryTheory.Limits.HasCoproduct f] {j j' : J} (w : j = j') {Z : C} (h : ∐ f ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι f j') h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι f j) h
• CategoryTheory.Limits.coproductUniqueIso_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [Unique β] (f : β → C) (b : β) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι f b) (CategoryTheory.Limits.coproductUniqueIso f).hom = CategoryTheory.eqToHom ⋯
• CategoryTheory.Limits.productUniqueIso_inv 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [Unique β] (f : β → C) (b : β) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.productUniqueIso f).inv (CategoryTheory.Limits.Pi.π f b) = CategoryTheory.eqToHom ⋯
• CategoryTheory.Limits.productUniqueIso_inv_π 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [Unique β] (f : β → C) (b : β) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.productUniqueIso f).inv (CategoryTheory.Limits.Pi.π f b) = CategoryTheory.eqToHom ⋯
• CategoryTheory.Limits.ι_coproductUniqueIso_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [Unique β] (f : β → C) (b : β) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι f b) (CategoryTheory.Limits.coproductUniqueIso f).hom = CategoryTheory.eqToHom ⋯
• CategoryTheory.Limits.Pi.map'_eq 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {α : Type w₂} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : α → C} {g : β → C} [CategoryTheory.Limits.HasProduct f] [CategoryTheory.Limits.HasProduct g] {p p' : β → α} {q : (b : β) → f (p b) ⟶ g b} {q' : (b : β) → f (p' b) ⟶ g b} (hp : p = p') (hq : ∀ (b : β), CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (q b) = q' b) : CategoryTheory.Limits.Pi.map' p q = CategoryTheory.Limits.Pi.map' p' q'
• CategoryTheory.Limits.Sigma.map'_eq 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {α : Type w₂} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : α → C} {g : β → C} [CategoryTheory.Limits.HasCoproduct f] [CategoryTheory.Limits.HasCoproduct g] {p p' : α → β} {q : (a : α) → f a ⟶ g (p a)} {q' : (a : α) → f a ⟶ g (p' a)} (hp : p = p') (hq : ∀ (a : α), CategoryTheory.CategoryStruct.comp (q a) (CategoryTheory.eqToHom ⋯) = q' a) : CategoryTheory.Limits.Sigma.map' p q = CategoryTheory.Limits.Sigma.map' p' q'
• CategoryTheory.Limits.productUniqueIso_inv_π_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [Unique β] (f : β → C) (b : β) {Z : C} (h : f b ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.productUniqueIso f).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π f b) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) h
• CategoryTheory.Limits.ι_coproductUniqueIso_hom_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [Unique β] (f : β → C) (b : β) {Z : C} (h : f default ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι f b) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coproductUniqueIso f).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) h
• CategoryTheory.Limits.colimitCoconeOfUnique_cocone_ι 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [Unique β] (f : β → C) : (CategoryTheory.Limits.colimitCoconeOfUnique f).cocone.ι = CategoryTheory.Discrete.natTrans fun x => match x with | { as := j } => CategoryTheory.eqToHom ⋯
• CategoryTheory.Limits.limitConeOfUnique_cone_π 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [Unique β] (f : β → C) : (CategoryTheory.Limits.limitConeOfUnique f).cone.π = CategoryTheory.Discrete.natTrans fun x => match x with | { as := j } => CategoryTheory.eqToHom ⋯
• CategoryTheory.Limits.Pi.whiskerEquiv_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type u_1} {K : Type u_2} {f : J → C} {g : K → C} (e : J ≃ K) (w : (j : J) → g (e j) ≅ f j) [CategoryTheory.Limits.HasProduct f] [CategoryTheory.Limits.HasProduct g] : (CategoryTheory.Limits.Pi.whiskerEquiv e w).hom = CategoryTheory.Limits.Pi.map' ⇑e.symm fun k => CategoryTheory.CategoryStruct.comp (w (e.symm k)).inv (CategoryTheory.eqToHom ⋯)
• CategoryTheory.Limits.Sigma.whiskerEquiv_inv 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type u_1} {K : Type u_2} {f : J → C} {g : K → C} (e : J ≃ K) (w : (j : J) → g (e j) ≅ f j) [CategoryTheory.Limits.HasCoproduct f] [CategoryTheory.Limits.HasCoproduct g] : (CategoryTheory.Limits.Sigma.whiskerEquiv e w).inv = CategoryTheory.Limits.Sigma.map' ⇑e.symm fun k => CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (w (e.symm k)).hom
• CategoryTheory.Limits.colimitCoconeOfUnique_isColimit_desc 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [Unique β] (f : β → C) (s : CategoryTheory.Limits.Cocone (CategoryTheory.Discrete.functor f)) : (CategoryTheory.Limits.colimitCoconeOfUnique f).isColimit.desc s = s.ι.app default
• CategoryTheory.Limits.limitConeOfUnique_isLimit_lift 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [Unique β] (f : β → C) (s : CategoryTheory.Limits.Cone (CategoryTheory.Discrete.functor f)) : (CategoryTheory.Limits.limitConeOfUnique f).isLimit.lift s = s.π.app default
• CategoryTheory.StructuredArrow.eqToHom_right 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S : D} {T : CategoryTheory.Functor C D} {X Y : CategoryTheory.StructuredArrow S T} (h : X = Y) : CategoryTheory.StructuredArrow.Hom.right (CategoryTheory.eqToHom h) = CategoryTheory.eqToHom ⋯
• CategoryTheory.CostructuredArrow.eqToHom_left 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T : D} {S : CategoryTheory.Functor C D} {X Y : CategoryTheory.CostructuredArrow S T} (h : X = Y) : (CategoryTheory.eqToHom h).left = CategoryTheory.eqToHom ⋯
• CategoryTheory.CostructuredArrow.obj_ext 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T : D} {S : CategoryTheory.Functor C D} (x y : CategoryTheory.CostructuredArrow S T) (hl : x.left = y.left) (hh : CategoryTheory.CategoryStruct.comp (S.map (CategoryTheory.eqToHom hl)) y.hom = x.hom) : x = y
• CategoryTheory.StructuredArrow.obj_ext 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S : D} {T : CategoryTheory.Functor C D} (x y : CategoryTheory.StructuredArrow S T) (hr : x.right = y.right) (hh : CategoryTheory.CategoryStruct.comp x.hom (T.map (CategoryTheory.eqToHom hr)) = y.hom) : x = y
• CategoryTheory.CostructuredArrow.mkPrecomp_id 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T : D} {Y : C} {S : CategoryTheory.Functor C D} (f : S.obj Y ⟶ T) : CategoryTheory.CostructuredArrow.mkPrecomp f (CategoryTheory.CategoryStruct.id Y) = CategoryTheory.eqToHom ⋯
• CategoryTheory.StructuredArrow.mkPostcomp_id 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S : D} {Y : C} {T : CategoryTheory.Functor C D} (f : S ⟶ T.obj Y) : CategoryTheory.StructuredArrow.mkPostcomp f (CategoryTheory.CategoryStruct.id Y) = CategoryTheory.eqToHom ⋯
• CategoryTheory.CostructuredArrow.homMk'_id 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T : D} {S : CategoryTheory.Functor C D} (f : CategoryTheory.CostructuredArrow S T) : f.homMk' (CategoryTheory.CategoryStruct.id f.left) = CategoryTheory.eqToHom ⋯
• CategoryTheory.StructuredArrow.homMk'_id 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S : D} {T : CategoryTheory.Functor C D} (f : CategoryTheory.StructuredArrow S T) : f.homMk' (CategoryTheory.CategoryStruct.id f.right) = CategoryTheory.eqToHom ⋯
• CategoryTheory.CostructuredArrow.homMk'_mk_id 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T : D} {Y : C} {S : CategoryTheory.Functor C D} (f : S.obj Y ⟶ T) : (CategoryTheory.CostructuredArrow.mk f).homMk' (CategoryTheory.CategoryStruct.id Y) = CategoryTheory.eqToHom ⋯
• CategoryTheory.StructuredArrow.homMk'_mk_id 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S : D} {Y : C} {T : CategoryTheory.Functor C D} (f : S ⟶ T.obj Y) : (CategoryTheory.StructuredArrow.mk f).homMk' (CategoryTheory.CategoryStruct.id Y) = CategoryTheory.eqToHom ⋯
• CategoryTheory.CostructuredArrow.mkPrecomp_comp 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T : D} {Y Y' Y'' : C} {S : CategoryTheory.Functor C D} (f : S.obj Y ⟶ T) (g : Y' ⟶ Y) (g' : Y'' ⟶ Y') : CategoryTheory.CostructuredArrow.mkPrecomp f (CategoryTheory.CategoryStruct.comp g' g) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (CategoryTheory.CostructuredArrow.mkPrecomp (CategoryTheory.CategoryStruct.comp (S.map g) f) g') (CategoryTheory.CostructuredArrow.mkPrecomp f g))
• CategoryTheory.StructuredArrow.mkPostcomp_comp 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S : D} {Y Y' Y'' : C} {T : CategoryTheory.Functor C D} (f : S ⟶ T.obj Y) (g : Y ⟶ Y') (g' : Y' ⟶ Y'') : CategoryTheory.StructuredArrow.mkPostcomp f (CategoryTheory.CategoryStruct.comp g g') = CategoryTheory.CategoryStruct.comp (CategoryTheory.StructuredArrow.mkPostcomp f g) (CategoryTheory.CategoryStruct.comp (CategoryTheory.StructuredArrow.mkPostcomp (CategoryTheory.CategoryStruct.comp f (T.map g)) g') (CategoryTheory.eqToHom ⋯))
• CategoryTheory.StructuredArrow.homMk'_comp 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S : D} {Y' Y'' : C} {T : CategoryTheory.Functor C D} (f : CategoryTheory.StructuredArrow S T) (g : f.right ⟶ Y') (g' : Y' ⟶ Y'') : f.homMk' (CategoryTheory.CategoryStruct.comp g g') = CategoryTheory.CategoryStruct.comp (f.homMk' g) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.StructuredArrow.mk (CategoryTheory.CategoryStruct.comp f.hom (T.map g))).homMk' g') (CategoryTheory.eqToHom ⋯))
• CategoryTheory.CostructuredArrow.homMk'_mk_comp 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T : D} {Y Y' Y'' : C} {S : CategoryTheory.Functor C D} (f : S.obj Y ⟶ T) (g : Y' ⟶ Y) (g' : Y'' ⟶ Y') : (CategoryTheory.CostructuredArrow.mk f).homMk' (CategoryTheory.CategoryStruct.comp g' g) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.CostructuredArrow.mk (CategoryTheory.CategoryStruct.comp (S.map g) f)).homMk' g') ((CategoryTheory.CostructuredArrow.mk f).homMk' g))
• CategoryTheory.StructuredArrow.homMk'_mk_comp 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S : D} {Y Y' Y'' : C} {T : CategoryTheory.Functor C D} (f : S ⟶ T.obj Y) (g : Y ⟶ Y') (g' : Y' ⟶ Y'') : (CategoryTheory.StructuredArrow.mk f).homMk' (CategoryTheory.CategoryStruct.comp g g') = CategoryTheory.CategoryStruct.comp ((CategoryTheory.StructuredArrow.mk f).homMk' g) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.StructuredArrow.mk (CategoryTheory.CategoryStruct.comp f (T.map g))).homMk' g') (CategoryTheory.eqToHom ⋯))
• CategoryTheory.CostructuredArrow.homMk'_comp 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T : D} {Y' Y'' : C} {S : CategoryTheory.Functor C D} (f : CategoryTheory.CostructuredArrow S T) (g : Y' ⟶ f.left) (g' : Y'' ⟶ Y') : f.homMk' (CategoryTheory.CategoryStruct.comp g' g) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.CostructuredArrow.mk (CategoryTheory.CategoryStruct.comp (S.map g) f.hom)).homMk' g') (f.homMk' g))
• CategoryTheory.Over.eqToHom_left 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} {f g : CategoryTheory.Over X} (h : f = g) : CategoryTheory.Over.Hom.left (CategoryTheory.eqToHom h) = CategoryTheory.eqToHom ⋯
• CategoryTheory.Under.eqToHom_right 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X : T} {f g : CategoryTheory.Under X} (h : f = g) : CategoryTheory.Under.Hom.right (CategoryTheory.eqToHom h) = CategoryTheory.eqToHom ⋯
• CategoryTheory.Under.mapCongr_hom_app 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X Y : T} (f g : X ⟶ Y) (h : f = g) (X✝ : CategoryTheory.Under Y) : (CategoryTheory.Under.mapCongr f g h).hom.app X✝ = CategoryTheory.eqToHom ⋯
• CategoryTheory.Under.mapCongr_inv_app 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X Y : T} (f g : X ⟶ Y) (h : f = g) (X✝ : CategoryTheory.Under Y) : (CategoryTheory.Under.mapCongr f g h).inv.app X✝ = CategoryTheory.eqToHom ⋯
• CategoryTheory.Under.mapComp_hom 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X Y Z : T} (f : X ⟶ Y) (g : Y ⟶ Z) : (CategoryTheory.Under.mapComp f g).hom = CategoryTheory.eqToHom ⋯
• CategoryTheory.Under.mapComp_inv 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  {T : Type u₁} [CategoryTheory.Category.{v₁, u₁} T] {X Y Z : T} (f : X ⟶ Y) (g : Y ⟶ Z) : (CategoryTheory.Under.mapComp f g).inv = CategoryTheory.eqToHom ⋯
• CategoryTheory.Limits.diagramIsoParallelPair_hom_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Equalizers
  {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair C) (X : CategoryTheory.Limits.WalkingParallelPair) : (CategoryTheory.Limits.diagramIsoParallelPair F).hom.app X = CategoryTheory.eqToHom ⋯
• CategoryTheory.Limits.diagramIsoParallelPair_inv_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Equalizers
  {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair C) (X : CategoryTheory.Limits.WalkingParallelPair) : (CategoryTheory.Limits.diagramIsoParallelPair F).inv.app X = CategoryTheory.eqToHom ⋯
• CategoryTheory.Limits.Cocone.ofCofork_ι 📋 Mathlib.CategoryTheory.Limits.Shapes.Equalizers
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair C} (t : CategoryTheory.Limits.Cofork (F.map CategoryTheory.Limits.WalkingParallelPairHom.left) (F.map CategoryTheory.Limits.WalkingParallelPairHom.right)) (j : CategoryTheory.Limits.WalkingParallelPair) : (CategoryTheory.Limits.Cocone.ofCofork t).ι.app j = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (t.ι.app j)
• CategoryTheory.Limits.Cone.ofFork_π 📋 Mathlib.CategoryTheory.Limits.Shapes.Equalizers
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair C} (t : CategoryTheory.Limits.Fork (F.map CategoryTheory.Limits.WalkingParallelPairHom.left) (F.map CategoryTheory.Limits.WalkingParallelPairHom.right)) (j : CategoryTheory.Limits.WalkingParallelPair) : (CategoryTheory.Limits.Cone.ofFork t).π.app j = CategoryTheory.CategoryStruct.comp (t.π.app j) (CategoryTheory.eqToHom ⋯)
• CategoryTheory.Limits.Cofork.ofCocone_ι 📋 Mathlib.CategoryTheory.Limits.Shapes.Equalizers
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair C} (t : CategoryTheory.Limits.Cocone F) (j : CategoryTheory.Limits.WalkingParallelPair) : (CategoryTheory.Limits.Cofork.ofCocone t).ι.app j = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (t.ι.app j)
• CategoryTheory.Limits.Fork.ofCone_π 📋 Mathlib.CategoryTheory.Limits.Shapes.Equalizers
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair C} (t : CategoryTheory.Limits.Cone F) (j : CategoryTheory.Limits.WalkingParallelPair) : (CategoryTheory.Limits.Fork.ofCone t).π.app j = CategoryTheory.CategoryStruct.comp (t.π.app j) (CategoryTheory.eqToHom ⋯)
• CategoryTheory.Limits.MonoFactorisation.ext 📋 Mathlib.CategoryTheory.Limits.Shapes.Images
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} {F F' : CategoryTheory.Limits.MonoFactorisation f} (hI : F.I = F'.I) (hm : F.m = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom hI) F'.m) : F = F'
• CategoryTheory.Limits.Pi.ι_π 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {β : Type w} [DecidableEq β] (f : β → C) [CategoryTheory.Limits.HasProduct f] (b c : β) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.ι f b) (CategoryTheory.Limits.Pi.π f c) = if h : b = c then CategoryTheory.eqToHom ⋯ else 0
• CategoryTheory.Limits.Sigma.ι_π 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {β : Type w} [DecidableEq β] (f : β → C) [CategoryTheory.Limits.HasCoproduct f] (b c : β) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι f b) (CategoryTheory.Limits.Sigma.π f c) = if h : b = c then CategoryTheory.eqToHom ⋯ else 0
• CategoryTheory.Limits.Pi.ι_π_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {β : Type w} [DecidableEq β] (f : β → C) [CategoryTheory.Limits.HasProduct f] (b c : β) {Z : C} (h : f c ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.ι f b) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π f c) h) = CategoryTheory.CategoryStruct.comp (if h : b = c then CategoryTheory.eqToHom ⋯ else 0) h
• CategoryTheory.Limits.Sigma.ι_π_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {β : Type w} [DecidableEq β] (f : β → C) [CategoryTheory.Limits.HasCoproduct f] (b c : β) {Z : C} (h : f c ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι f b) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.π f c) h) = CategoryTheory.CategoryStruct.comp (if h : b = c then CategoryTheory.eqToHom ⋯ else 0) h
• CategoryTheory.Limits.limitBiconeOfUnique_bicone_ι 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [Unique J] (f : J → C) (j : J) : (CategoryTheory.Limits.limitBiconeOfUnique f).bicone.ι j = CategoryTheory.eqToHom ⋯
• CategoryTheory.Limits.limitBiconeOfUnique_bicone_π 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [Unique J] (f : J → C) (j : J) : (CategoryTheory.Limits.limitBiconeOfUnique f).bicone.π j = CategoryTheory.eqToHom ⋯
• CategoryTheory.Limits.biproduct.eqToHom_comp_ι 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (f : J → C) [CategoryTheory.Limits.HasBiproduct f] {j j' : J} (w : j = j') : CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.Limits.biproduct.ι f j') = CategoryTheory.Limits.biproduct.ι f j
• CategoryTheory.Limits.biproduct.π_comp_eqToHom 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (f : J → C) [CategoryTheory.Limits.HasBiproduct f] {j j' : J} (w : j = j') : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.π f j) (CategoryTheory.eqToHom ⋯) = CategoryTheory.Limits.biproduct.π f j'
• CategoryTheory.Limits.biproduct.eqToHom_comp_ι_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (f : J → C) [CategoryTheory.Limits.HasBiproduct f] {j j' : J} (w : j = j') {Z : C} (h : ⨁ f ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι f j') h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι f j) h
• CategoryTheory.Limits.biproduct.π_comp_eqToHom_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (f : J → C) [CategoryTheory.Limits.HasBiproduct f] {j j' : J} (w : j = j') {Z : C} (h : f j' ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.π f j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.π f j') h
• CategoryTheory.Limits.limitBiconeOfUnique_isBilimit_isColimit 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [Unique J] (f : J → C) : (CategoryTheory.Limits.limitBiconeOfUnique f).isBilimit.isColimit = (CategoryTheory.Limits.colimitCoconeOfUnique f).isColimit
• CategoryTheory.Limits.limitBiconeOfUnique_isBilimit_isLimit 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [Unique J] (f : J → C) : (CategoryTheory.Limits.limitBiconeOfUnique f).isBilimit.isLimit = (CategoryTheory.Limits.limitConeOfUnique f).isLimit
• CategoryTheory.Limits.Bicone.ι_π 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} (self : CategoryTheory.Limits.Bicone F) (j j' : J) : CategoryTheory.CategoryStruct.comp (self.ι j) (self.π j') = if h : j = j' then CategoryTheory.eqToHom ⋯ else 0
• CategoryTheory.Limits.biproduct.ι_π 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [DecidableEq J] (f : J → C) [CategoryTheory.Limits.HasBiproduct f] (j j' : J) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι f j) (CategoryTheory.Limits.biproduct.π f j') = if h : j = j' then CategoryTheory.eqToHom ⋯ else 0
• CategoryTheory.Limits.Bicone.mk 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} (pt : C) (π : (j : J) → pt ⟶ F j) (ι : (j : J) → F j ⟶ pt) (ι_π : ∀ (j j' : J), CategoryTheory.CategoryStruct.comp (ι j) (π j') = if h : j = j' then CategoryTheory.eqToHom ⋯ else 0 := by aesop) : CategoryTheory.Limits.Bicone F
• CategoryTheory.Limits.Bicone.ι_of_isLimit 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {f : J → C} {t : CategoryTheory.Limits.Bicone f} (ht : CategoryTheory.Limits.IsLimit t.toCone) (j : J) : t.ι j = ht.lift (CategoryTheory.Limits.Fan.mk (f j) fun j' => if h : j = j' then CategoryTheory.eqToHom ⋯ else 0)
• CategoryTheory.Limits.Bicone.π_of_isColimit 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {f : J → C} {t : CategoryTheory.Limits.Bicone f} (ht : CategoryTheory.Limits.IsColimit t.toCocone) (j : J) : t.π j = ht.desc (CategoryTheory.Limits.Cofan.mk (f j) fun j' => if h : j' = j then CategoryTheory.eqToHom ⋯ else 0)
• CategoryTheory.Limits.biproduct.ι_π_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [DecidableEq J] (f : J → C) [CategoryTheory.Limits.HasBiproduct f] (j j' : J) {Z : C} (h : f j' ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι f j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.π f j') h) = CategoryTheory.CategoryStruct.comp (if h : j = j' then CategoryTheory.eqToHom ⋯ else 0) h
• CategoryTheory.Limits.Bicone.ofColimitCocone_π 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {f : J → C} {t : CategoryTheory.Limits.Cocone (CategoryTheory.Discrete.functor f)} (ht : CategoryTheory.Limits.IsColimit t) (j : J) : (CategoryTheory.Limits.Bicone.ofColimitCocone ht).π j = ht.desc (CategoryTheory.Limits.Cofan.mk (f j) fun j' => if h : j' = j then CategoryTheory.eqToHom ⋯ else 0)
• CategoryTheory.Limits.Bicone.ofLimitCone_ι 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {f : J → C} {t : CategoryTheory.Limits.Cone (CategoryTheory.Discrete.functor f)} (ht : CategoryTheory.Limits.IsLimit t) (j : J) : (CategoryTheory.Limits.Bicone.ofLimitCone ht).ι j = ht.lift (CategoryTheory.Limits.Fan.mk (f j) fun j' => if h : j = j' then CategoryTheory.eqToHom ⋯ else 0)
• CategoryTheory.Limits.biproduct.whiskerEquiv_hom_eq_lift 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {K : Type u_1} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {f : J → C} {g : K → C} (e : J ≃ K) (w : (j : J) → g (e j) ≅ f j) [CategoryTheory.Limits.HasBiproduct f] [CategoryTheory.Limits.HasBiproduct g] : (CategoryTheory.Limits.biproduct.whiskerEquiv e w).hom = CategoryTheory.Limits.biproduct.lift fun k => CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.π f (e.symm k)) (CategoryTheory.CategoryStruct.comp (w (e.symm k)).inv (CategoryTheory.eqToHom ⋯))
• CategoryTheory.Limits.biproduct.whiskerEquiv_inv 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {K : Type u_1} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {f : J → C} {g : K → C} (e : J ≃ K) (w : (j : J) → g (e j) ≅ f j) [CategoryTheory.Limits.HasBiproduct f] [CategoryTheory.Limits.HasBiproduct g] : (CategoryTheory.Limits.biproduct.whiskerEquiv e w).inv = CategoryTheory.Limits.biproduct.desc fun k => CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (w (e.symm k)).hom (CategoryTheory.Limits.biproduct.ι f (e.symm k)))
• CategoryTheory.MonoidalCategory.eqToHom_whiskerRight 📋 Mathlib.CategoryTheory.Monoidal.Category
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {X Y : C} (f : X = Y) (Z : C) : CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.eqToHom f) Z = CategoryTheory.eqToHom ⋯
• CategoryTheory.MonoidalCategory.whiskerLeft_eqToHom 📋 Mathlib.CategoryTheory.Monoidal.Category
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : C) {Y Z : C} (f : Y = Z) : CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.eqToHom f) = CategoryTheory.eqToHom ⋯
• CategoryTheory.MorphismProperty.ContainsIdentities.eqToHom 📋 Mathlib.CategoryTheory.MorphismProperty.Composition
  {C : Type u} [CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) [W.ContainsIdentities] {x y : C} (h : x = y) : W (CategoryTheory.eqToHom h)
• CategoryTheory.PrelaxFunctor.map₂_eqToHom 📋 Mathlib.CategoryTheory.Bicategory.Functor.Prelax
  {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.PrelaxFunctor B C) {x y : B} (f g : x ⟶ y) (hfg : f = g) : F.map₂ (CategoryTheory.eqToHom hfg) = CategoryTheory.eqToHom ⋯
• CategoryTheory.WithTerminal.liftStar_hom 📋 Mathlib.CategoryTheory.WithTerminal.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] {Z : D} (F : CategoryTheory.Functor C D) (M : (x : C) → F.obj x ⟶ Z) (hM : ∀ (x y : C) (f : x ⟶ y), CategoryTheory.CategoryStruct.comp (F.map f) (M y) = M x) : (CategoryTheory.WithTerminal.liftStar F M hM).hom = CategoryTheory.eqToHom ⋯
• CategoryTheory.WithTerminal.liftStar_inv 📋 Mathlib.CategoryTheory.WithTerminal.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] {Z : D} (F : CategoryTheory.Functor C D) (M : (x : C) → F.obj x ⟶ Z) (hM : ∀ (x y : C) (f : x ⟶ y), CategoryTheory.CategoryStruct.comp (F.map f) (M y) = M x) : (CategoryTheory.WithTerminal.liftStar F M hM).inv = CategoryTheory.eqToHom ⋯
• CategoryTheory.MorphismProperty.Comma.eqToHom_left 📋 Mathlib.CategoryTheory.MorphismProperty.Comma
  {A : Type u_1} [CategoryTheory.Category.{v_1, u_1} A] {B : Type u_2} [CategoryTheory.Category.{v_2, u_2} B] {T : Type u_3} [CategoryTheory.Category.{v_3, u_3} T] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} (P : CategoryTheory.MorphismProperty T) (Q : CategoryTheory.MorphismProperty A) (W : CategoryTheory.MorphismProperty B) [Q.IsMultiplicative] [W.IsMultiplicative] {X Y : CategoryTheory.MorphismProperty.Comma L R P Q W} (h : X = Y) : (CategoryTheory.eqToHom h).left = CategoryTheory.eqToHom ⋯
• CategoryTheory.MorphismProperty.Comma.eqToHom_right 📋 Mathlib.CategoryTheory.MorphismProperty.Comma
  {A : Type u_1} [CategoryTheory.Category.{v_1, u_1} A] {B : Type u_2} [CategoryTheory.Category.{v_2, u_2} B] {T : Type u_3} [CategoryTheory.Category.{v_3, u_3} T] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} (P : CategoryTheory.MorphismProperty T) (Q : CategoryTheory.MorphismProperty A) (W : CategoryTheory.MorphismProperty B) [Q.IsMultiplicative] [W.IsMultiplicative] {X Y : CategoryTheory.MorphismProperty.Comma L R P Q W} (h : X = Y) : (CategoryTheory.eqToHom h).right = CategoryTheory.eqToHom ⋯
• CategoryTheory.Functor.Elements.ext 📋 Mathlib.CategoryTheory.Elements
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C (Type w)} (x y : F.Elements) (h₁ : x.fst = y.fst) (h₂ : (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.eqToHom h₁))) x.snd = y.snd) : x = y
• CategoryTheory.Grothendieck.base_eqToHom 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {X Y : CategoryTheory.Grothendieck F} (h : X = Y) : (CategoryTheory.eqToHom h).base = CategoryTheory.eqToHom ⋯
• CategoryTheory.Grothendieck.eqToHom_eq 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {X Y : CategoryTheory.Grothendieck F} (hF : X = Y) : CategoryTheory.eqToHom hF = { base := CategoryTheory.eqToHom ⋯, fiber := CategoryTheory.eqToHom ⋯ }
• CategoryTheory.Grothendieck.id_fiber 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} (X : CategoryTheory.Grothendieck F) : (CategoryTheory.CategoryStruct.id X).fiber = CategoryTheory.eqToHom ⋯
• CategoryTheory.Grothendieck.fiber_eqToHom 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {X Y : CategoryTheory.Grothendieck F} (h : X = Y) : (CategoryTheory.eqToHom h).fiber = CategoryTheory.eqToHom ⋯
• CategoryTheory.Grothendieck.ι_map 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C CategoryTheory.Cat) (c : C) {X✝ Y✝ : ↑(F.obj c)} (f : X✝ ⟶ Y✝) : (CategoryTheory.Grothendieck.ι F c).map f = { base := CategoryTheory.CategoryStruct.id { base := c, fiber := X✝ }.base, fiber := CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) f }
• CategoryTheory.Grothendieck.transportIso_hom_fiber 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} (x : CategoryTheory.Grothendieck F) {c : C} (α : x.base ≅ c) : (x.transportIso α).hom.fiber = CategoryTheory.eqToHom ⋯
• CategoryTheory.Grothendieck.ext 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {X Y : CategoryTheory.Grothendieck F} (f g : X.Hom Y) (w_base : f.base = g.base) (w_fiber : CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) f.fiber = g.fiber) : f = g
• CategoryTheory.Grothendieck.congr 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {X Y : CategoryTheory.Grothendieck F} {f g : X ⟶ Y} (h : f = g) : f.fiber = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) g.fiber
• CategoryTheory.Grothendieck.isoMk_inv_fiber 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {X Y : CategoryTheory.Grothendieck F} (e₁ : X.base ≅ Y.base) (e₂ : (F.map e₁.hom).toFunctor.obj X.fiber ≅ Y.fiber) : (CategoryTheory.Grothendieck.isoMk e₁ e₂).inv.fiber = CategoryTheory.CategoryStruct.comp ((F.map e₁.inv).toFunctor.map e₂.inv) (CategoryTheory.eqToHom ⋯)
• CategoryTheory.Grothendieck.comp_fiber 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {X Y Z : CategoryTheory.Grothendieck F} (f : X ⟶ Y) (g : Y ⟶ Z) : (CategoryTheory.CategoryStruct.comp f g).fiber = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((F.map g.base).toFunctor.map f.fiber) g.fiber)
• CategoryTheory.Grothendieck.functorFrom 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {E : Type u_1} [CategoryTheory.Category.{v_1, u_1} E] (fib : (c : C) → CategoryTheory.Functor (↑(F.obj c)) E) (hom : {c c' : C} → (f : c ⟶ c') → fib c ⟶ (F.map f).toFunctor.comp (fib c')) (hom_id : ∀ (c : C), hom (CategoryTheory.CategoryStruct.id c) = CategoryTheory.eqToHom ⋯) (hom_comp : ∀ (c₁ c₂ c₃ : C) (f : c₁ ⟶ c₂) (g : c₂ ⟶ c₃), hom (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (hom f) (CategoryTheory.CategoryStruct.comp ((F.map f).toFunctor.whiskerLeft (hom g)) (CategoryTheory.eqToHom ⋯))) : CategoryTheory.Functor (CategoryTheory.Grothendieck F) E
• CategoryTheory.Grothendieck.functorFrom_obj 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {E : Type u_1} [CategoryTheory.Category.{v_1, u_1} E] (fib : (c : C) → CategoryTheory.Functor (↑(F.obj c)) E) (hom : {c c' : C} → (f : c ⟶ c') → fib c ⟶ (F.map f).toFunctor.comp (fib c')) (hom_id : ∀ (c : C), hom (CategoryTheory.CategoryStruct.id c) = CategoryTheory.eqToHom ⋯) (hom_comp : ∀ (c₁ c₂ c₃ : C) (f : c₁ ⟶ c₂) (g : c₂ ⟶ c₃), hom (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (hom f) (CategoryTheory.CategoryStruct.comp ((F.map f).toFunctor.whiskerLeft (hom g)) (CategoryTheory.eqToHom ⋯))) (X : CategoryTheory.Grothendieck F) : (CategoryTheory.Grothendieck.functorFrom fib hom hom_id hom_comp).obj X = (fib X.base).obj X.fiber
• CategoryTheory.Grothendieck.ιCompFunctorFrom 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {E : Type u_1} [CategoryTheory.Category.{v_1, u_1} E] (fib : (c : C) → CategoryTheory.Functor (↑(F.obj c)) E) (hom : {c c' : C} → (f : c ⟶ c') → fib c ⟶ (F.map f).toFunctor.comp (fib c')) (hom_id : ∀ (c : C), hom (CategoryTheory.CategoryStruct.id c) = CategoryTheory.eqToHom ⋯) (hom_comp : ∀ (c₁ c₂ c₃ : C) (f : c₁ ⟶ c₂) (g : c₂ ⟶ c₃), hom (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (hom f) (CategoryTheory.CategoryStruct.comp ((F.map f).toFunctor.whiskerLeft (hom g)) (CategoryTheory.eqToHom ⋯))) (c : C) : (CategoryTheory.Grothendieck.ι F c).comp (CategoryTheory.Grothendieck.functorFrom fib (fun {c c'} => hom) hom_id hom_comp) ≅ fib c
• CategoryTheory.Grothendieck.map_map 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F G : CategoryTheory.Functor C CategoryTheory.Cat} {α : F ⟶ G} {X Y : CategoryTheory.Grothendieck F} {f : X ⟶ Y} : (CategoryTheory.Grothendieck.map α).map f = { base := f.base, fiber := CategoryTheory.CategoryStruct.comp ((CategoryTheory.eqToHom ⋯).toNatTrans.app X.fiber) ((α.app Y.base).toFunctor.map f.fiber) }
• CategoryTheory.Grothendieck.functorFrom_map 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} {E : Type u_1} [CategoryTheory.Category.{v_1, u_1} E] (fib : (c : C) → CategoryTheory.Functor (↑(F.obj c)) E) (hom : {c c' : C} → (f : c ⟶ c') → fib c ⟶ (F.map f).toFunctor.comp (fib c')) (hom_id : ∀ (c : C), hom (CategoryTheory.CategoryStruct.id c) = CategoryTheory.eqToHom ⋯) (hom_comp : ∀ (c₁ c₂ c₃ : C) (f : c₁ ⟶ c₂) (g : c₂ ⟶ c₃), hom (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (hom f) (CategoryTheory.CategoryStruct.comp ((F.map f).toFunctor.whiskerLeft (hom g)) (CategoryTheory.eqToHom ⋯))) {X Y : CategoryTheory.Grothendieck F} (f : X ⟶ Y) : (CategoryTheory.Grothendieck.functorFrom fib hom hom_id hom_comp).map f = CategoryTheory.CategoryStruct.comp ((hom f.base).app X.fiber) ((fib Y.base).map f.fiber)
• CategoryTheory.Grothendieck.ιCompMap_hom_app_fiber 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F F' : CategoryTheory.Functor C CategoryTheory.Cat} (α : F ⟶ F') (c : C) (X : ↑(F.obj c)) : ((CategoryTheory.Grothendieck.ιCompMap α c).hom.app X).fiber = CategoryTheory.eqToHom ⋯
• CategoryTheory.Grothendieck.ιCompMap_inv_app_fiber 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F F' : CategoryTheory.Functor C CategoryTheory.Cat} (α : F ⟶ F') (c : C) (X : ↑(F.obj c)) : ((CategoryTheory.Grothendieck.ιCompMap α c).inv.app X).fiber = CategoryTheory.eqToHom ⋯
• CategoryTheory.Grothendieck.grothendieckTypeToCat_unitIso_hom_app_fiber 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] (G : CategoryTheory.Functor C (Type w)) (X : CategoryTheory.Grothendieck (G.comp CategoryTheory.typeToCat)) : ((CategoryTheory.Grothendieck.grothendieckTypeToCat G).unitIso.hom.app X).fiber = CategoryTheory.eqToHom ⋯
• CategoryTheory.Grothendieck.grothendieckTypeToCat_unitIso_inv_app_fiber 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] (G : CategoryTheory.Functor C (Type w)) (X : CategoryTheory.Grothendieck (G.comp CategoryTheory.typeToCat)) : ((CategoryTheory.Grothendieck.grothendieckTypeToCat G).unitIso.inv.app X).fiber = CategoryTheory.eqToHom ⋯
• CategoryTheory.Grothendieck.map_map_fiber 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F G : CategoryTheory.Functor C CategoryTheory.Cat} (α : F ⟶ G) {X Y : CategoryTheory.Grothendieck F} (f : X ⟶ Y) : ((CategoryTheory.Grothendieck.map α).map f).fiber = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) ((α.app Y.base).toFunctor.map f.fiber)
• CategoryTheory.cokernel.π_op 📋 Mathlib.CategoryTheory.Abelian.Opposite
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {X Y : C} (f : X ⟶ Y) : (CategoryTheory.Limits.cokernel.π f.op).unop = CategoryTheory.CategoryStruct.comp (CategoryTheory.cokernelOpUnop f).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι f) (CategoryTheory.eqToHom ⋯))
• CategoryTheory.kernel.ι_unop 📋 Mathlib.CategoryTheory.Abelian.Opposite
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {A B : Cᵒᵖ} (g : A ⟶ B) : (CategoryTheory.Limits.kernel.ι g.unop).op = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.π g) (CategoryTheory.kernelUnopOp g).inv)
• CategoryTheory.cokernel.π_unop 📋 Mathlib.CategoryTheory.Abelian.Opposite
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {A B : Cᵒᵖ} (g : A ⟶ B) : (CategoryTheory.Limits.cokernel.π g.unop).op = CategoryTheory.CategoryStruct.comp (CategoryTheory.cokernelUnopOp g).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι g) (CategoryTheory.eqToHom ⋯))
• CategoryTheory.kernel.ι_op 📋 Mathlib.CategoryTheory.Abelian.Opposite
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {X Y : C} (f : X ⟶ Y) : (CategoryTheory.Limits.kernel.ι f.op).unop = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.π f) (CategoryTheory.kernelOpUnop f).inv)
• CategoryTheory.Subobject.arrow_congr 📋 Mathlib.CategoryTheory.Subobject.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {A : C} (X Y : CategoryTheory.Subobject A) (h : X = Y) : CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) Y.arrow = X.arrow
• CategoryTheory.OverPresheafAux.YonedaCollection.ext 📋 Mathlib.CategoryTheory.Comma.Presheaf.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} {F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)} {X : C} {p q : CategoryTheory.OverPresheafAux.YonedaCollection F X} (h : p.fst = q.fst) (h' : (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.eqToHom ⋯))) q.snd = p.snd) : p = q
• CategoryTheory.OverPresheafAux.YonedaCollection.mk_snd 📋 Mathlib.CategoryTheory.Comma.Presheaf.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} {F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)} {X : C} (s : CategoryTheory.yoneda.obj X ⟶ A) (x : F.obj (Opposite.op (CategoryTheory.CostructuredArrow.mk s))) : (CategoryTheory.OverPresheafAux.YonedaCollection.mk s x).snd = (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.eqToHom ⋯))) x
• CategoryTheory.OverPresheafAux.YonedaCollection.map₂_snd 📋 Mathlib.CategoryTheory.Comma.Presheaf.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} {F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)} {X Y : C} (f : X ⟶ Y) (p : CategoryTheory.OverPresheafAux.YonedaCollection F Y) : (CategoryTheory.OverPresheafAux.YonedaCollection.map₂ F f p).snd = (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.CategoryStruct.comp (CategoryTheory.CostructuredArrow.mkPrecomp p.fst f).op (CategoryTheory.eqToHom ⋯)))) p.snd
• CategoryTheory.OverPresheafAux.counitForward_val_snd 📋 Mathlib.CategoryTheory.Comma.Presheaf.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} {F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)} (s : CategoryTheory.CostructuredArrow CategoryTheory.yoneda A) (x : F.obj (Opposite.op s)) : CategoryTheory.OverPresheafAux.YonedaCollection.snd (CategoryTheory.OverPresheafAux.counitForward F s x).val = (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.eqToHom ⋯))) x
• CategoryTheory.OverPresheafAux.YonedaCollection.map₁_snd 📋 Mathlib.CategoryTheory.Comma.Presheaf.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} {F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)} {X : C} {G : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)} (η : F ⟶ G) (p : CategoryTheory.OverPresheafAux.YonedaCollection F X) : (CategoryTheory.OverPresheafAux.YonedaCollection.map₁ η p).snd = (CategoryTheory.ConcreteCategory.hom (G.map (CategoryTheory.eqToHom ⋯))) ((CategoryTheory.ConcreteCategory.hom (η.app (Opposite.op (CategoryTheory.CostructuredArrow.mk p.fst)))) p.snd)

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using the Loogle command from the command palette. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. By subexpression:
   🔍 _ * (_ ^ _)
   finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

   The pattern can also be non-linear, as in
   🔍 Real.sqrt ?a * Real.sqrt ?a

   If the pattern has parameters, they are matched in any order. Both of these will find List.map:
   🔍 (?a -> ?b) -> List ?a -> List ?b
   🔍 List ?a -> (?a -> ?b) -> List ?b

4. By main conclusion:
   🔍 |- tsum _ = _ * tsum _
   finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

   As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
   🔍 |- _ < _ → tsum _ < tsum _
   will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

5. You can filter for definitions vs theorems: Using ⊢ (_ : Type _) finds all definitions which provide data while ⊢ (_ : Prop) finds all theorems (and definitions of proofs).

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO. Please review the Lean FRO Terms of Use and Privacy Policy.

This is Loogle revision 9f11169 serving mathlib revision ce5dd8c