-- 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'
a b : ↥s
h :
  P.part (↑a : α) = P.part (↑b : α) ↔
    (↑((Equiv.ofBijective (fun (a : ↥s) ↦ (⟨z a, ⋯⟩ : Fin #s)) bij : (a : ↥s) → Fin #s) a) : ℕ) % #P.parts =
      (↑((Equiv.ofBijective (fun (a : ↥s) ↦ (⟨z a, ⋯⟩ : Fin #s)) bij : (a : ↥s) → Fin #s) b) : ℕ) % #P.parts
h₁ :
  P.part (↑a : α) = P.part (↑b : α) ↔
    (↑((Equiv.ofBijective
                  (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))) :
                            ℕ),
                        ⋯⟩ :
                      Fin #s))
                  bij :
                (a : ↥s) → Fin #s)
              a) :
          ℕ) %
        #P.parts =
      (↑((Equiv.ofBijective
                  (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))) :
                            ℕ),
                        ⋯⟩ :
                      Fin #s))
                  bij :
                (a : ↥s) → Fin #s)
              b) :
          ℕ) %
        #P.parts
h₂ :
  P.part (↑a : α) = P.part (↑b : α) ↔
    (#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 =
      (#P.parts *
            (↑(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 α))) :
              ℕ) +
          (↑((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))) :
            ℕ)) %
        #P.parts
h₃ :
  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)) ↔
    (#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 =
      (#P.parts *
            (↑(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 α))) :
              ℕ) +
          (↑((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))) :
            ℕ)) %
        #P.parts
h₄ :
  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 : (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 =
      (↑((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))) :
          ℕ) %
        #P.parts
h₅ :
  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 : (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))) :
        ℕ) =
      (↑((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))) :
          ℕ) %
        #P.parts
h₆ :
  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 : (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))) :
        ℕ) =
      (↑((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))) :
        ℕ)
h₇ :
  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 (α := Fin #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)) :
        Fin #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)) :
        Fin #P.parts)
⊢ 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

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]

Premises used: Equiv.ofBijective_apply, Nat.mul_add_mod, Nat.mod_eq_of_lt, Equiv.apply_eq_iff_eq, Fin.val_eq_val