awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
hP : P.IsEquipartition
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst_3 : Nonempty α
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hε₁ : ε ≤ 1
hU : U ∈ P.parts
hV : V ∈ P.parts
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
⊢ HPow.hPow (β := ℕ) ε 5 / 50 ≤ HPow.hPow (β := ℕ) ε 5 / 49
have hd : LT.lt (α := ℝ) 0 49
Tactic: gcongr <;> [sz_positivity; norm_num]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
hP : P.IsEquipartition
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst_3 : Nonempty α
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hε₁ : ε ≤ 1
hU : U ∈ P.parts
hV : V ∈ P.parts
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
⊢ HPow.hPow (β := ℕ) ε 5 / 50 ≤ HPow.hPow (β := ℕ) ε 5 / 49
have hdb : LE.le (α := ℝ) 49 50
Tactic: gcongr <;> [sz_positivity; norm_num]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
hP : P.IsEquipartition
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst_3 : Nonempty α
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hε₁ : ε ≤ 1
hU : U ∈ P.parts
hV : V ∈ P.parts
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)) : ℝ) -
      (∑ ab ∈ A.product B, (↑(G.edgeDensity ab.1 ab.2) : ℝ)) / HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#B) : ℝ) ≤
    HPow.hPow (β := ℕ) ε 5 / 49
have 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
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]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
hP : P.IsEquipartition
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst_3 : Nonempty α
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hε₁ : ε ≤ 1
hU : U ∈ P.parts
hV : V ∈ P.parts
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)) : ℝ) -
      (∑ ab ∈ A.product B, (↑(G.edgeDensity ab.1 ab.2) : ℝ)) / HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#B) : ℝ) ≤
    HPow.hPow (β := ℕ) ε 5 / 50
