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
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)
nlinarith : 4 / 5 * ε * (4 / 5 * ε) * (9 / 16 * HPow.hPow (β := ℕ) ε 2) < HPow.hPow (β := ℕ) ε 4 / 3 → 5 / 5 = 1
nlinarith₁ :
  4 / 5 * ε * (4 / 5 * ε) * (9 / 16 * HPow.hPow (β := ℕ) ε 2) < HPow.hPow (β := ℕ) ε 4 / 3 → HMul.hMul (α := ℝ) 1 5 = 5
nlinarith₂ :
  4 / 5 * ε * (4 / 5 * ε) * (9 / 16 * HPow.hPow (β := ℕ) ε 2) < HPow.hPow (β := ℕ) ε 4 / 3 → HMul.hMul (α := ℝ) 5 1 = 5
nlinarith₃ : 4 / 5 * ε * (4 / 5 * ε) * (9 / 16 * HPow.hPow (β := ℕ) ε 2) < HPow.hPow (β := ℕ) ε 4 / 3 → 5 / 5 = 1
nlinarith₄ :
  4 / 5 * ε * (4 / 5 * ε) * (9 / 16 * HPow.hPow (β := ℕ) ε 2) < HPow.hPow (β := ℕ) ε 4 / 3 → HMul.hMul (α := ℝ) 1 5 = 5
nlinarith₅ :
  4 / 5 * ε * (4 / 5 * ε) * (9 / 16 * HPow.hPow (β := ℕ) ε 2) < HPow.hPow (β := ℕ) ε 4 / 3 → HMul.hMul (α := ℝ) 5 1 = 5
nlinarith₆ :
  4 / 5 * ε * (4 / 5 * ε) * (9 / 16 * HPow.hPow (β := ℕ) ε 2) < HPow.hPow (β := ℕ) ε 4 / 3 → HMul.hMul (α := ℝ) 5 5 = 25
nlinarith₇ : 4 / 5 * ε * (4 / 5 * ε) * (9 / 16 * HPow.hPow (β := ℕ) ε 2) < HPow.hPow (β := ℕ) ε 4 / 3 → 16 / 16 = 1
nlinarith₈ :
  4 / 5 * ε * (4 / 5 * ε) * (9 / 16 * HPow.hPow (β := ℕ) ε 2) < HPow.hPow (β := ℕ) ε 4 / 3 →
    HMul.hMul (α := ℝ) 1 16 = 16
nlinarith₉ :
  4 / 5 * ε * (4 / 5 * ε) * (9 / 16 * HPow.hPow (β := ℕ) ε 2) < HPow.hPow (β := ℕ) ε 4 / 3 →
    3 * HPow.hPow (α := ℝ) (β := ℕ) 1 2 = 3
nlinarith₁₀ :
  4 / 5 * ε * (4 / 5 * ε) * (9 / 16 * HPow.hPow (β := ℕ) ε 2) < HPow.hPow (β := ℕ) ε 4 / 3 →
    HMul.hMul (α := ℝ) 16 3 = 48
nlinarith₁₁ :
  4 / 5 * ε * (4 / 5 * ε) * (9 / 16 * HPow.hPow (β := ℕ) ε 2) < HPow.hPow (β := ℕ) ε 4 / 3 →
    HMul.hMul (α := ℝ) 25 48 = 1200
nlinarith₁₂ :
  4 / 5 * ε * (4 / 5 * ε) * (9 / 16 * HPow.hPow (β := ℕ) ε 2) < HPow.hPow (β := ℕ) ε 4 / 3 →
    400 * HPow.hPow (α := ℝ) (β := ℕ) 1 4 = 400
