Commit 2023-01-25 10:47 71647bc8

View on Github →

Feat: add List.perm_replicate_append_replicate (#1509) This is a forward-port of leanprover-community/mathlib#18126 Also golf a proof.

Estimated changes

Modified Mathlib/Data/List/Basic.lean

Modified Mathlib/Data/List/Perm.lean

modified theorem List.Perm.mem_iff

modified theorem List.Perm.subset

added theorem List.Perm.subset_congr_left

added theorem List.Perm.subset_congr_right

added theorem List.perm_replicate_append_replicate

Modified Mathlib/Logic/Basic.lean

added theorem Decidable.and_forall_ne

modified theorem and_forall_ne