have 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) : ℝ)
Tactic: rw [sub_le_iff_le_add, ← sub_le_iff_le_add']
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk (goal)
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
⊢ 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
have 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
Tactic: obtain hGε | hGε := le_total (G.edgeDensity U V : ℝ) (ε ^ 5 / 50)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk (goal)
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
⊢ 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
have 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
Tactic: obtain hGε | hGε := le_total (G.edgeDensity U V : ℝ) (ε ^ 5 / 50)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk (goal)
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
have inl : LE.le (α := ℝ) 0 (↑(G.edgeDensity U V) : ℝ)
Tactic: refine (sub_nonpos_of_le <| (sq_le ?_ ?_).trans <| hGε.trans ?_).trans (sq_nonneg _)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk (goal)
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) : ℝ)
⊢ 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
have inl₁ : LE.le (α := ℝ) (↑(G.edgeDensity U V) : ℝ) 1
Tactic: refine (sub_nonpos_of_le <| (sq_le ?_ ?_).trans <| hGε.trans ?_).trans (sq_nonneg _)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk (goal)
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
⊢ 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
have inl₂ : HPow.hPow (β := ℕ) ε 5 / 50 ≤ HPow.hPow (β := ℕ) ε 5 / 25
Tactic: refine (sub_nonpos_of_le <| (sq_le ?_ ?_).trans <| hGε.trans ?_).trans (sq_nonneg _)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk (goal)
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
⊢ 0 ≤ HPow.hPow (β := ℕ) ε 5
have sz_positivity : 0 < m → 0 ≤ HPow.hPow (β := ℕ) ε 5
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
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
⊢ 0 ≤ HPow.hPow (β := ℕ) ε 5
have sz_positivity₄ : 0 < m → 0 < ε → 0 ≤ HPow.hPow (β := ℕ) ε 5
Tactic: sz_positivity
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk (hypothesis)
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) : ℝ)
⊢ 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
have hGε₁ : 0 ≤ (↑(G.edgeDensity U V) : ℝ) - HPow.hPow (β := ℕ) ε 5 / 50
Tactic: rw [← sub_nonneg] at hGε
Cleared hypotheses: hGε
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk (goal)
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 ≤ ε
have sz_positivity : 0 < m → 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
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 ≤ ε
⊢ 0 ≤ ε
have sz_positivity₄ : 0 < m → 0 < ε → 0 ≤ ε
Tactic: sz_positivity
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk (hypothesis)
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
⊢ 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
have this : 0 ≤ ε
Tactic: have : 0 ≤ ε := by 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
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 - 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
have h₁ : LE.le (α := ℝ) (↑(G.edgeDensity U V) : ℝ) 1
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk (goal)
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) : ℝ) - HPow.hPow (β := ℕ) ε 5 / 50) 2 ≤
    HPow.hPow (β := ℕ)
      ((∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, (↑(G.edgeDensity ab.1 ab.2) : ℝ)) /
        HPow.hPow (α := ℝ) 16 #P.parts)
      2
have hab : (↑(G.edgeDensity U V) : ℝ) - HPow.hPow (β := ℕ) ε 5 / 50 ≤
  (∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, (↑(G.edgeDensity ab.1 ab.2) : ℝ)) /
    HPow.hPow (α := ℝ) 16 #P.parts
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk (hypothesis)
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 ≤ ε
⊢ (↑(G.edgeDensity U V) : ℝ) - HPow.hPow (β := ℕ) ε 5 / 50 ≤
    (∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, (↑(G.edgeDensity ab.1 ab.2) : ℝ)) /
      HPow.hPow (α := ℝ) 16 #P.parts
have rflU : (chunk hP G ε hU).parts ⊆ (chunk hP G ε hU).parts
Tactic: have rflU := Subset.refl (chunk hP G ε hU).parts
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk (hypothesis)
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 ≤ ε
rflU : (chunk hP G ε hU).parts ⊆ (chunk hP G ε hU).parts
⊢ (↑(G.edgeDensity U V) : ℝ) - HPow.hPow (β := ℕ) ε 5 / 50 ≤
    (∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, (↑(G.edgeDensity ab.1 ab.2) : ℝ)) /
      HPow.hPow (α := ℝ) 16 #P.parts
have rflV : (chunk hP G ε hV).parts ⊆ (chunk hP G ε hV).parts
Tactic: have rflV := Subset.refl (chunk hP G ε hV).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
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 ≤ ε
rflU : (chunk hP G ε hU).parts ⊆ (chunk hP G ε hU).parts
rflV : (chunk hP G ε hV).parts ⊆ (chunk hP G ε hV).parts
⊢ (↑(G.edgeDensity U V) : ℝ) - HPow.hPow (β := ℕ) ε 5 / 50 ≤
    (∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, (↑(G.edgeDensity ab.1 ab.2) : ℝ)) /
      HPow.hPow (α := ℝ) 16 #P.parts
have hab : (↑(G.edgeDensity U V) : ℝ) - HPow.hPow (β := ℕ) ε 5 / 50 ≤
  (↑(G.edgeDensity ((chunk hP G ε hU).parts.biUnion id) ((chunk hP G ε hV).parts.biUnion id)) : ℝ) -
    HPow.hPow (β := ℕ) ε 5 / 50
Tactic: refine (le_trans ?_ <| density_sub_eps_le_sum_density_div_card hPα hPε rflU rflV).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
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 ≤ ε
rflU : (chunk hP G ε hU).parts ⊆ (chunk hP G ε hU).parts
rflV : (chunk hP G ε hV).parts ⊆ (chunk hP G ε hV).parts
hab :
  (↑(G.edgeDensity U V) : ℝ) - HPow.hPow (β := ℕ) ε 5 / 50 ≤
    (↑(G.edgeDensity ((chunk hP G ε hU).parts.biUnion id) ((chunk hP G ε hV).parts.biUnion id)) : ℝ) -
      HPow.hPow (β := ℕ) ε 5 / 50
⊢ (↑(G.edgeDensity U V) : ℝ) - HPow.hPow (β := ℕ) ε 5 / 50 ≤
    (∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, (↑(G.edgeDensity ab.1 ab.2) : ℝ)) /
      HPow.hPow (α := ℝ) 16 #P.parts
have hab₁ : (∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, (↑(G.edgeDensity ab.1 ab.2) : ℝ)) /
    HMul.hMul (α := ℝ) (↑(#(chunk hP G ε hU).parts) : ℝ) (↑(#(chunk hP G ε hV).parts) : ℝ) ≤
  (∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, (↑(G.edgeDensity ab.1 ab.2) : ℝ)) /
    HPow.hPow (α := ℝ) 16 #P.parts
Tactic: refine (le_trans ?_ <| density_sub_eps_le_sum_density_div_card hPα hPε rflU rflV).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
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 ≤ ε
rflU : (chunk hP G ε hU).parts ⊆ (chunk hP G ε hU).parts
rflV : (chunk hP G ε hV).parts ⊆ (chunk hP G ε hV).parts
⊢ (↑(G.edgeDensity U V) : ℝ) - HPow.hPow (β := ℕ) ε 5 / 50 ≤
    (↑(G.edgeDensity ((chunk hP G ε hU).parts.biUnion id) ((chunk hP G ε hV).parts.biUnion id)) : ℝ) -
      HPow.hPow (β := ℕ) ε 5 / 50
have hab : (↑(G.edgeDensity U V) : ℝ) - HPow.hPow (β := ℕ) ε 5 / 50 ≤
  (↑(G.edgeDensity U ((chunk hP G ε hV).parts.biUnion id)) : ℝ) - HPow.hPow (β := ℕ) ε 5 / 50
Tactic: rw [biUnion_parts, biUnion_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
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 ≤ ε
rflU : (chunk hP G ε hU).parts ⊆ (chunk hP G ε hU).parts
rflV : (chunk hP G ε hV).parts ⊆ (chunk hP G ε hV).parts
hab :
  (↑(G.edgeDensity U V) : ℝ) - HPow.hPow (β := ℕ) ε 5 / 50 ≤
    (↑(G.edgeDensity U ((chunk hP G ε hV).parts.biUnion id)) : ℝ) - HPow.hPow (β := ℕ) ε 5 / 50
⊢ (↑(G.edgeDensity U V) : ℝ) - HPow.hPow (β := ℕ) ε 5 / 50 ≤
    (↑(G.edgeDensity ((chunk hP G ε hU).parts.biUnion id) ((chunk hP G ε hV).parts.biUnion id)) : ℝ) -
      HPow.hPow (β := ℕ) ε 5 / 50
have hab₁ : (↑(G.edgeDensity U V) : ℝ) - HPow.hPow (β := ℕ) ε 5 / 50 ≤ (↑(G.edgeDensity U V) : ℝ) - HPow.hPow (β := ℕ) ε 5 / 50
Tactic: rw [biUnion_parts, biUnion_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
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 ≤ ε
rflU : (chunk hP G ε hU).parts ⊆ (chunk hP G ε hU).parts
rflV : (chunk hP G ε hV).parts ⊆ (chunk hP G ε hV).parts
⊢ (∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, (↑(G.edgeDensity ab.1 ab.2) : ℝ)) /
      HMul.hMul (α := ℝ) (↑(#(chunk hP G ε hU).parts) : ℝ) (↑(#(chunk hP G ε hV).parts) : ℝ) ≤
    (∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, (↑(G.edgeDensity ab.1 ab.2) : ℝ)) /
      HPow.hPow (α := ℝ) 16 #P.parts
have hab : (∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, (↑(G.edgeDensity ab.1 ab.2) : ℝ)) /
    HPow.hPow (α := ℝ) (↑(HMul.hMul (α := ℕ) 4 4) : ℝ) #P.parts ≤
  (∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, (↑(G.edgeDensity ab.1 ab.2) : ℝ)) /
    HPow.hPow (α := ℝ) 16 #P.parts
Tactic: rw [card_chunk (m_pos hPα).ne', card_chunk (m_pos hPα).ne', ← cast_mul, ← mul_pow, cast_pow]