-- 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 neg.intro.intro.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
u : Finset α
hu₁ : u ∈ P.parts
hu₂ : m + 1 ≤ #u
t : Finset α
htu : t ⊆ u
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
hR₂ : ∀ 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 only [extend_parts, filter_insert, htn, hn, m.succ_ne_self.symm.ite_eq_right_iff]

Result:
case neg.intro.intro.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
u : Finset α
hu₁ : u ∈ P.parts
hu₂ : m + 1 ≤ #u
t : Finset α
htu : t ⊆ u
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
hR₂ : ∀ 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 pos.intro.intro
α : 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
⊢ ∃ 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:
have ht : t.Nonempty := by rwa [← card_pos, htn]

Result:
case pos.intro.intro
α : 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
⊢ ∃ 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

Proof state:
α : 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
⊢ (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = #(s \ t)

Tactic:
rw [card_sdiff ‹t ⊆ s›, htn, hn₃]

Result:
no goals

Proof state:
case inl
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a b : ℕ
P : Finpartition s
hs : a * 0 + b * (0 + 1) = #s
⊢ ∀ x ∈ P.parts, ∀ ⦃x_1 : α⦄, x_1 ∈ x → ∃ a ∈ ⊥.parts, (∀ ⦃x_2 : α⦄, x_2 ∈ a → x_2 ∈ x) ∧ x_1 ∈ a

Tactic:
exact fun x hx a ha =>
  ⟨{a}, mem_map_of_mem _ (P.le hx ha), singleton_subset_iff.2 ha, mem_singleton_self _⟩

Result:
no goals