nlinarith₁₃ : 4 / 5 * ε * (4 / 5 * ε) * (9 / 16 * HPow.hPow (β := ℕ) ε 2) < HPow.hPow (β := ℕ) ε 4 / 3 → 3 / 3 = 1
nlinarith₁₄ :
  4 / 5 * ε * (4 / 5 * ε) * (9 / 16 * HPow.hPow (β := ℕ) ε 2) < HPow.hPow (β := ℕ) ε 4 / 3 →
    HMul.hMul (α := ℝ) 400 3 = 1200
⊢ HPow.hPow (β := ℕ) ε 4 / 3 ≤ 4 / 5 * ε * (4 / 5 * ε) * (9 / 16 * HPow.hPow (β := ℕ) ε 2)
have nlinarith₁₅ : 4 / 5 * ε * (4 / 5 * ε) * (9 / 16 * HPow.hPow (β := ℕ) ε 2) < HPow.hPow (β := ℕ) ε 4 / 3 → GT.gt (α := ℝ) 1200 0
Tactic: nlinarith
-- 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
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 ≤ 9 / HPow.hPow (α := ℝ) (β := ℕ) 4 2 * HPow.hPow (β := ℕ) ε 2
have bc : 0 ≤ HPow.hPow (β := ℕ) ε 2
Tactic: simp
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
hP : P.IsEquipartition
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
U 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
⊢ 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
have t : (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
-- 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
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 ≤ ε
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
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 ≤ ε
⊢ 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
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
⊢ 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
have hε : 0 ≤ ε
Tactic: have hε : 0 ≤ ε := by 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
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 ≤ ε
⊢ 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
have sp : ∀ (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
-- 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
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
⊢ 0 ≤ 3 / 4 * ε
have linarith : 3 / 4 * ε < 0 → 4 / 4 = 1
Tactic: linarith
-- 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
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
⊢ 0 ≤ 3 / 4 * ε
have linarith₁ : 3 / 4 * ε < 0 → HMul.hMul (α := ℝ) 1 4 = 4
Tactic: linarith
-- 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
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
⊢ 0 ≤ 3 / 4 * ε
have linarith₂ : 3 / 4 * ε < 0 → HMul.hMul (α := ℝ) 4 1 = 4
Tactic: linarith
-- 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
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
⊢ 0 ≤ 3 / 4 * ε
have linarith₃ : 3 / 4 * ε < 0 → GT.gt (α := ℝ) 4 0
Tactic: linarith
-- 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
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
⊢ 0 ≤ 3 / 4 * ε
have linarith₄ : 3 / 4 * ε < 0 → 3 * (0 - ε) + (HMul.hMul (α := ℝ) 1 3 * (1 * ε) - HMul.hMul (α := ℝ) 4 0) = 0
Tactic: linarith
-- 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
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
⊢ 0 ≤ 3 / 4 * ε
have linarith₅ : 3 / 4 * ε < 0 → GT.gt (α := ℝ) 3 0
Tactic: linarith
-- 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
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
⊢ 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
have refine_3 : ∀
  (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 +
      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: have := add_div_le_sum_sq_div_card t (fun x => (G.edgeDensity x.1 x.2 : ℝ))
        ((G.edgeDensity U V : ℝ) ^ 2 - ε ^ 5 / ↑25) (show 0 ≤ 3 / 4 * ε by linarith) ?_ ?_
-- 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
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_3 :
  ∀
    (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 +
        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
⊢ 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
have refine_1 : 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: have := add_div_le_sum_sq_div_card t (fun x => (G.edgeDensity x.1 x.2 : ℝ))
        ((G.edgeDensity U V : ℝ) ^ 2 - ε ^ 5 / ↑25) (show 0 ≤ 3 / 4 * ε by linarith) ?_ ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
hP : P.IsEquipartition
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
U 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 +
      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
have 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
Tactic: simp_rw [sp, card_product, card_chunk (m_pos hPα).ne', ← mul_pow, cast_pow, mul_pow,
          div_pow, ← mul_assoc] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
hP : P.IsEquipartition
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
U 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 ≤
    (∑ 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
have 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
Tactic: norm_num at this
Cleared hypotheses: this