-- Lean 4 proof step from Mathlib.Order.Partition.Equipartition (hypothesis)
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 (α := ℕ)
    ((Equiv.symm (#P.parts).divModEquiv : (a : ℕ × Fin #P.parts) → ℕ)
        (((Sigma.snd (β := fun (t : ↥P.parts) ↦ Fin #(↑t : Finset α))
                ((f : (a : ↥s) → (t : ↥P.parts) × Fin #(↑t : Finset α)) a)).1,
            (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) :
      ℕ)
    ((Equiv.symm (#P.parts).divModEquiv : (a : ℕ × Fin #P.parts) → ℕ)
        (((Sigma.snd (β := fun (t : ↥P.parts) ↦ Fin #(↑t : Finset α))
                ((f : (a : ↥s) → (t : ↥P.parts) × Fin #(↑t : Finset α)) b)).1,
            (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) :
      ℕ)
⊢ a = b
have 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))
Tactic: simp only [Equiv.apply_eq_iff_eq, Prod.mk.injEq] at e
Cleared hypotheses: e