-- Mathlib/Order/Partition/Equipartition.lean
theorem IsEquipartition.exists_partsEquiv (hP : P.IsEquipartition) :
    ∃ f : P.parts ≃ Fin #P.parts, ∀ t, #t.1 = #s / #P.parts + 1 ↔ f t < #s % #P.parts

Proof state:
case h
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
sneg : { x // x ∈ P.parts ∧ ¬#x = #s / #P.parts + 1 } ≃ { x // x ∈ P.parts ∧ #x = #s / #P.parts } :=
  (Equiv.refl (Finset α)).subtypeEquiv ⋯
el : { x // #↑x = #s / #P.parts + 1 } ≃ Fin (#s % #P.parts)
es : { x // ¬#↑x = #s / #P.parts + 1 } ≃ Fin (#P.parts - #s % #P.parts)
f : { x // x ∈ P.parts } ≃ Fin (#s % #P.parts + (#P.parts - #s % #P.parts)) :=
  (Equiv.sumCompl fun a => #↑a = #s / #P.parts + 1).symm.trans ((el.sumCongr es).trans finSumFinEquiv)
p : Finset α
property✝ : p ∈ P.parts
⊢ #p = #s / #P.parts + 1 ↔
    ↑(finSumFinEquiv (Sum.map (⇑el) (⇑es) ((Equiv.sumCompl fun a => #↑a = #s / #P.parts + 1).symm ⟨p, property✝⟩))) <
      #s % #P.parts

Tactic:
by_cases hc : #p = #s / #P.parts + 1 <;> simp [hc]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
es : { x // x ∈ filter (fun p => #p = #s / #P.parts) P.parts } ≃ Fin #(filter (fun p => #p = #s / #P.parts) P.parts) :=
  (filter (fun p => #p = #s / #P.parts) P.parts).equivFin
el : { x // x ∈ P.parts ∧ #x = #s / #P.parts + 1 } ≃ Fin (#s % #P.parts)
⊢ ∃ f, ∀ (t : { x // x ∈ P.parts }), #↑t = #s / #P.parts + 1 ↔ ↑(f t) < #s % #P.parts

Tactic:
simp_rw [mem_filter, hP.card_small_parts_eq_mod] at es

Result:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
el : { x // x ∈ P.parts ∧ #x = #s / #P.parts + 1 } ≃ Fin (#s % #P.parts)
es : { x // x ∈ P.parts ∧ #x = #s / #P.parts } ≃ Fin (#P.parts - #s % #P.parts)
⊢ ∃ f, ∀ (t : { x // x ∈ P.parts }), #↑t = #s / #P.parts + 1 ↔ ↑(f t) < #s % #P.parts

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
el : { x // x ∈ filter (fun p => #p = #s / #P.parts + 1) P.parts } ≃
  Fin #(filter (fun p => #p = #s / #P.parts + 1) P.parts) :=
  (filter (fun p => #p = #s / #P.parts + 1) P.parts).equivFin
es : { x // x ∈ filter (fun p => #p = #s / #P.parts) P.parts } ≃ Fin #(filter (fun p => #p = #s / #P.parts) P.parts) :=
  (filter (fun p => #p = #s / #P.parts) P.parts).equivFin
⊢ ∃ f, ∀ (t : { x // x ∈ P.parts }), #↑t = #s / #P.parts + 1 ↔ ↑(f t) < #s % #P.parts

Tactic:
simp_rw [mem_filter, hP.card_large_parts_eq_mod] at el

Result:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
es : { x // x ∈ filter (fun p => #p = #s / #P.parts) P.parts } ≃ Fin #(filter (fun p => #p = #s / #P.parts) P.parts) :=
  (filter (fun p => #p = #s / #P.parts) P.parts).equivFin
el : { x // x ∈ P.parts ∧ #x = #s / #P.parts + 1 } ≃ Fin (#s % #P.parts)
⊢ ∃ f, ∀ (t : { x // x ∈ P.parts }), #↑t = #s / #P.parts + 1 ↔ ↑(f t) < #s % #P.parts

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
sneg : { x // x ∈ P.parts ∧ ¬#x = #s / #P.parts + 1 } ≃ { x // x ∈ P.parts ∧ #x = #s / #P.parts } :=
  (Equiv.refl (Finset α)).subtypeEquiv ⋯
el : { x // #↑x = #s / #P.parts + 1 } ≃ Fin (#s % #P.parts)
es : { x // ¬#↑x = #s / #P.parts + 1 } ≃ Fin (#P.parts - #s % #P.parts)
f : { x // x ∈ P.parts } ≃ Fin (#s % #P.parts + (#P.parts - #s % #P.parts)) :=
  (Equiv.sumCompl fun a => #↑a = #s / #P.parts + 1).symm.trans ((el.sumCongr es).trans finSumFinEquiv)
⊢ ∃ f, ∀ (t : { x // x ∈ P.parts }), #↑t = #s / #P.parts + 1 ↔ ↑(f t) < #s % #P.parts

Tactic:
use f.trans (finCongr (Nat.add_sub_of_le P.card_mod_card_parts_le))

Result:
case h
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
sneg : { x // x ∈ P.parts ∧ ¬#x = #s / #P.parts + 1 } ≃ { x // x ∈ P.parts ∧ #x = #s / #P.parts } :=
  (Equiv.refl (Finset α)).subtypeEquiv ⋯
el : { x // #↑x = #s / #P.parts + 1 } ≃ Fin (#s % #P.parts)
es : { x // ¬#↑x = #s / #P.parts + 1 } ≃ Fin (#P.parts - #s % #P.parts)
f : { x // x ∈ P.parts } ≃ Fin (#s % #P.parts + (#P.parts - #s % #P.parts)) :=
  (Equiv.sumCompl fun a => #↑a = #s / #P.parts + 1).symm.trans ((el.sumCongr es).trans finSumFinEquiv)
⊢ ∀ (t : { x // x ∈ P.parts }), #↑t = #s / #P.parts + 1 ↔ ↑((f.trans (finCongr ⋯)) t) < #s % #P.parts

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
el : { x // x ∈ P.parts ∧ #x = #s / #P.parts + 1 } ≃ Fin (#s % #P.parts)
es : { x // x ∈ P.parts ∧ #x = #s / #P.parts } ≃ Fin (#P.parts - #s % #P.parts)
⊢ ∀ (a : Finset α),
    a ∈ P.parts ∧ ¬#a = #s / #P.parts + 1 ↔
      (Equiv.refl (Finset α)) a ∈ P.parts ∧ #((Equiv.refl (Finset α)) a) = #s / #P.parts

Tactic:
simp only [Equiv.refl_apply, and_congr_right_iff]

Result:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
el : { x // x ∈ P.parts ∧ #x = #s / #P.parts + 1 } ≃ Fin (#s % #P.parts)
es : { x // x ∈ P.parts ∧ #x = #s / #P.parts } ≃ Fin (#P.parts - #s % #P.parts)
⊢ ∀ a ∈ P.parts, ¬#a = #s / #P.parts + 1 ↔ #a = #s / #P.parts

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
el : { x // x ∈ filter (fun p => #p = #s / #P.parts + 1) P.parts } ≃
  Fin #(filter (fun p => #p = #s / #P.parts + 1) P.parts) :=
  (filter (fun p => #p = #s / #P.parts + 1) P.parts).equivFin
⊢ ∃ f, ∀ (t : { x // x ∈ P.parts }), #↑t = #s / #P.parts + 1 ↔ ↑(f t) < #s % #P.parts

Tactic:
let es := {p ∈ P.parts | #p = #s / #P.parts}.equivFin

Result:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
el : { x // x ∈ filter (fun p => #p = #s / #P.parts + 1) P.parts } ≃
  Fin #(filter (fun p => #p = #s / #P.parts + 1) P.parts) :=
  (filter (fun p => #p = #s / #P.parts + 1) P.parts).equivFin
es : { x // x ∈ filter (fun p => #p = #s / #P.parts) P.parts } ≃ Fin #(filter (fun p => #p = #s / #P.parts) P.parts) :=
  (filter (fun p => #p = #s / #P.parts) P.parts).equivFin
⊢ ∃ f, ∀ (t : { x // x ∈ P.parts }), #↑t = #s / #P.parts + 1 ↔ ↑(f t) < #s % #P.parts

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
sneg : { x // x ∈ P.parts ∧ ¬#x = #s / #P.parts + 1 } ≃ { x // x ∈ P.parts ∧ #x = #s / #P.parts } :=
  (Equiv.refl (Finset α)).subtypeEquiv ⋯
el : { x // #↑x = #s / #P.parts + 1 } ≃ Fin (#s % #P.parts)
es : { x // ¬#↑x = #s / #P.parts + 1 } ≃ Fin (#P.parts - #s % #P.parts)
⊢ ∃ f, ∀ (t : { x // x ∈ P.parts }), #↑t = #s / #P.parts + 1 ↔ ↑(f t) < #s % #P.parts

Tactic:
let f := (Equiv.sumCompl _).symm.trans ((el.sumCongr es).trans finSumFinEquiv)

Result:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
sneg : { x // x ∈ P.parts ∧ ¬#x = #s / #P.parts + 1 } ≃ { x // x ∈ P.parts ∧ #x = #s / #P.parts } :=
  (Equiv.refl (Finset α)).subtypeEquiv ⋯
el : { x // #↑x = #s / #P.parts + 1 } ≃ Fin (#s % #P.parts)
es : { x // ¬#↑x = #s / #P.parts + 1 } ≃ Fin (#P.parts - #s % #P.parts)
f : { x // x ∈ P.parts } ≃ Fin (#s % #P.parts + (#P.parts - #s % #P.parts)) :=
  (Equiv.sumCompl fun a => #↑a = #s / #P.parts + 1).symm.trans ((el.sumCongr es).trans finSumFinEquiv)
⊢ ∃ f, ∀ (t : { x // x ∈ P.parts }), #↑t = #s / #P.parts + 1 ↔ ↑(f t) < #s % #P.parts

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
el : { x // x ∈ P.parts ∧ #x = #s / #P.parts + 1 } ≃ Fin (#s % #P.parts)
es : { x // x ∈ P.parts ∧ #x = #s / #P.parts } ≃ Fin (#P.parts - #s % #P.parts)
⊢ ∀ a ∈ P.parts, ¬#a = #s / #P.parts + 1 ↔ #a = #s / #P.parts

Tactic:
exact fun _ ha ↦ by rw [hP.card_part_eq_average_iff ha, ne_eq]

Result:
no goals