-- Lean 4 proof step from Mathlib.Order.Partition.Equipartition (goal)
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
pos :
  ∀ (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
⊢ #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
have neg : ∀ (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: by_cases hc : #p = #s / #P.parts + 1