-- Mathlib/Order/Partition/Equipartition.lean
theorem IsEquipartition.exists_partPreservingEquiv (hP : P.IsEquipartition) : ∃ f : s ≃ Fin #s,
    ∀ a b : s, P.part a = P.part b ↔ f a % #P.parts = f b % #P.parts

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
f : { x // x ∈ s } ≃ (t : { x // x ∈ P.parts }) × Fin #↑t
hf : ∀ (a b : { x // x ∈ s }), P.part ↑a = P.part ↑b ↔ (f a).fst = (f b).fst
g : { x // x ∈ P.parts } ≃ Fin #P.parts
hg : ∀ (t : { x // x ∈ P.parts }), #↑t = #s / #P.parts + 1 ↔ ↑(g t) < #s % #P.parts
z : { x // x ∈ s } → ℕ := fun a => #P.parts * ↑(f a).snd + ↑(g (f a).fst)
gl : ∀ (a : { x // x ∈ s }), ↑(g (f a).fst) < #P.parts
less : ∀ (a : { x // x ∈ s }), z a < #s
z' : { x // x ∈ s } → Fin #s := fun a => ⟨z a, ⋯⟩
a b : { x // x ∈ s }
this : NeZero #P.parts
e : (f a).snd.1 = (f b).snd.1 ∧ (f a).fst = (f b).fst
⊢ #↑(f a).fst = #↑(f b).fst

Tactic:
rw [e.2]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
f : { x // x ∈ s } ≃ (t : { x // x ∈ P.parts }) × Fin #↑t
hf : ∀ (a b : { x // x ∈ s }), P.part ↑a = P.part ↑b ↔ (f a).fst = (f b).fst
g : { x // x ∈ P.parts } ≃ Fin #P.parts
hg : ∀ (t : { x // x ∈ P.parts }), #↑t = #s / #P.parts + 1 ↔ ↑(g t) < #s % #P.parts
z : { x // x ∈ s } → ℕ := fun a => #P.parts * ↑(f a).snd + ↑(g (f a).fst)
gl : ∀ (a : { x // x ∈ s }), ↑(g (f a).fst) < #P.parts
less : ∀ (a : { x // x ∈ s }), z a < #s
z' : { x // x ∈ s } → Fin #s := fun a => ⟨z a, ⋯⟩
a b : { x // x ∈ s }
this : NeZero #P.parts
e : (#P.parts).divModEquiv.symm ((f a).snd.1, g (f a).fst) = (#P.parts).divModEquiv.symm ((f b).snd.1, g (f b).fst)
⊢ a = b

Tactic:
simp only [Equiv.apply_eq_iff_eq, Prod.mk.injEq] at e

Result:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
f : { x // x ∈ s } ≃ (t : { x // x ∈ P.parts }) × Fin #↑t
hf : ∀ (a b : { x // x ∈ s }), P.part ↑a = P.part ↑b ↔ (f a).fst = (f b).fst
g : { x // x ∈ P.parts } ≃ Fin #P.parts
hg : ∀ (t : { x // x ∈ P.parts }), #↑t = #s / #P.parts + 1 ↔ ↑(g t) < #s % #P.parts
z : { x // x ∈ s } → ℕ := fun a => #P.parts * ↑(f a).snd + ↑(g (f a).fst)
gl : ∀ (a : { x // x ∈ s }), ↑(g (f a).fst) < #P.parts
less : ∀ (a : { x // x ∈ s }), z a < #s
z' : { x // x ∈ s } → Fin #s := fun a => ⟨z a, ⋯⟩
a b : { x // x ∈ s }
this : NeZero #P.parts
e : (f a).snd.1 = (f b).snd.1 ∧ (f a).fst = (f b).fst
⊢ a = b

Proof state:
case intro.intro
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
f : { x // x ∈ s } ≃ (t : { x // x ∈ P.parts }) × Fin #↑t
hf : ∀ (a b : { x // x ∈ s }), P.part ↑a = P.part ↑b ↔ (f a).fst = (f b).fst
g : { x // x ∈ P.parts } ≃ Fin #P.parts
hg : ∀ (t : { x // x ∈ P.parts }), #↑t = #s / #P.parts + 1 ↔ ↑(g t) < #s % #P.parts
z : { x // x ∈ s } → ℕ := fun a => #P.parts * ↑(f a).snd + ↑(g (f a).fst)
gl : ∀ (a : { x // x ∈ s }), ↑(g (f a).fst) < #P.parts
less : ∀ (a : { x // x ∈ s }), z a < #s
z' : { x // x ∈ s } → Fin #s := fun a => ⟨z a, ⋯⟩
⊢ ∃ f, ∀ (a b : { x // x ∈ s }), P.part ↑a = P.part ↑b ↔ ↑(f a) % #P.parts = ↑(f b) % #P.parts

Tactic:
have bij : z'.Bijective := by
  refine (bijective_iff_injective_and_card z').mpr ⟨fun a b e ↦ ?_, by simp⟩
  simp_rw [z', z, Fin.mk.injEq, mul_comm #P.parts] at e
  haveI : NeZero #P.parts := ⟨((Nat.zero_le _).trans_lt (gl a)).ne'⟩
  change (#P.parts).divModEquiv.symm (_, _) = (#P.parts).divModEquiv.symm (_, _) at e
  simp only [Equiv.apply_eq_iff_eq, Prod.mk.injEq] at e
  apply_fun f
  exact Sigma.ext e.2 <| (Fin.heq_ext_iff (by rw [e.2])).mpr e.1

Result:
case intro.intro
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
f : { x // x ∈ s } ≃ (t : { x // x ∈ P.parts }) × Fin #↑t
hf : ∀ (a b : { x // x ∈ s }), P.part ↑a = P.part ↑b ↔ (f a).fst = (f b).fst
g : { x // x ∈ P.parts } ≃ Fin #P.parts
hg : ∀ (t : { x // x ∈ P.parts }), #↑t = #s / #P.parts + 1 ↔ ↑(g t) < #s % #P.parts
z : { x // x ∈ s } → ℕ := fun a => #P.parts * ↑(f a).snd + ↑(g (f a).fst)
gl : ∀ (a : { x // x ∈ s }), ↑(g (f a).fst) < #P.parts
less : ∀ (a : { x // x ∈ s }), z a < #s
z' : { x // x ∈ s } → Fin #s := fun a => ⟨z a, ⋯⟩
bij : Function.Bijective z'
⊢ ∃ f, ∀ (a b : { x // x ∈ s }), P.part ↑a = P.part ↑b ↔ ↑(f a) % #P.parts = ↑(f b) % #P.parts

Proof state:
case intro.intro
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
f : { x // x ∈ s } ≃ (t : { x // x ∈ P.parts }) × Fin #↑t
hf : ∀ (a b : { x // x ∈ s }), P.part ↑a = P.part ↑b ↔ (f a).fst = (f b).fst
g : { x // x ∈ P.parts } ≃ Fin #P.parts
hg : ∀ (t : { x // x ∈ P.parts }), #↑t = #s / #P.parts + 1 ↔ ↑(g t) < #s % #P.parts
z : { x // x ∈ s } → ℕ := fun a => #P.parts * ↑(f a).snd + ↑(g (f a).fst)
gl : ∀ (a : { x // x ∈ s }), ↑(g (f a).fst) < #P.parts
less : ∀ (a : { x // x ∈ s }), z a < #s
z' : { x // x ∈ s } → Fin #s := fun a => ⟨z a, ⋯⟩
bij : Function.Bijective z'
⊢ ∃ f, ∀ (a b : { x // x ∈ s }), P.part ↑a = P.part ↑b ↔ ↑(f a) % #P.parts = ↑(f b) % #P.parts

Tactic:
use Equiv.ofBijective _ bij

Result:
case h
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
f : { x // x ∈ s } ≃ (t : { x // x ∈ P.parts }) × Fin #↑t
hf : ∀ (a b : { x // x ∈ s }), P.part ↑a = P.part ↑b ↔ (f a).fst = (f b).fst
g : { x // x ∈ P.parts } ≃ Fin #P.parts
hg : ∀ (t : { x // x ∈ P.parts }), #↑t = #s / #P.parts + 1 ↔ ↑(g t) < #s % #P.parts
z : { x // x ∈ s } → ℕ := fun a => #P.parts * ↑(f a).snd + ↑(g (f a).fst)
gl : ∀ (a : { x // x ∈ s }), ↑(g (f a).fst) < #P.parts
less : ∀ (a : { x // x ∈ s }), z a < #s
z' : { x // x ∈ s } → Fin #s := fun a => ⟨z a, ⋯⟩
bij : Function.Bijective z'
⊢ ∀ (a b : { x // x ∈ s }),
    P.part ↑a = P.part ↑b ↔ ↑((Equiv.ofBijective z' bij) a) % #P.parts = ↑((Equiv.ofBijective z' bij) b) % #P.parts

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
f : { x // x ∈ s } ≃ (t : { x // x ∈ P.parts }) × Fin #↑t
hf : ∀ (a b : { x // x ∈ s }), P.part ↑a = P.part ↑b ↔ (f a).fst = (f b).fst
g : { x // x ∈ P.parts } ≃ Fin #P.parts
hg : ∀ (t : { x // x ∈ P.parts }), #↑t = #s / #P.parts + 1 ↔ ↑(g t) < #s % #P.parts
z : { x // x ∈ s } → ℕ := fun a => #P.parts * ↑(f a).snd + ↑(g (f a).fst)
gl : ∀ (a : { x // x ∈ s }), ↑(g (f a).fst) < #P.parts
less : ∀ (a : { x // x ∈ s }), z a < #s
z' : { x // x ∈ s } → Fin #s := fun a => ⟨z a, ⋯⟩
a b : { x // x ∈ s }
e : ↑(f a).snd * #P.parts + ↑(g (f a).fst) = ↑(f b).snd * #P.parts + ↑(g (f b).fst)
⊢ a = b

Tactic:
haveI : NeZero #P.parts := ⟨((Nat.zero_le _).trans_lt (gl a)).ne'⟩

Result:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
f : { x // x ∈ s } ≃ (t : { x // x ∈ P.parts }) × Fin #↑t
hf : ∀ (a b : { x // x ∈ s }), P.part ↑a = P.part ↑b ↔ (f a).fst = (f b).fst
g : { x // x ∈ P.parts } ≃ Fin #P.parts
hg : ∀ (t : { x // x ∈ P.parts }), #↑t = #s / #P.parts + 1 ↔ ↑(g t) < #s % #P.parts
z : { x // x ∈ s } → ℕ := fun a => #P.parts * ↑(f a).snd + ↑(g (f a).fst)
gl : ∀ (a : { x // x ∈ s }), ↑(g (f a).fst) < #P.parts
less : ∀ (a : { x // x ∈ s }), z a < #s
z' : { x // x ∈ s } → Fin #s := fun a => ⟨z a, ⋯⟩
a b : { x // x ∈ s }
e : ↑(f a).snd * #P.parts + ↑(g (f a).fst) = ↑(f b).snd * #P.parts + ↑(g (f b).fst)
this : NeZero #P.parts
⊢ a = b