Commit 2022-08-24 13:42 9e017ff8
View on Github →feat: port List.length_injective_iff and List.length_injective (#378)
Replace commented-out Lean 3 List.length_injective_iff and List.length_injective lemmas, port them to Lean 4.
Compare to the current mathlib3 versions: https://github.com/leanprover-community/mathlib/blob/6f1ad8258079beb8437c2e402d4218f4e6b7f9f6/src/data/list/basic.lean#L256-L266