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
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
h : ¬0 < a
neg : t ∉ {i ∈ R.parts | #i = m + 1}
⊢ #(insert t ({i ∈ R.parts | #i = m + 1})) = b

Tactic:
rw [card_insert_of_notMem, hR₃, if_neg h, Nat.sub_add_cancel (hab.resolve_left h)]

Premises used: Or.resolve_left, Finset.card_insert_of_notMem, Nat.sub_add_cancel, if_neg
-- 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
h : ¬0 < a
H : t ∈ {i ∈ R.parts | #i = m + 1}
⊢ False

Tactic:
ht.ne_empty (le_sdiff_right.1 <| R.le <| filter_subset _ _ H)

Premises used: le_sdiff_right, Finset.filter_subset, Finset.Nonempty.ne_empty, Iff.mp, 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
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
h : ¬0 < a
H : t ∈ {i ∈ R.parts | #i = m + 1}
⊢ False

Tactic:
exact ht.ne_empty (le_sdiff_right.1 <| R.le <| filter_subset _ _ H)

Premises used: le_sdiff_right, Finset.filter_subset, Finset.Nonempty.ne_empty, Iff.mp, Finpartition.le
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
m a b : ℕ
P : Finpartition s
h : a * m + b * (m + 1) = #s
⊢ t ∈ parts (equitabilise (P := P) h) → #t = m ∨ #t = m + 1

Tactic:
(P.equitabilise_aux h).choose_spec.1 _

Premises used: Exists.choose_spec, Finpartition.equitabilise_aux, Set.Mem, setOf, And.left
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
m a b : ℕ
P : Finpartition s
h : a * m + b * (m + 1) = #s
⊢ IsEquipartition (equitabilise (P := P) h)

Tactic:
Set.equitableOn_iff_exists_eq_eq_add_one.2 ⟨m, fun _ => card_eq_of_mem_parts_equitabilise⟩

Premises used: Iff.mpr, Exists.intro, Finpartition.card_eq_of_mem_parts_equitabilise, Set.equitableOn_iff_exists_eq_eq_add_one, Finpartition.IsEquipartition
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
m a b : ℕ
P : Finpartition s
h : a * m + b * (m + 1) = #s
⊢ #({u ∈ parts (equitabilise (P := P) h) | #u = m + 1}) = b

Tactic:
(P.equitabilise_aux h).choose_spec.2.2

Premises used: Exists.choose_spec, Finpartition.equitabilise_aux, And.right
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
m a b : ℕ
P : Finpartition s
h : a * m + b * (m + 1) = #s
hm : m ≠ 0
⊢ #({u ∈ parts (equitabilise (P := P) h) | #u = m}) = a

Tactic:
(mul_eq_mul_right_iff.1 <| (add_left_inj (b * (m + 1))).1 ?_).resolve_right hm

Premises used: HMul.hMul, mul_eq_mul_right_iff, add_left_inj, HAdd.hAdd, Iff.mp, Or.resolve_right, OfNat.ofNat
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
m a b : ℕ
P : Finpartition s
h : a * m + b * (m + 1) = #s
hm : m ≠ 0
refine : #({u ∈ parts (equitabilise (P := P) h) | #u = m}) * m + b * (m + 1) = a * m + b * (m + 1)
⊢ #({u ∈ parts (equitabilise (P := P) h) | #u = m}) = a

Tactic:
refine (mul_eq_mul_right_iff.1 <| (add_left_inj (b * (m + 1))).1 ?_).resolve_right hm

Premises used: HMul.hMul, mul_eq_mul_right_iff, add_left_inj, HAdd.hAdd, Iff.mp, Or.resolve_right, OfNat.ofNat
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
m a b : ℕ
P : Finpartition s
h : a * m + b * (m + 1) = #s
hm : m ≠ 0
rw : #({u ∈ parts (equitabilise (P := P) h) | #u = m}) * m + b * (m + 1) = ∑ i ∈ parts (equitabilise (P := P) h), #i
⊢ #({u ∈ parts (equitabilise (P := P) h) | #u = m}) * m + b * (m + 1) = a * m + b * (m + 1)

Tactic:
rw [h, ← (P.equitabilise h).sum_card_parts]

Premises used: Finpartition.equitabilise, Finpartition.sum_card_parts
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
m a b : ℕ
P : Finpartition s
h : a * m + b * (m + 1) = #s
hm : m ≠ 0
rw : ∀ x ∈ parts (equitabilise (P := P) h), #x = m ∨ #x = m + 1
⊢ parts (equitabilise (P := P) h) =
    {u ∈ parts (equitabilise (P := P) h) | #u = m} ∪ {u ∈ parts (equitabilise (P := P) h) | #u = m + 1}

Tactic:
rw [← filter_or, filter_true_of_mem]

Premises used: Finset.filter_true_of_mem, Finset.filter_or
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
m a b : ℕ
P : Finpartition s
h : a * m + b * (m + 1) = #s
hm : m ≠ 0
⊢ ∀ x ∈ parts (equitabilise (P := P) h), #x = m ∨ #x = m + 1

Tactic:
fun x => card_eq_of_mem_parts_equitabilise

Premises used: Finpartition.card_eq_of_mem_parts_equitabilise
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
m a b : ℕ
P : Finpartition s
h : a * m + b * (m + 1) = #s
hm : m ≠ 0
⊢ ∀ x ∈ parts (equitabilise (P := P) h), #x = m ∨ #x = m + 1

Tactic:
exact fun x => card_eq_of_mem_parts_equitabilise

Premises used: Finpartition.card_eq_of_mem_parts_equitabilise
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
m a b : ℕ
P : Finpartition s
h : a * m + b * (m + 1) = #s
hm : m ≠ 0
⊢ parts (equitabilise (P := P) h) =
    {u ∈ parts (equitabilise (P := P) h) | #u = m} ∪ {u ∈ parts (equitabilise (P := P) h) | #u = m + 1}

Tactic:
have hunion :
    (P.equitabilise h).parts =
      {u ∈ (P.equitabilise h).parts | #u = m} ∪ {u ∈ (P.equitabilise h).parts | #u = m + 1} := by
    rw [← filter_or, filter_true_of_mem]
    exact fun x => card_eq_of_mem_parts_equitabilise
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
m a b : ℕ
P : Finpartition s
h : a * m + b * (m + 1) = #s
hm : m ≠ 0
hunion :
  parts (equitabilise (P := P) h) =
    {u ∈ parts (equitabilise (P := P) h) | #u = m} ∪ {u ∈ parts (equitabilise (P := P) h) | #u = m + 1}
nth_rw :
  #({u ∈ parts (equitabilise (P := P) h) | #u = m}) * m + b * (m + 1) =
    ∑ i ∈ {u ∈ parts (equitabilise (P := P) h) | #u = m} ∪ {u ∈ parts (equitabilise (P := P) h) | #u = m + 1}, #i
⊢ #({u ∈ parts (equitabilise (P := P) h) | #u = m}) * m + b * (m + 1) = ∑ i ∈ parts (equitabilise (P := P) h), #i

Tactic:
nth_rw 2 [hunion]
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
m a b : ℕ
P : Finpartition s
h : a * m + b * (m + 1) = #s
hm : m ≠ 0
hunion :
  parts (equitabilise (P := P) h) =
    {u ∈ parts (equitabilise (P := P) h) | #u = m} ∪ {u ∈ parts (equitabilise (P := P) h) | #u = m + 1}
rw : Disjoint ({u ∈ parts (equitabilise (P := P) h) | #u = m}) ({u ∈ parts (equitabilise (P := P) h) | #u = m + 1})
⊢ #({u ∈ parts (equitabilise (P := P) h) | #u = m}) * m + b * (m + 1) =
    ∑ i ∈ {u ∈ parts (equitabilise (P := P) h) | #u = m} ∪ {u ∈ parts (equitabilise (P := P) h) | #u = m + 1}, #i

Tactic:
rw [sum_union, sum_const_nat fun x hx => (mem_filter.1 hx).2,
    sum_const_nat fun x hx => (mem_filter.1 hx).2, P.card_filter_equitabilise_big]

Premises used: Finpartition.card_filter_equitabilise_big, Finset.sum_union, Finset.sum_const_nat, And.right, Iff.mp, Finset.mem_filter
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
m a b : ℕ
P : Finpartition s
h : a * m + b * (m + 1) = #s
hm : m ≠ 0
hunion :
  parts (equitabilise (P := P) h) =
    {u ∈ parts (equitabilise (P := P) h) | #u = m} ∪ {u ∈ parts (equitabilise (P := P) h) | #u = m + 1}
⊢ Disjoint ({u ∈ parts (equitabilise (P := P) h) | #u = m}) ({u ∈ parts (equitabilise (P := P) h) | #u = m + 1})

Tactic:
disjoint_filter_filter' _ _ ?_

Premises used: Finset.disjoint_filter_filter'
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
m a b : ℕ
P : Finpartition s
h : a * m + b * (m + 1) = #s
hm : m ≠ 0
hunion :
  parts (equitabilise (P := P) h) =
    {u ∈ parts (equitabilise (P := P) h) | #u = m} ∪ {u ∈ parts (equitabilise (P := P) h) | #u = m + 1}
refine : Disjoint.{u_1} (α := Finset α → Prop) (fun (u : Finset α) ↦ #u = m) fun (u : Finset α) ↦ #u = m + 1
⊢ Disjoint ({u ∈ parts (equitabilise (P := P) h) | #u = m}) ({u ∈ parts (equitabilise (P := P) h) | #u = m + 1})

Tactic:
refine disjoint_filter_filter' _ _ ?_

Premises used: Finset.disjoint_filter_filter'
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
m a b : ℕ
P : Finpartition s
h_1 : a * m + b * (m + 1) = #s
hm : m ≠ 0
hunion :
  parts (equitabilise (P := P) h_1) =
    {u ∈ parts (equitabilise (P := P) h_1) | #u = m} ∪ {u ∈ parts (equitabilise (P := P) h_1) | #u = m + 1}
x : Finset α → Prop
ha : x ≤ fun (u : Finset α) ↦ #u = m
hb : x ≤ fun (u : Finset α) ↦ #u = m + 1
i : Finset α
h : x i
apply : m.succ = m
⊢ ⊥ i

Tactic:
apply succ_ne_self m _

Premises used: Nat.succ_ne_self
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
m a b : ℕ
P : Finpartition s
h_1 : a * m + b * (m + 1) = #s
hm : m ≠ 0
hunion :
  parts (equitabilise (P := P) h_1) =
    {u ∈ parts (equitabilise (P := P) h_1) | #u = m} ∪ {u ∈ parts (equitabilise (P := P) h_1) | #u = m + 1}
x : Finset α → Prop
ha : x ≤ fun (u : Finset α) ↦ #u = m
hb : x ≤ fun (u : Finset α) ↦ #u = m + 1
i : Finset α
h : x i
⊢ m.succ = m

Tactic:
(hb i h).symm.trans (ha i h)

Premises used: Eq.symm, Eq.trans
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
m a b : ℕ
P : Finpartition s
h_1 : a * m + b * (m + 1) = #s
hm : m ≠ 0
hunion :
  parts (equitabilise (P := P) h_1) =
    {u ∈ parts (equitabilise (P := P) h_1) | #u = m} ∪ {u ∈ parts (equitabilise (P := P) h_1) | #u = m + 1}
x : Finset α → Prop
ha : x ≤ fun (u : Finset α) ↦ #u = m
hb : x ≤ fun (u : Finset α) ↦ #u = m + 1
i : Finset α
h : x i
⊢ m.succ = m

Tactic:
exact (hb i h).symm.trans (ha i h)

Premises used: Eq.symm, Eq.trans
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
m a b : ℕ
P : Finpartition s
h : a * m + b * (m + 1) = #s
hm : m ≠ 0
rw : Disjoint ({x ∈ parts (equitabilise (P := P) h) | #x = m}) ({x ∈ parts (equitabilise (P := P) h) | #x = m + 1})
⊢ #(parts (equitabilise (P := P) h)) = a + b

Tactic:
rw [← filter_true_of_mem fun x => card_eq_of_mem_parts_equitabilise, filter_or,
    card_union_of_disjoint, P.card_filter_equitabilise_small _ hm, P.card_filter_equitabilise_big]

Premises used: Finpartition.card_filter_equitabilise_big, Finset.filter_true_of_mem, Finset.filter_or, Finpartition.card_filter_equitabilise_small, Finpartition.card_eq_of_mem_parts_equitabilise, Finset.card_union_of_disjoint
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
m a b : ℕ
P : Finpartition s
h : a * m + b * (m + 1) = #s
hm : m ≠ 0
⊢ Disjoint ({x ∈ parts (equitabilise (P := P) h) | #x = m}) ({x ∈ parts (equitabilise (P := P) h) | #x = m + 1})

Tactic:
aesop (add norm disjoint_filter)

Premises used: Finset.disjoint_filter
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
m a b : ℕ
P : Finpartition s
h : a * m + b * (m + 1) = #s
⊢ t ∈ P.parts → #(t \ {u ∈ parts (equitabilise (P := P) h) | u ⊆ t}.biUnion id) ≤ m

Tactic:
(Classical.choose_spec <| P.equitabilise_aux h).2.1 t

Premises used: Finpartition.equitabilise_aux, Classical.choose_spec, And.right, And.left
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
n : ℕ
hn : n ≠ 0
hs : n ≤ #s
⊢ 0 < n

Tactic:
rw [← pos_iff_ne_zero] at hn

Premises used: pos_iff_ne_zero
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
n : ℕ
hn : n ≠ 0
hs : n ≤ #s
hn₁ : 0 < n
⊢ n ≤ #s

Tactic:
rw [← pos_iff_ne_zero] at hn

Premises used: pos_iff_ne_zero
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
n : ℕ
hn : 0 < n
hs : n ≤ #s
rw : n * (#s / n) - #s % n * (#s / n) + #s % n * (#s / n + 1) = #s
rw₁ : n * (#s / n) - #s % n * (#s / n) + (#s % n * (#s / n) + #s % n * 1) = #s
rw₂ : n * (#s / n) - #s % n * (#s / n) + #s % n * (#s / n) + #s % n * 1 = #s
rw₃ : n * (#s / n) + #s % n * 1 = #s
rw₄ : n * (#s / n) + #s % n = #s
rw₅ : #s % n + n * (#s / n) = #s
rw₆ rw₇ : #s = #s
⊢ (n - #s % n) * (#s / n) + #s % n * (#s / n + 1) = #s

Tactic:
rw [tsub_mul, mul_add, ← add_assoc,
      tsub_add_cancel_of_le (Nat.mul_le_mul_right _ (mod_lt _ hn).le), mul_one, add_comm,
      mod_add_div]

Premises used: Nat.mul_le_mul_right, add_assoc, tsub_add_cancel_of_le, LT.lt.le, add_comm, Nat.mod_lt, Nat.mod_add_div, mul_add, mul_one, tsub_mul
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
n : ℕ
hn : 0 < n
hs : n ≤ #s
⊢ (n - #s % n) * (#s / n) + #s % n * (#s / n + 1) = #s

Tactic:
have : (n - #s % n) * (#s / n) + #s % n * (#s / n + 1) = #s := by
    rw [tsub_mul, mul_add, ← add_assoc,
      tsub_add_cancel_of_le (Nat.mul_le_mul_right _ (mod_lt _ hn).le), mul_one, add_comm,
      mod_add_div]
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
n : ℕ
hn : 0 < n
hs : n ≤ #s
this : (n - #s % n) * (#s / n) + #s % n * (#s / n + 1) = #s
⊢ ∃ (P : Finpartition s), P.IsEquipartition ∧ #P.parts = n

Tactic:
⟨(indiscrete (card_pos.1 <| hn.trans_le hs).ne_empty).equitabilise this,
      equitabilise_isEquipartition, ?_⟩

Premises used: Finpartition.equitabilise, And.intro, Exists.intro, Finpartition.equitabilise_isEquipartition
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
n : ℕ
hn : 0 < n
hs : n ≤ #s
this : (n - #s % n) * (#s / n) + #s % n * (#s / n + 1) = #s
this₁ : #(parts (equitabilise (P := indiscrete ⋯) this)) = n
⊢ ∃ (P : Finpartition s), P.IsEquipartition ∧ #P.parts = n

Tactic:
refine
    ⟨(indiscrete (card_pos.1 <| hn.trans_le hs).ne_empty).equitabilise this,
      equitabilise_isEquipartition, ?_⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
n : ℕ
hn : 0 < n
hs : n ≤ #s
this : (n - #s % n) * (#s / n) + #s % n * (#s / n + 1) = #s
rw : n - #s % n + #s % n = n
rw₁ rw₂ : n = n
⊢ #(parts (equitabilise (P := indiscrete ⋯) this)) = n

Tactic:
rw [card_parts_equitabilise _ _ (Nat.div_pos hs hn).ne', tsub_add_cancel_of_le (mod_lt _ hn).le]

Premises used: tsub_add_cancel_of_le, LT.lt.le, Nat.mod_lt, LT.lt.ne', Finpartition.card_parts_equitabilise, Nat.div_pos
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Increment
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
hP : P.IsEquipartition
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPG : ¬P.IsUniform G ε
grw : #P.parts * HPow.hPow (α := ℕ) 4 #P.parts ≤ #P.parts * HPow.hPow (α := ℕ) 16 #P.parts
⊢ stepBound #P.parts ≤ Fintype.card α

Tactic:
grw [← hPα, stepBound]

Premises used: SzemerediRegularity.stepBound
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Increment
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
hP : P.IsEquipartition
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPG : ¬P.IsUniform G ε
bc : LE.le (α := ℕ) 4 16
⊢ #P.parts * HPow.hPow (α := ℕ) 4 #P.parts ≤ #P.parts * HPow.hPow (α := ℕ) 16 #P.parts

Tactic:
gcongr
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Increment
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
hP : P.IsEquipartition
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPG : ¬P.IsUniform G ε
⊢ LE.le (α := ℕ) 4 16

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Increment
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
hP : P.IsEquipartition
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPG : ¬P.IsUniform G ε
⊢ stepBound #P.parts ≤ Fintype.card α

Tactic:
have hPα' : stepBound #P.parts ≤ card α := by grw [← hPα, stepBound]; gcongr; simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Increment
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
hP : P.IsEquipartition
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPG : ¬P.IsUniform G ε
hPα' : stepBound #P.parts ≤ Fintype.card α
⊢ 0 < stepBound #P.parts

Tactic:
have hPpos : 0 < stepBound #P.parts := stepBound_pos (nonempty_of_not_uniform hPG).card_pos
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Increment
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
hP : P.IsEquipartition
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPG : ¬P.IsUniform G ε
hPα' : stepBound #P.parts ≤ Fintype.card α
hPpos : 0 < stepBound #P.parts
rw : ∑ A ∈ P.parts.attach, #(chunk hP G ε ⋯).parts = stepBound #P.parts
⊢ #(increment hP G ε).parts = stepBound #P.parts

Tactic:
rw [increment, card_bind]

Premises used: SzemerediRegularity.increment, Finpartition.card_bind
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Increment
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
hP : P.IsEquipartition
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPG : ¬P.IsUniform G ε
hPα' : stepBound #P.parts ≤ Fintype.card α
hPpos : 0 < stepBound #P.parts
simp_rw :
  HAdd.hAdd (α := ℕ)
      (∑ x :
        ↥({x ∈ P.parts.attach | #(↑x : Finset α) = m * 4 ^ #P.parts + (Fintype.card α / #P.parts - m * 4 ^ #P.parts)}),
        #(parts
            (equitabilise (P :=
              atomise (↑(↑x : ↥P.parts) : Finset α) (P.nonuniformWitnesses G ε (↑(↑x : ↥P.parts) : Finset α))) ⋯)))
      (∑ x :
        ↥({x ∈ P.parts.attach | ¬#(↑x : Finset α) = m * 4 ^ #P.parts + (Fintype.card α / #P.parts - m * 4 ^ #P.parts)}),
        #(parts
            (equitabilise (P :=
              atomise (↑(↑x : ↥P.parts) : Finset α) (P.nonuniformWitnesses G ε (↑(↑x : ↥P.parts) : Finset α))) ⋯))) =
    stepBound #P.parts
⊢ ∑ A ∈ P.parts.attach, #(chunk hP G ε ⋯).parts = stepBound #P.parts

Tactic:
simp_rw [chunk, apply_dite Finpartition.parts, apply_dite card, sum_dite]

Premises used: apply_dite, SzemerediRegularity.chunk, Finpartition.parts, Finset.card, Finset.sum_dite
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Increment
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
hP : P.IsEquipartition
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPG : ¬P.IsUniform G ε
hPα' : stepBound #P.parts ≤ Fintype.card α
hPpos : 0 < stepBound #P.parts
⊢ ∀
    (x :
      ↥({x ∈ P.parts.attach |
          ¬#(↑x : Finset α) =
              m * HPow.hPow (α := ℕ) 4 #P.parts + (Fintype.card α / #P.parts - m * HPow.hPow (α := ℕ) 4 #P.parts)})),
    Membership.mem (γ :=
        Finset
          ↥({x ∈ P.parts.attach |
              ¬#(↑x : Finset α) =
                  m * HPow.hPow (α := ℕ) 4 #P.parts + (Fintype.card α / #P.parts - m * HPow.hPow (α := ℕ) 4 #P.parts)}))
        univ x →
      #(parts
            (equitabilise (P :=
              atomise (↑(↑x : ↥P.parts) : Finset α) (P.nonuniformWitnesses G ε (↑(↑x : ↥P.parts) : Finset α))) ⋯)) =
        HPow.hPow (α := ℕ) 4 #P.parts - (Fintype.card α / #P.parts - m * HPow.hPow (α := ℕ) 4 #P.parts + 1) +
          (Fintype.card α / #P.parts - m * HPow.hPow (α := ℕ) 4 #P.parts + 1)

Tactic:
fun x hx => card_parts_equitabilise _ _ (Nat.div_pos hPα' hPpos).ne'

Premises used: LT.lt.ne', Finset.sum_dite._proof_1, Finpartition.card_parts_equitabilise, Finpartition.atomise, Finpartition.nonuniformWitnesses, SzemerediRegularity.card_aux₂, Subtype.val, Nat.div_pos, Subtype.property