feat: some finset lemmas (#13686)

* From the Sobolev inequality project
* The increase in imports in `Mathlib.Data.Finset.Update` is not problematic: it is only imported in MeasureTheory files.
* Add `DepRewrite` to `Tactic.Common`.
* Change the normal form of `{x} ∪ {y}` to `{x, y}` (previously `{y, x}`).

Co-authored-by: Heather Macbeth 25316162+hrmacbeth@users.noreply.github.com

Author: fpvandoorn

Mathlib/Algebra/Group/Finsupp.lean

@@ -153,7 +153,7 @@ lemma support_single_add_single [DecidableEq ι] {f₁ f₂ : ι} {g₁ g₂ : M
     (H : f₁ ≠ f₂) (hg₁ : g₁ ≠ 0) (hg₂ : g₂ ≠ 0) :
     (single f₁ g₁ + single f₂ g₂).support = {f₁, f₂} := by
   rw [support_add_eq, support_single_ne_zero _ hg₁, support_single_ne_zero _ hg₂]
-  · simp [pair_comm f₂ f₁]
+  · simp
   · simp [support_single_ne_zero, *]
 
 lemma support_single_add_single_subset [DecidableEq ι] {f₁ f₂ : ι} {g₁ g₂ : M} :

Mathlib/Combinatorics/SimpleGraph/StronglyRegular.lean

@@ -113,7 +113,7 @@ theorem compl_neighborFinset_sdiff_inter_eq {v w : V} :
 theorem sdiff_compl_neighborFinset_inter_eq {v w : V} (h : G.Adj v w) :
     ((G.neighborFinset v)ᶜ ∩ (G.neighborFinset w)ᶜ) \ ({w} ∪ {v}) =
       (G.neighborFinset v)ᶜ ∩ (G.neighborFinset w)ᶜ := by
-  simpa using ⟨(adj_symm _ h), h⟩
+  simpa using ⟨h, adj_symm _ h⟩
 
 theorem IsSRGWith.compl_is_regular (h : G.IsSRGWith n k ℓ μ) :
     Gᶜ.IsRegularOfDegree (n - k - 1) := by

Mathlib/Data/Finset/Basic.lean

@@ -582,22 +582,49 @@ def Finset.union (s t : Finset α) (h : Disjoint s t) :
   Equiv.setCongr (coe_union _ _) |>.trans (Equiv.Set.union (disjoint_coe.mpr h)) |>.symm
 
 @[simp]
-theorem Finset.union_symm_inl (h : Disjoint s t) (x : s) :
+theorem Finset.union_inl (h : Disjoint s t) (x : s) :
     Equiv.Finset.union s t h (Sum.inl x) = ⟨x, Finset.mem_union.mpr <| Or.inl x.2⟩ :=
   rfl
 
 @[simp]
-theorem Finset.union_symm_inr (h : Disjoint s t) (y : t) :
+theorem Finset.union_inr (h : Disjoint s t) (y : t) :
     Equiv.Finset.union s t h (Sum.inr y) = ⟨y, Finset.mem_union.mpr <| Or.inr y.2⟩ :=
   rfl
 
+@[deprecated (since := "2024-06-07")] alias Finset.union_symm_inl := Finset.union_inl
+@[deprecated (since := "2024-06-07")] alias Finset.union_symm_inr := Finset.union_inr
+
+@[simp]
+theorem Finset.union_symm_left (h : Disjoint s t) {i : α} (hi : i ∈ s)
+    (hi' : i ∈ s ∪ t) : (Equiv.Finset.union s t h).symm ⟨i, hi'⟩ = Sum.inl ⟨i, hi⟩ := by
+  simp [Equiv.symm_apply_eq]
+
+@[simp]
+theorem Finset.union_symm_right (h : Disjoint s t) {i : α} (hi : i ∈ t)
+    (hi' : i ∈ s ∪ t) : (Equiv.Finset.union s t h).symm ⟨i, hi'⟩ = Sum.inr ⟨i, hi⟩ := by
+  simp [Equiv.symm_apply_eq]
+
 /-- The type of dependent functions on the disjoint union of finsets `s ∪ t` is equivalent to the
   type of pairs of functions on `s` and on `t`. This is similar to `Equiv.sumPiEquivProdPi`. -/
 def piFinsetUnion {ι} [DecidableEq ι] (α : ι → Type*) {s t : Finset ι} (h : Disjoint s t) :
     ((∀ i : s, α i) × ∀ i : t, α i) ≃ ∀ i : (s ∪ t : Finset ι), α i :=
   let e := Equiv.Finset.union s t h
   sumPiEquivProdPi (fun b ↦ α (e b)) |>.symm.trans (.piCongrLeft (fun i : ↥(s ∪ t) ↦ α i) e)
 
+lemma piFinsetUnion_left {ι} [DecidableEq ι] (α : ι → Type*) {s t : Finset ι}
+    (h : Disjoint s t) {f g} {i : ι} (hi : i ∈ s) (hi' : i ∈ s ∪ t) :
+    piFinsetUnion α h (f, g) ⟨i, hi'⟩ = f ⟨i, hi⟩ := by
+  simp_rw [piFinsetUnion, sumPiEquivProdPi, piCongrLeft, piCongrLeft', trans_apply, coe_fn_symm_mk]
+  rw! [Finset.union_symm_left h hi hi']
+  rfl
+
+lemma piFinsetUnion_right {ι} [DecidableEq ι] (α : ι → Type*) {s t : Finset ι}
+    (h : Disjoint s t) {f g} {i : ι} (hi : i ∈ t) (hi' : i ∈ s ∪ t) :
+    Equiv.piFinsetUnion α h (f, g) ⟨i, hi'⟩ = g ⟨i, hi⟩ := by
+  simp_rw [piFinsetUnion, sumPiEquivProdPi, piCongrLeft, piCongrLeft', trans_apply, coe_fn_symm_mk]
+  rw! [Finset.union_symm_right h hi hi']
+  rfl
+
 /-- A finset is equivalent to its coercion as a set. -/
 def _root_.Finset.equivToSet (s : Finset α) : s ≃ (s : Set α) where
   toFun a := ⟨a.1, mem_coe.2 a.2⟩

Mathlib/Data/Finset/Lattice/Lemmas.lean

@@ -72,7 +72,10 @@ theorem insert_eq (a : α) (s : Finset α) : insert a s = {a} ∪ s :=
 lemma singleton_union (x : α) (s : Finset α) : {x} ∪ s = insert x s :=
   rfl
 
-@[simp, grind =]
+/- We lower the simp-priority of `union_singleton` to ensure that `{x} ∪ {y}`
+simplifies to `{x, y}` and not `{y, x}`. -/
+
+@[simp 900, grind =]
 lemma union_singleton (x : α) (s : Finset α) : s ∪ {x} = insert x s := by
   rw [Finset.union_comm, singleton_union]
 

Mathlib/Data/Finset/Update.lean

@@ -6,6 +6,7 @@ Authors: Floris van Doorn
 module
 
 public import Mathlib.Data.Finset.Pi
+public import Mathlib.Data.Fintype.Defs
 public import Mathlib.Logic.Function.DependsOn
 
 /-!
@@ -20,6 +21,7 @@ for other purposes.
 
 @[expose] public section
 variable {ι : Sort _} {π : ι → Sort _} {x : ∀ i, π i} [DecidableEq ι]
+  {s t : Finset ι} {y : ∀ i : s, π i} {z : ∀ i : t, π i} {i : ι}
 
 namespace Function
 
@@ -30,22 +32,22 @@ def updateFinset (x : ∀ i, π i) (s : Finset ι) (y : ∀ i : ↥s, π i) (i :
 
 open Finset Equiv
 
-theorem updateFinset_def {s : Finset ι} {y} :
+theorem updateFinset_def :
     updateFinset x s y = fun i ↦ if hi : i ∈ s then y ⟨i, hi⟩ else x i :=
   rfl
 
 @[simp] theorem updateFinset_empty {y} : updateFinset x ∅ y = x :=
   rfl
 
-theorem updateFinset_singleton {i y} :
+theorem updateFinset_singleton {y} :
     updateFinset x {i} y = Function.update x i (y ⟨i, mem_singleton_self i⟩) := by
   congr with j
   by_cases hj : j = i
   · cases hj
     simp only [dif_pos, Finset.mem_singleton, update_self, updateFinset]
   · simp [hj, updateFinset]
 
-theorem update_eq_updateFinset {i y} :
+theorem update_eq_updateFinset {y} :
     Function.update x i y = updateFinset x {i} (uniqueElim y) := by
   congr with j
   by_cases hj : j = i
@@ -71,8 +73,7 @@ theorem _root_.DependsOn.update {α : Type*} {f : (Π i, π i) → α} {s : Fins
   simp_rw [Function.update_eq_updateFinset, erase_eq, coe_sdiff]
   exact hf.updateFinset _
 
-theorem updateFinset_updateFinset {s t : Finset ι} (hst : Disjoint s t)
-    {y : ∀ i : ↥s, π i} {z : ∀ i : ↥t, π i} :
+theorem updateFinset_updateFinset (hst : Disjoint s t) :
     updateFinset (updateFinset x s y) t z =
     updateFinset x (s ∪ t) (Equiv.piFinsetUnion π hst ⟨y, z⟩) := by
   set e := Equiv.Finset.union s t hst
@@ -107,4 +108,22 @@ lemma updateFinset_restrict {s : Finset ι} (x : Π i, π i) :
   ext i
   simp [updateFinset]
 
+-- this would be slightly nicer if we had a version of `Equiv.piFinsetUnion` for `insert`.
+theorem update_updateFinset {z} (hi : i ∉ s) :
+    Function.update (updateFinset x s y) i z = updateFinset x (s ∪ {i})
+      ((Equiv.piFinsetUnion π <| Finset.disjoint_singleton_right.mpr hi) (y, uniqueElim z)) := by
+  rw [update_eq_updateFinset, updateFinset_updateFinset]
+
+theorem updateFinset_congr (h : s = t) :
+    updateFinset x s y = updateFinset x t (fun i ↦ y ⟨i, h ▸ i.prop⟩) := by
+  subst h; rfl
+
+theorem updateFinset_univ [Fintype ι] {y : ∀ i : Finset.univ, π i} :
+    updateFinset x .univ y = fun i : ι ↦ y ⟨i, Finset.mem_univ i⟩ := by
+  simp [updateFinset_def]
+
+theorem updateFinset_univ_apply [Fintype ι] {y : ∀ i : Finset.univ, π i} {i : ι} :
+    updateFinset x .univ y i = y ⟨i, Finset.mem_univ i⟩ := by
+  simp [updateFinset_def]
+
 end Function

Mathlib/RingTheory/MvPolynomial/IrreducibleQuadratic.lean

@@ -220,7 +220,7 @@ theorem irreducible_sumSMulXSMulY [IsDomain R]
   · rwa [MvPolynomial.mem_support_iff, hcoeff, ← Finsupp.mem_support_iff]
   · simp [ι]
   · rw [hsupp, Finset.coe_map, ι.injective.injOn.pairwiseDisjoint_image]
-    suffices (c.support : Set n).PairwiseDisjoint fun x ↦ {Sum.inr x, Sum.inl x} by
+    suffices (c.support : Set n).PairwiseDisjoint fun x ↦ {Sum.inl x, Sum.inr x} by
       simpa [ι, Function.comp_def, Finsupp.support_add_eq, Finsupp.support_single_ne_zero]
     simp [Set.PairwiseDisjoint, Set.Pairwise, ne_comm]
   · intro r hr

Mathlib/Tactic/Common.lean

@@ -55,6 +55,7 @@ public import Mathlib.Tactic.Conv
 public import Mathlib.Tactic.Convert
 public import Mathlib.Tactic.DefEqTransformations
 public import Mathlib.Tactic.DeprecateTo
+public import Mathlib.Tactic.DepRewrite
 public import Mathlib.Tactic.ErwQuestion
 public import Mathlib.Tactic.Eqns
 public import Mathlib.Tactic.ExistsI