Commit 2026-08-16 19:51 29e01041

View on Github →

feat(Data/List): add TFAE lemmas for append and permutations (#41022) This PR adds some TFAE lemmas in Mathlib/Data/List/TFAE: a sublist monotonicity lemma, an append criterion, and congruence under list permutations. It also rewrites tfae_cons_of_mem as a specialization of the append lemma. Created with the help of codex.

Estimated changes

added theorem List.tfae_append
added theorem List.tfae_concat
added theorem List.tfae_cons
added theorem List.tfae_cons_cons
added theorem List.tfae_cons_of_mem
added theorem List.tfae_cons_self
added theorem List.tfae_iff_pairwise
added theorem List.tfae_of_cycle
added theorem List.Perm.tfae_iff
added theorem List.TFAE.subset
added theorem List.tfae_congr
deleted theorem List.tfae_cons_cons
deleted theorem List.tfae_cons_of_mem
deleted theorem List.tfae_cons_self
modified theorem List.tfae_not_iff
deleted theorem List.tfae_of_cycle
modified theorem List.tfae_of_forall
added theorem List.tfae_reverse