Commit 2024-07-25 09:37 a54cd21b

View on Github →

chore: robustifying for debug.byAsSorry (part 2) (#15119) Followup to #14993. Hopefully these are all independently positive or neutral. These help get Mathlib compiling under set_option debug.byAsSorry true.

Estimated changes

Modified Mathlib/Algebra/Group/Subsemigroup/Operations.lean

modified def Subsemigroup.gciMapComap

Modified Mathlib/Algebra/Order/GroupWithZero/Canonical.lean

Modified Mathlib/Algebra/Order/Monoid/Unbundled/Pow.lean

Modified Mathlib/Algebra/Regular/Basic.lean

Modified Mathlib/CategoryTheory/Adjunction/Basic.lean

modified def CategoryTheory.Adjunction.adjunctionOfEquivRight

modified def CategoryTheory.Adjunction.leftAdjointOfEquiv

modified def CategoryTheory.Adjunction.rightAdjointOfEquiv

Modified Mathlib/CategoryTheory/Bicategory/Basic.lean

Modified Mathlib/CategoryTheory/Endomorphism.lean

Modified Mathlib/CategoryTheory/Quotient.lean

modified def CategoryTheory.Quotient.lift

Modified Mathlib/Data/List/EditDistance/Defs.lean

Modified Mathlib/Data/Multiset/Basic.lean

Modified Mathlib/Order/Bounds/Basic.lean

Modified Mathlib/Order/Interval/Set/Pi.lean

Modified Mathlib/Order/Minimal.lean

modified theorem mem_minimals_iff

Modified Mathlib/Order/ModularLattice.lean