Normalize

📁 Source: Mathlib/Tactic/CategoryTheory/Monoidal/Normalize.lean

Statistics

Metric	Count
Definitions instMkEvalCompMonoidalM, instMkEvalHorizontalCompMonoidalM, instMkEvalMonoidalM, instMkEvalWhiskerLeftMonoidalM, instMkEvalWhiskerRightMonoidalM, instMkMor₂MonoidalM_1, instMonadNormalExprMonoidalM	7
Theorems evalComp_cons, evalComp_nil_cons, evalComp_nil_nil, evalHorizontalCompAux'_of_whisker, evalHorizontalCompAux'_whisker, evalHorizontalCompAux_cons, evalHorizontalCompAux_of, evalHorizontalComp_cons_cons, evalHorizontalComp_cons_nil, evalHorizontalComp_nil_cons, evalHorizontalComp_nil_nil, evalWhiskerLeft_comp, evalWhiskerLeft_id, evalWhiskerLeft_nil, evalWhiskerLeft_of_cons, evalWhiskerRightAux_cons, evalWhiskerRightAux_of, evalWhiskerRight_comp, evalWhiskerRight_cons_of, evalWhiskerRight_cons_of_of, evalWhiskerRight_cons_whisker, evalWhiskerRight_id, evalWhiskerRight_nil, eval_comp, eval_monoidalComp, eval_of, eval_tensorHom, eval_whiskerLeft, eval_whiskerRight	29
Total	36

Mathlib.Tactic.Monoidal

Definitions

Name	Category	Theorems
instMkEvalCompMonoidalM 📖	CompOp	—
instMkEvalHorizontalCompMonoidalM 📖	CompOp	—
instMkEvalMonoidalM 📖	CompOp	—
instMkEvalWhiskerLeftMonoidalM 📖	CompOp	—
instMkEvalWhiskerRightMonoidalM 📖	CompOp	—
instMkMor₂MonoidalM_1 📖	CompOp	—
instMonadNormalExprMonoidalM 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
evalComp_cons 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.Iso.hom	—	CategoryTheory.Category.assoc
evalComp_nil_cons 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Iso.hom CategoryTheory.Iso.trans	—	CategoryTheory.Category.assoc
evalComp_nil_nil 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.Iso.trans	—	—
evalHorizontalCompAux'_of_whisker 📖	mathematical	CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Iso.hom CategoryTheory.Iso.refl CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.Iso.inv	CategoryTheory.MonoidalCategoryStruct.whiskerLeft	—	CategoryTheory.MonoidalCategory.tensorHom_def CategoryTheory.MonoidalCategory.whiskerRight_tensor CategoryTheory.Category.assoc CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp CategoryTheory.MonoidalCategory.tensor_whiskerLeft CategoryTheory.Iso.inv_hom_id
evalHorizontalCompAux'_whisker 📖	—	CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.Iso.hom	—	—	CategoryTheory.MonoidalCategory.tensorHom_def CategoryTheory.MonoidalCategory.whisker_assoc CategoryTheory.MonoidalCategory.tensor_whiskerLeft CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id_assoc CategoryTheory.MonoidalCategory.whiskerLeft_comp
evalHorizontalCompAux_cons 📖	—	CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Iso.hom CategoryTheory.Iso.refl CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.associator	—	—	CategoryTheory.MonoidalCategory.associator_conjugation CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
evalHorizontalCompAux_of 📖	mathematical	—	CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Iso.hom CategoryTheory.Iso.refl	—	CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
evalHorizontalComp_cons_cons 📖	—	CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Iso.hom CategoryTheory.MonoidalCategory.tensorIso	—	—	CategoryTheory.MonoidalCategory.tensorHom_comp_tensorHom
evalHorizontalComp_cons_nil 📖	mathematical	CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Iso.hom CategoryTheory.Iso.refl CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.tensorIso	CategoryTheory.MonoidalCategoryStruct.tensorHom	—	CategoryTheory.MonoidalCategory.tensorHom_def' CategoryTheory.MonoidalCategory.comp_whiskerRight CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp CategoryTheory.Category.assoc
evalHorizontalComp_nil_cons 📖	mathematical	CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Iso.hom CategoryTheory.Iso.refl CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.tensorIso	CategoryTheory.MonoidalCategoryStruct.tensorHom	—	CategoryTheory.MonoidalCategory.tensorHom_def CategoryTheory.MonoidalCategory.whiskerLeft_comp CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp CategoryTheory.Category.assoc
evalHorizontalComp_nil_nil 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategory.tensorIso	—	—
evalWhiskerLeft_comp 📖	—	CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.Iso.hom	—	—	CategoryTheory.MonoidalCategory.tensor_whiskerLeft
evalWhiskerLeft_id 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.leftUnitor CategoryTheory.Iso.hom	CategoryTheory.MonoidalCategoryStruct.whiskerLeft	—	CategoryTheory.MonoidalCategory.id_whiskerLeft
evalWhiskerLeft_nil 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategory.whiskerLeftIso	—	—
evalWhiskerLeft_of_cons 📖	mathematical	CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.whiskerLeftIso	—	CategoryTheory.MonoidalCategory.whiskerLeft_comp
evalWhiskerRightAux_cons 📖	—	CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Iso.hom CategoryTheory.Iso.refl CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.associator	—	—	CategoryTheory.MonoidalCategory.tensorHom_def CategoryTheory.MonoidalCategory.comp_whiskerRight CategoryTheory.MonoidalCategory.whisker_assoc CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp CategoryTheory.MonoidalCategory.whiskerRight_tensor CategoryTheory.Category.assoc CategoryTheory.Iso.hom_inv_id_assoc
evalWhiskerRightAux_of 📖	mathematical	—	CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Iso.hom CategoryTheory.Iso.refl	—	CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
evalWhiskerRight_comp 📖	—	CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.Iso.inv	—	—	CategoryTheory.MonoidalCategory.whiskerRight_tensor
evalWhiskerRight_cons_of 📖	—	CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Iso.hom CategoryTheory.MonoidalCategory.whiskerRightIso	—	—	CategoryTheory.MonoidalCategory.comp_whiskerRight
evalWhiskerRight_cons_of_of 📖	—	CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Iso.hom CategoryTheory.MonoidalCategory.whiskerRightIso	—	—	CategoryTheory.MonoidalCategory.comp_whiskerRight
evalWhiskerRight_cons_whisker 📖	—	CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Iso.hom CategoryTheory.Iso.refl CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.MonoidalCategory.whiskerRightIso	—	—	CategoryTheory.MonoidalCategory.comp_whiskerRight CategoryTheory.MonoidalCategory.whisker_assoc CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp CategoryTheory.Category.assoc
evalWhiskerRight_id 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.rightUnitor CategoryTheory.Iso.hom	CategoryTheory.MonoidalCategoryStruct.whiskerRight	—	CategoryTheory.MonoidalCategory.whiskerRight_id
evalWhiskerRight_nil 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategory.whiskerRightIso	—	—
eval_comp 📖	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	—	—
eval_monoidalComp 📖	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Iso.hom	—	—	—
eval_of 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Iso.hom CategoryTheory.Iso.refl	—	CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
eval_tensorHom 📖	—	CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct	—	—	—
eval_whiskerLeft 📖	—	CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct	—	—	—
eval_whiskerRight 📖	—	CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct	—	—	—

---

← Back to Index