Commit 2023-03-04 09:18 f2a5deba

View on Github →

chore: address some porting notes mentioning congr (#2595) Switch to using congr! instead, which is analogous to mathlib 3's congr'.

Estimated changes

Modified Mathlib/CategoryTheory/Limits/Preserves/Basic.lean

modified def CategoryTheory.Limits.isLimitOfReflects

Modified Mathlib/Combinatorics/SimpleGraph/Subgraph.lean

Modified Mathlib/Data/List/Basic.lean

Modified Mathlib/Data/PNat/Factors.lean

Modified Mathlib/Order/SupIndep.lean

Modified Mathlib/Topology/CompactOpen.lean