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
A B : Finset (Finset α)
hA : A ⊆ (chunk hP G ε hU).parts
hB : B ⊆ (chunk hP G ε hV).parts
left :
  (∑ ab ∈ A.product B, (↑(G.edgeDensity ab.1 ab.2) : ℝ)) / HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#B) : ℝ) ≤
    (↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) : ℝ) + HPow.hPow (β := ℕ) ε 5 / 49
⊢ (∑ ab ∈ A.product B, (↑(G.edgeDensity ab.1 ab.2) : ℝ)) / HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#B) : ℝ) -
      (↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) : ℝ) ≤
    HPow.hPow (β := ℕ) ε 5 / 49

Tactic:
rw [sub_le_iff_le_add']

Premises used: sub_le_iff_le_add'
-- 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
A B : Finset (Finset α)
hA : A ⊆ (chunk hP G ε hU).parts
hB : B ⊆ (chunk hP G ε hV).parts
⊢ (∑ ab ∈ A.product B, (↑(G.edgeDensity ab.1 ab.2) : ℝ)) / HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#B) : ℝ) ≤
    (↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) : ℝ) + HPow.hPow (β := ℕ) ε 5 / 49

Tactic:
sum_density_div_card_le_density_add_eps hPα hPε hε₁ hA hB

Premises used: _private.0.SzemerediRegularity.sum_density_div_card_le_density_add_eps
-- 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
A B : Finset (Finset α)
hA : A ⊆ (chunk hP G ε hU).parts
hB : B ⊆ (chunk hP G ε hV).parts
⊢ (∑ ab ∈ A.product B, (↑(G.edgeDensity ab.1 ab.2) : ℝ)) / HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#B) : ℝ) ≤
    (↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) : ℝ) + HPow.hPow (β := ℕ) ε 5 / 49

Tactic:
exact sum_density_div_card_le_density_add_eps hPα hPε hε₁ hA hB

Premises used: _private.0.SzemerediRegularity.sum_density_div_card_le_density_add_eps
-- 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
A B : Finset (Finset α)
hA : A ⊆ (chunk hP G ε hU).parts
hB : B ⊆ (chunk hP G ε hV).parts
this :
  (↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) : ℝ) -
      (∑ ab ∈ A.product B, (↑(G.edgeDensity ab.1 ab.2) : ℝ)) / HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#B) : ℝ) ≤
    HPow.hPow (β := ℕ) ε 5 / 50
apply : HPow.hPow (β := ℕ) ε 5 / 50 ≤ HPow.hPow (β := ℕ) ε 5 / 49
⊢ (↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) : ℝ) -
      (∑ ab ∈ A.product B, (↑(G.edgeDensity ab.1 ab.2) : ℝ)) / HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#B) : ℝ) ≤
    HPow.hPow (β := ℕ) ε 5 / 49

Tactic:
apply this.trans

Premises used: LE.le.trans
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
hP : P.IsEquipartition
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst_3 : Nonempty α
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hε₁ : ε ≤ 1
hU : U ∈ P.parts
hV : V ∈ P.parts
A B : Finset (Finset α)
hA : A ⊆ (chunk hP G ε hU).parts
hB : B ⊆ (chunk hP G ε hV).parts
this :
  (↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) : ℝ) -
      (∑ ab ∈ A.product B, (↑(G.edgeDensity ab.1 ab.2) : ℝ)) / HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#B) : ℝ) ≤
    HPow.hPow (β := ℕ) ε 5 / 50
hc : 0 ≤ HPow.hPow (β := ℕ) ε 5
hdb : LE.le (α := ℝ) 49 50
⊢ HPow.hPow (β := ℕ) ε 5 / 50 ≤ HPow.hPow (β := ℕ) ε 5 / 49

Tactic:
gcongr
-- 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
A B : Finset (Finset α)
hA : A ⊆ (chunk hP G ε hU).parts
hB : B ⊆ (chunk hP G ε hV).parts
this :
  (↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) : ℝ) -
      (∑ ab ∈ A.product B, (↑(G.edgeDensity ab.1 ab.2) : ℝ)) / HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#B) : ℝ) ≤
    HPow.hPow (β := ℕ) ε 5 / 50
hc hc₁ hc₂ hc₃ : 0 < m → 0 ≤ HPow.hPow (β := ℕ) ε 5
hc₄ hc₅ : 0 < m → 0 < ε → 0 ≤ HPow.hPow (β := ℕ) ε 5
⊢ 0 ≤ HPow.hPow (β := ℕ) ε 5

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
A B : Finset (Finset α)
hA : A ⊆ (chunk hP G ε hU).parts
hB : B ⊆ (chunk hP G ε hV).parts
this :
  (↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) : ℝ) -
      (∑ ab ∈ A.product B, (↑(G.edgeDensity ab.1 ab.2) : ℝ)) / HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#B) : ℝ) ≤
    HPow.hPow (β := ℕ) ε 5 / 50
