awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk (goal)
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
⊢ 3 / 4 * ε ≤
    |HDiv.hDiv (α := ℝ)
          (∑ i ∈ (star hP G ε hU V).product (star hP G ε hV U),
            (fun (x : Finset α × Finset α) ↦ ((↑(G.edgeDensity x.1 x.2) : ℝ) : ℝ)) i)
          (↑(#((star hP G ε hU V).product (star hP G ε hV U))) : ℝ) -
        HDiv.hDiv (α := ℝ)
          (∑ i ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts,
            (fun (x : Finset α × Finset α) ↦ ((↑(G.edgeDensity x.1 x.2) : ℝ) : ℝ)) i)
          (↑(#((chunk hP G ε hU).parts.product (chunk hP G ε hV).parts)) : ℝ)|
have refine_1 : 3 / 4 * ε ≤
  |HDiv.hDiv (α := ℝ) (∑ x ∈ star hP G ε hU V ×ˢ star hP G ε hV U, (↑(G.edgeDensity x.1 x.2) : ℝ))
        (↑(#(star hP G ε hU V) * #(star hP G ε hV U)) : ℝ) -
      HDiv.hDiv (α := ℝ) (∑ x ∈ (chunk hP G ε hU).parts ×ˢ (chunk hP G ε hV).parts, (↑(G.edgeDensity x.1 x.2) : ℝ))
        (↑(HMul.hMul (α := ℕ) 4 4 ^ #P.parts) : ℝ)|
Tactic: simp_rw [sp, card_product, card_chunk (m_pos hPα).ne', ← mul_pow]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk (goal)
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 (α := ℝ) (β := ℕ) (↑(G.edgeDensity U V) : ℝ) 2 - HPow.hPow (β := ℕ) ε 5 / 25 ≤
    HPow.hPow (β := ℕ)
      (HDiv.hDiv (α := ℝ)
        (∑ i ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts,
          (fun (x : Finset α × Finset α) ↦ ((↑(G.edgeDensity x.1 x.2) : ℝ) : ℝ)) i)
        (↑(#((chunk hP G ε hU).parts.product (chunk hP G ε hV).parts)) : ℝ))
      2
have refine_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: rw [sp, card_product]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk (goal)
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 (α := ℝ) (β := ℕ) (↑(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
have 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
Tactic: apply (edgeDensity_chunk_aux hP hPα hPε hU hV).trans
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk (goal)
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)
        (↑(#(chunk hP G ε hU).parts * #(chunk hP G ε hV).parts) : ℝ))
      2
have 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
Tactic: rw [card_chunk (m_pos hPα).ne', card_chunk (m_pos hPα).ne', ← mul_pow]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk (goal)
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 (α := ℝ) (β := ℕ) (↑(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
have 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
Tactic: apply (edgeDensity_chunk_aux (hP := hP) hPα hPε hU hV).trans
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk (goal)
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)) : ℝ)
have rw : HPow.hPow (α := ℝ) 16 #P.parts = (↑(HMul.hMul (α := ℕ) 4 4 ^ #P.parts) : ℝ)
Tactic: rw [card_product, cast_mul, card_chunk (m_pos hPα).ne', card_chunk (m_pos hPα).ne', ←
      cast_mul, ← mul_pow]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk (goal)
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 = (↑(HMul.hMul (α := ℕ) 4 4 ^ #P.parts) : ℝ)
have norm_cast : HPow.hPow (α := ℕ) 16 #P.parts = HMul.hMul (α := ℕ) 4 4 ^ #P.parts
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk (hypothesis)
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 (β := ℕ)
      ((∑ 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
have key : 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
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk (goal)
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 (β := ℕ)
      ((∑ 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
have 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)) : ℝ)
Tactic: simp_rw [key]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Energy (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
G : SimpleGraph α
inst_1 : DecidableRel G.Adj
⊢ (↑(#P.parts.offDiag) : ℚ) ≤ 1 * HPow.hPow (α := ℚ) (β := ℕ) (↑(#P.parts) : ℚ) 2
have rw : (↑(#P.parts * #P.parts - #P.parts) : ℚ) ≤ HPow.hPow (α := ℚ) (β := ℕ) (↑(#P.parts) : ℚ) 2
Tactic: rw [offDiag_card, one_mul]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Energy (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
G : SimpleGraph α
inst_1 : DecidableRel G.Adj
⊢ (↑(#P.parts * #P.parts - #P.parts) : ℚ) ≤ HPow.hPow (α := ℚ) (β := ℕ) (↑(#P.parts) : ℚ) 2
have norm_cast : #P.parts * #P.parts - #P.parts ≤ HPow.hPow (β := ℕ) (#P.parts) 2
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Energy (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
P : Finpartition s
G : SimpleGraph α
inst_1 : DecidableRel G.Adj
⊢ #P.parts * #P.parts - #P.parts ≤ HPow.hPow (β := ℕ) (#P.parts) 2
have rw : #P.parts * #P.parts - #P.parts ≤ #P.parts * #P.parts
Tactic: rw [sq]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Energy (goal)
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 𝕜
⊢ (↑((∑ 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
have 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) : ℚ)
Tactic: norm_cast
-- 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
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
have 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
Tactic: obtain rfl | m_pos := m.eq_zero_or_pos
Cleared hypotheses: m, hs
-- 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
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
⊢ ∃ (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
have 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
Tactic: obtain rfl | m_pos := m.eq_zero_or_pos
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
a b : ℕ
P : Finpartition s
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
have inl : ∀ x ∈ P.parts, #(x \ Finset.biUnion ({y ∈ parts (a := s) ⊥ | y ⊆ x}) id) ≤ 0
Tactic: refine ⟨⊥, by simp, ?_, by simpa [Finset.filter_true_of_mem] using hs.symm⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise (goal)
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 \ Finset.biUnion ({y ∈ parts (a := s) ⊥ | y ⊆ x}) id) ≤ 0
have 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
Tactic: simp only [le_zero_iff, card_eq_zero, mem_biUnion, mem_filter, id,
      and_assoc, sdiff_eq_empty_iff_subset, subset_iff]
-- 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
hs : a * m + b * (m + 1) = #s
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
have 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
Tactic: induction s using Finset.strongInduction generalizing a b with | H s ih => _
Cleared hypotheses: s, a, b, P, hs
-- 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
⊢ ∃ (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
have 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
Tactic: by_cases hab : a = 0 ∧ b = 0
-- 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
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
⊢ ∃ (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
have 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
Tactic: by_cases hab : a = 0 ∧ b = 0
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise (hypothesis)
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
⊢ ∃ (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
have hs₁ : s = ⊥
Tactic: simp only [hab.1, hab.2, add_zero, zero_mul, eq_comm, card_eq_zero, ← bot_eq_empty] at hs
Cleared hypotheses: hs
-- 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
hab : a = 0 ∧ b = 0
hs : 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
have 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
Tactic: subst hs
Cleared hypotheses: s, ih, P, hs
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise (hypothesis)
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)
⊢ ∃ (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
have hab₁ : 0 < a ∨ 0 < b
Tactic: simp_rw [not_and_or, ← Ne.eq_def, ← pos_iff_ne_zero] at hab
Cleared hypotheses: hab
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise (hypothesis)
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
⊢ ∃ (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
have hn : let n := if 0 < a then m else m + 1;
n = if 0 < a then m else m + 1
Tactic: set n := if 0 < a then m else m + 1 with hn
-- 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
⊢ 0 < n ∧
    n ≤ m + 1 ∧
      n ≤ a * m + b * (m + 1) ∧ (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = #s - n
have rw : (0 < if 0 < a then m else m + 1) ∧
  (if 0 < a then m else m + 1) ≤ m + 1 ∧
    (if 0 < a then m else m + 1) ≤ a * m + b * (m + 1) ∧
      (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) =
        a * m + b * (m + 1) - if 0 < a then m else m + 1
Tactic: rw [hn, ← hs]