-- Mathlib/Combinatorics/SimpleGraph/Regularity/Equitabilise.lean
theorem equitabilise_aux (hs : a * m + b * (m + 1) = #s) :
    ∃ Q : Finpartition s,
      (∀ x : Finset α, x ∈ Q.parts → #x = m ∨ #x = m + 1) ∧
        (∀ x, x ∈ P.parts → #(x \ {y ∈ Q.parts | y ⊆ x}.biUnion id) ≤ m) ∧
          #{i ∈ Q.parts | #i = m + 1} = b

Proof state:
case pos.intro.intro.intro.intro.intro.refine_3
α : Type u_1
inst✝ : DecidableEq α
m : ℕ
m_pos : m > 0
s : Finset α
ih :
  ∀ t ⊂ s,
    ∀ {a b : ℕ} {P : Finpartition t},
      a * m + b * (m + 1) = #t →
        ∃ Q,
          (∀ x ∈ Q.parts, #x = m ∨ #x = m + 1) ∧
            (∀ x ∈ P.parts, #(x \ (filter (fun y => y ⊆ x) Q.parts).biUnion id) ≤ m) ∧
              #(filter (fun i => #i = m + 1) Q.parts) = b
a b : ℕ
P : Finpartition s
hs : a * m + b * (m + 1) = #s
hab : 0 < a ∨ 0 < b
n : ℕ := if 0 < a then m else m + 1
hn : n = if 0 < a then m else m + 1
hn₀ : 0 < n
hn₁ : n ≤ m + 1
hn₂ : n ≤ a * m + b * (m + 1)
hn₃ : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = #s - n
h : ∀ u ∈ P.parts, #u < m + 1
t : Finset α
hts : t ⊆ s
htn : #t = n
ht : t.Nonempty
hcard : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = #(s \ t)
R : Finpartition (s \ t)
hR₁ : ∀ x ∈ R.parts, #x = m ∨ #x = m + 1
left✝ : ∀ x ∈ (P.avoid t).parts, #(x \ (filter (fun y => y ⊆ x) R.parts).biUnion id) ≤ m
hR₃ : #(filter (fun i => #i = m + 1) R.parts) = if 0 < a then b else b - 1
⊢ #(filter (fun i => #i = m + 1) (R.extend ⋯ ⋯ ⋯).parts) = b

Tactic:
simp_rw [extend_parts, filter_insert, htn, n, m.succ_ne_self.symm.ite_eq_right_iff]

Result:
case pos.intro.intro.intro.intro.intro.refine_3
α : Type u_1
inst✝ : DecidableEq α
m : ℕ
m_pos : m > 0
s : Finset α
ih :
  ∀ t ⊂ s,
    ∀ {a b : ℕ} {P : Finpartition t},
      a * m + b * (m + 1) = #t →
        ∃ Q,
          (∀ x ∈ Q.parts, #x = m ∨ #x = m + 1) ∧
            (∀ x ∈ P.parts, #(x \ (filter (fun y => y ⊆ x) Q.parts).biUnion id) ≤ m) ∧
              #(filter (fun i => #i = m + 1) Q.parts) = b
a b : ℕ
P : Finpartition s
hs : a * m + b * (m + 1) = #s
hab : 0 < a ∨ 0 < b
n : ℕ := if 0 < a then m else m + 1
hn : n = if 0 < a then m else m + 1
hn₀ : 0 < n
hn₁ : n ≤ m + 1
hn₂ : n ≤ a * m + b * (m + 1)
hn₃ : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = #s - n
h : ∀ u ∈ P.parts, #u < m + 1
t : Finset α
hts : t ⊆ s
htn : #t = n
ht : t.Nonempty
hcard : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = #(s \ t)
R : Finpartition (s \ t)
hR₁ : ∀ x ∈ R.parts, #x = m ∨ #x = m + 1
left✝ : ∀ x ∈ (P.avoid t).parts, #(x \ (filter (fun y => y ⊆ x) R.parts).biUnion id) ≤ m
hR₃ : #(filter (fun i => #i = m + 1) R.parts) = if 0 < a then b else b - 1
⊢ #(if ¬0 < a then insert t (filter (fun i => #i = m + 1) R.parts) else filter (fun i => #i = m + 1) R.parts) = b

Proof state:
case neg
α : Type u_1
inst✝ : DecidableEq α
m : ℕ
m_pos : m > 0
s : Finset α
ih :
  ∀ t ⊂ s,
    ∀ {a b : ℕ} {P : Finpartition t},
      a * m + b * (m + 1) = #t →
        ∃ Q,
          (∀ x ∈ Q.parts, #x = m ∨ #x = m + 1) ∧
            (∀ x ∈ P.parts, #(x \ (filter (fun y => y ⊆ x) Q.parts).biUnion id) ≤ m) ∧
              #(filter (fun i => #i = m + 1) Q.parts) = b
a b : ℕ
P : Finpartition s
hs : a * m + b * (m + 1) = #s
hab : 0 < a ∨ 0 < b
⊢ ∃ Q,
    (∀ x ∈ Q.parts, #x = m ∨ #x = m + 1) ∧
      (∀ x ∈ P.parts, #(x \ (filter (fun y => y ⊆ x) Q.parts).biUnion id) ≤ m) ∧
        #(filter (fun i => #i = m + 1) Q.parts) = b

Tactic:
set n := if 0 < a then m else m + 1 with hn

Result:
case neg
α : Type u_1
inst✝ : DecidableEq α
m : ℕ
m_pos : m > 0
s : Finset α
ih :
  ∀ t ⊂ s,
    ∀ {a b : ℕ} {P : Finpartition t},
      a * m + b * (m + 1) = #t →
        ∃ Q,
          (∀ x ∈ Q.parts, #x = m ∨ #x = m + 1) ∧
            (∀ x ∈ P.parts, #(x \ (filter (fun y => y ⊆ x) Q.parts).biUnion id) ≤ m) ∧
              #(filter (fun i => #i = m + 1) Q.parts) = b
a b : ℕ
P : Finpartition s
hs : a * m + b * (m + 1) = #s
hab : 0 < a ∨ 0 < b
n : ℕ := if 0 < a then m else m + 1
hn : n = if 0 < a then m else m + 1
⊢ ∃ Q,
    (∀ x ∈ Q.parts, #x = m ∨ #x = m + 1) ∧
      (∀ x ∈ P.parts, #(x \ (filter (fun y => y ⊆ x) Q.parts).biUnion id) ≤ m) ∧
        #(filter (fun i => #i = m + 1) Q.parts) = b