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 : 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
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
⊢ 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

Tactic:
simp only [not_exists, mem_biUnion, and_imp, mem_filter,
      not_and, mem_sdiff, id, mem_sdiff] at hx ⊢

Premises used: and_imp, not_exists, id, Finset.mem_sdiff, Finset.mem_filter, not_and, Finset.mem_biUnion
-- 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 : 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
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
⊢ ∃ (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
-- 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 : 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_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:
⟨B, hB₁, hB₂, fun A hA AB => hx A hA <| AB.trans hB₁.2.1⟩

Premises used: HasSubset.Subset.trans, And.right, And.left, And.intro, Exists.intro
-- 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 : 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_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:
exact ⟨B, hB₁, hB₂, fun A hA AB => hx A hA <| AB.trans hB₁.2.1⟩
-- 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 : 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 ⊆
    {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⟩
-- 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 : 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
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
⊢ #(G.nonuniformWitness ε U V \ (star hP G ε hU V).biUnion id) ≤ HPow.hPow (α := ℕ) 2 (#P.parts - 1) * m

Tactic:
apply (card_le_card q).trans (card_biUnion_le.trans _)

Premises used: Finset.card_le_card, Finset.card_biUnion_le, 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 : 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)
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
⊢ ∑ 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:
trans ∑ B ∈ (atomise U <| P.nonuniformWitnesses G ε U).parts with
    B ⊆ G.nonuniformWitness ε U V ∧ B.Nonempty, m

Premises used: Finpartition.parts, Finpartition.atomise, Finpartition.nonuniformWitnesses, SimpleGraph.nonuniformWitness
-- 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 : 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
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
⊢ 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:
gcongr with B hB
-- 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 : 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
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:
this B <| filter_subset _ _ hB

Premises used: Finset.filter_subset
-- 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 : 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
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:
exact this B <| filter_subset _ _ hB

Premises used: Finset.filter_subset
-- 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 : 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
suffices :
  ∀ 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)

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
-- 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 : 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
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)) ⋯) | 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

Tactic:
split_ifs with h₁
-- 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 : 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))
h₁ : #U = m * HPow.hPow (α := ℕ) 4 #P.parts + (Fintype.card α / #P.parts - m * HPow.hPow (α := ℕ) 4 #P.parts)
⊢ #(B \ {u ∈ parts (equitabilise (P := atomise U (P.nonuniformWitnesses G ε U)) ⋯) | u ⊆ B}.biUnion id) ≤ m

Tactic:
card_parts_equitabilise_subset_le _ (card_aux₁ h₁) hB

Premises used: Finpartition.card_parts_equitabilise_subset_le, SzemerediRegularity.card_aux₁
-- 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 : 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))
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

Tactic:
convert! card_parts_equitabilise_subset_le _ (card_aux₁ h₁) hB

Premises used: Finpartition.card_parts_equitabilise_subset_le, SzemerediRegularity.card_aux₁
-- 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 : 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))
h₁ : ¬#U = m * HPow.hPow (α := ℕ) 4 #P.parts + (Fintype.card α / #P.parts - m * HPow.hPow (α := ℕ) 4 #P.parts)
⊢ #(B \ {u ∈ parts (equitabilise (P := atomise U (P.nonuniformWitnesses G ε U)) ⋯) | u ⊆ B}.biUnion id) ≤ m

Tactic:
card_parts_equitabilise_subset_le _ (card_aux₂ hP hU h₁) hB

Premises used: Finpartition.card_parts_equitabilise_subset_le, SzemerediRegularity.card_aux₂
-- 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 : 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))
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

Tactic:
convert! card_parts_equitabilise_subset_le _ (card_aux₂ hP hU h₁) hB

Premises used: Finpartition.card_parts_equitabilise_subset_le, SzemerediRegularity.card_aux₂
-- 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 : 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
h₁ h₃ : LE.le (α := ℕ) 1 2
⊢ ∑ 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:
grw [sum_const, smul_eq_mul, card_filter_atomise_le_two_pow (s := U) hX,
    Finpartition.card_nonuniformWitnesses_le, filter_subset]

Premises used: Finpartition.card_nonuniformWitnesses_le, Finset.filter_subset, Finpartition.card_filter_atomise_le_two_pow, smul_eq_mul, Finset.sum_const
-- 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 : 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 (α := ℕ) 1 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 : 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
⊢ 0 < #P.parts

Tactic:
have hP₁ : 0 < #P.parts := Finset.card_pos.2 ⟨_, hU⟩
-- 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 : 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)
rw₁ : 0 < ε
⊢ HPow.hPow (α := ℝ) 2 #P.parts * (↑m : ℝ) / ((↑(#U) : ℝ) * ε) ≤ ε / 10

Tactic:
rw [← div_div, div_le_iff₀']

Premises used: div_div, div_le_iff₀'
-- 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 : 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
sz_positivity sz_positivity₁ sz_positivity₂ sz_positivity₃ : 0 < ε → 0 < ε
⊢ 0 < ε

Tactic:
sz_positivity
-- 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 : 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)

Tactic:
le_of_mul_le_mul_left ?_ (pow_pos zero_lt_two #P.parts)

Premises used: pow_pos, Finpartition.parts, le_of_mul_le_mul_left, Finset.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 : 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
refine :
  HPow.hPow (α := ℝ) 2 #P.parts * (HPow.hPow (α := ℝ) 2 #P.parts * (↑m : ℝ) / (↑(#U) : ℝ)) ≤
    HPow.hPow (α := ℝ) 2 #P.parts * (ε * (ε / 10))
⊢ HPow.hPow (α := ℝ) 2 #P.parts * (↑m : ℝ) / (↑(#U) : ℝ) ≤ ε * (ε / 10)

Tactic:
refine le_of_mul_le_mul_left ?_ (pow_pos zero_lt_two #P.parts)

Premises used: pow_pos, Finpartition.parts, le_of_mul_le_mul_left, Finset.card