feat: add Finset.cons_swap (#17413)

``` (s.cons a _).cons b _ = (s.cons b _).cons a _ ``` Co-authored-by: qawbecrdtey <[email protected]> Co-authored-by: qawbecrdtey <[email protected]>
leanprover-community · Oct 6, 2024 · 54d30b7 · 54d30b7
1 parent eb8e7ea
commit 54d30b7
Showing 1 changed file with 6 additions and 1 deletion.
diff --git a/Mathlib/Data/Finset/Basic.lean b/Mathlib/Data/Finset/Basic.lean
@@ -807,6 +807,11 @@ theorem ssubset_iff_exists_cons_subset : s ⊂ t ↔ ∃ (a : _) (h : a ∉ s),
   obtain ⟨a, hs, ht⟩ := not_subset.1 h.2
   exact ⟨a, ht, cons_subset.2 ⟨hs, h.subset⟩⟩
 
+theorem cons_swap (hb : b ∉ s) (ha : a ∉ s.cons b hb) :
+    (s.cons b hb).cons a ha = (s.cons a fun h ↦ ha (mem_cons.mpr (.inr h))).cons b fun h ↦
+      ha (mem_cons.mpr (.inl ((mem_cons.mp h).elim symm (fun h ↦ False.elim (hb h))))) :=
+  eq_of_veq <| Multiset.cons_swap a b s.val
+
 end Cons
 
 /-! ### disjoint -/
@@ -3093,4 +3098,4 @@ def proveFinsetNonempty {u : Level} {α : Q(Type u)} (s : Q(Finset $α)) :
 
 end Mathlib.Meta
 
-set_option linter.style.longFile 3100
+set_option linter.style.longFile 3200