⊢ LE.le (α := ℝ) 49 50

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
A B : Finset (Finset α)
hA : A ⊆ (chunk hP G ε hU).parts
hB : B ⊆ (chunk hP G ε hV).parts
this :
  (↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) : ℝ) -
      (∑ ab ∈ A.product B, (↑(G.edgeDensity ab.1 ab.2) : ℝ)) / HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#B) : ℝ) ≤
    HPow.hPow (β := ℕ) ε 5 / 50
hc : 0 ≤ HPow.hPow (β := ℕ) ε 5
hd : LT.lt (α := ℝ) 0 49
hc₁ : 0 ≤ HPow.hPow (β := ℕ) ε 5
hdb : LE.le (α := ℝ) 49 50
hc₂ : 0 ≤ HPow.hPow (β := ℕ) ε 5
hdb₁ : LE.le (α := ℝ) 49 50
⊢ HPow.hPow (β := ℕ) ε 5 / 50 ≤ HPow.hPow (β := ℕ) ε 5 / 49

Tactic:
gcongr <;> [sz_positivity; 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
A B : Finset (Finset α)
hA : A ⊆ (chunk hP G ε hU).parts
hB : B ⊆ (chunk hP G ε hV).parts
right :
  (↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) : ℝ) -
      (∑ ab ∈ A.product B, (↑(G.edgeDensity ab.1 ab.2) : ℝ)) / HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#B) : ℝ) ≤
    HPow.hPow (β := ℕ) ε 5 / 50
⊢ (↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) : ℝ) -
      (∑ ab ∈ A.product B, (↑(G.edgeDensity ab.1 ab.2) : ℝ)) / HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#B) : ℝ) ≤
    HPow.hPow (β := ℕ) ε 5 / 49

Tactic:
suffices (G.edgeDensity (A.biUnion id) (B.biUnion id) : ℝ) -
      (∑ ab ∈ A.product B, (G.edgeDensity ab.1 ab.2 : ℝ)) / (#A * #B) ≤ ε ^ 5 / 50 by
    apply this.trans
    gcongr <;> [sz_positivity; 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
A B : Finset (Finset α)
hA : A ⊆ (chunk hP G ε hU).parts
hB : B ⊆ (chunk hP G ε hV).parts
right :
  (↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) : ℝ) - HPow.hPow (β := ℕ) ε 5 / 50 ≤
    (∑ ab ∈ A.product B, (↑(G.edgeDensity ab.1 ab.2) : ℝ)) / HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#B) : ℝ)
⊢ (↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) : ℝ) -
      (∑ ab ∈ A.product B, (↑(G.edgeDensity ab.1 ab.2) : ℝ)) / HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#B) : ℝ) ≤
    HPow.hPow (β := ℕ) ε 5 / 50

Tactic:
rw [sub_le_iff_le_add, ← sub_le_iff_le_add']

Premises used: sub_le_iff_le_add, sub_le_iff_le_add'
-- 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
A B : Finset (Finset α)
hA : A ⊆ (chunk hP G ε hU).parts
hB : B ⊆ (chunk hP G ε hV).parts
⊢ (↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) : ℝ) - HPow.hPow (β := ℕ) ε 5 / 50 ≤
    (∑ ab ∈ A.product B, (↑(G.edgeDensity ab.1 ab.2) : ℝ)) / HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#B) : ℝ)

Tactic:
apply density_sub_eps_le_sum_density_div_card hPα hPε hA hB

Premises used: _private.0.SzemerediRegularity.density_sub_eps_le_sum_density_div_card
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst_3 : Nonempty α
hP : P.IsEquipartition
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
inl :
  ∀ (hGε : (↑(G.edgeDensity U V) : ℝ) ≤ HPow.hPow (β := ℕ) ε 5 / 50),
    HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity U V) : ℝ) 2 - HPow.hPow (β := ℕ) ε 5 / 25 ≤
      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
inr :
  ∀ (hGε : HPow.hPow (β := ℕ) ε 5 / 50 ≤ (↑(G.edgeDensity U V) : ℝ)),
    HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity U V) : ℝ) 2 - HPow.hPow (β := ℕ) ε 5 / 25 ≤
      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 (α := ℝ) (β := ℕ) (↑(G.edgeDensity U V) : ℝ) 2 - HPow.hPow (β := ℕ) ε 5 / 25 ≤
    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

