Commit 2024-07-25 23:15 7865b704

View on Github →

chore: more adaptations for debugAsSorry (#15133)

Estimated changes

Modified Mathlib/Algebra/Order/Interval/Basic.lean

Modified Mathlib/Order/Atoms.lean

Modified Mathlib/Order/Interval/Finset/Nat.lean

modified theorem Nat.cauchy_induction'

modified theorem Nat.cauchy_induction_mul

Modified Mathlib/Order/SuccPred/Relation.lean