awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise
Goal:
α : Type u_1
inst : DecidableEq α
m : ℕ
m_pos : m > 0
s : Finset α
ih :
  ∀ t ⊂ s,
    ∀ {a b : ℕ} {P : Finpartition t} (hs : a * m + b * (m + 1) = #t),
      ∃ (Q : Finpartition t),
        (∀ x ∈ Q.parts, #x = m ∨ #x = m + 1) ∧
          (∀ x ∈ P.parts, #(x \ {y ∈ Q.parts | y ⊆ x}.biUnion id) ≤ m) ∧ #({i ∈ Q.parts | #i = m + 1}) = 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, m + 1 ≤ #u
neg :
  ∀ (u : Finset α) (hu₁ : u ∈ P.parts) (hu₂ : m + 1 ≤ #u),
    ∃ (Q : Finpartition s),
      (∀ x ∈ Q.parts, #x = m ∨ #x = m + 1) ∧
        (∀ x ∈ P.parts, #(x \ {y ∈ Q.parts | y ⊆ x}.biUnion id) ≤ m) ∧ #({i ∈ Q.parts | #i = m + 1}) = b
⊢ ∃ (Q : Finpartition s),
    (∀ x ∈ Q.parts, #x = m ∨ #x = m + 1) ∧
      (∀ x ∈ P.parts, #(x \ {y ∈ Q.parts | y ⊆ x}.biUnion id) ≤ m) ∧ #({i ∈ Q.parts | #i = m + 1}) = b

Tactic:
obtain ⟨u, hu₁, hu₂⟩ := h
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise
Goal:
α : Type u_1
inst : DecidableEq α
m : ℕ
m_pos : m > 0
s : Finset α
ih :
  ∀ t ⊂ s,
    ∀ {a b : ℕ} {P : Finpartition t} (hs : a * m + b * (m + 1) = #t),
      ∃ (Q : Finpartition t),
        (∀ x ∈ Q.parts, #x = m ∨ #x = m + 1) ∧
          (∀ x ∈ P.parts, #(x \ {y ∈ Q.parts | y ⊆ x}.biUnion id) ≤ m) ∧ #({i ∈ Q.parts | #i = m + 1}) = 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
neg :
  ∀ (t : Finset α) (htu : t ⊆ u) (htn : #t = n),
    ∃ (Q : Finpartition s),
      (∀ x ∈ Q.parts, #x = m ∨ #x = m + 1) ∧
        (∀ x ∈ P.parts, #(x \ {y ∈ Q.parts | y ⊆ x}.biUnion id) ≤ m) ∧ #({i ∈ Q.parts | #i = m + 1}) = b
⊢ ∃ (Q : Finpartition s),
    (∀ x ∈ Q.parts, #x = m ∨ #x = m + 1) ∧
      (∀ x ∈ P.parts, #(x \ {y ∈ Q.parts | y ⊆ x}.biUnion id) ≤ m) ∧ #({i ∈ Q.parts | #i = m + 1}) = b

Tactic:
obtain ⟨t, htu, htn⟩ := exists_subset_card_eq (hn₁.trans hu₂)

Premises used: Finset.exists_subset_card_eq, LE.le.trans
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise
Goal:
α : Type u_1
inst : DecidableEq α
m : ℕ
m_pos : m > 0
s : Finset α
ih :
  ∀ t ⊂ s,
    ∀ {a b : ℕ} {P : Finpartition t} (hs : a * m + b * (m + 1) = #t),
      ∃ (Q : Finpartition t),
        (∀ x ∈ Q.parts, #x = m ∨ #x = m + 1) ∧
          (∀ x ∈ P.parts, #(x \ {y ∈ Q.parts | y ⊆ x}.biUnion id) ≤ m) ∧ #({i ∈ Q.parts | #i = m + 1}) = 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
rwa : 0 < #t
rwa₁ rwa₂ rwa₃ rwa₄ : 0 < n
⊢ t.Nonempty

Tactic:
rwa [← card_pos, htn]

Premises used: Finset.card_pos
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise
Goal:
α : Type u_1
inst : DecidableEq α
m : ℕ
m_pos : m > 0
s : Finset α
ih :
  ∀ t ⊂ s,
    ∀ {a b : ℕ} {P : Finpartition t} (hs : a * m + b * (m + 1) = #t),
      ∃ (Q : Finpartition t),
        (∀ x ∈ Q.parts, #x = m ∨ #x = m + 1) ∧
          (∀ x ∈ P.parts, #(x \ {y ∈ Q.parts | y ⊆ x}.biUnion id) ≤ m) ∧ #({i ∈ Q.parts | #i = m + 1}) = 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
⊢ t.Nonempty

Tactic:
have ht : t.Nonempty := by rwa [← card_pos, htn]
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise
Goal:
α : Type u_1
inst : DecidableEq α
m : ℕ
m_pos : m > 0
s : Finset α
ih :
  ∀ t ⊂ s,
    ∀ {a b : ℕ} {P : Finpartition t} (hs : a * m + b * (m + 1) = #t),
      ∃ (Q : Finpartition t),
        (∀ x ∈ Q.parts, #x = m ∨ #x = m + 1) ∧
          (∀ x ∈ P.parts, #(x \ {y ∈ Q.parts | y ⊆ x}.biUnion id) ≤ m) ∧ #({i ∈ Q.parts | #i = m + 1}) = 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
rw : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = #s - #t
rw₁ : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = #s - n
rw₂ rw₃ : #s - n = #s - n
⊢ (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_of_subset (htu.trans <| P.le hu₁), htn, hn₃]

Premises used: Finset.card_sdiff_of_subset, HasSubset.Subset.trans, Finpartition.le
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise
Goal:
α : Type u_1
inst : DecidableEq α
m : ℕ
m_pos : m > 0
s : Finset α
ih :
  ∀ t ⊂ s,
    ∀ {a b : ℕ} {P : Finpartition t} (hs : a * m + b * (m + 1) = #t),
      ∃ (Q : Finpartition t),
        (∀ x ∈ Q.parts, #x = m ∨ #x = m + 1) ∧
          (∀ x ∈ P.parts, #(x \ {y ∈ Q.parts | y ⊆ x}.biUnion id) ≤ m) ∧ #({i ∈ Q.parts | #i = m + 1}) = 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
⊢ (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = #(s \ t)

Tactic:
have hcard : ite (0 < a) (a - 1) a * m + ite (0 < a) b (b - 1) * (m + 1) = #(s \ t) := by
    rw [card_sdiff_of_subset (htu.trans <| P.le hu₁), htn, hn₃]
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise
Goal:
α : Type u_1
inst : DecidableEq α
m : ℕ
m_pos : m > 0
s : Finset α
ih :
  ∀ t ⊂ s,
    ∀ {a b : ℕ} {P : Finpartition t} (hs : a * m + b * (m + 1) = #t),
      ∃ (Q : Finpartition t),
        (∀ x ∈ Q.parts, #x = m ∨ #x = m + 1) ∧
          (∀ x ∈ P.parts, #(x \ {y ∈ Q.parts | y ⊆ x}.biUnion id) ≤ m) ∧ #({i ∈ Q.parts | #i = m + 1}) = 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)
neg :
  ∀ (R : Finpartition (s \ t)) (hR₁ : ∀ x ∈ R.parts, #x = m ∨ #x = m + 1)
    (hR₂ : ∀ x ∈ parts (a := s \ t) (P.avoid t : Finpartition (s \ t)), #(x \ {y ∈ R.parts | y ⊆ x}.biUnion id) ≤ m)
    (hR₃ : #({i ∈ R.parts | #i = m + 1}) = if 0 < a then b else b - 1),
    ∃ (Q : Finpartition s),
      (∀ x ∈ Q.parts, #x = m ∨ #x = m + 1) ∧
        (∀ x ∈ P.parts, #(x \ {y ∈ Q.parts | y ⊆ x}.biUnion id) ≤ m) ∧ #({i ∈ Q.parts | #i = m + 1}) = b
⊢ ∃ (Q : Finpartition s),
    (∀ x ∈ Q.parts, #x = m ∨ #x = m + 1) ∧
      (∀ x ∈ P.parts, #(x \ {y ∈ Q.parts | y ⊆ x}.biUnion id) ≤ m) ∧ #({i ∈ Q.parts | #i = m + 1}) = b

Tactic:
obtain ⟨R, hR₁, hR₂, hR₃⟩ :=
    @ih (s \ t) (sdiff_ssubset (htu.trans <| P.le hu₁) ht) (if 0 < a then a - 1 else a)
      (if 0 < a then b else b - 1) (P.avoid t) hcard

Premises used: HasSubset.Subset.trans, SDiff.sdiff, Finpartition.le, Finset.sdiff_ssubset
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise
Goal:
α : Type u_1
inst : DecidableEq α
m : ℕ
m_pos : m > 0
s : Finset α
ih :
  ∀ t ⊂ s,
    ∀ {a b : ℕ} {P : Finpartition t} (hs : a * m + b * (m + 1) = #t),
      ∃ (Q : Finpartition t),
        (∀ x ∈ Q.parts, #x = m ∨ #x = m + 1) ∧
          (∀ x ∈ P.parts, #(x \ {y ∈ Q.parts | y ⊆ x}.biUnion id) ≤ m) ∧ #({i ∈ Q.parts | #i = m + 1}) = 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 ∈ parts (a := s \ t) (P.avoid t : Finpartition (s \ t)), #(x \ {y ∈ R.parts | y ⊆ x}.biUnion id) ≤ m
hR₃ : #({i ∈ R.parts | #i = m + 1}) = if 0 < a then b else b - 1
⊢ ∃ (Q : Finpartition s),
    (∀ x ∈ Q.parts, #x = m ∨ #x = m + 1) ∧
      (∀ x ∈ P.parts, #(x \ {y ∈ Q.parts | y ⊆ x}.biUnion id) ≤ m) ∧ #({i ∈ Q.parts | #i = m + 1}) = b

Tactic:
⟨R.extend ht.ne_empty sdiff_disjoint (sdiff_sup_cancel <| htu.trans <| P.le hu₁), ?_, ?_, ?_⟩

Premises used: sdiff_sup_cancel, HasSubset.Subset.trans, Finset.Nonempty.ne_empty, Finpartition.extend, And.intro, Exists.intro, Finpartition.le, Finset.sdiff_disjoint
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise
Goal:
α : Type u_1
inst : DecidableEq α
m : ℕ
m_pos : m > 0
s : Finset α
ih :
  ∀ t ⊂ s,
    ∀ {a b : ℕ} {P : Finpartition t} (hs : a * m + b * (m + 1) = #t),
      ∃ (Q : Finpartition t),
        (∀ x ∈ Q.parts, #x = m ∨ #x = m + 1) ∧
          (∀ x ∈ P.parts, #(x \ {y ∈ Q.parts | y ⊆ x}.biUnion id) ≤ m) ∧ #({i ∈ Q.parts | #i = m + 1}) = 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 ∈ parts (a := s \ t) (P.avoid t : Finpartition (s \ t)), #(x \ {y ∈ R.parts | y ⊆ x}.biUnion id) ≤ m
hR₃ : #({i ∈ R.parts | #i = m + 1}) = if 0 < a then b else b - 1
neg : ∀ x ∈ parts (a := s) (R.extend ⋯ ⋯ ⋯), #x = m ∨ #x = m + 1
neg₁ : ∀ x ∈ P.parts, #(x \ {y ∈ parts (a := s) (R.extend ⋯ ⋯ ⋯) | y ⊆ x}.biUnion id) ≤ m
neg₂ : #({i ∈ parts (a := s) (R.extend ⋯ ⋯ ⋯) | #i = m + 1}) = b
⊢ ∃ (Q : Finpartition s),
    (∀ x ∈ Q.parts, #x = m ∨ #x = m + 1) ∧
      (∀ x ∈ P.parts, #(x \ {y ∈ Q.parts | y ⊆ x}.biUnion id) ≤ m) ∧ #({i ∈ Q.parts | #i = m + 1}) = b

Tactic:
refine
    ⟨R.extend ht.ne_empty sdiff_disjoint (sdiff_sup_cancel <| htu.trans <| P.le hu₁), ?_, ?_, ?_⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise
Goal:
α : Type u_1
inst : DecidableEq α
m : ℕ
m_pos : m > 0
s : Finset α
ih :
  ∀ t ⊂ s,
    ∀ {a b : ℕ} {P : Finpartition t} (hs : a * m + b * (m + 1) = #t),
      ∃ (Q : Finpartition t),
        (∀ x ∈ Q.parts, #x = m ∨ #x = m + 1) ∧
          (∀ x ∈ P.parts, #(x \ {y ∈ Q.parts | y ⊆ x}.biUnion id) ≤ m) ∧ #({i ∈ Q.parts | #i = m + 1}) = 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 ∈ parts (a := s \ t) (P.avoid t : Finpartition (s \ t)), #(x \ {y ∈ R.parts | y ⊆ x}.biUnion id) ≤ m
hR₃ : #({i ∈ R.parts | #i = m + 1}) = if 0 < a then b else b - 1
neg : (if 0 < a then m else m + 1) = m ∨ (if 0 < a then m else m + 1) = m + 1
⊢ ∀ x ∈ parts (a := s) (R.extend ⋯ ⋯ ⋯), #x = m ∨ #x = m + 1

Tactic:
simp only [mem_insert, forall_eq_or_imp, extend_parts, and_iff_left hR₁, htn, hn]

Premises used: and_iff_left, Finpartition.extend_parts, Finset.mem_insert, forall_eq_or_imp
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise
Goal:
α : Type u_1
inst : DecidableEq α
m : ℕ
m_pos : m > 0
s : Finset α
ih :
  ∀ t ⊂ s,
    ∀ {a b : ℕ} {P : Finpartition t} (hs : a * m + b * (m + 1) = #t),
      ∃ (Q : Finpartition t),
        (∀ x ∈ Q.parts, #x = m ∨ #x = m + 1) ∧
          (∀ x ∈ P.parts, #(x \ {y ∈ Q.parts | y ⊆ x}.biUnion id) ≤ m) ∧ #({i ∈ Q.parts | #i = m + 1}) = 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 ∈ parts (a := s \ t) (P.avoid t : Finpartition (s \ t)), #(x \ {y ∈ R.parts | y ⊆ x}.biUnion id) ≤ m
hR₃ : #({i ∈ R.parts | #i = m + 1}) = if 0 < a then b else b - 1
⊢ (if 0 < a then m else m + 1) = m ∨ (if 0 < a then m else m + 1) = m + 1

Tactic:
ite_eq_or_eq _ _ _

Premises used: ite_eq_or_eq
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise
Goal:
α : Type u_1
inst : DecidableEq α
m : ℕ
m_pos : m > 0
s : Finset α
ih :
  ∀ t ⊂ s,
    ∀ {a b : ℕ} {P : Finpartition t} (hs : a * m + b * (m + 1) = #t),
      ∃ (Q : Finpartition t),
        (∀ x ∈ Q.parts, #x = m ∨ #x = m + 1) ∧
          (∀ x ∈ P.parts, #(x \ {y ∈ Q.parts | y ⊆ x}.biUnion id) ≤ m) ∧ #({i ∈ Q.parts | #i = m + 1}) = 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 ∈ parts (a := s \ t) (P.avoid t : Finpartition (s \ t)), #(x \ {y ∈ R.parts | y ⊆ x}.biUnion id) ≤ m
hR₃ : #({i ∈ R.parts | #i = m + 1}) = if 0 < a then b else b - 1
⊢ (if 0 < a then m else m + 1) = m ∨ (if 0 < a then m else m + 1) = m + 1

Tactic:
exact ite_eq_or_eq _ _ _

Premises used: ite_eq_or_eq
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise
Goal:
α : Type u_1
inst : DecidableEq α
m : ℕ
m_pos : m > 0
s : Finset α
ih :
  ∀ t ⊂ s,
    ∀ {a b : ℕ} {P : Finpartition t} (hs : a * m + b * (m + 1) = #t),
      ∃ (Q : Finpartition t),
        (∀ x ∈ Q.parts, #x = m ∨ #x = m + 1) ∧
          (∀ x ∈ P.parts, #(x \ {y ∈ Q.parts | y ⊆ x}.biUnion id) ≤ m) ∧ #({i ∈ Q.parts | #i = m + 1}) = 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 ∈ parts (a := s \ t) (P.avoid t : Finpartition (s \ t)), #(x \ {y ∈ R.parts | y ⊆ x}.biUnion id) ≤ m
hR₃ : #({i ∈ R.parts | #i = m + 1}) = if 0 < a then b else b - 1
x : Finset α
rw : x ∈ insert u (P.parts.erase u)
| x ∈ P.parts

Tactic:
rw [← insert_erase hu₁]

Premises used: Finset.insert_erase
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise
Goal:
α : Type u_1
inst : DecidableEq α
m : ℕ
m_pos : m > 0
s : Finset α
ih :
  ∀ t ⊂ s,
    ∀ {a b : ℕ} {P : Finpartition t} (hs : a * m + b * (m + 1) = #t),
      ∃ (Q : Finpartition t),
        (∀ x ∈ Q.parts, #x = m ∨ #x = m + 1) ∧
          (∀ x ∈ P.parts, #(x \ {y ∈ Q.parts | y ⊆ x}.biUnion id) ≤ m) ∧ #({i ∈ Q.parts | #i = m + 1}) = 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 ∈ parts (a := s \ t) (P.avoid t : Finpartition (s \ t)), #(x \ {y ∈ R.parts | y ⊆ x}.biUnion id) ≤ m
hR₃ : #({i ∈ R.parts | #i = m + 1}) = if 0 < a then b else b - 1
neg : ∀ x ∈ insert u (P.parts.erase u), #(x \ {y ∈ parts (a := s) (R.extend ⋯ ⋯ ⋯) | y ⊆ x}.biUnion id) ≤ m
⊢ ∀ x ∈ P.parts, #(x \ {y ∈ parts (a := s) (R.extend ⋯ ⋯ ⋯) | y ⊆ x}.biUnion id) ≤ m

Tactic:
conv in _ ∈ _ => rw [← insert_erase hu₁]

Premises used: Finset.insert_erase
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise
Goal:
α : Type u_1
inst : DecidableEq α
m : ℕ
m_pos : m > 0
s : Finset α
ih :
  ∀ t ⊂ s,
    ∀ {a b : ℕ} {P : Finpartition t} (hs : a * m + b * (m + 1) = #t),
      ∃ (Q : Finpartition t),
        (∀ x ∈ Q.parts, #x = m ∨ #x = m + 1) ∧
          (∀ x ∈ P.parts, #(x \ {y ∈ Q.parts | y ⊆ x}.biUnion id) ≤ m) ∧ #({i ∈ Q.parts | #i = m + 1}) = 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 ∈ parts (a := s \ t) (P.avoid t : Finpartition (s \ t)), #(x \ {y ∈ R.parts | y ⊆ x}.biUnion id) ≤ m
hR₃ : #({i ∈ R.parts | #i = m + 1}) = if 0 < a then b else b - 1
neg :
  #(u \ {y ∈ insert t R.parts | y ⊆ u}.biUnion id) ≤ m ∧
    ∀ a ∈ P.parts.erase u, #(a \ {y ∈ insert t R.parts | y ⊆ a}.biUnion id) ≤ m
⊢ ∀ x ∈ insert u (P.parts.erase u), #(x \ {y ∈ parts (a := s) (R.extend ⋯ ⋯ ⋯) | y ⊆ x}.biUnion id) ≤ m

Tactic:
simp only [mem_insert, forall_eq_or_imp, extend_parts]

Premises used: Finpartition.extend_parts, Finset.mem_insert, forall_eq_or_imp
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise
Goal:
α : Type u_1
inst : DecidableEq α
m : ℕ
m_pos : m > 0
s : Finset α
ih :
  ∀ t ⊂ s,
    ∀ {a b : ℕ} {P : Finpartition t} (hs : a * m + b * (m + 1) = #t),
      ∃ (Q : Finpartition t),
        (∀ x ∈ Q.parts, #x = m ∨ #x = m + 1) ∧
          (∀ x ∈ P.parts, #(x \ {y ∈ Q.parts | y ⊆ x}.biUnion id) ≤ m) ∧ #({i ∈ Q.parts | #i = m + 1}) = 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 ∈ parts (a := s \ t) (P.avoid t : Finpartition (s \ t)), #(x \ {y ∈ R.parts | y ⊆ x}.biUnion id) ≤ m
hR₃ : #({i ∈ R.parts | #i = m + 1}) = if 0 < a then b else b - 1
⊢ #(u \ {y ∈ insert t R.parts | y ⊆ u}.biUnion id) ≤ m ∧
    ∀ a ∈ P.parts.erase u, #(a \ {y ∈ insert t R.parts | y ⊆ a}.biUnion id) ≤ m

Tactic:
⟨?_, fun x hx => (card_le_card ?_).trans <| hR₂ x ?_⟩

Premises used: Finset.card_le_card, And.intro, LE.le.trans
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise
Goal:
α : Type u_1
inst : DecidableEq α
m : ℕ
m_pos : m > 0
s : Finset α
ih :
  ∀ t ⊂ s,
    ∀ {a b : ℕ} {P : Finpartition t} (hs : a * m + b * (m + 1) = #t),
      ∃ (Q : Finpartition t),
        (∀ x ∈ Q.parts, #x = m ∨ #x = m + 1) ∧
          (∀ x ∈ P.parts, #(x \ {y ∈ Q.parts | y ⊆ x}.biUnion id) ≤ m) ∧ #({i ∈ Q.parts | #i = m + 1}) = 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 ∈ parts (a := s \ t) (P.avoid t : Finpartition (s \ t)), #(x \ {y ∈ R.parts | y ⊆ x}.biUnion id) ≤ m
hR₃ : #({i ∈ R.parts | #i = m + 1}) = if 0 < a then b else b - 1
neg : #(u \ {y ∈ insert t R.parts | y ⊆ u}.biUnion id) ≤ m
neg₁ :
  ∀ (x : Finset α) (hx : x ∈ P.parts.erase u),
    x \ {y ∈ insert t R.parts | y ⊆ x}.biUnion id ⊆ x \ {y ∈ R.parts | y ⊆ x}.biUnion id
neg₂ : ∀ (x : Finset α) (hx : x ∈ P.parts.erase u), x ∈ parts (a := s \ t) (P.avoid t : Finpartition (s \ t))
⊢ #(u \ {y ∈ insert t R.parts | y ⊆ u}.biUnion id) ≤ m ∧
    ∀ a ∈ P.parts.erase u, #(a \ {y ∈ insert t R.parts | y ⊆ a}.biUnion id) ≤ m

Tactic:
refine ⟨?_, fun x hx => (card_le_card ?_).trans <| hR₂ x ?_⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise
Goal:
α : Type u_1
inst : DecidableEq α
m : ℕ
m_pos : m > 0
s : Finset α
ih :
  ∀ t ⊂ s,
    ∀ {a b : ℕ} {P : Finpartition t} (hs : a * m + b * (m + 1) = #t),
      ∃ (Q : Finpartition t),
        (∀ x ∈ Q.parts, #x = m ∨ #x = m + 1) ∧
          (∀ x ∈ P.parts, #(x \ {y ∈ Q.parts | y ⊆ x}.biUnion id) ≤ m) ∧ #({i ∈ Q.parts | #i = m + 1}) = 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 ∈ parts (a := s \ t) (P.avoid t : Finpartition (s \ t)), #(x \ {y ∈ R.parts | y ⊆ x}.biUnion id) ≤ m
hR₃ : #({i ∈ R.parts | #i = m + 1}) = if 0 < a then b else b - 1
neg : #(u \ (t ∪ {y ∈ R.parts | y ⊆ u}.biUnion id)) ≤ m
⊢ #(u \ {y ∈ insert t R.parts | y ⊆ u}.biUnion id) ≤ m

Tactic:
simp only [filter_insert, if_pos htu, biUnion_insert, id]

Premises used: id, if_pos, Finset.biUnion_insert, Finset.filter_insert