awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise (goal)
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
hut : u ≠ t
⊢ #(u \ (t ∪ {y ∈ R.parts | y ⊆ u}.biUnion id)) ≤ m
have neg : ∀ i ∈ u \ (t ∪ {y ∈ R.parts | y ⊆ u}.biUnion id), i ∈ (u \ t) \ {y ∈ R.parts | y ⊆ u \ t}.biUnion id
Tactic: refine
        (card_le_card fun i => ?_).trans
          (hR₂ (u \ t) <| P.mem_avoid.2 ⟨u, hu₁, fun i => hut <| i.antisymm htu, rfl⟩)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise (goal)
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 α
hx : x ∈ P.parts.erase u
⊢ x \ {y ∈ insert t R.parts | y ⊆ x}.biUnion id ⊆ x \ {y ∈ R.parts | y ⊆ x}.biUnion id
have apply : {y ∈ R.parts | y ⊆ x} ⊆ {y ∈ insert t R.parts | y ⊆ x}
Tactic: apply sdiff_subset_sdiff Subset.rfl (biUnion_subset_biUnion_of_subset_left _ _)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise (goal)
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 α
hx : x ∈ P.parts.erase u
⊢ x ∈ parts (a := s \ t) (P.avoid t : Finpartition (s \ t))
have neg : x ≠ ∅ ∧ ∃ a ∈ P.parts, a \ t = x
Tactic: simp only [avoid, ofErase, mem_erase, mem_image, bot_eq_empty]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise (goal)
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
⊢ #({i ∈ parts (a := s) (R.extend ⋯ ⋯ ⋯) | #i = m + 1}) = b
have neg : #(if ¬0 < a then insert t ({i ∈ R.parts | #i = m + 1}) else {i ∈ R.parts | #i = m + 1}) = b
Tactic: simp only [extend_parts, filter_insert, htn, hn, m.succ_ne_self.symm.ite_eq_right_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise (goal)
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 insert t ({i ∈ R.parts | #i = m + 1}) else {i ∈ R.parts | #i = m + 1}) = b
have pos : ∀ (h : 0 < a), #({i ∈ R.parts | #i = m + 1}) = b
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise (goal)
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
pos : ∀ (h : 0 < a), #({i ∈ R.parts | #i = m + 1}) = b
⊢ #(if ¬0 < a then insert t ({i ∈ R.parts | #i = m + 1}) else {i ∈ R.parts | #i = m + 1}) = b
have neg : ∀ (h : ¬0 < a), #(insert t ({i ∈ R.parts | #i = m + 1})) = b
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise (goal)
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
⊢ #({i ∈ R.parts | #i = m + 1}) = b
have pos : (if 0 < a then b else b - 1) = b
Tactic: rw [hR₃, if_pos h]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise (goal)
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
pos : (if 0 < a then b else b - 1) = b
⊢ #({i ∈ R.parts | #i = m + 1}) = b
have pos₁ : b = b
Tactic: rw [hR₃, if_pos h]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise (goal)
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
⊢ #(insert t ({i ∈ R.parts | #i = m + 1})) = b
have neg : t ∉ {i ∈ R.parts | #i = m + 1}
Tactic: rw [card_insert_of_notMem, hR₃, if_neg h, Nat.sub_add_cancel (hab.resolve_left h)]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise (goal)
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
have refine : #({u ∈ parts (equitabilise (P := P) h) | #u = m}) * m + b * (m + 1) = a * m + b * (m + 1)
Tactic: refine (mul_eq_mul_right_iff.1 <| (add_left_inj (b * (m + 1))).1 ?_).resolve_right hm
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise (goal)
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}) * m + b * (m + 1) = a * m + b * (m + 1)
have rw : #({u ∈ parts (equitabilise (P := P) h) | #u = m}) * m + b * (m + 1) = ∑ i ∈ parts (equitabilise (P := P) h), #i
Tactic: rw [h, ← (P.equitabilise h).sum_card_parts]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise (goal)
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}
have rw : ∀ x ∈ parts (equitabilise (P := P) h), #x = m ∨ #x = m + 1
Tactic: rw [← filter_or, filter_true_of_mem]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise (hypothesis)
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}) * m + b * (m + 1) = ∑ i ∈ parts (equitabilise (P := P) h), #i
have hunion : 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
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise (goal)
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}
⊢ #({u ∈ parts (equitabilise (P := P) h) | #u = m}) * m + b * (m + 1) = ∑ i ∈ parts (equitabilise (P := P) h), #i
have 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
Tactic: nth_rw 2 [hunion]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise (goal)
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}
⊢ #({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
have rw : Disjoint ({u ∈ parts (equitabilise (P := P) h) | #u = m}) ({u ∈ parts (equitabilise (P := P) h) | #u = m + 1})
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]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise (goal)
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})
have refine : Disjoint.{u_1} (α := Finset α → Prop) (fun (u : Finset α) ↦ #u = m) fun (u : Finset α) ↦ #u = m + 1
Tactic: refine disjoint_filter_filter' _ _ ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise (goal)
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
⊢ ⊥ i
have apply : m.succ = m
Tactic: apply succ_ne_self m _
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise (goal)
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)) = a + b
have rw : Disjoint ({x ∈ parts (equitabilise (P := P) h) | #x = m}) ({x ∈ parts (equitabilise (P := P) h) | #x = m + 1})
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]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
n : ℕ
hn : n ≠ 0
hs : n ≤ #s
⊢ ∃ (P : Finpartition s), P.IsEquipartition ∧ #P.parts = n
have hn₁ : 0 < n
Tactic: rw [← pos_iff_ne_zero] at hn
Cleared hypotheses: hn, hs
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise (goal)
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
have rw : n * (#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]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise (goal)
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
⊢ (n - #s % n) * (#s / n) + #s % n * (#s / n + 1) = #s
have rw₁ : n * (#s / n) - #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]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise (goal)
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
⊢ (n - #s % n) * (#s / n) + #s % n * (#s / n + 1) = #s
have rw₂ : n * (#s / n) - #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]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise (goal)
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
⊢ (n - #s % n) * (#s / n) + #s % n * (#s / n + 1) = #s
have rw₃ : 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]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise (goal)
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
⊢ (n - #s % n) * (#s / n) + #s % n * (#s / n + 1) = #s
have rw₄ : n * (#s / n) + #s % n = #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]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise (goal)
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
⊢ (n - #s % n) * (#s / n) + #s % n * (#s / n + 1) = #s
have rw₅ : #s % n + n * (#s / n) = #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]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise (goal)
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
⊢ (n - #s % n) * (#s / n) + #s % n * (#s / n + 1) = #s
have rw₆ : #s = #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]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
n : ℕ
hn : 0 < n
hs : n ≤ #s
⊢ ∃ (P : Finpartition s), P.IsEquipartition ∧ #P.parts = n
have this : (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]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise (goal)
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
have this₁ : #(parts (equitabilise (P := indiscrete sorry) this)) = n
Tactic: refine
    ⟨(indiscrete (card_pos.1 <| hn.trans_le hs).ne_empty).equitabilise this,
      equitabilise_isEquipartition, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise (goal)
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
⊢ #(parts (equitabilise (P := indiscrete ⋯) this)) = n
have rw : n - #s % n + #s % n = n
Tactic: rw [card_parts_equitabilise _ _ (Nat.div_pos hs hn).ne', tsub_add_cancel_of_le (mod_lt _ hn).le]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise (goal)
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
⊢ #(parts (equitabilise (P := indiscrete ⋯) this)) = n
have rw₁ : n = n
Tactic: rw [card_parts_equitabilise _ _ (Nat.div_pos hs hn).ne', tsub_add_cancel_of_le (mod_lt _ hn).le]