-- 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:
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

Tactic:
intro a b

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
a : { x // x ∈ s }
⊢ z a < #s

Tactic:
rcases hP.card_parts_eq_average (f a).1.2 with (c | c)

Result:
case inl
α : 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
a : { x // x ∈ s }
c : #↑(f a).fst = #s / #P.parts
⊢ z a < #s

case inr
α : 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
a : { x // x ∈ s }
c : #↑(f a).fst = #s / #P.parts + 1
⊢ z a < #s

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, ⋯⟩
⊢ Function.Bijective z'

Tactic:
refine (bijective_iff_injective_and_card z').mpr ⟨fun a b e ↦ ?_, by simp⟩

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 : z' a = z' b
⊢ 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
⊢ ∃ f, ∀ (a b : { x // x ∈ s }), P.part ↑a = P.part ↑b ↔ ↑(f a) % #P.parts = ↑(f b) % #P.parts

Tactic:
let z := fun a ↦ #P.parts * (f a).2 + g (f a).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)
⊢ ∃ f, ∀ (a b : { x // x ∈ 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 }
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

Tactic:
change (#P.parts).divModEquiv.symm (_, _) = (#P.parts).divModEquiv.symm (_, _) 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 : (#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