feat: Link finpartitions and setoids (#8735)

Co-authored-by: Yakov Pechersky <ypechersky@treeline.bio>

Mathlib/Order/Partition/Finpartition.lean

@@ -31,6 +31,8 @@ We provide many ways to build finpartitions:
 * `Finpartition.discrete`: The discrete finpartition of `s : Finset α` made of singletons.
 * `Finpartition.bind`: Puts together the finpartitions of the parts of a finpartition into a new
   finpartition.
+* `Finpartition.ofSetoid`: With `Fintype α`, constructs the finpartition of `univ : Finset α`
+  induced by the equivalence classes of `s : Setoid α`.
 * `Finpartition.atomise`: Makes a finpartition of `s : Finset α` by breaking `s` along all finsets
   in `F : Finset (Finset α)`. Two elements of `s` belong to the same part iff they belong to the
   same elements of `F`.
@@ -48,8 +50,6 @@ not because the parts of `P` and the parts of `Q` have the same elements that `P
 
 ## TODO
 
-Link `Finpartition` and `Setoid.isPartition`.
-
 The order is the wrong way around to make `Finpartition a` a graded order. Is it bad to depart from
 the literature and turn the order around?
 -/
@@ -119,6 +119,29 @@ def copy {a b : α} (P : Finpartition a) (h : a = b) : Finpartition b
   not_bot_mem := P.not_bot_mem
 #align finpartition.copy Finpartition.copy
 
+/-- Transfer a finpartition over an order isomorphism. -/
+def map {β : Type*} [Lattice β] [OrderBot β] {a : α} (e : α ≃o β) (P : Finpartition a) :
+    Finpartition (e a) where
+  parts := P.parts.map e
+  supIndep u hu _ hb hbu _ hx hxu := by
+    rw [← map_symm_subset] at hu
+    simp only [mem_map_equiv] at hb
+    have := P.supIndep hu hb (by simp [hbu]) (map_rel e.symm hx) ?_
+    · rw [← e.symm.map_bot] at this
+      exact e.symm.map_rel_iff.mp this
+    · convert e.symm.map_rel_iff.mpr hxu
+      rw [map_finset_sup, sup_map]
+      rfl
+  sup_parts := by simp [← P.sup_parts]
+  not_bot_mem := by
+    rw [mem_map_equiv]
+    convert P.not_bot_mem
+    exact e.symm.map_bot
+
+@[simp]
+theorem parts_map {β : Type*} [Lattice β] [OrderBot β] {a : α} {e : α ≃o β} {P : Finpartition a} :
+    (P.map e).parts = P.parts.map e := rfl
+
 variable (α)
 
 /-- The empty finpartition. -/
@@ -466,7 +489,7 @@ theorem nonempty_of_mem_parts {a : Finset α} (ha : a ∈ P.parts) : a.Nonempty
 lemma eq_of_mem_parts (ht : t ∈ P.parts) (hu : u ∈ P.parts) (hat : a ∈ t) (hau : a ∈ u) : t = u :=
   P.disjoint.elim ht hu <| not_disjoint_iff.2 ⟨a, hat, hau⟩
 
-theorem exists_mem {a : α} (ha : a ∈ s) : ∃ t ∈ P.parts, a ∈ t := by
+theorem exists_mem (ha : a ∈ s) : ∃ t ∈ P.parts, a ∈ t := by
   simp_rw [← P.sup_parts] at ha
   exact mem_sup.1 ha
 #align finpartition.exists_mem Finpartition.exists_mem
@@ -475,6 +498,29 @@ theorem biUnion_parts : P.parts.biUnion id = s :=
   (sup_eq_biUnion _ _).symm.trans P.sup_parts
 #align finpartition.bUnion_parts Finpartition.biUnion_parts
 
+theorem existsUnique_mem (ha : a ∈ s) : ∃! t, t ∈ P.parts ∧ a ∈ t := by
+  obtain ⟨t, ht, ht'⟩ := P.exists_mem ha
+  refine' ⟨t, ⟨ht, ht'⟩, _⟩
+  rintro u ⟨hu, hu'⟩
+  exact P.eq_of_mem_parts hu ht hu' ht'
+
+/-- The part of the finpartition that `a` lies in. -/
+def part (a : α) : Finset α := if ha : a ∈ s then choose (hp := P.existsUnique_mem ha) else ∅
+
+theorem part_mem (ha : a ∈ s) : P.part a ∈ P.parts := by simp [part, ha, choose_mem]
+
+theorem mem_part (ha : a ∈ s) : a ∈ P.part a := by simp [part, ha, choose_property]
+
+theorem part_surjOn : Set.SurjOn P.part s P.parts := fun p hp ↦ by
+  obtain ⟨x, hx⟩ := P.nonempty_of_mem_parts hp
+  have hx' := mem_of_subset ((le_sup hp).trans P.sup_parts.le) hx
+  use x, hx', (P.existsUnique_mem hx').unique ⟨P.part_mem hx', P.mem_part hx'⟩ ⟨hp, hx⟩
+
+theorem exists_subset_part_bijOn : ∃ r ⊆ s, Set.BijOn P.part r P.parts := by
+  obtain ⟨r, hrs, hr⟩ := P.part_surjOn.exists_bijOn_subset
+  lift r to Finset α using s.finite_toSet.subset hrs
+  exact ⟨r, mod_cast hrs, hr⟩
+
 theorem sum_card_parts : ∑ i in P.parts, i.card = s.card := by
   convert congr_arg Finset.card P.biUnion_parts
   rw [card_biUnion P.supIndep.pairwiseDisjoint]
@@ -519,6 +565,45 @@ theorem card_parts_le_card (P : Finpartition s) : P.parts.card ≤ s.card := by
   exact card_mono bot_le
 #align finpartition.card_parts_le_card Finpartition.card_parts_le_card
 
+variable [Fintype α]
+
+/-- A setoid over a finite type induces a finpartition of the type's elements,
+where the parts are the setoid's equivalence classes. -/
+def ofSetoid (s : Setoid α) [DecidableRel s.r] : Finpartition (univ : Finset α) where
+  parts := univ.image fun a => univ.filter (s.r a)
+  supIndep := by
+    simp only [mem_univ, forall_true_left, supIndep_iff_pairwiseDisjoint, Set.PairwiseDisjoint,
+      Set.Pairwise, coe_image, coe_univ, Set.image_univ, Set.mem_range, ne_eq,
+      forall_exists_index, forall_apply_eq_imp_iff]
+    intro _ _ q
+    contrapose! q
+    rw [not_disjoint_iff] at q
+    obtain ⟨c, ⟨d1, d2⟩⟩ := q
+    rw [id_eq, mem_filter] at d1 d2
+    ext y
+    simp only [mem_univ, forall_true_left, mem_filter, true_and]
+    exact ⟨fun r1 => s.trans (s.trans d2.2 (s.symm d1.2)) r1,
+           fun r2 => s.trans (s.trans d1.2 (s.symm d2.2)) r2⟩
+  sup_parts := by
+    ext a
+    simp only [sup_image, Function.id_comp, mem_univ, mem_sup, mem_filter, true_and, iff_true]
+    use a; exact s.refl a
+  not_bot_mem := by
+    rw [bot_eq_empty, mem_image, not_exists]
+    intro a
+    simp only [filter_eq_empty_iff, not_forall, mem_univ, forall_true_left, true_and, not_not]
+    use a; exact s.refl a
+
+theorem mem_part_ofSetoid_iff_rel {s : Setoid α} [DecidableRel s.r] {b : α} :
+    b ∈ (ofSetoid s).part a ↔ s.r a b := by
+  simp_rw [part, ofSetoid, mem_univ, reduceDite]
+  generalize_proofs H
+  have := choose_spec _ _ H
+  simp only [mem_univ, mem_image, true_and] at this
+  obtain ⟨⟨_, hc⟩, this⟩ := this
+  simp only [← hc, mem_univ, mem_filter, true_and] at this ⊢
+  exact ⟨s.trans (s.symm this), s.trans this⟩
+
 section Atomise
 
 /-- Cuts `s` along the finsets in `F`: Two elements of `s` will be in the same part if they are