Commit 2024-05-13 07:14 89b382e9

View on Github →

feat: backport adaptations for nightly-2024-05-11 (#12854) In https://github.com/leanprover/lean4/pull/4061, well-founded definitions become irreducible by default, and hence some rfl proofs stop working. This pre-emptively backports some of the adaptations from #12853.

Estimated changes

Modified Mathlib/Data/LazyList/Basic.lean

modified theorem LazyList.mem_nil

Modified Mathlib/Data/List/Indexes.lean

Modified Mathlib/Data/List/OfFn.lean

Modified Mathlib/Data/List/Sym.lean

Modified Mathlib/Data/Nat/Bitwise.lean

modified theorem Nat.bitwise_zero_left

Modified Mathlib/Data/Nat/Fib/Zeckendorf.lean

added theorem List.IsZeckendorfRep_nil

modified theorem Nat.sum_zeckendorf_fib

modified theorem Nat.zeckendorf_succ

modified theorem Nat.zeckendorf_zero

Modified Mathlib/Data/Nat/Prime.lean

modified theorem Nat.minFac_one

Modified Mathlib/Data/Num/Prime.lean

Modified Mathlib/Data/String/Basic.lean

Modified Mathlib/Data/Vector/Basic.lean