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
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
less : ∀ (a : ↥s), z a < #s
z' : ↥s → Fin #s := fun (a : ↥s) ↦ ⟨z a, ⋯⟩
⊢ Fintype.card.{u_1} ↥s = Fintype.card (Fin #s)

Tactic:
simp
-- 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
less : ∀ (a : ↥s), z a < #s
z' : ↥s → Fin #s := fun (a : ↥s) ↦ ⟨z a, ⋯⟩
refine : ∀ (a b : ↥s) (e : z' a = z' b), a = b
⊢ Function.Bijective z'

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

Premises used: Iff.mpr, Fintype.bijective_iff_injective_and_card, And.intro
-- 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
less : ∀ (a : ↥s), z a < #s
z' : ↥s → Fin #s := fun (a : ↥s) ↦ ⟨z a, ⋯⟩
a b : ↥s
e : z' a = z' b
⊢ (↑(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 +
      (↑((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))) :
        ℕ) =
    (↑(Sigma.snd (β := fun (t : ↥P.parts) ↦ Fin #(↑t : Finset α))
                ((f : (a : ↥s) → (t : ↥P.parts) × Fin #(↑t : Finset α)) b) :
              Fin
                (Finset.card.{u_1} (α := α)
                  (↑(Sigma.fst (β := fun (t : ↥P.parts) ↦ Fin #(↑t : Finset α))
                        ((f : (a : ↥s) → (t : ↥P.parts) × Fin #(↑t : Finset α)) b)) :
                    Finset α))) :
          ℕ) *
        #P.parts +
      (↑((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 α)) b))) :
        ℕ)

Tactic:
simp_rw [z', z, Fin.mk.injEq, mul_comm #P.parts] at e

Premises used: Fin.mk.injEq, Finpartition.parts, mul_comm, Finset.card
-- 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
less : ∀ (a : ↥s), z a < #s
z' : ↥s → Fin #s := fun (a : ↥s) ↦ ⟨z a, ⋯⟩
a b : ↥s
e :
  (↑(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 +
      (↑((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))) :
        ℕ) =
    (↑(Sigma.snd (β := fun (t : ↥P.parts) ↦ Fin #(↑t : Finset α))
                ((f : (a : ↥s) → (t : ↥P.parts) × Fin #(↑t : Finset α)) b) :
              Fin
                (Finset.card.{u_1} (α := α)
                  (↑(Sigma.fst (β := fun (t : ↥P.parts) ↦ Fin #(↑t : Finset α))
                        ((f : (a : ↥s) → (t : ↥P.parts) × Fin #(↑t : Finset α)) b)) :
                    Finset α))) :
          ℕ) *
        #P.parts +
      (↑((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 α)) b))) :
        ℕ)
⊢ NeZero #P.parts

Tactic:
haveI : NeZero #P.parts := ⟨((Nat.zero_le _).trans_lt (gl a)).ne'⟩
-- 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
less : ∀ (a : ↥s), z a < #s
z' : ↥s → Fin #s := fun (a : ↥s) ↦ ⟨z a, ⋯⟩
a b : ↥s
this : NeZero #P.parts
e :
  Eq (α := ℕ)
      (Sigma.snd (β := fun (t : ↥P.parts) ↦ Fin #(↑t : Finset α))
          ((f : (a : ↥s) → (t : ↥P.parts) × Fin #(↑t : Finset α)) a)).1
      (Sigma.snd (β := fun (t : ↥P.parts) ↦ Fin #(↑t : Finset α))
          ((f : (a : ↥s) → (t : ↥P.parts) × Fin #(↑t : Finset α)) b)).1 ∧
    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))
apply_fun :
  Eq (α := (t : ↥P.parts) × Fin #(↑t : Finset α))
    ((f : (a : ↥s) → (t : ↥P.parts) × Fin #(↑t : Finset α)) a : (t : ↥P.parts) × Fin #(↑t : Finset α))
    ((f : (a : ↥s) → (t : ↥P.parts) × Fin #(↑t : Finset α)) b : (t : ↥P.parts) × Fin #(↑t : Finset α))
⊢ a = b

Tactic:
apply_fun f
-- 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
less : ∀ (a : ↥s), z a < #s
z' : ↥s → Fin #s := fun (a : ↥s) ↦ ⟨z a, ⋯⟩
a b : ↥s
this : NeZero #P.parts
e :
  Eq (α := ℕ)
      (Sigma.snd (β := fun (t : ↥P.parts) ↦ Fin #(↑t : Finset α))
          ((f : (a : ↥s) → (t : ↥P.parts) × Fin #(↑t : Finset α)) a)).1
      (Sigma.snd (β := fun (t : ↥P.parts) ↦ Fin #(↑t : Finset α))
          ((f : (a : ↥s) → (t : ↥P.parts) × Fin #(↑t : Finset α)) b)).1 ∧
    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))
rw rw₁ :
  Finset.card.{u_1} (α := α)
      (↑(Sigma.fst (β := fun (t : ↥P.parts) ↦ Fin #(↑t : Finset α))
            ((f : (a : ↥s) → (t : ↥P.parts) × Fin #(↑t : Finset α)) b)) :
        Finset α) =
    Finset.card.{u_1} (α := α)
      (↑(Sigma.fst (β := fun (t : ↥P.parts) ↦ Fin #(↑t : Finset α))
            ((f : (a : ↥s) → (t : ↥P.parts) × Fin #(↑t : Finset α)) b)) :
        Finset α)
⊢ Finset.card.{u_1} (α := α)
      (↑(Sigma.fst (β := fun (t : ↥P.parts) ↦ Fin #(↑t : Finset α))
            ((f : (a : ↥s) → (t : ↥P.parts) × Fin #(↑t : Finset α)) a)) :
        Finset α) =
    Finset.card.{u_1} (α := α)
      (↑(Sigma.fst (β := fun (t : ↥P.parts) ↦ Fin #(↑t : Finset α))
            ((f : (a : ↥s) → (t : ↥P.parts) × Fin #(↑t : Finset α)) b)) :
        Finset α)

Tactic:
rw [e.2]

Premises used: And.right
-- 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
less : ∀ (a : ↥s), z a < #s
z' : ↥s → Fin #s := fun (a : ↥s) ↦ ⟨z a, ⋯⟩
a b : ↥s
this : NeZero #P.parts
e :
  Eq (α := ℕ)
      (Sigma.snd (β := fun (t : ↥P.parts) ↦ Fin #(↑t : Finset α))
          ((f : (a : ↥s) → (t : ↥P.parts) × Fin #(↑t : Finset α)) a)).1
      (Sigma.snd (β := fun (t : ↥P.parts) ↦ Fin #(↑t : Finset α))
          ((f : (a : ↥s) → (t : ↥P.parts) × Fin #(↑t : Finset α)) b)).1 ∧
    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))
⊢ Eq (α := (t : ↥P.parts) × Fin #(↑t : Finset α))
    ((f : (a : ↥s) → (t : ↥P.parts) × Fin #(↑t : Finset α)) a : (t : ↥P.parts) × Fin #(↑t : Finset α))
    ((f : (a : ↥s) → (t : ↥P.parts) × Fin #(↑t : Finset α)) b : (t : ↥P.parts) × Fin #(↑t : Finset α))

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

Premises used: Iff.mpr, Fin.heq_ext_iff, And.right, And.left, Sigma.ext
-- 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
less : ∀ (a : ↥s), z a < #s
z' : ↥s → Fin #s := fun (a : ↥s) ↦ ⟨z a, ⋯⟩
⊢ Function.Bijective z'

Tactic:
have bij : z'.Bijective := by
    refine (bijective_iff_injective_and_card z').mpr ⟨fun a b e ↦ ?_, by simp⟩
    simp_rw [z', z, Fin.mk.injEq, mul_comm #P.parts] at e
    haveI : NeZero #P.parts := ⟨((Nat.zero_le _).trans_lt (gl a)).ne'⟩
    change (#P.parts).divModEquiv.symm (_, _) = (#P.parts).divModEquiv.symm (_, _) at e
    simp only [Equiv.apply_eq_iff_eq, Prod.mk.injEq] at e
    apply_fun f
    exact Sigma.ext e.2 <| (Fin.heq_ext_iff (by rw [e.2])).mpr e.1
-- 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
less : ∀ (a : ↥s), z a < #s
z' : ↥s → Fin #s := fun (a : ↥s) ↦ ⟨z a, ⋯⟩
bij : Function.Bijective z'
h :
  ∀ (a b : ↥s),
    P.part (↑a : α) = P.part (↑b : α) ↔
      (↑((Equiv.ofBijective z' bij : (a : ↥s) → Fin #s) a) : ℕ) % #P.parts =
        (↑((Equiv.ofBijective z' bij : (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:
use Equiv.ofBijective _ bij

Premises used: Equiv.ofBijective
-- Module: Mathlib.Order.Partition.Equipartition
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
⊢ ∀ a ∈ (↑(parts (a := s) ⊥) : Set (Finset α)), #a = 1 ∨ #a = HAdd.hAdd (α := ℕ) 1 1

Tactic:
simp
-- Module: Mathlib.Order.Partition.Equipartition
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
inst_1 : Decidable (s = ∅)
⊢ IsEquipartition.{u_1} (α := α) (s := s) ⊤

Tactic:
Set.Subsingleton.isEquipartition (parts_top_subsingleton _)

Premises used: Set.Subsingleton.isEquipartition, Finpartition.parts_top_subsingleton
-- Module: Mathlib.Order.Partition.Equipartition
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
hs : s ≠ ∅
rw : Set.EquitableOn (α := Finset α) {s} Finset.card
⊢ IsEquipartition.{u_1} (α := α) (s := s) (indiscrete hs)

Tactic:
rw [IsEquipartition, indiscrete_parts, coe_singleton]

Premises used: Finset.coe_singleton, Finpartition.indiscrete_parts, Finpartition.IsEquipartition
-- Module: Mathlib.Order.Partition.Equipartition
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
hs : s ≠ ∅
⊢ Set.EquitableOn (α := Finset α) {s} Finset.card

Tactic:
Set.equitableOn_singleton s _

Premises used: Set.equitableOn_singleton
-- Module: Mathlib.Order.Partition.Equipartition
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
hs : s ≠ ∅
⊢ Set.EquitableOn (α := Finset α) {s} Finset.card

Tactic:
exact Set.equitableOn_singleton s _

Premises used: Set.equitableOn_singleton