Commit 2023-01-17 07:00 5fcca7a8

View on Github →

chore: adjust Nat.le_induction for compatibility with induction tactic (#1611) See Zulip.

Estimated changes

Modified Mathlib/Data/Nat/Basic.lean

modified theorem Nat.le_induction

Modified Mathlib/Data/Set/Pointwise/Basic.lean

modified theorem Set.pow_subset_pow_of_one_mem