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
Ul : 4 / 5 * ε ≤ (↑(#(star hP G ε hU V)) : ℝ) / HPow.hPow (α := ℝ) 4 #P.parts
Vl : 4 / 5 * ε ≤ (↑(#(star hP G ε hV U)) : ℝ) / HPow.hPow (α := ℝ) 4 #P.parts
this : 0 < ε
bc :
  ∀
    (UVl :
      4 / 5 * ε * (4 / 5 * ε) ≤
        (↑(#(star hP G ε hU V)) : ℝ) / HPow.hPow (α := ℝ) 4 #P.parts *
          ((↑(#(star hP G ε hV U)) : ℝ) / HPow.hPow (α := ℝ) 4 #P.parts)),
    HPow.hPow (β := ℕ) ε 4 / 3 ≤
      (↑(#(star hP G ε hU V)) : ℝ) / HPow.hPow (α := ℝ) 4 #P.parts *
          ((↑(#(star hP G ε hV U)) : ℝ) / HPow.hPow (α := ℝ) 4 #P.parts) *
        (9 / HPow.hPow (α := ℝ) (β := ℕ) 4 2 * HPow.hPow (β := ℕ) ε 2)
bc₁ : 0 ≤ (↑(#(star hP G ε hU V)) : ℝ) / HPow.hPow (α := ℝ) 4 #P.parts
⊢ HPow.hPow (β := ℕ) ε 4 / 3 ≤
    (↑(#(star hP G ε hU V)) : ℝ) / HPow.hPow (α := ℝ) 4 #P.parts *
        ((↑(#(star hP G ε hV U)) : ℝ) / HPow.hPow (α := ℝ) 4 #P.parts) *
      (9 / HPow.hPow (α := ℝ) (β := ℕ) 4 2 * HPow.hPow (β := ℕ) ε 2)

Tactic:
have UVl := mul_le_mul Ul Vl (by 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 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
Ul : 4 / 5 * ε ≤ (↑(#(star hP G ε hU V)) : ℝ) / HPow.hPow (α := ℝ) 4 #P.parts
Vl : 4 / 5 * ε ≤ (↑(#(star hP G ε hV U)) : ℝ) / HPow.hPow (α := ℝ) 4 #P.parts
this : 0 < ε
bc : LE.le (α := ℝ) 0 (↑(#(star hP G ε hU V)) : ℝ)
bc₁ : 0 ≤ HPow.hPow (α := ℝ) 4 #P.parts
⊢ 0 ≤ (↑(#(star hP G ε hU V)) : ℝ) / HPow.hPow (α := ℝ) 4 #P.parts

Tactic:
apply div_nonneg

Premises used: div_nonneg
-- 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
Ul : 4 / 5 * ε ≤ (↑(#(star hP G ε hU V)) : ℝ) / HPow.hPow (α := ℝ) 4 #P.parts
Vl : 4 / 5 * ε ≤ (↑(#(star hP G ε hV U)) : ℝ) / HPow.hPow (α := ℝ) 4 #P.parts
this : 0 < ε
⊢ LE.le (α := ℝ) 0 (↑(#(star hP G ε hU V)) : ℝ)

Tactic:
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 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
Ul : 4 / 5 * ε ≤ (↑(#(star hP G ε hU V)) : ℝ) / HPow.hPow (α := ℝ) 4 #P.parts
Vl : 4 / 5 * ε ≤ (↑(#(star hP G ε hV U)) : ℝ) / HPow.hPow (α := ℝ) 4 #P.parts
this : 0 < ε
⊢ 0 ≤ HPow.hPow (α := ℝ) 4 #P.parts

Tactic:
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 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
Ul : 4 / 5 * ε ≤ (↑(#(star hP G ε hU V)) : ℝ) / HPow.hPow (α := ℝ) 4 #P.parts
Vl : 4 / 5 * ε ≤ (↑(#(star hP G ε hV U)) : ℝ) / HPow.hPow (α := ℝ) 4 #P.parts
this : 0 < ε
UVl :
  4 / 5 * ε * (4 / 5 * ε) ≤
    (↑(#(star hP G ε hU V)) : ℝ) / HPow.hPow (α := ℝ) 4 #P.parts *
      ((↑(#(star hP G ε hV U)) : ℝ) / HPow.hPow (α := ℝ) 4 #P.parts)
⊢ HPow.hPow (β := ℕ) ε 4 / 3 ≤
    (↑(#(star hP G ε hU V)) : ℝ) / HPow.hPow (α := ℝ) 4 #P.parts *
        ((↑(#(star hP G ε hV U)) : ℝ) / HPow.hPow (α := ℝ) 4 #P.parts) *
      (9 / HPow.hPow (α := ℝ) (β := ℕ) 4 2 * HPow.hPow (β := ℕ) ε 2)

Tactic:
le_trans ?_ (mul_le_mul_of_nonneg_right UVl ?_)

Premises used: mul_le_mul_of_nonneg_right, 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
Ul : 4 / 5 * ε ≤ (↑(#(star hP G ε hU V)) : ℝ) / HPow.hPow (α := ℝ) 4 #P.parts
Vl : 4 / 5 * ε ≤ (↑(#(star hP G ε hV U)) : ℝ) / HPow.hPow (α := ℝ) 4 #P.parts
this : 0 < ε
UVl :
  4 / 5 * ε * (4 / 5 * ε) ≤
    (↑(#(star hP G ε hU V)) : ℝ) / HPow.hPow (α := ℝ) 4 #P.parts *
      ((↑(#(star hP G ε hV U)) : ℝ) / HPow.hPow (α := ℝ) 4 #P.parts)
bc :
  HPow.hPow (β := ℕ) ε 4 / 3 ≤ 4 / 5 * ε * (4 / 5 * ε) * (9 / HPow.hPow (α := ℝ) (β := ℕ) 4 2 * HPow.hPow (β := ℕ) ε 2)
bc₁ : 0 ≤ 9 / HPow.hPow (α := ℝ) (β := ℕ) 4 2 * HPow.hPow (β := ℕ) ε 2
⊢ HPow.hPow (β := ℕ) ε 4 / 3 ≤
    (↑(#(star hP G ε hU V)) : ℝ) / HPow.hPow (α := ℝ) 4 #P.parts *
        ((↑(#(star hP G ε hV U)) : ℝ) / HPow.hPow (α := ℝ) 4 #P.parts) *
      (9 / HPow.hPow (α := ℝ) (β := ℕ) 4 2 * HPow.hPow (β := ℕ) ε 2)

Tactic:
refine le_trans ?_ (mul_le_mul_of_nonneg_right UVl ?_)

Premises used: mul_le_mul_of_nonneg_right, 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
Ul : 4 / 5 * ε ≤ (↑(#(star hP G ε hU V)) : ℝ) / HPow.hPow (α := ℝ) 4 #P.parts
Vl : 4 / 5 * ε ≤ (↑(#(star hP G ε hV U)) : ℝ) / HPow.hPow (α := ℝ) 4 #P.parts
this : 0 < ε
UVl :
  4 / 5 * ε * (4 / 5 * ε) ≤
    (↑(#(star hP G ε hU V)) : ℝ) / HPow.hPow (α := ℝ) 4 #P.parts *
      ((↑(#(star hP G ε hV U)) : ℝ) / HPow.hPow (α := ℝ) 4 #P.parts)
bc : HPow.hPow (β := ℕ) ε 4 / 3 ≤ 4 / 5 * ε * (4 / 5 * ε) * (9 / 16 * HPow.hPow (β := ℕ) ε 2)
⊢ HPow.hPow (β := ℕ) ε 4 / 3 ≤ 4 / 5 * ε * (4 / 5 * ε) * (9 / HPow.hPow (α := ℝ) (β := ℕ) 4 2 * HPow.hPow (β := ℕ) ε 2)

Tactic:
norm_num
-- 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
Ul : 4 / 5 * ε ≤ (↑(#(star hP G ε hU V)) : ℝ) / HPow.hPow (α := ℝ) 4 #P.parts
Vl : 4 / 5 * ε ≤ (↑(#(star hP G ε hV U)) : ℝ) / HPow.hPow (α := ℝ) 4 #P.parts
this : 0 < ε
UVl :
  4 / 5 * ε * (4 / 5 * ε) ≤
    (↑(#(star hP G ε hU V)) : ℝ) / HPow.hPow (α := ℝ) 4 #P.parts *
      ((↑(#(star hP G ε hV U)) : ℝ) / HPow.hPow (α := ℝ) 4 #P.parts)
bc : 0 ≤ HPow.hPow (β := ℕ) ε 2
⊢ 0 ≤ 9 / HPow.hPow (α := ℝ) (β := ℕ) 4 2 * HPow.hPow (β := ℕ) ε 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
hε₁ : ε ≤ 1
hU : U ∈ P.parts
hV : V ∈ P.parts
hUVne : U ≠ V
hUV : ¬G.IsUniform ε U V
Ul : 4 / 5 * ε ≤ (↑(#(star hP G ε hU V)) : ℝ) / HPow.hPow (α := ℝ) 4 #P.parts
Vl : 4 / 5 * ε ≤ (↑(#(star hP G ε hV U)) : ℝ) / HPow.hPow (α := ℝ) 4 #P.parts
this : 0 < ε
UVl :
  4 / 5 * ε * (4 / 5 * ε) ≤
    (↑(#(star hP G ε hU V)) : ℝ) / HPow.hPow (α := ℝ) 4 #P.parts *
      ((↑(#(star hP G ε hV U)) : ℝ) / HPow.hPow (α := ℝ) 4 #P.parts)
⊢ 0 ≤ HPow.hPow (β := ℕ) ε 2

Tactic:
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 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
⊢ (star hP G ε hU V).product (star hP G ε hV U) ⊆ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts

Tactic:
have t : (star hP G ε hU V).product (star hP G ε hV U) ⊆
          (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts :=
        product_subset_product star_subset_chunk star_subset_chunk
-- 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
sz_positivity sz_positivity₁ sz_positivity₂ sz_positivity₃ : 0 < m → 0 ≤ ε
sz_positivity₄ sz_positivity₅ : 0 < m → 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 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
⊢ 0 ≤ ε

Tactic:
have hε : 0 ≤ ε := by 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 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 ≤ ε
⊢ ∀ (a b : Finset (Finset α)), a.product b = a ×ˢ b

Tactic:
have sp : ∀ (a b : Finset (Finset α)), a.product b = a ×ˢ b := fun a b => rfl
-- 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
linarith : 3 / 4 * ε < 0 → 4 / 4 = 1
linarith₁ : 3 / 4 * ε < 0 → HMul.hMul (α := ℝ) 1 4 = 4
linarith₂ : 3 / 4 * ε < 0 → HMul.hMul (α := ℝ) 4 1 = 4
linarith₃ : 3 / 4 * ε < 0 → GT.gt (α := ℝ) 4 0
linarith₄ : 3 / 4 * ε < 0 → 3 * (0 - ε) + (HMul.hMul (α := ℝ) 1 3 * (1 * ε) - HMul.hMul (α := ℝ) 4 0) = 0
linarith₅ : 3 / 4 * ε < 0 → GT.gt (α := ℝ) 3 0
⊢ 0 ≤ 3 / 4 * ε

Tactic:
linarith
-- 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
this :
  HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity U V) : ℝ) 2 - HPow.hPow (β := ℕ) ε 5 / 25 +
      HDiv.hDiv (α := ℝ) (↑(#((star hP G ε hU V).product (star hP G ε hV U))) : ℝ)
          (↑(#((chunk hP G ε hU).parts.product (chunk hP G ε hV).parts)) : ℝ) *
        HPow.hPow (β := ℕ) (3 / 4 * ε) 2 ≤
    HDiv.hDiv (α := ℝ)
      (∑ i ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts,
        HPow.hPow (α := ℝ) (β := ℕ) ((fun (x : Finset α × Finset α) ↦ ((↑(G.edgeDensity x.1 x.2) : ℝ) : ℝ)) i) 2)
      (↑(#((chunk hP G ε hU).parts.product (chunk hP G ε hV).parts)) : ℝ)
⊢ HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity U V) : ℝ) 2 - HPow.hPow (β := ℕ) ε 5 / 25 +
      (↑(#(star hP G ε hU V) * #(star hP G ε hV U)) : ℝ) / HPow.hPow (α := ℝ) (↑(HMul.hMul (α := ℕ) 4 4) : ℝ) #P.parts *
          (HPow.hPow (α := ℝ) (β := ℕ) 3 2 / HPow.hPow (α := ℝ) (β := ℕ) 4 2) *
        HPow.hPow (β := ℕ) ε 2 ≤
    (∑ x ∈ (chunk hP G ε hU).parts ×ˢ (chunk hP G ε hV).parts,
        HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity x.1 x.2) : ℝ) 2) /
      HPow.hPow (α := ℝ) (↑(HMul.hMul (α := ℕ) 4 4) : ℝ) #P.parts

Tactic:
simp_rw [sp, card_product, card_chunk (m_pos hPα).ne', ← mul_pow, cast_pow, mul_pow,
          div_pow, ← mul_assoc] at this

Premises used: SzemerediRegularity.card_chunk, Finset.card_product, mul_assoc, SzemerediRegularity.m_pos, LT.lt.ne', div_pow, Nat.cast_pow, 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
this :
  HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity U V) : ℝ) 2 - HPow.hPow (β := ℕ) ε 5 / 25 +
      (↑(#(star hP G ε hU V) * #(star hP G ε hV U)) : ℝ) / HPow.hPow (α := ℝ) (↑(HMul.hMul (α := ℕ) 4 4) : ℝ) #P.parts *
          (HPow.hPow (α := ℝ) (β := ℕ) 3 2 / HPow.hPow (α := ℝ) (β := ℕ) 4 2) *
        HPow.hPow (β := ℕ) ε 2 ≤
    (∑ x ∈ (chunk hP G ε hU).parts ×ˢ (chunk hP G ε hV).parts,
        HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity x.1 x.2) : ℝ) 2) /
      HPow.hPow (α := ℝ) (↑(HMul.hMul (α := ℕ) 4 4) : ℝ) #P.parts
⊢ HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity U V) : ℝ) 2 - HPow.hPow (β := ℕ) ε 5 / 25 +
      HMul.hMul (α := ℝ) (↑(#(star hP G ε hU V)) : ℝ) (↑(#(star hP G ε hV U)) : ℝ) / HPow.hPow (α := ℝ) 16 #P.parts *
          (9 / 16) *
        HPow.hPow (β := ℕ) ε 2 ≤
    (∑ x ∈ (chunk hP G ε hU).parts ×ˢ (chunk hP G ε hV).parts,
        HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity x.1 x.2) : ℝ) 2) /
      HPow.hPow (α := ℝ) 16 #P.parts

Tactic:
norm_num at this
-- 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
this :
  HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity U V) : ℝ) 2 - HPow.hPow (β := ℕ) ε 5 / 25 +
      HMul.hMul (α := ℝ) (↑(#(star hP G ε hU V)) : ℝ) (↑(#(star hP G ε hV U)) : ℝ) / HPow.hPow (α := ℝ) 16 #P.parts *
          (9 / 16) *
        HPow.hPow (β := ℕ) ε 2 ≤
    (∑ x ∈ (chunk hP G ε hU).parts ×ˢ (chunk hP G ε hV).parts,
        HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity x.1 x.2) : ℝ) 2) /
      HPow.hPow (α := ℝ) 16 #P.parts
⊢ HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity U V) : ℝ) 2 - HPow.hPow (β := ℕ) ε 5 / 25 +
      HMul.hMul (α := ℝ) (↑(#(star hP G ε hU V)) : ℝ) (↑(#(star hP G ε hV U)) : ℝ) / HPow.hPow (α := ℝ) 16 #P.parts *
          (9 / 16) *
        HPow.hPow (β := ℕ) ε 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:
this
-- 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
this :
  HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity U V) : ℝ) 2 - HPow.hPow (β := ℕ) ε 5 / 25 +
      HMul.hMul (α := ℝ) (↑(#(star hP G ε hU V)) : ℝ) (↑(#(star hP G ε hV U)) : ℝ) / HPow.hPow (α := ℝ) 16 #P.parts *
          (9 / 16) *
        HPow.hPow (β := ℕ) ε 2 ≤
    (∑ x ∈ (chunk hP G ε hU).parts ×ˢ (chunk hP G ε hV).parts,
        HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity x.1 x.2) : ℝ) 2) /
      HPow.hPow (α := ℝ) 16 #P.parts
⊢ HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity U V) : ℝ) 2 - HPow.hPow (β := ℕ) ε 5 / 25 +
      HMul.hMul (α := ℝ) (↑(#(star hP G ε hU V)) : ℝ) (↑(#(star hP G ε hV U)) : ℝ) / HPow.hPow (α := ℝ) 16 #P.parts *
          (9 / 16) *
        HPow.hPow (β := ℕ) ε 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:
exact this
-- 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_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) : ℝ)|
⊢ 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)) : ℝ)|

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

Premises used: SzemerediRegularity.card_chunk, Finset.card_product, 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
⊢ 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:
simpa using edgeDensity_star_not_uniform hPα hPε hε₁ hUVne hUV

Premises used: _private.0.SzemerediRegularity.edgeDensity_star_not_uniform
-- 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 (α := ℝ) (β := ℕ) (↑(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
⊢ 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

Tactic:
rw [sp, card_product]

Premises used: Finset.card_product