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

Tactic:
let z' : s → Fin #s := fun a ↦ ⟨z a, less a⟩

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, ⋯⟩
⊢ ∃ 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, ⋯⟩
⊢ Fintype.card { x // x ∈ s } = Fintype.card (Fin #s)

Tactic:
simp

Result:
no goals

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

Tactic:
obtain ⟨g, hg⟩ := hP.exists_partsEquiv

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

Tactic:
obtain ⟨f, hf⟩ := P.exists_enumeration

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

Tactic:
omega

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 }
e : z' a = z' b
⊢ a = b

Tactic:
simp_rw [z', z, Fin.mk.injEq, mul_comm #P.parts] 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 }
e : ↑(f a).snd * #P.parts + ↑(g (f a).fst) = ↑(f b).snd * #P.parts + ↑(g (f b).fst)
⊢ a = b

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

Tactic:
exact add_lt_add_of_le_of_lt (mul_le_mul_left' (by omega) _) ((hg (f a).1).mp c)

Result:
no goals