Commit 2024-09-09 14:40 f9e5fd45

View on Github →

chore(Order/SuccPred/Limit): improve induction principles (#16575) This PR does the following:

We define isSuccPrelimitRecOn without using tactics, which allows us to golf a proof slightly.
We define prelimitRecOn using cast instead of Eq.subst, which is more idiomatic.
We introduce variants of prelimitRecOn_succ for orders without maximum elements.
Better variable management throughout.

Estimated changes

Modified Mathlib/Order/SuccPred/Limit.lean

modified theorem Order.isPredPrelimitRecOn_limit

modified theorem Order.isPredPrelimitRecOn_pred'

modified theorem Order.isSuccPrelimitRecOn_limit

modified theorem Order.isSuccPrelimitRecOn_succ'

modified theorem Order.isSuccPrelimitRecOn_succ

modified theorem PredOrder.prelimitRecOn_limit

added theorem PredOrder.prelimitRecOn_pred'

modified theorem PredOrder.prelimitRecOn_pred

modified theorem SuccOrder.prelimitRecOn_limit

added theorem SuccOrder.prelimitRecOn_succ'

modified theorem SuccOrder.prelimitRecOn_succ

Modified Mathlib/SetTheory/Ordinal/Arithmetic.lean