-- 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:
simp_rw [z', z, Equiv.ofBijective_apply, hf a b, Nat.mul_add_mod,
  Nat.mod_eq_of_lt (gl a), Nat.mod_eq_of_lt (gl b), Fin.val_eq_val, g.apply_eq_iff_eq]

Result:
no goals

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

Tactic:
have gl := fun a ↦ (g (f a).1).2

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
⊢ ∃ 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 }
this : NeZero #P.parts
e : (f a).snd.1 = (f b).snd.1 ∧ (f a).fst = (f b).fst
⊢ f a = f b

Tactic:
exact Sigma.ext e.2 <| (Fin.heq_ext_iff (by rw [e.2])).mpr e.1

Result:
no goals

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

Tactic:
rw [← Nat.div_add_mod #s #P.parts]

Result:
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 < #P.parts * (#s / #P.parts) + #s % #P.parts

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

Tactic:
calc
  _ < #P.parts * ((f a).2 + 1) := add_lt_add_left (gl a) _
  _ ≤ #P.parts * (#s / #P.parts) := mul_le_mul_left' (c ▸ (f a).2.2) _
  _ ≤ #P.parts * (#s / #P.parts) + #s % #P.parts := Nat.le_add_right ..
  _ = _ := Nat.div_add_mod ..

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 : (f a).snd.1 = (f b).snd.1 ∧ (f a).fst = (f b).fst
⊢ a = b

Tactic:
apply_fun f

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
⊢ f a = f b