Proving a finpartition equivalence

Stream: mathlib4

[Jeremy Tan]

How can I prove the following, which states that given a finpartition P of s, there exists an equivalence between the elements of s and dependent pairs (part of element, index)?

import Mathlib.Order.Partition.Finpartition

open Finset Function

variable {α : Type*} [DecidableEq α] {s : Finset α} (P : Finpartition s)

namespace Finpartition

lemma exists_enumeration : ∃ f : s ≃ (t : P.parts) × Fin t.1.card,
    ∀ a b : s, P.part a = P.part b ↔ (f a).1 = (f b).1 := by
  let k : (t : P.parts) → t.1 ≃ Fin t.1.card := fun t ↦ t.1.equivFin
  sorry

[Yaël Dillies]

State it like def something : s ≃ Σ t : P.parts, t.1?

[Jeremy Tan]

Context is that I want to replace this wonky code in #9317 with the above:

/-- First equivalence in the `IsEquipartition.partPreservingEquiv` chain. -/
noncomputable def equivProduct : s ≃ { t : Finset α × ℕ // t.1 ∈ P.parts ∧ t.2 < t.1.card } where
  toFun x := by
    let p := P.part x.1
    exact ⟨⟨p, p.equivFin ⟨x.1, P.mem_part x.2⟩⟩, ⟨P.part_mem x.2, Fin.prop _⟩⟩
  invFun t := by
    obtain ⟨⟨p, i⟩, ⟨m, l⟩⟩ := t
    let x := p.equivFin.symm ⟨i, l⟩
    exact ⟨x.1, mem_of_subset ((le_sup m).trans P.sup_parts.le) x.2⟩
  left_inv x := by simp
  right_inv t := by
    obtain ⟨⟨p, i⟩, ⟨m, l⟩⟩ := t
    let x := p.equivFin.symm ⟨i, l⟩
    change ⟨(P.part x, (P.part x).equivFin ⟨x, _⟩), _⟩ = Subtype.mk (p, i) _
    have ξ : x.1 ∈ s := mem_of_subset ((le_sup m).trans P.sup_parts.le) x.2
    have ξ' : P.part x.1 = p := P.eq_of_mem_parts (P.part_mem ξ) m (P.mem_part ξ) x.2
    simp only [ξ', Subtype.mk.injEq, Prod.mk.injEq, true_and]
    have : p.equivFin x = i := by simp [x]
    convert this

[Yaël Dillies]

Then use docs#Set.unionEqSigmaOfDisjoint

[Jeremy Tan]

/-- Equivalence between a finpartition's parts as a dependent sum and the partitioned set. -/
def equivSigmaParts : s ≃ Σ t : P.parts, t.1 where
  toFun x := ⟨⟨P.part x.1, P.part_mem x.2⟩, ⟨x, P.mem_part x.2⟩⟩
  invFun x := ⟨x.2, mem_of_subset (P.le x.1.2) x.2.2⟩
  left_inv x := by simp
  right_inv x := by
    ext e
    · obtain ⟨⟨p, mp⟩, ⟨f, mf⟩⟩ := x
      dsimp only at mf ⊢
      have mfs := mem_of_subset (P.le mp) mf
      rw [P.eq_of_mem_parts mp (P.part_mem mfs) mf (P.mem_part mfs)]
    · simp

hmm...

[Jeremy Tan]

lemma exists_enumeration : ∃ f : s ≃ Σ t : P.parts, Fin t.1.card,
    ∀ a b : s, P.part a = P.part b ↔ (f a).1 = (f b).1 := by
  let k : (t : P.parts) → t.1 ≃ Fin t.1.card := fun t ↦ t.1.equivFin
  let kk := P.equivSigmaParts
  sorry

Actually, now what?

[Yaël Dillies]

docs#Equiv.sigmaCongr ?

[Yaël Dillies]

Also it seems that you missed docs#Equiv.setCongr

[Jeremy Tan]

wow, that was easy

lemma exists_enumeration : ∃ f : s ≃ Σ t : P.parts, Fin t.1.card,
    ∀ a b : s, P.part a = P.part b ↔ (f a).1 = (f b).1 := by
  use P.equivSigmaParts.trans ((Equiv.refl _).sigmaCongr (fun t ↦ t.1.equivFin))
  simp [equivSigmaParts, Equiv.sigmaCongr, Equiv.sigmaCongrLeft]