-- 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
⊢ #(if ¬0 < a then insert t (filter (fun i => #i = m + 1) R.parts) else filter (fun i => #i = m + 1) R.parts) = b

Tactic:
split_ifs with ha

Result:
case pos
α : 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
ha : 0 < a
⊢ #(filter (fun i => #i = m + 1) R.parts) = b

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
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
ha : ¬0 < a
⊢ #(insert t (filter (fun i => #i = m + 1) R.parts)) = b

Proof state:
case neg.intro.intro.intro.intro.intro.intro.intro.refine_2.refine_1.inl
α : 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
htu : u ⊆ u
htn : #u = n
ht : u.Nonempty
hcard : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = #(s \ u)
R : Finpartition (s \ u)
hR₁ : ∀ x ∈ R.parts, #x = m ∨ #x = m + 1
hR₂ : ∀ x ∈ (P.avoid u).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
⊢ #(u \ (u ∪ (filter (fun y => y ⊆ u) R.parts).biUnion id)) ≤ m

Tactic:
rw [sdiff_eq_empty_iff_subset.2 subset_union_left]

Result:
case neg.intro.intro.intro.intro.intro.intro.intro.refine_2.refine_1.inl
α : 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
htu : u ⊆ u
htn : #u = n
ht : u.Nonempty
hcard : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = #(s \ u)
R : Finpartition (s \ u)
hR₁ : ∀ x ∈ R.parts, #x = m ∨ #x = m + 1
hR₂ : ∀ x ∈ (P.avoid u).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
⊢ #∅ ≤ m

Proof state:
α : Type u_1
inst✝ : DecidableEq α
m : ℕ
m_pos : m > 0
a b : ℕ
hab : a = 0 ∧ b = 0
ih :
  ∀ t ⊂ ∅,
    ∀ {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
P : Finpartition ∅
this : P = Finpartition.empty (Finset α)
⊢ ∀ x ∈ (Finpartition.empty (Finset α)).parts, #x = m ∨ #x = m + 1

Tactic:
simp

Result:
no goals