Tactic:
obtain hGε | hGε := le_total (G.edgeDensity U V : ℝ) (ε ^ 5 / 50)

Premises used: SimpleGraph.edgeDensity, HDiv.hDiv, Rat.cast, le_total, HPow.hPow, OfNat.ofNat
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst_3 : Nonempty α
hP : P.IsEquipartition
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
hGε : (↑(G.edgeDensity U V) : ℝ) ≤ HPow.hPow (β := ℕ) ε 5 / 50
⊢ HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity U V) : ℝ) 2 - HPow.hPow (β := ℕ) ε 5 / 25 ≤
    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

Tactic:
(sub_nonpos_of_le <| (sq_le ?_ ?_).trans <| hGε.trans ?_).trans (sq_nonneg _)

Premises used: sq_le, sq_nonneg, sub_nonpos_of_le, LE.le.trans
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst_3 : Nonempty α
hP : P.IsEquipartition
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
hGε : (↑(G.edgeDensity U V) : ℝ) ≤ HPow.hPow (β := ℕ) ε 5 / 50
inl : LE.le (α := ℝ) 0 (↑(G.edgeDensity U V) : ℝ)
inl₁ : LE.le (α := ℝ) (↑(G.edgeDensity U V) : ℝ) 1
inl₂ : HPow.hPow (β := ℕ) ε 5 / 50 ≤ HPow.hPow (β := ℕ) ε 5 / 25
⊢ HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity U V) : ℝ) 2 - HPow.hPow (β := ℕ) ε 5 / 25 ≤
    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

Tactic:
refine (sub_nonpos_of_le <| (sq_le ?_ ?_).trans <| hGε.trans ?_).trans (sq_nonneg _)

Premises used: sq_le, sq_nonneg, sub_nonpos_of_le, LE.le.trans
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst_3 : Nonempty α
hP : P.IsEquipartition
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
hGε : (↑(G.edgeDensity U V) : ℝ) ≤ HPow.hPow (β := ℕ) ε 5 / 50
⊢ LE.le (α := ℝ) 0 (↑(G.edgeDensity U V) : ℝ)

Tactic:
mod_cast G.edgeDensity_nonneg _ _

Premises used: congrArg, SimpleGraph.edgeDensity, cast, Rat.cast, Rat.natCast_le_cast._simp_1, LE.le, congrFun', Nat.cast_zero, Eq.symm, SimpleGraph.edgeDensity_nonneg, Eq.trans
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst_3 : Nonempty α
hP : P.IsEquipartition
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
hGε : (↑(G.edgeDensity U V) : ℝ) ≤ HPow.hPow (β := ℕ) ε 5 / 50
⊢ LE.le (α := ℝ) 0 (↑(G.edgeDensity U V) : ℝ)

Tactic:
exact mod_cast G.edgeDensity_nonneg _ _

Premises used: SimpleGraph.edgeDensity_nonneg
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst_3 : Nonempty α
hP : P.IsEquipartition
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
hGε : (↑(G.edgeDensity U V) : ℝ) ≤ HPow.hPow (β := ℕ) ε 5 / 50
⊢ LE.le (α := ℝ) (↑(G.edgeDensity U V) : ℝ) 1

Tactic:
mod_cast G.edgeDensity_le_one _ _

Premises used: SimpleGraph.edgeDensity_le_one, congrArg, SimpleGraph.edgeDensity, cast, Rat.cast, LE.le, Rat.cast_le_natCast._simp_1, Eq.symm, Nat.cast_one, Eq.trans
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst_3 : Nonempty α
hP : P.IsEquipartition
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
hGε : (↑(G.edgeDensity U V) : ℝ) ≤ HPow.hPow (β := ℕ) ε 5 / 50
⊢ LE.le (α := ℝ) (↑(G.edgeDensity U V) : ℝ) 1

Tactic:
exact mod_cast G.edgeDensity_le_one _ _

Premises used: SimpleGraph.edgeDensity_le_one
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst_3 : Nonempty α
hP : P.IsEquipartition
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
hGε : (↑(G.edgeDensity U V) : ℝ) ≤ HPow.hPow (β := ℕ) ε 5 / 50
sz_positivity sz_positivity₁ sz_positivity₂ sz_positivity₃ : 0 < m → 0 ≤ HPow.hPow (β := ℕ) ε 5
sz_positivity₄ sz_positivity₅ : 0 < m → 0 < ε → 0 ≤ HPow.hPow (β := ℕ) ε 5
⊢ 0 ≤ HPow.hPow (β := ℕ) ε 5

