Commit 2023-06-28 05:50 e703ae87

View on Github →

chore: better TypeMax instances for limits in Type (#5535) Preliminary to the full forward port of https://github.com/leanprover-community/mathlib/pull/19153, this is a slight generalization along with explanation of the problem with the instances.

Estimated changes

Modified Mathlib/CategoryTheory/Limits/Shapes/Types.lean

added theorem CategoryTheory.Limits.Types.pi_lift_π_apply'

modified theorem CategoryTheory.Limits.Types.pi_lift_π_apply

added theorem CategoryTheory.Limits.Types.pi_map_π_apply'

modified theorem CategoryTheory.Limits.Types.pi_map_π_apply

modified theorem CategoryTheory.Limits.Types.productIso_hom_comp_eval

modified theorem CategoryTheory.Limits.Types.productIso_inv_comp_π

modified def CategoryTheory.Limits.Types.productLimitCone

Modified Mathlib/CategoryTheory/Limits/Types.lean

Modified Mathlib/Topology/Sheaves/SheafCondition/UniqueGluing.lean