Documentation Verification Report

PureCoherence

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

Statistics

Metric	Count
Definitions `instMkEqOfNaturalityMonoidalM`, `instMonadNormalizeNaturalityMonoidalM`, `normalizeIsoComp`, `pureCoherence`, `tacticMonoidal_coherence`	5
Theorems `mk_eq_of_naturality`, `naturality_associator`, `naturality_comp`, `naturality_id`, `naturality_inv`, `naturality_leftUnitor`, `naturality_rightUnitor`, `naturality_tensorHom`, `naturality_whiskerLeft`, `naturality_whiskerRight`, `of_normalize_eq`	11
Total	16

Mathlib.Tactic.Monoidal

Definitions

Name	Category	Theorems
`instMkEqOfNaturalityMonoidalM` 📖	CompOp	—
`instMonadNormalizeNaturalityMonoidalM` 📖	CompOp	—
`normalizeIsoComp` 📖	CompOp	6 math math: `naturality_associator`, `naturality_whiskerLeft`, `naturality_rightUnitor`, `naturality_tensorHom`, `naturality_leftUnitor`, `naturality_whiskerRight`
`pureCoherence` 📖	CompOp	—
`tacticMonoidal_coherence` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mk_eq_of_naturality` 📖	—	`CategoryTheory.Iso.hom` `CategoryTheory.Iso.trans` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.MonoidalCategory.whiskerLeftIso`	—	—	`Mathlib.Tactic.Reassoc.eq_whisker'` `CategoryTheory.MonoidalCategory.id_whiskerLeft` `CategoryTheory.Category.assoc` `CategoryTheory.Iso.hom_inv_id_assoc` `CategoryTheory.Iso.inv_hom_id` `CategoryTheory.Category.comp_id` `CategoryTheory.Iso.inv_hom_id_assoc`
`naturality_associator` 📖	mathematical	—	`CategoryTheory.Iso.trans` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalCategory.whiskerLeftIso` `CategoryTheory.MonoidalCategoryStruct.associator` `normalizeIsoComp`	—	`CategoryTheory.Iso.ext` `CategoryTheory.MonoidalCategory.whiskerRight_tensor` `CategoryTheory.Category.assoc` `CategoryTheory.Iso.hom_inv_id_assoc` `CategoryTheory.MonoidalCategory.pentagon_hom_inv_inv_inv_inv_assoc` `CategoryTheory.MonoidalCategory.whiskerRightIso_trans` `CategoryTheory.Iso.trans_assoc`
`naturality_comp` 📖	—	`CategoryTheory.Iso.trans` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalCategory.whiskerLeftIso`	—	—	`CategoryTheory.MonoidalCategory.whiskerLeftIso_trans` `CategoryTheory.Iso.trans_assoc`
`naturality_id` 📖	mathematical	—	`CategoryTheory.Iso.trans` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalCategory.whiskerLeftIso` `CategoryTheory.Iso.refl`	—	`CategoryTheory.MonoidalCategory.whiskerLeftIso_refl` `CategoryTheory.Iso.refl_trans`
`naturality_inv` 📖	mathematical	`CategoryTheory.Iso.trans` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalCategory.whiskerLeftIso`	`CategoryTheory.Iso.symm`	—	`CategoryTheory.Iso.ext` `CategoryTheory.MonoidalCategory.whiskerLeft_inv_hom_assoc`
`naturality_leftUnitor` 📖	mathematical	—	`CategoryTheory.Iso.trans` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.MonoidalCategory.whiskerLeftIso` `CategoryTheory.MonoidalCategoryStruct.leftUnitor` `normalizeIsoComp` `CategoryTheory.MonoidalCategoryStruct.rightUnitor`	—	`CategoryTheory.Iso.ext` `CategoryTheory.MonoidalCategory.triangle_assoc_comp_right_assoc`
`naturality_rightUnitor` 📖	mathematical	—	`CategoryTheory.Iso.trans` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.MonoidalCategory.whiskerLeftIso` `CategoryTheory.MonoidalCategoryStruct.rightUnitor` `normalizeIsoComp`	—	`CategoryTheory.Iso.ext` `CategoryTheory.MonoidalCategory.whiskerLeft_rightUnitor` `CategoryTheory.Category.assoc` `CategoryTheory.MonoidalCategory.whiskerRight_id` `CategoryTheory.Iso.inv_hom_id` `CategoryTheory.Category.comp_id`
`naturality_tensorHom` 📖	mathematical	`CategoryTheory.Iso.trans` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalCategory.whiskerLeftIso`	`CategoryTheory.MonoidalCategory.tensorIso` `normalizeIsoComp`	—	`CategoryTheory.MonoidalCategory.tensorIso_def` `naturality_comp` `naturality_whiskerRight` `naturality_whiskerLeft`
`naturality_whiskerLeft` 📖	mathematical	`CategoryTheory.Iso.trans` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalCategory.whiskerLeftIso`	`normalizeIsoComp`	—	`CategoryTheory.Iso.ext` `CategoryTheory.MonoidalCategory.tensor_whiskerLeft` `CategoryTheory.Category.assoc` `CategoryTheory.Iso.inv_hom_id_assoc`
`naturality_whiskerRight` 📖	mathematical	`CategoryTheory.Iso.trans` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalCategory.whiskerLeftIso`	`CategoryTheory.MonoidalCategory.whiskerRightIso` `normalizeIsoComp`	—	`CategoryTheory.Iso.ext` `CategoryTheory.MonoidalCategory.whiskerRightIso_trans` `CategoryTheory.Iso.trans_assoc` `CategoryTheory.MonoidalCategory.whisker_assoc` `CategoryTheory.Category.assoc` `CategoryTheory.Iso.inv_hom_id_assoc`
`of_normalize_eq` 📖	—	`CategoryTheory.Iso.trans` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.MonoidalCategory.whiskerLeftIso`	—	—	`CategoryTheory.Iso.ext` `Mathlib.Tactic.Reassoc.eq_whisker'` `CategoryTheory.MonoidalCategory.id_whiskerLeft` `CategoryTheory.Category.assoc` `CategoryTheory.Iso.hom_inv_id_assoc` `CategoryTheory.Iso.inv_hom_id` `CategoryTheory.Category.comp_id` `CategoryTheory.Iso.inv_hom_id_assoc`

---

← Back to Index