Tactic:
sz_positivity
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst_3 : Nonempty α
hP : P.IsEquipartition
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
hGε : (↑(G.edgeDensity U V) : ℝ) ≤ HPow.hPow (β := ℕ) ε 5 / 50
⊢ LT.lt (α := ℝ) 0 25

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst_3 : Nonempty α
hP : P.IsEquipartition
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
hGε : (↑(G.edgeDensity U V) : ℝ) ≤ HPow.hPow (β := ℕ) ε 5 / 50
⊢ LE.le (α := ℝ) 25 50

Tactic:
norm_num
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst_3 : Nonempty α
hP : P.IsEquipartition
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
hGε : (↑(G.edgeDensity U V) : ℝ) ≤ HPow.hPow (β := ℕ) ε 5 / 50
⊢ HPow.hPow (β := ℕ) ε 5 / 50 ≤ HPow.hPow (β := ℕ) ε 5 / 25

Tactic:
exact div_le_div_of_nonneg_left (by sz_positivity) (by simp) (by norm_num)

Premises used: div_le_div_of_nonneg_left
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst_3 : Nonempty α
hP : P.IsEquipartition
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
hGε : HPow.hPow (β := ℕ) ε 5 / 50 ≤ (↑(G.edgeDensity U V) : ℝ)
⊢ 0 ≤ (↑(G.edgeDensity U V) : ℝ) - HPow.hPow (β := ℕ) ε 5 / 50

Tactic:
rw [← sub_nonneg] at hGε

Premises used: sub_nonneg
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst_3 : Nonempty α
hP : P.IsEquipartition
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
hGε : 0 ≤ (↑(G.edgeDensity U V) : ℝ) - HPow.hPow (β := ℕ) ε 5 / 50
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
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst_3 : Nonempty α
hP : P.IsEquipartition
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
hGε : 0 ≤ (↑(G.edgeDensity U V) : ℝ) - HPow.hPow (β := ℕ) ε 5 / 50
⊢ 0 ≤ ε

Tactic:
have : 0 ≤ ε := by sz_positivity
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst_3 : Nonempty α
hP : P.IsEquipartition
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
hGε : 0 ≤ (↑(G.edgeDensity U V) : ℝ) - HPow.hPow (β := ℕ) ε 5 / 50
this : 0 ≤ ε
⊢ HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity U V) : ℝ) 2 - HPow.hPow (β := ℕ) ε 5 / 25 =
    HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity U V) : ℝ) 2 - 1 * HPow.hPow (β := ℕ) ε 5 / 25 +
      HPow.hPow (α := ℝ) (β := ℕ) 0 10 / 2500

Tactic:
ring
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst_3 : Nonempty α
hP : P.IsEquipartition
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
hGε : 0 ≤ (↑(G.edgeDensity U V) : ℝ) - HPow.hPow (β := ℕ) ε 5 / 50
this : 0 ≤ ε
h₁ : LE.le (α := ℝ) (↑(G.edgeDensity U V) : ℝ) 1
⊢ HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity U V) : ℝ) 2 - 1 * HPow.hPow (β := ℕ) ε 5 / 25 +
      HPow.hPow (α := ℝ) (β := ℕ) 0 10 / 2500 ≤
    HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity U V) : ℝ) 2 -
        (↑(G.edgeDensity U V) : ℝ) * HPow.hPow (β := ℕ) ε 5 / 25 +
      HPow.hPow (β := ℕ) ε 10 / 2500

Tactic:
gcongr
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst_3 : Nonempty α
hP : P.IsEquipartition
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
hGε : 0 ≤ (↑(G.edgeDensity U V) : ℝ) - HPow.hPow (β := ℕ) ε 5 / 50
this : 0 ≤ ε
⊢ LE.le (α := ℝ) (↑(G.edgeDensity U V) : ℝ) 1

Tactic:
mod_cast G.edgeDensity_le_one ..

Premises used: SimpleGraph.edgeDensity_le_one, congrArg, SimpleGraph.edgeDensity, cast, Rat.cast, LE.le, Rat.cast_le_natCast._simp_1, Eq.symm, Nat.cast_one, Eq.trans
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst_3 : Nonempty α
hP : P.IsEquipartition
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
hGε : 0 ≤ (↑(G.edgeDensity U V) : ℝ) - HPow.hPow (β := ℕ) ε 5 / 50
this : 0 ≤ ε
⊢ LE.le (α := ℝ) (↑(G.edgeDensity U V) : ℝ) 1

Tactic:
exact mod_cast G.edgeDensity_le_one ..

Premises used: SimpleGraph.edgeDensity_le_one