awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Bound (goal)
Goal:
ι : Type u_2
𝕜 : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s t : Finset ι
x : 𝕜
hst : s ⊆ t
f : ι → 𝕜
d : 𝕜
hx : 0 ≤ x
hs : x ≤ |HDiv.hDiv (α := 𝕜) (∑ i ∈ s, f i) (↑(#s) : 𝕜) - HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)|
ht : d ≤ HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)) 2
hscard : LT.lt.{u_3} (α := 𝕜) 0 (↑(#s) : 𝕜)
htcard : LT.lt.{u_3} (α := 𝕜) 0 (↑(#t) : 𝕜)
h₁ :
  HPow.hPow (β := ℕ) x 2 ≤
    HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ s, f i) (↑(#s) : 𝕜) - HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)) 2
h₂ :
  HPow.hPow (β := ℕ) x 2 ≤
    HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ s, (f i - HDiv.hDiv (α := 𝕜) (∑ j ∈ t, f j) (↑(#t) : 𝕜))) (↑(#s) : 𝕜))
      2
h₃ :
  (↑(#s) : 𝕜) * HPow.hPow (β := ℕ) x 2 ≤
    ∑ i ∈ t, HPow.hPow (α := 𝕜) (β := ℕ) ((fun (i : ι) ↦ f i - HDiv.hDiv (α := 𝕜) (∑ j ∈ t, f j) (↑(#t) : 𝕜)) i) 2
⊢ HPow.hPow (α := 𝕜) (β := ℕ) (∑ i ∈ t, f i) 2 * (↑(#t) : 𝕜) +
      ((∑ i ∈ t, HPow.hPow (β := ℕ) (f i) 2) * HPow.hPow (α := 𝕜) (β := ℕ) (↑(#t) : 𝕜) 2 -
          (HMul.hMul (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜) + HMul.hMul (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)) *
            ∑ i ∈ t, f i +
        (↑(#t) : 𝕜) * HPow.hPow (α := 𝕜) (β := ℕ) (∑ i ∈ t, f i) 2) ≤
    (∑ i ∈ t, HPow.hPow (β := ℕ) (f i) 2) * HPow.hPow (α := 𝕜) (β := ℕ) (↑(#t) : 𝕜) 2
have inr : HPow.hPow (α := 𝕜) (β := ℕ) (↑(#t) : 𝕜) 2 * ∑ x ∈ t, HPow.hPow (β := ℕ) (f x) 2 ≤
  HPow.hPow (α := 𝕜) (β := ℕ) (↑(#t) : 𝕜) 2 * ∑ x ∈ t, HPow.hPow (β := ℕ) (f x) 2
Tactic: ring_nf
-- 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 : Finset α
hU : U ∈ P.parts
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
h₂ : ¬G.IsUniform ε U V
⊢ #(G.nonuniformWitness ε U V \ (star hP G ε hU V).biUnion id) ≤ HPow.hPow (α := ℕ) 2 (#P.parts - 1) * m
have hX : G.nonuniformWitness ε U V ∈ P.nonuniformWitnesses G ε U
Tactic: have hX : G.nonuniformWitness ε U V ∈ P.nonuniformWitnesses G ε U :=
    nonuniformWitness_mem_nonuniformWitnesses h₂ hV hUV
-- 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 : Finset α
hU : U ∈ P.parts
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
h₂ : ¬G.IsUniform ε U V
hX : G.nonuniformWitness ε U V ∈ P.nonuniformWitnesses G ε U
x : α
hx : x ∈ G.nonuniformWitness ε U V \ (star hP G ε hU V).biUnion id
⊢ Membership.mem (γ := Finset α)
    ({B ∈ parts (atomise U (P.nonuniformWitnesses G ε U)) | B ⊆ G.nonuniformWitness ε U V ∧ B.Nonempty}.biUnion
      fun (B : Finset α) ↦ B \ {A ∈ (chunk hP G ε hU).parts | A ⊆ B}.biUnion id)
    x
have hx₁ : (∃ a ∈ {u ∈ parts (atomise U (P.nonuniformWitnesses G ε U)) | u ⊆ G.nonuniformWitness ε U V ∧ u.Nonempty}, x ∈ id a) ∧
  x ∉ {A ∈ (chunk hP G ε hU).parts | A ⊆ G.nonuniformWitness ε U V}.biUnion id
Tactic: rw [← biUnion_filter_atomise hX (G.nonuniformWitness_subset h₂), star, mem_sdiff,
      mem_biUnion] at hx
Cleared hypotheses: hx
-- 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 : Finset α
hU : U ∈ P.parts
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
h₂ : ¬G.IsUniform ε U V
hX : G.nonuniformWitness ε U V ∈ P.nonuniformWitnesses G ε U
x : α
hx :
  (∃ a ∈ {u ∈ parts (atomise U (P.nonuniformWitnesses G ε U)) | u ⊆ G.nonuniformWitness ε U V ∧ u.Nonempty}, x ∈ id a) ∧
    x ∉ {A ∈ (chunk hP G ε hU).parts | A ⊆ G.nonuniformWitness ε U V}.biUnion id
⊢ Membership.mem (γ := Finset α)
    ({B ∈ parts (atomise U (P.nonuniformWitnesses G ε U)) | B ⊆ G.nonuniformWitness ε U V ∧ B.Nonempty}.biUnion
      fun (B : Finset α) ↦ B \ {A ∈ (chunk hP G ε hU).parts | A ⊆ B}.biUnion id)
    x
have simp : ∀
  (hx :
    (∃ (a : Finset α),
        (a ∈ parts (atomise U (P.nonuniformWitnesses G ε U)) ∧ a ⊆ G.nonuniformWitness ε U V ∧ a.Nonempty) ∧ x ∈ a) ∧
      ∀ x_1 ∈ (chunk hP G ε hU).parts, x_1 ⊆ G.nonuniformWitness ε U V → x ∉ x_1),
  ∃ (a : Finset α),
    (a ∈ parts (atomise U (P.nonuniformWitnesses G ε U)) ∧ a ⊆ G.nonuniformWitness ε U V ∧ a.Nonempty) ∧
      x ∈ a ∧ ∀ x_1 ∈ (chunk hP G ε hU).parts, x_1 ⊆ a → x ∉ x_1
Tactic: simp only [not_exists, mem_biUnion, and_imp, mem_filter,
      not_and, mem_sdiff, id, mem_sdiff] at hx ⊢
Cleared hypotheses: hx
-- 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 : Finset α
hU : U ∈ P.parts
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
h₂ : ¬G.IsUniform ε U V
hX : G.nonuniformWitness ε U V ∈ P.nonuniformWitnesses G ε U
x : α
hx :
  (∃ (a : Finset α),
      (a ∈ parts (atomise U (P.nonuniformWitnesses G ε U)) ∧ a ⊆ G.nonuniformWitness ε U V ∧ a.Nonempty) ∧ x ∈ a) ∧
    ∀ x_1 ∈ (chunk hP G ε hU).parts, x_1 ⊆ G.nonuniformWitness ε U V → x ∉ x_1
⊢ ∃ (a : Finset α),
    (a ∈ parts (atomise U (P.nonuniformWitnesses G ε U)) ∧ a ⊆ G.nonuniformWitness ε U V ∧ a.Nonempty) ∧
      x ∈ a ∧ ∀ x_1 ∈ (chunk hP G ε hU).parts, x_1 ⊆ a → x ∉ x_1
have obtain : ∀ (hx : ∀ x_1 ∈ (chunk hP G ε hU).parts, x_1 ⊆ G.nonuniformWitness ε U V → x ∉ x_1) (B : Finset α)
  (hB₁ : B ∈ parts (atomise U (P.nonuniformWitnesses G ε U)) ∧ B ⊆ G.nonuniformWitness ε U V ∧ B.Nonempty)
  (hB₂ : x ∈ B),
  ∃ (a : Finset α),
    (a ∈ parts (atomise U (P.nonuniformWitnesses G ε U)) ∧ a ⊆ G.nonuniformWitness ε U V ∧ a.Nonempty) ∧
      x ∈ a ∧ ∀ x_1 ∈ (chunk hP G ε hU).parts, x_1 ⊆ a → x ∉ x_1
Tactic: obtain ⟨⟨B, hB₁, hB₂⟩, hx⟩ := hx
Cleared hypotheses: hx
-- 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 : Finset α
hU : U ∈ P.parts
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
h₂ : ¬G.IsUniform ε U V
hX : G.nonuniformWitness ε U V ∈ P.nonuniformWitnesses G ε U
⊢ #(G.nonuniformWitness ε U V \ (star hP G ε hU V).biUnion id) ≤ HPow.hPow (α := ℕ) 2 (#P.parts - 1) * m
have q : G.nonuniformWitness ε U V \ (star hP G ε hU V).biUnion id ⊆
  {B ∈ parts (atomise U (P.nonuniformWitnesses G ε U)) | B ⊆ G.nonuniformWitness ε U V ∧ B.Nonempty}.biUnion
    fun (B : Finset α) ↦ B \ {A ∈ (chunk hP G ε hU).parts | A ⊆ B}.biUnion id
Tactic: have q : G.nonuniformWitness ε U V \ (star hP G ε hU V).biUnion id ⊆
      {B ∈ (atomise U <| P.nonuniformWitnesses G ε U).parts |
        B ⊆ G.nonuniformWitness ε U V ∧ B.Nonempty}.biUnion
        fun B => B \ {A ∈ (chunk hP G ε hU).parts | A ⊆ B}.biUnion id := by
    intro x hx
    rw [← biUnion_filter_atomise hX (G.nonuniformWitness_subset h₂), star, mem_sdiff,
      mem_biUnion] at hx
    simp only [not_exists, mem_biUnion, and_imp, mem_filter,
      not_and, mem_sdiff, id, mem_sdiff] at hx ⊢
    obtain ⟨⟨B, hB₁, hB₂⟩, hx⟩ := hx
    exact ⟨B, hB₁, hB₂, fun A hA AB => hx A hA <| AB.trans hB₁.2.1⟩
-- 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 : Finset α
hU : U ∈ P.parts
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
h₂ : ¬G.IsUniform ε U V
hX : G.nonuniformWitness ε U V ∈ P.nonuniformWitnesses G ε U
q :
  G.nonuniformWitness ε U V \ (star hP G ε hU V).biUnion id ⊆
    {B ∈ parts (atomise U (P.nonuniformWitnesses G ε U)) | B ⊆ G.nonuniformWitness ε U V ∧ B.Nonempty}.biUnion
      fun (B : Finset α) ↦ B \ {A ∈ (chunk hP G ε hU).parts | A ⊆ B}.biUnion id
⊢ #(G.nonuniformWitness ε U V \ (star hP G ε hU V).biUnion id) ≤ HPow.hPow (α := ℕ) 2 (#P.parts - 1) * m
have apply : ∑ a ∈ parts (atomise U (P.nonuniformWitnesses G ε U)) with a ⊆ G.nonuniformWitness ε U V ∧ a.Nonempty,
    #(a \ {A ∈ (chunk hP G ε hU).parts | A ⊆ a}.biUnion id) ≤
  HPow.hPow (α := ℕ) 2 (#P.parts - 1) * m
Tactic: apply (card_le_card q).trans (card_biUnion_le.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 : Finset α
hU : U ∈ P.parts
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
h₂ : ¬G.IsUniform ε U V
hX : G.nonuniformWitness ε U V ∈ P.nonuniformWitnesses G ε U
q :
  G.nonuniformWitness ε U V \ (star hP G ε hU V).biUnion id ⊆
    {B ∈ parts (atomise U (P.nonuniformWitnesses G ε U)) | B ⊆ G.nonuniformWitness ε U V ∧ B.Nonempty}.biUnion
      fun (B : Finset α) ↦ B \ {A ∈ (chunk hP G ε hU).parts | A ⊆ B}.biUnion id
⊢ ∑ a ∈ parts (atomise U (P.nonuniformWitnesses G ε U)) with a ⊆ G.nonuniformWitness ε U V ∧ a.Nonempty,
      #(a \ {A ∈ (chunk hP G ε hU).parts | A ⊆ a}.biUnion id) ≤
    HPow.hPow (α := ℕ) 2 (#P.parts - 1) * m
have trans : LE.le (α := ℕ)
  (∑ a ∈ parts (atomise U (P.nonuniformWitnesses G ε U)) with a ⊆ G.nonuniformWitness ε U V ∧ a.Nonempty,
    #(a \ {A ∈ (chunk hP G ε hU).parts | A ⊆ a}.biUnion id))
  (∑ B ∈ parts (atomise U (P.nonuniformWitnesses G ε U)) with B ⊆ G.nonuniformWitness ε U V ∧ B.Nonempty, m)
Tactic: trans ∑ B ∈ (atomise U <| P.nonuniformWitnesses G ε U).parts with
    B ⊆ G.nonuniformWitness ε U V ∧ B.Nonempty, m
-- 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 : Finset α
hU : U ∈ P.parts
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
h₂ : ¬G.IsUniform ε U V
hX : G.nonuniformWitness ε U V ∈ P.nonuniformWitnesses G ε U
q :
  G.nonuniformWitness ε U V \ (star hP G ε hU V).biUnion id ⊆
    {B ∈ parts (atomise U (P.nonuniformWitnesses G ε U)) | B ⊆ G.nonuniformWitness ε U V ∧ B.Nonempty}.biUnion
      fun (B : Finset α) ↦ B \ {A ∈ (chunk hP G ε hU).parts | A ⊆ B}.biUnion id
trans :
  LE.le (α := ℕ)
    (∑ a ∈ parts (atomise U (P.nonuniformWitnesses G ε U)) with a ⊆ G.nonuniformWitness ε U V ∧ a.Nonempty,
      #(a \ {A ∈ (chunk hP G ε hU).parts | A ⊆ a}.biUnion id))
    (∑ B ∈ parts (atomise U (P.nonuniformWitnesses G ε U)) with B ⊆ G.nonuniformWitness ε U V ∧ B.Nonempty, m)
⊢ ∑ a ∈ parts (atomise U (P.nonuniformWitnesses G ε U)) with a ⊆ G.nonuniformWitness ε U V ∧ a.Nonempty,
      #(a \ {A ∈ (chunk hP G ε hU).parts | A ⊆ a}.biUnion id) ≤
    HPow.hPow (α := ℕ) 2 (#P.parts - 1) * m
have trans₁ : ∑ B ∈ parts (atomise U (P.nonuniformWitnesses G ε U)) with B ⊆ G.nonuniformWitness ε U V ∧ B.Nonempty, m ≤
  HPow.hPow (α := ℕ) 2 (#P.parts - 1) * m
Tactic: trans ∑ B ∈ (atomise U <| P.nonuniformWitnesses G ε U).parts with
    B ⊆ G.nonuniformWitness ε U V ∧ B.Nonempty, m
-- 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 : Finset α
hU : U ∈ P.parts
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
h₂ : ¬G.IsUniform ε U V
hX : G.nonuniformWitness ε U V ∈ P.nonuniformWitnesses G ε U
q :
  G.nonuniformWitness ε U V \ (star hP G ε hU V).biUnion id ⊆
    {B ∈ parts (atomise U (P.nonuniformWitnesses G ε U)) | B ⊆ G.nonuniformWitness ε U V ∧ B.Nonempty}.biUnion
      fun (B : Finset α) ↦ B \ {A ∈ (chunk hP G ε hU).parts | A ⊆ B}.biUnion id
this :
  ∀ B ∈ parts (atomise U (P.nonuniformWitnesses G ε U)), #(B \ {A ∈ (chunk hP G ε hU).parts | A ⊆ B}.biUnion id) ≤ m
⊢ LE.le (α := ℕ)
    (∑ a ∈ parts (atomise U (P.nonuniformWitnesses G ε U)) with a ⊆ G.nonuniformWitness ε U V ∧ a.Nonempty,
      #(a \ {A ∈ (chunk hP G ε hU).parts | A ⊆ a}.biUnion id))
    (∑ B ∈ parts (atomise U (P.nonuniformWitnesses G ε U)) with B ⊆ G.nonuniformWitness ε U V ∧ B.Nonempty, m)
have h : ∀ (B : Finset α)
  (hB : B ∈ {B ∈ parts (atomise U (P.nonuniformWitnesses G ε U)) | B ⊆ G.nonuniformWitness ε U V ∧ B.Nonempty}),
  #(B \ {A ∈ (chunk hP G ε hU).parts | A ⊆ B}.biUnion id) ≤ m
Tactic: gcongr with B hB
-- 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 : Finset α
hU : U ∈ P.parts
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
h₂ : ¬G.IsUniform ε U V
hX : G.nonuniformWitness ε U V ∈ P.nonuniformWitnesses G ε U
q :
  G.nonuniformWitness ε U V \ (star hP G ε hU V).biUnion id ⊆
    {B ∈ parts (atomise U (P.nonuniformWitnesses G ε U)) | B ⊆ G.nonuniformWitness ε U V ∧ B.Nonempty}.biUnion
      fun (B : Finset α) ↦ B \ {A ∈ (chunk hP G ε hU).parts | A ⊆ B}.biUnion id
⊢ LE.le (α := ℕ)
    (∑ a ∈ parts (atomise U (P.nonuniformWitnesses G ε U)) with a ⊆ G.nonuniformWitness ε U V ∧ a.Nonempty,
      #(a \ {A ∈ (chunk hP G ε hU).parts | A ⊆ a}.biUnion id))
    (∑ B ∈ parts (atomise U (P.nonuniformWitnesses G ε U)) with B ⊆ G.nonuniformWitness ε U V ∧ B.Nonempty, m)
have suffices : ∀ B ∈ parts (atomise U (P.nonuniformWitnesses G ε U)), #(B \ {A ∈ (chunk hP G ε hU).parts | A ⊆ B}.biUnion id) ≤ m
Tactic: suffices ∀ B ∈ (atomise U <| P.nonuniformWitnesses G ε U).parts,
        #(B \ {A ∈ (chunk hP G ε hU).parts | A ⊆ B}.biUnion id) ≤ m by
      gcongr with B hB
      exact this B <| filter_subset _ _ hB
-- 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 : Finset α
hU : U ∈ P.parts
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
h₂ : ¬G.IsUniform ε U V
hX : G.nonuniformWitness ε U V ∈ P.nonuniformWitnesses G ε U
q :
  G.nonuniformWitness ε U V \ (star hP G ε hU V).biUnion id ⊆
    {B ∈ parts (atomise U (P.nonuniformWitnesses G ε U)) | B ⊆ G.nonuniformWitness ε U V ∧ B.Nonempty}.biUnion
      fun (B : Finset α) ↦ B \ {A ∈ (chunk hP G ε hU).parts | A ⊆ B}.biUnion id
B : Finset α
hB : B ∈ parts (atomise U (P.nonuniformWitnesses G ε U))
⊢ #(B \
        Finset.biUnion
          ({A ∈
              parts (a := U)
                (if hUcard :
                    #U =
                      m * HPow.hPow (α := ℕ) 4 #P.parts +
                        (Fintype.card α / #P.parts - m * HPow.hPow (α := ℕ) 4 #P.parts) then
                  equitabilise (P := atomise U (P.nonuniformWitnesses G ε U)) ⋯
                else equitabilise (P := atomise U (P.nonuniformWitnesses G ε U)) ⋯) |
            A ⊆ B})
          id) ≤
    m
have pos : ∀ (h₁ : #U = m * HPow.hPow (α := ℕ) 4 #P.parts + (Fintype.card α / #P.parts - m * HPow.hPow (α := ℕ) 4 #P.parts)),
  #(B \ {A ∈ parts (equitabilise (P := atomise U (P.nonuniformWitnesses G ε U)) sorry) | A ⊆ B}.biUnion id) ≤ m
Tactic: split_ifs with h₁
-- 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 : Finset α
hU : U ∈ P.parts
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
h₂ : ¬G.IsUniform ε U V
hX : G.nonuniformWitness ε U V ∈ P.nonuniformWitnesses G ε U
q :
  G.nonuniformWitness ε U V \ (star hP G ε hU V).biUnion id ⊆
    {B ∈ parts (atomise U (P.nonuniformWitnesses G ε U)) | B ⊆ G.nonuniformWitness ε U V ∧ B.Nonempty}.biUnion
      fun (B : Finset α) ↦ B \ {A ∈ (chunk hP G ε hU).parts | A ⊆ B}.biUnion id
B : Finset α
hB : B ∈ parts (atomise U (P.nonuniformWitnesses G ε U))
pos :
  ∀ (h₁ : #U = m * HPow.hPow (α := ℕ) 4 #P.parts + (Fintype.card α / #P.parts - m * HPow.hPow (α := ℕ) 4 #P.parts)),
    #(B \ {A ∈ parts (equitabilise (P := atomise U (P.nonuniformWitnesses G ε U)) ⋯) | A ⊆ B}.biUnion id) ≤ m
⊢ #(B \
        Finset.biUnion
          ({A ∈
              parts (a := U)
                (if hUcard :
                    #U =
                      m * HPow.hPow (α := ℕ) 4 #P.parts +
                        (Fintype.card α / #P.parts - m * HPow.hPow (α := ℕ) 4 #P.parts) then
                  equitabilise (P := atomise U (P.nonuniformWitnesses G ε U)) ⋯
                else equitabilise (P := atomise U (P.nonuniformWitnesses G ε U)) ⋯) |
            A ⊆ B})
          id) ≤
    m
have neg : ∀ (h₁ : ¬#U = m * HPow.hPow (α := ℕ) 4 #P.parts + (Fintype.card α / #P.parts - m * HPow.hPow (α := ℕ) 4 #P.parts)),
  #(B \ {A ∈ parts (equitabilise (P := atomise U (P.nonuniformWitnesses G ε U)) sorry) | A ⊆ B}.biUnion id) ≤ m
Tactic: split_ifs with h₁
-- 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 : Finset α
hU : U ∈ P.parts
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
h₂ : ¬G.IsUniform ε U V
hX : G.nonuniformWitness ε U V ∈ P.nonuniformWitnesses G ε U
q :
  G.nonuniformWitness ε U V \ (star hP G ε hU V).biUnion id ⊆
    {B ∈ parts (atomise U (P.nonuniformWitnesses G ε U)) | B ⊆ G.nonuniformWitness ε U V ∧ B.Nonempty}.biUnion
      fun (B : Finset α) ↦ B \ {A ∈ (chunk hP G ε hU).parts | A ⊆ B}.biUnion id
⊢ ∑ B ∈ parts (atomise U (P.nonuniformWitnesses G ε U)) with B ⊆ G.nonuniformWitness ε U V ∧ B.Nonempty, m ≤
    HPow.hPow (α := ℕ) 2 (#P.parts - 1) * m
have h₁ : LE.le (α := ℕ) 1 2
Tactic: grw [sum_const, smul_eq_mul, card_filter_atomise_le_two_pow (s := U) hX,
    Finpartition.card_nonuniformWitnesses_le, filter_subset]
-- 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 : Finset α
hU : U ∈ P.parts
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hε₁ : ε ≤ 1
⊢ (1 - ε / 10) * (↑(#(G.nonuniformWitness ε U V)) : ℝ) ≤ (↑(#((star hP G ε hU V).biUnion id)) : ℝ)
have hP₁ : 0 < #P.parts
Tactic: have hP₁ : 0 < #P.parts := Finset.card_pos.2 ⟨_, hU⟩
-- 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 : Finset α
hU : U ∈ P.parts
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hε₁ : ε ≤ 1
hP₁ : 0 < #P.parts
⊢ HPow.hPow (α := ℝ) 2 #P.parts * (↑m : ℝ) / ((↑(#U) : ℝ) * ε) ≤ ε / 10
have rw : HPow.hPow (α := ℝ) 2 #P.parts * (↑m : ℝ) / (↑(#U) : ℝ) ≤ ε * (ε / 10)
Tactic: rw [← div_div, div_le_iff₀']
-- 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 : Finset α
hU : U ∈ P.parts
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hε₁ : ε ≤ 1
hP₁ : 0 < #P.parts
rw : HPow.hPow (α := ℝ) 2 #P.parts * (↑m : ℝ) / (↑(#U) : ℝ) ≤ ε * (ε / 10)
⊢ HPow.hPow (α := ℝ) 2 #P.parts * (↑m : ℝ) / ((↑(#U) : ℝ) * ε) ≤ ε / 10
have rw₁ : 0 < ε
Tactic: rw [← div_div, div_le_iff₀']
-- 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 : Finset α
hU : U ∈ P.parts
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hε₁ : ε ≤ 1
hP₁ : 0 < #P.parts
⊢ 0 < ε
have sz_positivity : 0 < ε → 0 < ε
Tactic: sz_positivity
-- 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 : Finset α
hU : U ∈ P.parts
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hε₁ : ε ≤ 1
hP₁ : 0 < #P.parts
⊢ HPow.hPow (α := ℝ) 2 #P.parts * (↑m : ℝ) / (↑(#U) : ℝ) ≤ ε * (ε / 10)
have refine : HPow.hPow (α := ℝ) 2 #P.parts * (HPow.hPow (α := ℝ) 2 #P.parts * (↑m : ℝ) / (↑(#U) : ℝ)) ≤
  HPow.hPow (α := ℝ) 2 #P.parts * (ε * (ε / 10))
Tactic: refine le_of_mul_le_mul_left ?_ (pow_pos zero_lt_two #P.parts)
-- 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 : Finset α
hU : U ∈ P.parts
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hε₁ : ε ≤ 1
hP₁ : 0 < #P.parts
⊢ HPow.hPow (α := ℝ) 2 #P.parts * (HPow.hPow (α := ℝ) 2 #P.parts * (↑m : ℝ) / (↑(#U) : ℝ)) =
    HMul.hMul (α := ℝ) 2 2 ^ #P.parts * (↑m : ℝ) / (↑(#U) : ℝ)
have rw : HPow.hPow (α := ℝ) 2 #P.parts * (HPow.hPow (α := ℝ) 2 #P.parts * (↑m : ℝ) / (↑(#U) : ℝ)) =
  HPow.hPow (α := ℝ) 2 #P.parts * HPow.hPow (α := ℝ) 2 #P.parts * (↑m : ℝ) / (↑(#U) : ℝ)
Tactic: rw [mul_pow, ← mul_div_assoc, mul_assoc]
-- 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 : Finset α
hU : U ∈ P.parts
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hε₁ : ε ≤ 1
hP₁ : 0 < #P.parts
rw :
  HPow.hPow (α := ℝ) 2 #P.parts * (HPow.hPow (α := ℝ) 2 #P.parts * (↑m : ℝ) / (↑(#U) : ℝ)) =
    HPow.hPow (α := ℝ) 2 #P.parts * HPow.hPow (α := ℝ) 2 #P.parts * (↑m : ℝ) / (↑(#U) : ℝ)
⊢ HPow.hPow (α := ℝ) 2 #P.parts * (HPow.hPow (α := ℝ) 2 #P.parts * (↑m : ℝ) / (↑(#U) : ℝ)) =
    HMul.hMul (α := ℝ) 2 2 ^ #P.parts * (↑m : ℝ) / (↑(#U) : ℝ)
have rw₁ : HPow.hPow (α := ℝ) 2 #P.parts * (HPow.hPow (α := ℝ) 2 #P.parts * (↑m : ℝ)) / (↑(#U) : ℝ) =
  HPow.hPow (α := ℝ) 2 #P.parts * HPow.hPow (α := ℝ) 2 #P.parts * (↑m : ℝ) / (↑(#U) : ℝ)
Tactic: rw [mul_pow, ← mul_div_assoc, mul_assoc]