awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
hP : P.IsEquipartition
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst_3 : Nonempty α
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hε₁ : ε ≤ 1
hU : U ∈ P.parts
hV : V ∈ P.parts
hUVne : U ≠ V
hUV : ¬G.IsUniform ε U V
t : (star hP G ε hU V).product (star hP G ε hV U) ⊆ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts
hε : 0 ≤ ε
sp : ∀ (a b : Finset (Finset α)), a.product b = a ×ˢ b
refine_2 :
  HPow.hPow (β := ℕ)
      ((∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, (↑(G.edgeDensity ab.1 ab.2) : ℝ)) /
        HPow.hPow (α := ℝ) 16 #P.parts)
      2 ≤
    HPow.hPow (β := ℕ)
      (HDiv.hDiv (α := ℝ)
        (∑ i ∈ (chunk hP G ε hU).parts ×ˢ (chunk hP G ε hV).parts,
          (fun (x : Finset α × Finset α) ↦ ((↑(G.edgeDensity x.1 x.2) : ℝ) : ℝ)) i)
        (↑(#(chunk hP G ε hU).parts * #(chunk hP G ε hV).parts) : ℝ))
      2
⊢ HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity U V) : ℝ) 2 - HPow.hPow (β := ℕ) ε 5 / 25 ≤
    HPow.hPow (β := ℕ)
      (HDiv.hDiv (α := ℝ)
        (∑ i ∈ (chunk hP G ε hU).parts ×ˢ (chunk hP G ε hV).parts,
          (fun (x : Finset α × Finset α) ↦ ((↑(G.edgeDensity x.1 x.2) : ℝ) : ℝ)) i)
        (↑(#(chunk hP G ε hU).parts * #(chunk hP G ε hV).parts) : ℝ))
      2

Tactic:
apply (edgeDensity_chunk_aux hP hPα hPε hU hV).trans

Premises used: _private.0.SzemerediRegularity.edgeDensity_chunk_aux, LE.le.trans
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
hP : P.IsEquipartition
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst_3 : Nonempty α
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hε₁ : ε ≤ 1
hU : U ∈ P.parts
hV : V ∈ P.parts
hUVne : U ≠ V
hUV : ¬G.IsUniform ε U V
t : (star hP G ε hU V).product (star hP G ε hV U) ⊆ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts
hε : 0 ≤ ε
sp : ∀ (a b : Finset (Finset α)), a.product b = a ×ˢ b
refine_2 :
  HPow.hPow (β := ℕ)
      ((∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, (↑(G.edgeDensity ab.1 ab.2) : ℝ)) /
        HPow.hPow (α := ℝ) 16 #P.parts)
      2 ≤
    HPow.hPow (β := ℕ)
      (HDiv.hDiv (α := ℝ)
        (∑ i ∈ (chunk hP G ε hU).parts ×ˢ (chunk hP G ε hV).parts,
          (fun (x : Finset α × Finset α) ↦ ((↑(G.edgeDensity x.1 x.2) : ℝ) : ℝ)) i)
        (↑(HMul.hMul (α := ℕ) 4 4 ^ #P.parts) : ℝ))
      2
⊢ HPow.hPow (β := ℕ)
      ((∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, (↑(G.edgeDensity ab.1 ab.2) : ℝ)) /
        HPow.hPow (α := ℝ) 16 #P.parts)
      2 ≤
    HPow.hPow (β := ℕ)
      (HDiv.hDiv (α := ℝ)
        (∑ i ∈ (chunk hP G ε hU).parts ×ˢ (chunk hP G ε hV).parts,
          (fun (x : Finset α × Finset α) ↦ ((↑(G.edgeDensity x.1 x.2) : ℝ) : ℝ)) i)
        (↑(#(chunk hP G ε hU).parts * #(chunk hP G ε hV).parts) : ℝ))
      2

Tactic:
rw [card_chunk (m_pos hPα).ne', card_chunk (m_pos hPα).ne', ← mul_pow]

Premises used: SzemerediRegularity.card_chunk, SzemerediRegularity.m_pos, LT.lt.ne', mul_pow
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
hP : P.IsEquipartition
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst_3 : Nonempty α
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hε₁ : ε ≤ 1
hU : U ∈ P.parts
hV : V ∈ P.parts
hUVne : U ≠ V
hUV : ¬G.IsUniform ε U V
t : (star hP G ε hU V).product (star hP G ε hV U) ⊆ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts
hε : 0 ≤ ε
sp : ∀ (a b : Finset (Finset α)), a.product b = a ×ˢ b
⊢ HPow.hPow (β := ℕ)
      ((∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, (↑(G.edgeDensity ab.1 ab.2) : ℝ)) /
        HPow.hPow (α := ℝ) 16 #P.parts)
      2 ≤
    HPow.hPow (β := ℕ)
      (HDiv.hDiv (α := ℝ)
        (∑ i ∈ (chunk hP G ε hU).parts ×ˢ (chunk hP G ε hV).parts,
          (fun (x : Finset α × Finset α) ↦ ((↑(G.edgeDensity x.1 x.2) : ℝ) : ℝ)) i)
        (↑(HMul.hMul (α := ℕ) 4 4 ^ #P.parts) : ℝ))
      2

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
hP : P.IsEquipartition
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst_3 : Nonempty α
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hU : U ∈ P.parts
hV : V ∈ P.parts
apply :
  HPow.hPow (β := ℕ)
      ((∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, (↑(G.edgeDensity ab.1 ab.2) : ℝ)) /
        HPow.hPow (α := ℝ) 16 #P.parts)
      2 ≤
    (∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts,
        HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity ab.1 ab.2) : ℝ) 2) /
      HPow.hPow (α := ℝ) 16 #P.parts
⊢ HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity U V) : ℝ) 2 - HPow.hPow (β := ℕ) ε 5 / 25 ≤
    (∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts,
        HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity ab.1 ab.2) : ℝ) 2) /
      HPow.hPow (α := ℝ) 16 #P.parts

Tactic:
apply (edgeDensity_chunk_aux (hP := hP) hPα hPε hU hV).trans

Premises used: _private.0.SzemerediRegularity.edgeDensity_chunk_aux, LE.le.trans
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
hP : P.IsEquipartition
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst_3 : Nonempty α
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hU : U ∈ P.parts
hV : V ∈ P.parts
rw : HPow.hPow (α := ℝ) 16 #P.parts = (↑(HMul.hMul (α := ℕ) 4 4 ^ #P.parts) : ℝ)
⊢ HPow.hPow (α := ℝ) 16 #P.parts = (↑(#((chunk hP G ε hU).parts ×ˢ (chunk hP G ε hV).parts)) : ℝ)

Tactic:
rw [card_product, cast_mul, card_chunk (m_pos hPα).ne', card_chunk (m_pos hPα).ne', ←
      cast_mul, ← mul_pow]

Premises used: SzemerediRegularity.card_chunk, Finset.card_product, SzemerediRegularity.m_pos, LT.lt.ne', Nat.cast_mul, mul_pow
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
hP : P.IsEquipartition
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst_3 : Nonempty α
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hU : U ∈ P.parts
hV : V ∈ P.parts
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : HPow.hPow (α := ℕ) 16 #P.parts = HMul.hMul (α := ℕ) 4 4 ^ #P.parts
⊢ HPow.hPow (α := ℝ) 16 #P.parts = (↑(HMul.hMul (α := ℕ) 4 4 ^ #P.parts) : ℝ)

Tactic:
norm_cast
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
hP : P.IsEquipartition
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst_3 : Nonempty α
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hU : U ∈ P.parts
hV : V ∈ P.parts
⊢ HPow.hPow (α := ℝ) 16 #P.parts = (↑(#((chunk hP G ε hU).parts ×ˢ (chunk hP G ε hV).parts)) : ℝ)

Tactic:
have key : (16 : ℝ) ^ #P.parts = #((chunk hP G ε hU).parts ×ˢ (chunk hP G ε hV).parts) := by
    rw [card_product, cast_mul, card_chunk (m_pos hPα).ne', card_chunk (m_pos hPα).ne', ←
      cast_mul, ← mul_pow]; norm_cast
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
hP : P.IsEquipartition
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst_3 : Nonempty α
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hU : U ∈ P.parts
hV : V ∈ P.parts
key : HPow.hPow (α := ℝ) 16 #P.parts = (↑(#((chunk hP G ε hU).parts ×ˢ (chunk hP G ε hV).parts)) : ℝ)
simp_rw :
  HPow.hPow (β := ℕ)
      (HDiv.hDiv (α := ℝ)
        (∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, (↑(G.edgeDensity ab.1 ab.2) : ℝ))
        (↑(#((chunk hP G ε hU).parts ×ˢ (chunk hP G ε hV).parts)) : ℝ))
      2 ≤
    HDiv.hDiv (α := ℝ)
      (∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts,
        HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity ab.1 ab.2) : ℝ) 2)
      (↑(#((chunk hP G ε hU).parts ×ˢ (chunk hP G ε hV).parts)) : ℝ)
⊢ HPow.hPow (β := ℕ)
      ((∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, (↑(G.edgeDensity ab.1 ab.2) : ℝ)) /
        HPow.hPow (α := ℝ) 16 #P.parts)
      2 ≤
    (∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts,
        HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity ab.1 ab.2) : ℝ) 2) /
      HPow.hPow (α := ℝ) 16 #P.parts

Tactic:
simp_rw [key]
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
hP : P.IsEquipartition
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst_3 : Nonempty α
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hU : U ∈ P.parts
hV : V ∈ P.parts
key : HPow.hPow (α := ℝ) 16 #P.parts = (↑(#((chunk hP G ε hU).parts ×ˢ (chunk hP G ε hV).parts)) : ℝ)
⊢ HPow.hPow (β := ℕ)
      (HDiv.hDiv (α := ℝ)
        (∑ i ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, (↑(G.edgeDensity i.1 i.2) : ℝ))
        (↑(#((chunk hP G ε hU).parts.product (chunk hP G ε hV).parts)) : ℝ))
      2 ≤
    HDiv.hDiv (α := ℝ)
      (∑ i ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts,
        HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity i.1 i.2) : ℝ) 2)
      (↑(#((chunk hP G ε hU).parts.product (chunk hP G ε hV).parts)) : ℝ)

Tactic:
sum_div_card_sq_le_sum_sq_div_card (α := ℝ)

Premises used: sum_div_card_sq_le_sum_sq_div_card
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
hP : P.IsEquipartition
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst_3 : Nonempty α
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hU : U ∈ P.parts
hV : V ∈ P.parts
key : HPow.hPow (α := ℝ) 16 #P.parts = (↑(#((chunk hP G ε hU).parts ×ˢ (chunk hP G ε hV).parts)) : ℝ)
⊢ HPow.hPow (β := ℕ)
      (HDiv.hDiv (α := ℝ)
        (∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, (↑(G.edgeDensity ab.1 ab.2) : ℝ))
        (↑(#((chunk hP G ε hU).parts ×ˢ (chunk hP G ε hV).parts)) : ℝ))
      2 ≤
    HDiv.hDiv (α := ℝ)
      (∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts,
        HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity ab.1 ab.2) : ℝ) 2)
      (↑(#((chunk hP G ε hU).parts ×ˢ (chunk hP G ε hV).parts)) : ℝ)

Tactic:
convert! sum_div_card_sq_le_sum_sq_div_card (α := ℝ)

Premises used: sum_div_card_sq_le_sum_sq_div_card
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Energy
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
G : SimpleGraph α
inst_1 : DecidableRel G.Adj
⊢ 0 ≤ P.energy G

Tactic:
div_nonneg (Finset.sum_nonneg fun _ _ => sq_nonneg _) <| sq_nonneg _

Premises used: SimpleGraph.edgeDensity, Finpartition.energy, Finset.sum_nonneg, Prod.fst, sq_nonneg, div_nonneg, Prod.snd
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Energy
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
G : SimpleGraph α
inst_1 : DecidableRel G.Adj
⊢ 0 ≤ P.energy G

Tactic:
exact div_nonneg (Finset.sum_nonneg fun _ _ => sq_nonneg _) <| sq_nonneg _

Premises used: sq_nonneg, div_nonneg
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Energy
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
G : SimpleGraph α
inst_1 : DecidableRel G.Adj
rw : (↑(#P.parts * #P.parts - #P.parts) : ℚ) ≤ HPow.hPow (α := ℚ) (β := ℕ) (↑(#P.parts) : ℚ) 2
⊢ (↑(#P.parts.offDiag) : ℚ) ≤ 1 * HPow.hPow (α := ℚ) (β := ℕ) (↑(#P.parts) : ℚ) 2

Tactic:
rw [offDiag_card, one_mul]

Premises used: Finset.offDiag_card, one_mul
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Energy
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
G : SimpleGraph α
inst_1 : DecidableRel G.Adj
norm_cast : #P.parts * #P.parts - #P.parts ≤ HPow.hPow (β := ℕ) (#P.parts) 2
⊢ (↑(#P.parts * #P.parts - #P.parts) : ℚ) ≤ HPow.hPow (α := ℚ) (β := ℕ) (↑(#P.parts) : ℚ) 2

Tactic:
norm_cast
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Energy
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
G : SimpleGraph α
inst_1 : DecidableRel G.Adj
rw : #P.parts * #P.parts - #P.parts ≤ #P.parts * #P.parts
⊢ #P.parts * #P.parts - #P.parts ≤ HPow.hPow (β := ℕ) (#P.parts) 2

Tactic:
rw [sq]

Premises used: sq
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Energy
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
G : SimpleGraph α
inst_1 : DecidableRel G.Adj
⊢ #P.parts * #P.parts - #P.parts ≤ #P.parts * #P.parts

Tactic:
tsub_le_self

Premises used: tsub_le_self
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Energy
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
G : SimpleGraph α
inst_1 : DecidableRel G.Adj
⊢ #P.parts * #P.parts - #P.parts ≤ #P.parts * #P.parts

Tactic:
exact tsub_le_self

Premises used: tsub_le_self
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Energy
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
G : SimpleGraph α
inst_1 : DecidableRel G.Adj
𝕜 : Type u_2
inst_2 : Field 𝕜
inst_3 : LinearOrder 𝕜
inst_4 : IsStrictOrderedRing 𝕜
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ :
  HDiv.hDiv (α := ℚ) (∑ uv ∈ P.parts.offDiag, HPow.hPow (β := ℕ) (G.edgeDensity uv.1 uv.2) 2)
      (↑(HPow.hPow (β := ℕ) (#P.parts) 2) : ℚ) =
    HDiv.hDiv (α := ℚ) (∑ i ∈ P.parts.offDiag, HPow.hPow (β := ℕ) (G.edgeDensity i.1 i.2) 2)
      (↑(HPow.hPow (β := ℕ) (#P.parts) 2) : ℚ)
⊢ (↑((∑ uv ∈ P.parts.offDiag, HPow.hPow (β := ℕ) (G.edgeDensity uv.1 uv.2) 2) /
          HPow.hPow (α := ℚ) (β := ℕ) (↑(#P.parts) : ℚ) 2) :
      𝕜) =
    (∑ uv ∈ P.parts.offDiag, HPow.hPow (α := 𝕜) (β := ℕ) (↑(G.edgeDensity uv.1 uv.2) : 𝕜) 2) /
      HPow.hPow (α := 𝕜) (β := ℕ) (↑(#P.parts) : 𝕜) 2

Tactic:
norm_cast
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
m a b : ℕ
P : Finpartition s
hs : a * m + b * (m + 1) = #s
inl :
  ∀ (hs : a * 0 + b * HAdd.hAdd (α := ℕ) 0 1 = #s),
    ∃ (Q : Finpartition s),
      (∀ x ∈ Q.parts, #x = 0 ∨ #x = HAdd.hAdd (α := ℕ) 0 1) ∧
        (∀ x ∈ P.parts, #(x \ {y ∈ Q.parts | y ⊆ x}.biUnion id) ≤ 0) ∧
          #({i ∈ Q.parts | #i = HAdd.hAdd (α := ℕ) 0 1}) = b
inr :
  ∀ (m_pos : m > 0),
    ∃ (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 rfl | m_pos := m.eq_zero_or_pos

Premises used: Nat.eq_zero_or_pos, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
a b : ℕ
P : Finpartition s
hs : a * 0 + b * HAdd.hAdd (α := ℕ) 0 1 = #s
⊢ ∀ (x : Finset α), Membership.mem (γ := Finset (Finset α)) (parts (a := s) ⊥) x → #x = 0 ∨ #x = HAdd.hAdd (α := ℕ) 0 1

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
a b : ℕ
P : Finpartition s
hs : a * 0 + b * HAdd.hAdd (α := ℕ) 0 1 = #s
⊢ card.{u_1} (α := Finset α) ({i ∈ parts (a := s) ⊥ | #i = HAdd.hAdd (α := ℕ) 0 1}) = b

Tactic:
simpa [Finset.filter_true_of_mem] using hs.symm

Premises used: Finset.filter_true_of_mem, Eq.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
a b : ℕ
P : Finpartition s
hs : a * 0 + b * HAdd.hAdd (α := ℕ) 0 1 = #s
inl : ∀ x ∈ P.parts, #(x \ Finset.biUnion ({y ∈ parts (a := s) ⊥ | y ⊆ x}) id) ≤ 0
⊢ ∃ (Q : Finpartition s),
    (∀ x ∈ Q.parts, #x = 0 ∨ #x = HAdd.hAdd (α := ℕ) 0 1) ∧
      (∀ x ∈ P.parts, #(x \ {y ∈ Q.parts | y ⊆ x}.biUnion id) ≤ 0) ∧ #({i ∈ Q.parts | #i = HAdd.hAdd (α := ℕ) 0 1}) = b

Tactic:
refine ⟨⊥, by simp, ?_, by simpa [Finset.filter_true_of_mem] using hs.symm⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
a b : ℕ
P : Finpartition s
hs : a * 0 + b * HAdd.hAdd (α := ℕ) 0 1 = #s
inl :
  ∀ x ∈ P.parts,
    ∀ ⦃x_1 : α⦄,
      x_1 ∈ x →
        ∃ (a : Finset α),
          Membership.mem (γ := Finset (Finset α)) (parts (a := s) ⊥) a ∧ (∀ ⦃x_2 : α⦄, x_2 ∈ a → x_2 ∈ x) ∧ x_1 ∈ a
⊢ ∀ x ∈ P.parts, #(x \ Finset.biUnion ({y ∈ parts (a := s) ⊥ | y ⊆ x}) id) ≤ 0

Tactic:
simp only [le_zero_iff, card_eq_zero, mem_biUnion, mem_filter, id,
      and_assoc, sdiff_eq_empty_iff_subset, subset_iff]

Premises used: le_zero_iff, id, Finset.sdiff_eq_empty_iff_subset, Finset.subset_iff, Finset.card_eq_zero, and_assoc, Finset.mem_filter, Finset.mem_biUnion
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
a b : ℕ
P : Finpartition s
hs : a * 0 + b * HAdd.hAdd (α := ℕ) 0 1 = #s
⊢ ∀ x ∈ P.parts,
    ∀ ⦃x_1 : α⦄,
      x_1 ∈ x →
        ∃ (a : Finset α),
          Membership.mem (γ := Finset (Finset α)) (parts (a := s) ⊥) a ∧ (∀ ⦃x_2 : α⦄, x_2 ∈ a → x_2 ∈ x) ∧ x_1 ∈ a

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

Premises used: Iff.mpr, Finset.mem_singleton_self, Function.Embedding.mk, Finset.singleton_subset_iff, Finset.singleton_injective, And.intro, Exists.intro, Finpartition.le, Singleton.singleton, Finset.mem_map_of_mem
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
a b : ℕ
P : Finpartition s
hs : a * 0 + b * HAdd.hAdd (α := ℕ) 0 1 = #s
⊢ ∀ x ∈ P.parts,
    ∀ ⦃x_1 : α⦄,
      x_1 ∈ x →
        ∃ (a : Finset α),
          Membership.mem (γ := Finset (Finset α)) (parts (a := s) ⊥) a ∧ (∀ ⦃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 _⟩
-- 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
⊢ ∃ (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:
_
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
m a b : ℕ
P : Finpartition s
hs : a * m + b * (m + 1) = #s
m_pos : m > 0
inr :
  ∀ (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),
    ∃ (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:
induction s using Finset.strongInduction generalizing a b with | H s ih => _

Premises used: Finset.strongInduction
-- 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
pos :
  ∀ (hab : a = 0 ∧ b = 0),
    ∃ (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
neg :
  ∀ (hab : ¬(a = 0 ∧ b = 0)),
    ∃ (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:
by_cases hab : a = 0 ∧ b = 0
-- 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 : a = 0 ∧ b = 0
⊢ s = ⊥

Tactic:
simp only [hab.1, hab.2, add_zero, zero_mul, eq_comm, card_eq_zero, ← bot_eq_empty] at hs

Premises used: Finset.bot_eq_empty, MulZeroClass.zero_mul, eq_comm, And.right, And.left, Finset.card_eq_zero, add_zero
-- 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
hab : a = 0 ∧ b = 0
hs : s = ⊥
pos :
  ∀
    (ih :
      ∀ t ⊂ ⊥,
        ∀ {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)
    {P : Finpartition (α := Finset α) ⊥},
    ∃ (Q : Finpartition (α := Finset α) ⊥),
      (∀ 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:
subst hs