awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Partition.Equipartition
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
el : ↥({p ∈ P.parts | #p = #s / #P.parts + 1}) ≃ Fin #({p ∈ P.parts | #p = #s / #P.parts + 1}) :=
  {p ∈ P.parts | #p = #s / #P.parts + 1}.equivFin
es : ↥({p ∈ P.parts | #p = #s / #P.parts}) ≃ Fin #({p ∈ P.parts | #p = #s / #P.parts}) :=
  {p ∈ P.parts | #p = #s / #P.parts}.equivFin
simp_rw :
  ∀ (el : { x : Finset α // x ∈ P.parts ∧ #x = #s / #P.parts + 1 } ≃ Fin (#s % #P.parts)),
    ∃ (f : ↥P.parts ≃ Fin #P.parts),
      ∀ (t : ↥P.parts),
        #(↑t : Finset α) = #s / #P.parts + 1 ↔ (↑((f : (a : ↥P.parts) → Fin #P.parts) t) : ℕ) < #s % #P.parts
⊢ ∃ (f : ↥P.parts ≃ Fin #P.parts),
    ∀ (t : ↥P.parts),
      #(↑t : Finset α) = #s / #P.parts + 1 ↔ (↑((f : (a : ↥P.parts) → Fin #P.parts) t) : ℕ) < #s % #P.parts

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

Premises used: Finpartition.IsEquipartition.card_large_parts_eq_mod, Finset.mem_filter
-- Module: Mathlib.Order.Partition.Equipartition
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
es : ↥({p ∈ P.parts | #p = #s / #P.parts}) ≃ Fin #({p ∈ P.parts | #p = #s / #P.parts}) :=
  {p ∈ P.parts | #p = #s / #P.parts}.equivFin
el : { x : Finset α // x ∈ P.parts ∧ #x = #s / #P.parts + 1 } ≃ Fin (#s % #P.parts)
simp_rw :
  ∀ (es : { x : Finset α // x ∈ P.parts ∧ #x = #s / #P.parts } ≃ Fin (#P.parts - #s % #P.parts)),
    ∃ (f : ↥P.parts ≃ Fin #P.parts),
      ∀ (t : ↥P.parts),
        #(↑t : Finset α) = #s / #P.parts + 1 ↔ (↑((f : (a : ↥P.parts) → Fin #P.parts) t) : ℕ) < #s % #P.parts
⊢ ∃ (f : ↥P.parts ≃ Fin #P.parts),
    ∀ (t : ↥P.parts),
      #(↑t : Finset α) = #s / #P.parts + 1 ↔ (↑((f : (a : ↥P.parts) → Fin #P.parts) t) : ℕ) < #s % #P.parts

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

Premises used: Finpartition.IsEquipartition.card_small_parts_eq_mod, Finset.mem_filter
-- Module: Mathlib.Order.Partition.Equipartition
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
el : { x : Finset α // x ∈ P.parts ∧ #x = #s / #P.parts + 1 } ≃ Fin (#s % #P.parts)
es : { x : Finset α // x ∈ P.parts ∧ #x = #s / #P.parts } ≃ Fin (#P.parts - #s % #P.parts)
apply :
  ∀ (a : Finset α),
    a ∈ P.parts ∧ ¬#a = #s / #P.parts + 1 ↔
      Membership.mem (α := Finset α) P.parts ((Equiv.refl (Finset α) : (a : Finset α) → Finset α) a : Finset α) ∧
        Finset.card.{u_1} (α := α) ((Equiv.refl (Finset α) : (a : Finset α) → Finset α) a) = #s / #P.parts
⊢ { x : Finset α // x ∈ P.parts ∧ ¬#x = #s / #P.parts + 1 } ≃ { x : Finset α // x ∈ P.parts ∧ #x = #s / #P.parts }

Tactic:
apply (Equiv.refl _).subtypeEquiv

Premises used: Equiv.subtypeEquiv, Equiv.refl
-- Module: Mathlib.Order.Partition.Equipartition
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
el : { x : Finset α // x ∈ P.parts ∧ #x = #s / #P.parts + 1 } ≃ Fin (#s % #P.parts)
es : { x : Finset α // x ∈ P.parts ∧ #x = #s / #P.parts } ≃ Fin (#P.parts - #s % #P.parts)
simp : ∀ a ∈ P.parts, ¬#a = #s / #P.parts + 1 ↔ #a = #s / #P.parts
⊢ ∀ (a : Finset α),
    a ∈ P.parts ∧ ¬#a = #s / #P.parts + 1 ↔
      Membership.mem (α := Finset α) P.parts ((Equiv.refl (Finset α) : (a : Finset α) → Finset α) a : Finset α) ∧
        Finset.card.{u_1} (α := α) ((Equiv.refl (Finset α) : (a : Finset α) → Finset α) a) = #s / #P.parts

Tactic:
simp only [Equiv.refl_apply, and_congr_right_iff]

Premises used: Equiv.refl_apply, and_congr_right_iff
-- Module: Mathlib.Order.Partition.Equipartition
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
el : { x : Finset α // x ∈ P.parts ∧ #x = #s / #P.parts + 1 } ≃ Fin (#s % #P.parts)
es : { x : Finset α // x ∈ P.parts ∧ #x = #s / #P.parts } ≃ Fin (#P.parts - #s % #P.parts)
x : Finset α
ha : x ∈ P.parts
rw : ¬#x = #s / #P.parts + 1 ↔ #x ≠ #s / #P.parts + 1
rw₁ rw₂ : ¬#x = #s / #P.parts + 1 ↔ ¬#x = #s / #P.parts + 1
⊢ ¬#x = #s / #P.parts + 1 ↔ #x = #s / #P.parts

Tactic:
rw [hP.card_part_eq_average_iff ha, ne_eq]

Premises used: Finpartition.IsEquipartition.card_part_eq_average_iff, ne_eq
-- Module: Mathlib.Order.Partition.Equipartition
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
el : { x : Finset α // x ∈ P.parts ∧ #x = #s / #P.parts + 1 } ≃ Fin (#s % #P.parts)
es : { x : Finset α // 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]
-- Module: Mathlib.Order.Partition.Equipartition
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
el : { x : Finset α // x ∈ P.parts ∧ #x = #s / #P.parts + 1 } ≃ Fin (#s % #P.parts)
es : { x : Finset α // x ∈ P.parts ∧ #x = #s / #P.parts } ≃ Fin (#P.parts - #s % #P.parts)
sneg : { x : Finset α // x ∈ P.parts ∧ ¬#x = #s / #P.parts + 1 } ≃
  { x : Finset α // x ∈ P.parts ∧ #x = #s / #P.parts } :=
  Equiv.subtypeEquiv (p := fun (a : Finset α) ↦ a ∈ P.parts ∧ ¬#a = #s / #P.parts + 1) (q := fun (b : Finset α) ↦
    b ∈ P.parts ∧ #b = #s / #P.parts) (Equiv.refl (Finset α)) ⋯
replace :
  ∀ (el : { x : ↥P.parts // #(↑x : Finset α) = #s / #P.parts + 1 } ≃ Fin (#s % #P.parts)),
    ∃ (f : ↥P.parts ≃ Fin #P.parts),
      ∀ (t : ↥P.parts),
        #(↑t : Finset α) = #s / #P.parts + 1 ↔ (↑((f : (a : ↥P.parts) → Fin #P.parts) t) : ℕ) < #s % #P.parts
⊢ ∃ (f : ↥P.parts ≃ Fin #P.parts),
    ∀ (t : ↥P.parts),
      #(↑t : Finset α) = #s / #P.parts + 1 ↔ (↑((f : (a : ↥P.parts) → Fin #P.parts) t) : ℕ) < #s % #P.parts

Tactic:
replace el : { x : P.parts // #x.1 = #s / #P.parts + 1 } ≃
      Fin (#s % #P.parts) := (Equiv.Set.sep ..).symm.trans el
-- Module: Mathlib.Order.Partition.Equipartition
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
es : { x : Finset α // x ∈ P.parts ∧ #x = #s / #P.parts } ≃ Fin (#P.parts - #s % #P.parts)
sneg : { x : Finset α // x ∈ P.parts ∧ ¬#x = #s / #P.parts + 1 } ≃
  { x : Finset α // x ∈ P.parts ∧ #x = #s / #P.parts } :=
  Equiv.subtypeEquiv (p := fun (a : Finset α) ↦ a ∈ P.parts ∧ ¬#a = #s / #P.parts + 1) (q := fun (b : Finset α) ↦
    b ∈ P.parts ∧ #b = #s / #P.parts) (Equiv.refl (Finset α)) ⋯
el : { x : ↥P.parts // #(↑x : Finset α) = #s / #P.parts + 1 } ≃ Fin (#s % #P.parts)
replace :
  ∀ (es : { x : ↥P.parts // ¬#(↑x : Finset α) = #s / #P.parts + 1 } ≃ Fin (#P.parts - #s % #P.parts)),
    ∃ (f : ↥P.parts ≃ Fin #P.parts),
      ∀ (t : ↥P.parts),
        #(↑t : Finset α) = #s / #P.parts + 1 ↔ (↑((f : (a : ↥P.parts) → Fin #P.parts) t) : ℕ) < #s % #P.parts
⊢ ∃ (f : ↥P.parts ≃ Fin #P.parts),
    ∀ (t : ↥P.parts),
      #(↑t : Finset α) = #s / #P.parts + 1 ↔ (↑((f : (a : ↥P.parts) → Fin #P.parts) t) : ℕ) < #s % #P.parts

Tactic:
replace es : { x : P.parts // ¬#x.1 = #s / #P.parts + 1 } ≃
      Fin (#P.parts - #s % #P.parts) := (Equiv.Set.sep ..).symm.trans (sneg.trans es)
-- Module: Mathlib.Order.Partition.Equipartition
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
sneg : { x : Finset α // x ∈ P.parts ∧ ¬#x = #s / #P.parts + 1 } ≃
  { x : Finset α // x ∈ P.parts ∧ #x = #s / #P.parts } :=
  Equiv.subtypeEquiv (p := fun (a : Finset α) ↦ a ∈ P.parts ∧ ¬#a = #s / #P.parts + 1) (q := fun (b : Finset α) ↦
    b ∈ P.parts ∧ #b = #s / #P.parts) (Equiv.refl (Finset α)) ⋯
el : { x : ↥P.parts // #(↑x : Finset α) = #s / #P.parts + 1 } ≃ Fin (#s % #P.parts)
es : { x : ↥P.parts // ¬#(↑x : Finset α) = #s / #P.parts + 1 } ≃ Fin (#P.parts - #s % #P.parts)
f : ↥P.parts ≃ Fin (#s % #P.parts + (#P.parts - #s % #P.parts)) :=
  Equiv.trans (Equiv.symm (Equiv.sumCompl fun (a : ↥P.parts) ↦ #(↑a : Finset α) = #s / #P.parts + 1))
    ((el.sumCongr es).trans finSumFinEquiv)
h :
  ∀ (t : ↥P.parts),
    #(↑t : Finset α) = #s / #P.parts + 1 ↔
      (↑((f.trans (finCongr ⋯) : (a : ↥P.parts) → Fin #P.parts) t) : ℕ) < #s % #P.parts
⊢ ∃ (f : ↥P.parts ≃ Fin #P.parts),
    ∀ (t : ↥P.parts),
      #(↑t : Finset α) = #s / #P.parts + 1 ↔ (↑((f : (a : ↥P.parts) → Fin #P.parts) t) : ℕ) < #s % #P.parts

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

Premises used: Equiv.trans, finCongr, Nat.add_sub_of_le, Finpartition.card_mod_card_parts_le
-- Module: Mathlib.Order.Partition.Equipartition
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
sneg : { x : Finset α // x ∈ P.parts ∧ ¬#x = #s / #P.parts + 1 } ≃
  { x : Finset α // x ∈ P.parts ∧ #x = #s / #P.parts } :=
  Equiv.subtypeEquiv (p := fun (a : Finset α) ↦ a ∈ P.parts ∧ ¬#a = #s / #P.parts + 1) (q := fun (b : Finset α) ↦
    b ∈ P.parts ∧ #b = #s / #P.parts) (Equiv.refl (Finset α)) ⋯
el : { x : ↥P.parts // #(↑x : Finset α) = #s / #P.parts + 1 } ≃ Fin (#s % #P.parts)
es : { x : ↥P.parts // ¬#(↑x : Finset α) = #s / #P.parts + 1 } ≃ Fin (#P.parts - #s % #P.parts)
f : ↥P.parts ≃ Fin (#s % #P.parts + (#P.parts - #s % #P.parts)) :=
  Equiv.trans (Equiv.symm (Equiv.sumCompl fun (a : ↥P.parts) ↦ #(↑a : Finset α) = #s / #P.parts + 1))
    ((el.sumCongr es).trans finSumFinEquiv)
p : Finset α
property : p ∈ P.parts
h :
  #p = #s / #P.parts + 1 ↔
    (↑((finSumFinEquiv :
              (a : Fin (#s % #P.parts) ⊕ Fin (#P.parts - #s % #P.parts)) →
                Fin (#s % #P.parts + (#P.parts - #s % #P.parts)))
            (Sum.map (α := { x : ↥P.parts // #(↑x : Finset α) = #s / #P.parts + 1 }) (β :=
              { x : ↥P.parts // ¬#(↑x : Finset α) = #s / #P.parts + 1 })
              (⇑el : (a : { x : ↥P.parts // #(↑x : Finset α) = #s / #P.parts + 1 }) → Fin (#s % #P.parts))
              (⇑es : (a : { x : ↥P.parts // ¬#(↑x : Finset α) = #s / #P.parts + 1 }) → Fin (#P.parts - #s % #P.parts))
              ((Equiv.symm (Equiv.sumCompl fun (a : ↥P.parts) ↦ #(↑a : Finset α) = #s / #P.parts + 1) :
                  (a : ↥P.parts) →
                    { a : ↥P.parts // #(↑a : Finset α) = #s / #P.parts + 1 } ⊕
                      { a : ↥P.parts // ¬#(↑a : Finset α) = #s / #P.parts + 1 })
                (Subtype.mk (p := fun (x : Finset α) ↦ x ∈ P.parts) p property)))) :
        ℕ) <
      #s % #P.parts
⊢ #(↑(Subtype.mk (p := fun (x : Finset α) ↦ x ∈ P.parts) p property) : Finset α) = #s / #P.parts + 1 ↔
    (↑((f.trans (finCongr ⋯) : (a : ↥P.parts) → Fin #P.parts)
            (Subtype.mk (p := fun (x : Finset α) ↦ x ∈ P.parts) p property)) :
        ℕ) <
      #s % #P.parts

Tactic:
simp_rw [f, Equiv.trans_apply, Equiv.sumCongr_apply, finCongr_apply, Fin.val_cast]

Premises used: finCongr_apply, Equiv.trans_apply, Equiv.sumCongr_apply, Fin.val_cast
-- Module: Mathlib.Order.Partition.Equipartition
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
sneg : { x : Finset α // x ∈ P.parts ∧ ¬#x = #s / #P.parts + 1 } ≃
  { x : Finset α // x ∈ P.parts ∧ #x = #s / #P.parts } :=
  Equiv.subtypeEquiv (p := fun (a : Finset α) ↦ a ∈ P.parts ∧ ¬#a = #s / #P.parts + 1) (q := fun (b : Finset α) ↦
    b ∈ P.parts ∧ #b = #s / #P.parts) (Equiv.refl (Finset α)) ⋯
el : { x : ↥P.parts // #(↑x : Finset α) = #s / #P.parts + 1 } ≃ Fin (#s % #P.parts)
es : { x : ↥P.parts // ¬#(↑x : Finset α) = #s / #P.parts + 1 } ≃ Fin (#P.parts - #s % #P.parts)
f : ↥P.parts ≃ Fin (#s % #P.parts + (#P.parts - #s % #P.parts)) :=
  Equiv.trans (Equiv.symm (Equiv.sumCompl fun (a : ↥P.parts) ↦ #(↑a : Finset α) = #s / #P.parts + 1))
    ((el.sumCongr es).trans finSumFinEquiv)
p : Finset α
property : p ∈ P.parts
hc : #p = #s / #P.parts + 1
⊢ #p = #s / #P.parts + 1 ↔
    (↑((finSumFinEquiv :
              (a : Fin (#s % #P.parts) ⊕ Fin (#P.parts - #s % #P.parts)) →
                Fin (#s % #P.parts + (#P.parts - #s % #P.parts)))
            (Sum.map (α := { x : ↥P.parts // #(↑x : Finset α) = #s / #P.parts + 1 }) (β :=
              { x : ↥P.parts // ¬#(↑x : Finset α) = #s / #P.parts + 1 })
              (⇑el : (a : { x : ↥P.parts // #(↑x : Finset α) = #s / #P.parts + 1 }) → Fin (#s % #P.parts))
              (⇑es : (a : { x : ↥P.parts // ¬#(↑x : Finset α) = #s / #P.parts + 1 }) → Fin (#P.parts - #s % #P.parts))
              ((Equiv.symm (Equiv.sumCompl fun (a : ↥P.parts) ↦ #(↑a : Finset α) = #s / #P.parts + 1) :
                  (a : ↥P.parts) →
                    { a : ↥P.parts // #(↑a : Finset α) = #s / #P.parts + 1 } ⊕
                      { a : ↥P.parts // ¬#(↑a : Finset α) = #s / #P.parts + 1 })
                (Subtype.mk (p := fun (x : Finset α) ↦ x ∈ P.parts) p property)))) :
        ℕ) <
      #s % #P.parts

Tactic:
simp [hc]
-- Module: Mathlib.Order.Partition.Equipartition
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
sneg : { x : Finset α // x ∈ P.parts ∧ ¬#x = #s / #P.parts + 1 } ≃
  { x : Finset α // x ∈ P.parts ∧ #x = #s / #P.parts } :=
  Equiv.subtypeEquiv (p := fun (a : Finset α) ↦ a ∈ P.parts ∧ ¬#a = #s / #P.parts + 1) (q := fun (b : Finset α) ↦
    b ∈ P.parts ∧ #b = #s / #P.parts) (Equiv.refl (Finset α)) ⋯
el : { x : ↥P.parts // #(↑x : Finset α) = #s / #P.parts + 1 } ≃ Fin (#s % #P.parts)
es : { x : ↥P.parts // ¬#(↑x : Finset α) = #s / #P.parts + 1 } ≃ Fin (#P.parts - #s % #P.parts)
f : ↥P.parts ≃ Fin (#s % #P.parts + (#P.parts - #s % #P.parts)) :=
  Equiv.trans (Equiv.symm (Equiv.sumCompl fun (a : ↥P.parts) ↦ #(↑a : Finset α) = #s / #P.parts + 1))
    ((el.sumCongr es).trans finSumFinEquiv)
p : Finset α
property : p ∈ P.parts
hc : ¬#p = #s / #P.parts + 1
⊢ #p = #s / #P.parts + 1 ↔
    (↑((finSumFinEquiv :
              (a : Fin (#s % #P.parts) ⊕ Fin (#P.parts - #s % #P.parts)) →
                Fin (#s % #P.parts + (#P.parts - #s % #P.parts)))
            (Sum.map (α := { x : ↥P.parts // #(↑x : Finset α) = #s / #P.parts + 1 }) (β :=
              { x : ↥P.parts // ¬#(↑x : Finset α) = #s / #P.parts + 1 })
              (⇑el : (a : { x : ↥P.parts // #(↑x : Finset α) = #s / #P.parts + 1 }) → Fin (#s % #P.parts))
              (⇑es : (a : { x : ↥P.parts // ¬#(↑x : Finset α) = #s / #P.parts + 1 }) → Fin (#P.parts - #s % #P.parts))
              ((Equiv.symm (Equiv.sumCompl fun (a : ↥P.parts) ↦ #(↑a : Finset α) = #s / #P.parts + 1) :
                  (a : ↥P.parts) →
                    { a : ↥P.parts // #(↑a : Finset α) = #s / #P.parts + 1 } ⊕
                      { a : ↥P.parts // ¬#(↑a : Finset α) = #s / #P.parts + 1 })
                (Subtype.mk (p := fun (x : Finset α) ↦ x ∈ P.parts) p property)))) :
        ℕ) <
      #s % #P.parts

Tactic:
simp [hc]
-- Module: Mathlib.Order.Partition.Equipartition
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
obtain :
  ∀ (f : ↥s ≃ (t : ↥P.parts) × Fin #(↑t : Finset α))
    (hf :
      ∀ (a b : ↥s),
        P.part (↑a : α) = P.part (↑b : α) ↔
          Eq.{u_1 + 1} (α := ↥P.parts)
            (Sigma.fst (β := fun (t : ↥P.parts) ↦ Fin #(↑t : Finset α))
              ((f : (a : ↥s) → (t : ↥P.parts) × Fin #(↑t : Finset α)) a))
            (Sigma.fst (β := fun (t : ↥P.parts) ↦ Fin #(↑t : Finset α))
              ((f : (a : ↥s) → (t : ↥P.parts) × Fin #(↑t : Finset α)) b))),
    ∃ (f : ↥s ≃ Fin #s),
      ∀ (a b : ↥s),
        P.part (↑a : α) = P.part (↑b : α) ↔
          (↑((f : (a : ↥s) → Fin #s) a) : ℕ) % #P.parts = (↑((f : (a : ↥s) → Fin #s) b) : ℕ) % #P.parts
⊢ ∃ (f : ↥s ≃ Fin #s),
    ∀ (a b : ↥s),
      P.part (↑a : α) = P.part (↑b : α) ↔
        (↑((f : (a : ↥s) → Fin #s) a) : ℕ) % #P.parts = (↑((f : (a : ↥s) → Fin #s) b) : ℕ) % #P.parts

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

Premises used: Finpartition.exists_enumeration
-- Module: Mathlib.Order.Partition.Equipartition
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
f : ↥s ≃ (t : ↥P.parts) × Fin #(↑t : Finset α)
hf :
  ∀ (a b : ↥s),
    P.part (↑a : α) = P.part (↑b : α) ↔
      Eq.{u_1 + 1} (α := ↥P.parts)
        (Sigma.fst (β := fun (t : ↥P.parts) ↦ Fin #(↑t : Finset α))
          ((f : (a : ↥s) → (t : ↥P.parts) × Fin #(↑t : Finset α)) a))
        (Sigma.fst (β := fun (t : ↥P.parts) ↦ Fin #(↑t : Finset α))
          ((f : (a : ↥s) → (t : ↥P.parts) × Fin #(↑t : Finset α)) b))
obtain :
  ∀ (g : ↥P.parts ≃ Fin #P.parts)
    (hg :
      ∀ (t : ↥P.parts),
        #(↑t : Finset α) = #s / #P.parts + 1 ↔ (↑((g : (a : ↥P.parts) → Fin #P.parts) t) : ℕ) < #s % #P.parts),
    ∃ (f : ↥s ≃ Fin #s),
      ∀ (a b : ↥s),
        P.part (↑a : α) = P.part (↑b : α) ↔
          (↑((f : (a : ↥s) → Fin #s) a) : ℕ) % #P.parts = (↑((f : (a : ↥s) → Fin #s) b) : ℕ) % #P.parts
⊢ ∃ (f : ↥s ≃ Fin #s),
    ∀ (a b : ↥s),
      P.part (↑a : α) = P.part (↑b : α) ↔
        (↑((f : (a : ↥s) → Fin #s) a) : ℕ) % #P.parts = (↑((f : (a : ↥s) → Fin #s) b) : ℕ) % #P.parts

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

Premises used: Finpartition.IsEquipartition.exists_partsEquiv
-- Module: Mathlib.Order.Partition.Equipartition
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
f : ↥s ≃ (t : ↥P.parts) × Fin #(↑t : Finset α)
hf :
  ∀ (a b : ↥s),
    P.part (↑a : α) = P.part (↑b : α) ↔
      Eq.{u_1 + 1} (α := ↥P.parts)
        (Sigma.fst (β := fun (t : ↥P.parts) ↦ Fin #(↑t : Finset α))
          ((f : (a : ↥s) → (t : ↥P.parts) × Fin #(↑t : Finset α)) a))
        (Sigma.fst (β := fun (t : ↥P.parts) ↦ Fin #(↑t : Finset α))
          ((f : (a : ↥s) → (t : ↥P.parts) × Fin #(↑t : Finset α)) b))
g : ↥P.parts ≃ Fin #P.parts
hg :
  ∀ (t : ↥P.parts),
    #(↑t : Finset α) = #s / #P.parts + 1 ↔ (↑((g : (a : ↥P.parts) → Fin #P.parts) t) : ℕ) < #s % #P.parts
z : (a : ↥s) → ℕ :=
  fun (a : ↥s) ↦
    #P.parts *
        (↑(Sigma.snd (β := fun (t : ↥P.parts) ↦ Fin #(↑t : Finset α))
                ((f : (a : ↥s) → (t : ↥P.parts) × Fin #(↑t : Finset α)) a) :
              Fin
                (Finset.card.{u_1} (α := α)
                  (↑(Sigma.fst (β := fun (t : ↥P.parts) ↦ Fin #(↑t : Finset α))
                        ((f : (a : ↥s) → (t : ↥P.parts) × Fin #(↑t : Finset α)) a)) :
                    Finset α))) :
          ℕ) +
      (↑((g : (a : ↥P.parts) → Fin #P.parts)
            (Sigma.fst (β := fun (t : ↥P.parts) ↦ Fin #(↑t : Finset α))
              ((f : (a : ↥s) → (t : ↥P.parts) × Fin #(↑t : Finset α)) a))) :
        ℕ)
⊢ ∀ (a : ↥s),
    (↑((g : (a : ↥P.parts) → Fin #P.parts)
            (Sigma.fst (β := fun (t : ↥P.parts) ↦ Fin #(↑t : Finset α))
              ((f : (a : ↥s) → (t : ↥P.parts) × Fin #(↑t : Finset α)) a))) :
        ℕ) <
      #P.parts

Tactic:
have gl := fun a ↦ (g (f a).1).2
-- Module: Mathlib.Order.Partition.Equipartition
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
f : ↥s ≃ (t : ↥P.parts) × Fin #(↑t : Finset α)
hf :
  ∀ (a b : ↥s),
    P.part (↑a : α) = P.part (↑b : α) ↔
      Eq.{u_1 + 1} (α := ↥P.parts)
        (Sigma.fst (β := fun (t : ↥P.parts) ↦ Fin #(↑t : Finset α))
          ((f : (a : ↥s) → (t : ↥P.parts) × Fin #(↑t : Finset α)) a))
        (Sigma.fst (β := fun (t : ↥P.parts) ↦ Fin #(↑t : Finset α))
          ((f : (a : ↥s) → (t : ↥P.parts) × Fin #(↑t : Finset α)) b))
g : ↥P.parts ≃ Fin #P.parts
hg :
  ∀ (t : ↥P.parts),
    #(↑t : Finset α) = #s / #P.parts + 1 ↔ (↑((g : (a : ↥P.parts) → Fin #P.parts) t) : ℕ) < #s % #P.parts
z : (a : ↥s) → ℕ :=
  fun (a : ↥s) ↦
    #P.parts *
        (↑(Sigma.snd (β := fun (t : ↥P.parts) ↦ Fin #(↑t : Finset α))
                ((f : (a : ↥s) → (t : ↥P.parts) × Fin #(↑t : Finset α)) a) :
              Fin
                (Finset.card.{u_1} (α := α)
                  (↑(Sigma.fst (β := fun (t : ↥P.parts) ↦ Fin #(↑t : Finset α))
                        ((f : (a : ↥s) → (t : ↥P.parts) × Fin #(↑t : Finset α)) a)) :
                    Finset α))) :
          ℕ) +
      (↑((g : (a : ↥P.parts) → Fin #P.parts)
            (Sigma.fst (β := fun (t : ↥P.parts) ↦ Fin #(↑t : Finset α))
              ((f : (a : ↥s) → (t : ↥P.parts) × Fin #(↑t : Finset α)) a))) :
        ℕ)
gl :
  ∀ (a : ↥s),
    (↑((g : (a : ↥P.parts) → Fin #P.parts)
            (Sigma.fst (β := fun (t : ↥P.parts) ↦ Fin #(↑t : Finset α))
              ((f : (a : ↥s) → (t : ↥P.parts) × Fin #(↑t : Finset α)) a))) :
        ℕ) <
      #P.parts
a : ↥s
inl :
  ∀
    (c :
      Finset.card.{u_1} (α := α)
          (↑(Sigma.fst (β := fun (t : ↥P.parts) ↦ Fin #(↑t : Finset α))
                ((f : (a : ↥s) → (t : ↥P.parts) × Fin #(↑t : Finset α)) a)) :
            Finset α) =
        #s / #P.parts),
    z a < #s
inr :
  ∀
    (c :
      Finset.card.{u_1} (α := α)
          (↑(Sigma.fst (β := fun (t : ↥P.parts) ↦ Fin #(↑t : Finset α))
                ((f : (a : ↥s) → (t : ↥P.parts) × Fin #(↑t : Finset α)) a)) :
            Finset α) =
        #s / #P.parts + 1),
    z a < #s
⊢ z a < #s

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

Premises used: Finpartition.IsEquipartition.card_parts_eq_average, Sigma.fst, DFunLike.coe, Subtype.property
-- Module: Mathlib.Order.Partition.Equipartition
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
f : ↥s ≃ (t : ↥P.parts) × Fin #(↑t : Finset α)
hf :
  ∀ (a b : ↥s),
    P.part (↑a : α) = P.part (↑b : α) ↔
      Eq.{u_1 + 1} (α := ↥P.parts)
        (Sigma.fst (β := fun (t : ↥P.parts) ↦ Fin #(↑t : Finset α))
          ((f : (a : ↥s) → (t : ↥P.parts) × Fin #(↑t : Finset α)) a))
        (Sigma.fst (β := fun (t : ↥P.parts) ↦ Fin #(↑t : Finset α))
          ((f : (a : ↥s) → (t : ↥P.parts) × Fin #(↑t : Finset α)) b))
g : ↥P.parts ≃ Fin #P.parts
hg :
  ∀ (t : ↥P.parts),
    #(↑t : Finset α) = #s / #P.parts + 1 ↔ (↑((g : (a : ↥P.parts) → Fin #P.parts) t) : ℕ) < #s % #P.parts
z : (a : ↥s) → ℕ :=
  fun (a : ↥s) ↦
    #P.parts *
        (↑(Sigma.snd (β := fun (t : ↥P.parts) ↦ Fin #(↑t : Finset α))
                ((f : (a : ↥s) → (t : ↥P.parts) × Fin #(↑t : Finset α)) a) :
              Fin
                (Finset.card.{u_1} (α := α)
                  (↑(Sigma.fst (β := fun (t : ↥P.parts) ↦ Fin #(↑t : Finset α))
                        ((f : (a : ↥s) → (t : ↥P.parts) × Fin #(↑t : Finset α)) a)) :
                    Finset α))) :
          ℕ) +
      (↑((g : (a : ↥P.parts) → Fin #P.parts)
            (Sigma.fst (β := fun (t : ↥P.parts) ↦ Fin #(↑t : Finset α))
              ((f : (a : ↥s) → (t : ↥P.parts) × Fin #(↑t : Finset α)) a))) :
        ℕ)
gl :
  ∀ (a : ↥s),
    (↑((g : (a : ↥P.parts) → Fin #P.parts)
            (Sigma.fst (β := fun (t : ↥P.parts) ↦ Fin #(↑t : Finset α))
              ((f : (a : ↥s) → (t : ↥P.parts) × Fin #(↑t : Finset α)) a))) :
        ℕ) <
      #P.parts
a : ↥s
c :
  Finset.card.{u_1} (α := α)
      (↑(Sigma.fst (β := fun (t : ↥P.parts) ↦ Fin #(↑t : Finset α))
            ((f : (a : ↥s) → (t : ↥P.parts) × Fin #(↑t : Finset α)) a)) :
        Finset α) =
    #s / #P.parts
bc :
  (↑((g : (a : ↥P.parts) → Fin #P.parts)
          (Sigma.fst (β := fun (t : ↥P.parts) ↦ Fin #(↑t : Finset α))
            ((f : (a : ↥s) → (t : ↥P.parts) × Fin #(↑t : Finset α)) a))) :
      ℕ) <
    #P.parts
⊢ #P.parts *
        (↑(Sigma.snd (β := fun (t : ↥P.parts) ↦ Fin #(↑t : Finset α))
                ((f : (a : ↥s) → (t : ↥P.parts) × Fin #(↑t : Finset α)) a) :
              Fin
                (Finset.card.{u_1} (α := α)
                  (↑(Sigma.fst (β := fun (t : ↥P.parts) ↦ Fin #(↑t : Finset α))
                        ((f : (a : ↥s) → (t : ↥P.parts) × Fin #(↑t : Finset α)) a)) :
                    Finset α))) :
          ℕ) +
      (↑((g : (a : ↥P.parts) → Fin #P.parts)
            (Sigma.fst (β := fun (t : ↥P.parts) ↦ Fin #(↑t : Finset α))
              ((f : (a : ↥s) → (t : ↥P.parts) × Fin #(↑t : Finset α)) a))) :
        ℕ) <
    #P.parts *
        (↑(Sigma.snd (β := fun (t : ↥P.parts) ↦ Fin #(↑t : Finset α))
                ((f : (a : ↥s) → (t : ↥P.parts) × Fin #(↑t : Finset α)) a) :
              Fin
                (Finset.card.{u_1} (α := α)
                  (↑(Sigma.fst (β := fun (t : ↥P.parts) ↦ Fin #(↑t : Finset α))
                        ((f : (a : ↥s) → (t : ↥P.parts) × Fin #(↑t : Finset α)) a)) :
                    Finset α))) :
          ℕ) +
      #P.parts

Tactic:
gcongr