feat(Order): lemmas about iSupIndep (#29791)

* generalize `Finset.SupIndep` "bind" operations from `DistribLattice` to `IsModularLattice`
* new lemma `iSupIndep.iInf`
* more characterizations of `iSupIndep` on submodules:
  * `iSupIndep_iff_finset_sum_eq_zero_imp_eq_zero`
  * `iSupIndep_iff_finset_sum_eq_imp_eq`
* add `@[simp]` and `@[grind]` attributes which were helpful for these proofs

Original motivation was to have the following fact:
```lean
theorem iSupIndep_iInf_genEigenspace [NoZeroSMulDivisors R M] {α : Type*} (f : α → End R M)
    (k : ℕ∞) : iSupIndep fun μ : α → R ↦ ⨅ a : α, ((f a).genEigenspace (μ a)) k :=
  .iInf (f · |>.genEigenspace · k) (f · |>.independent_genEigenspace k)
```

Co-authored-by: Aristotle Harmonic <aristotle-harmonic@harmonic.fun>

Author: llllvvuu

Mathlib/Data/Finset/Disjoint.lean

@@ -180,7 +180,7 @@ variable [DecidableEq α] {s t u v : Finset α} {a b : α} {f : α → β}
 theorem disjoint_insert_left : Disjoint (insert a s) t ↔ a ∉ t ∧ Disjoint s t := by
   simp only [disjoint_left, mem_insert, or_imp, forall_and, forall_eq]
 
-@[simp]
+@[simp, grind =]
 theorem disjoint_insert_right : Disjoint s (insert a t) ↔ a ∉ s ∧ Disjoint s t :=
   disjoint_comm.trans <| by rw [disjoint_insert_left, _root_.disjoint_comm]
 

Mathlib/Data/Finset/Lattice/Fold.lean

@@ -52,7 +52,7 @@ theorem sup_empty : (∅ : Finset β).sup f = ⊥ :=
 theorem sup_cons {b : β} (h : b ∉ s) : (cons b s h).sup f = f b ⊔ s.sup f :=
   fold_cons h
 
-@[simp]
+@[simp, grind =]
 theorem sup_insert [DecidableEq β] {b : β} : (insert b s : Finset β).sup f = f b ⊔ s.sup f :=
   fold_insert_idem
 
@@ -109,6 +109,7 @@ lemma isLUB_sup_id {s : Finset α} : IsLUB s (s.sup id) := by simpa using isLUB_
 
 theorem le_sup_of_le {b : β} (hb : b ∈ s) (h : a ≤ f b) : a ≤ s.sup f := h.trans <| le_sup hb
 
+@[grind _=_]
 theorem sup_union [DecidableEq β] : (s₁ ∪ s₂).sup f = s₁.sup f ⊔ s₂.sup f :=
   eq_of_forall_ge_iff fun c => by simp [or_imp, forall_and]
 
@@ -125,11 +126,11 @@ theorem sup_ite (p : β → Prop) [DecidablePred p] :
     (s.sup fun i => ite (p i) (f i) (g i)) = (s.filter p).sup f ⊔ (s.filter fun i => ¬p i).sup g :=
   fold_ite _
 
-@[gcongr]
+@[gcongr, grind ←]
 theorem sup_mono_fun {g : β → α} (h : ∀ b ∈ s, f b ≤ g b) : s.sup f ≤ s.sup g :=
   Finset.sup_le fun b hb => le_trans (h b hb) (le_sup hb)
 
-@[gcongr]
+@[gcongr, grind ←]
 theorem sup_mono (h : s₁ ⊆ s₂) : s₁.sup f ≤ s₂.sup f :=
   Finset.sup_le (fun _ hb => le_sup (h hb))
 

Mathlib/Data/Finset/Lattice/Union.lean

@@ -27,7 +27,7 @@ section Sup
 
 variable [SemilatticeSup α] [OrderBot α]
 
-@[simp]
+@[simp, grind =]
 theorem sup_biUnion [DecidableEq β] (s : Finset γ) (t : γ → Finset β) :
     (s.biUnion t).sup f = s.sup fun x => (t x).sup f :=
   eq_of_forall_ge_iff fun c => by simp [@forall_swap _ β]
@@ -38,7 +38,7 @@ section Inf
 
 variable [SemilatticeInf α] [OrderTop α]
 
-@[simp] theorem inf_biUnion [DecidableEq β] (s : Finset γ) (t : γ → Finset β) :
+@[simp, grind =] theorem inf_biUnion [DecidableEq β] (s : Finset γ) (t : γ → Finset β) :
     (s.biUnion t).inf f = s.inf fun x => (t x).inf f :=
   @sup_biUnion αᵒᵈ _ _ _ _ _ _ _ _
 

Mathlib/Data/Finset/Sigma.lean

@@ -43,7 +43,7 @@ protected def sigma : Finset (Σ i, α i) :=
 
 variable {s s₁ s₂ t t₁ t₂}
 
-@[simp]
+@[simp, grind =]
 theorem mem_sigma {a : Σ i, α i} : a ∈ s.sigma t ↔ a.1 ∈ s ∧ a.2 ∈ t a.1 :=
   Multiset.mem_sigma
 

Mathlib/GroupTheory/Perm/Cycle/Factors.lean

@@ -5,6 +5,7 @@ Authors: Chris Hughes, Yaël Dillies
 -/
 
 import Mathlib.Data.List.Iterate
+import Mathlib.Data.Set.Pairwise.List
 import Mathlib.GroupTheory.Perm.Cycle.Basic
 import Mathlib.GroupTheory.NoncommPiCoprod
 import Mathlib.Tactic.Group

Mathlib/LinearAlgebra/DFinsupp.lean

@@ -581,6 +581,40 @@ theorem iSupIndep_iff_dfinsupp_lsum_injective (p : ι → Submodule R N) :
     iSupIndep p ↔ Function.Injective (lsum ℕ fun i => (p i).subtype) :=
   ⟨iSupIndep.dfinsupp_lsum_injective, iSupIndep_of_dfinsupp_lsum_injective p⟩
 
+theorem iSupIndep_iff_finset_sum_eq_zero_imp_eq_zero (p : ι → Submodule R N) :
+    iSupIndep p ↔ ∀ (s : Finset ι) (v : ι → N),
+    (∀ i ∈ s, v i ∈ p i) → (∑ i ∈ s, v i = 0) → ∀ i ∈ s, v i = 0 := by
+  simp_rw [iSupIndep_def, Submodule.disjoint_def]
+  constructor
+  · intro h s v hv hv0 i hi
+    apply h _ _ (hv i hi)
+    rw [← s.add_sum_erase _ hi, add_eq_zero_iff_neg_eq] at hv0
+    rw [← Submodule.neg_mem_iff, hv0]
+    exact SetLike.le_def.mp (biSup_mono <| by grind) (Submodule.sum_mem_biSup <| by grind)
+  · intro h i x hx hsup
+    obtain ⟨f, hf, rfl⟩ := (Submodule.mem_iSup_iff_exists_finsupp ..).mp hsup
+    contrapose! h
+    use insert i f.support, fun j ↦ if j = i then -f.sum fun _ x ↦ x else f j
+    refine ⟨fun j hj ↦ ?_, ?_, by grind [neg_eq_zero, Finsupp.mem_support_iff]⟩
+    · beta_reduce
+      split_ifs with h
+      · exact (p j).neg_mem (h ▸ hx)
+      · simpa [h] using hf j
+    · specialize hf i
+      simp at hf
+      grind [Finsupp.sum, Finset.sum_congr, Finsupp.mem_support_iff]
+
+theorem iSupIndep_iff_finset_sum_eq_imp_eq (p : ι → Submodule R N) :
+    iSupIndep p ↔ ∀ (s : Finset ι) (v w : ι → N),
+    (∀ i ∈ s, v i ∈ p i ∧ w i ∈ p i) → (∑ i ∈ s, v i = ∑ i ∈ s, w i) → ∀ i ∈ s, v i = w i := by
+  rw [iSupIndep_iff_finset_sum_eq_zero_imp_eq_zero]
+  constructor
+  · intro h s v w hvw
+    simpa [sub_eq_zero] using h s (v - w) fun i hi => (p i).sub_mem (hvw i hi).1 (hvw i hi).2
+  · intro h s v hv hv0
+    specialize h s v 0
+    simp_all
+
 /-- A family of additive subgroups over an additive group are independent if and only if
 `DFinsupp.sumAddHom` applied with `AddSubgroup.subtype` is injective. -/
 theorem iSupIndep_iff_dfinsuppSumAddHom_injective (p : ι → AddSubgroup N) :

Mathlib/LinearAlgebra/Eigenspace/Basic.lean

@@ -673,7 +673,7 @@ theorem independent_maxGenEigenspace [NoZeroSMulDivisors R M] (f : End R M) :
 any eigenspace has trivial intersection with the span of all the other eigenspaces. -/
 theorem eigenspaces_iSupIndep [NoZeroSMulDivisors R M] (f : End R M) :
     iSupIndep f.eigenspace :=
-  (f.independent_genEigenspace 1).mono fun _ ↦ le_rfl
+  f.independent_genEigenspace 1
 
 /-- Eigenvectors corresponding to distinct eigenvalues of a linear operator are linearly
 independent. -/

Mathlib/Logic/Embedding/Basic.lean

@@ -300,6 +300,8 @@ variable {α α' : Type*} {β : α → Type*} {β' : α' → Type*}
 def sigmaMk (a : α) : β a ↪ Σ x, β x :=
   ⟨Sigma.mk a, sigma_mk_injective⟩
 
+attribute [grind =] sigmaMk_apply
+
 /-- If `f : α ↪ α'` is an embedding and `g : Π a, β α ↪ β' (f α)` is a family
 of embeddings, then `Sigma.map f g` is an embedding. -/
 @[simps apply]

Mathlib/Order/CompactlyGenerated/Basic.lean

@@ -510,6 +510,28 @@ section
 
 variable [IsModularLattice α] [IsCompactlyGenerated α]
 
+/--
+If each family `f i` is `iSupIndep`, then the family of pointwise infima
+`k ↦ ⨅ i, f i (k i)` is also `iSupIndep`.
+-/
+theorem iSupIndep.iInf {ι : Type*} {κ : ι → Type*} (f : (i : ι) → κ i → α)
+    (h_indep : ∀ i : ι, iSupIndep (f i)) : iSupIndep (fun k : (i : ι) → κ i ↦ ⨅ i, f i (k i)) := by
+  rw [iSupIndep_iff_supIndep_of_injOn (iSupIndep.injOn_iInf _ h_indep)]
+  intro s
+  induction s using Finset.strongInduction with
+  | H s ih =>
+    by_cases hs : 1 < s.card; swap
+    · by_cases hcard0 : s.card = 0 <;> grind [Finset.card_eq_zero, Finset.card_eq_one]
+    · obtain ⟨k₁, k₂, _, _, h⟩ := Finset.one_lt_card_iff.mp hs
+      obtain ⟨i, hi⟩ : ∃ i : ι, k₁ i ≠ k₂ i := Function.ne_iff.mp h
+      classical
+      rw [← Finset.image_biUnion_filter_eq s (· i)]
+      refine Finset.SupIndep.biUnion ?_ (by grind)
+      apply ((h_indep i).supIndep' _).mono
+      simp_rw [Finset.sup_le_iff, Finset.mem_filter, and_imp]
+      rintro _ _ _ _ rfl
+      exact iInf_le _ _
+
 instance (priority := 100) isAtomic_of_complementedLattice [ComplementedLattice α] : IsAtomic α :=
   ⟨fun b => by
     by_cases h : { c : α | CompleteLattice.IsCompactElement c ∧ c ≤ b } ⊆ {⊥}

Mathlib/Order/Partition/Finpartition.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies, Bhavik Mehta
 -/
 import Mathlib.Data.Finset.Lattice.Prod
+import Mathlib.Data.Finset.Pairwise
 import Mathlib.Data.Fintype.Powerset
 import Mathlib.Data.Setoid.Basic
 import Mathlib.Order.Atoms