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
p : ℝ :=
  (∑ ab ∈ (star hP G ε hU V).product (star hP G ε hV U), (↑(G.edgeDensity ab.1 ab.2) : ℝ)) /
    HMul.hMul (α := ℝ) (↑(#(star hP G ε hU V)) : ℝ) (↑(#(star hP G ε hV U)) : ℝ)
q : ℝ :=
  (∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, (↑(G.edgeDensity ab.1 ab.2) : ℝ)) /
    (HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (α := ℝ) 4 #P.parts)
r : ℝ := (↑(G.edgeDensity ((star hP G ε hU V).biUnion id) ((star hP G ε hV U).biUnion id)) : ℝ)
s : ℝ := (↑(G.edgeDensity (G.nonuniformWitness ε U V) (G.nonuniformWitness ε V U)) : ℝ)
t : ℝ := (↑(G.edgeDensity U V) : ℝ)
hrs : |r - s| ≤ ε / 5
hst : ε ≤ |s - t|
hpr : |p - r| ≤ HPow.hPow (β := ℕ) ε 5 / 49
hqt : |q - t| ≤ HPow.hPow (β := ℕ) ε 5 / 49
⊢ 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
p : ℝ :=
  (∑ ab ∈ (star hP G ε hU V).product (star hP G ε hV U), (↑(G.edgeDensity ab.1 ab.2) : ℝ)) /
    HMul.hMul (α := ℝ) (↑(#(star hP G ε hU V)) : ℝ) (↑(#(star hP G ε hV U)) : ℝ)
q : ℝ :=
  (∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, (↑(G.edgeDensity ab.1 ab.2) : ℝ)) /
    (HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (α := ℝ) 4 #P.parts)
r : ℝ := (↑(G.edgeDensity ((star hP G ε hU V).biUnion id) ((star hP G ε hV U).biUnion id)) : ℝ)
s : ℝ := (↑(G.edgeDensity (G.nonuniformWitness ε U V) (G.nonuniformWitness ε V U)) : ℝ)
t : ℝ := (↑(G.edgeDensity U V) : ℝ)
hrs : |r - s| ≤ ε / 5
hst : ε ≤ |s - t|
hpr : |p - r| ≤ HPow.hPow (β := ℕ) ε 5 / 49
hqt : |q - t| ≤ HPow.hPow (β := ℕ) ε 5 / 49
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
p : ℝ :=
  (∑ ab ∈ (star hP G ε hU V).product (star hP G ε hV U), (↑(G.edgeDensity ab.1 ab.2) : ℝ)) /
    HMul.hMul (α := ℝ) (↑(#(star hP G ε hU V)) : ℝ) (↑(#(star hP G ε hV U)) : ℝ)
q : ℝ :=
  (∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, (↑(G.edgeDensity ab.1 ab.2) : ℝ)) /
    (HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (α := ℝ) 4 #P.parts)
r : ℝ := (↑(G.edgeDensity ((star hP G ε hU V).biUnion id) ((star hP G ε hV U).biUnion id)) : ℝ)
s : ℝ := (↑(G.edgeDensity (G.nonuniformWitness ε U V) (G.nonuniformWitness ε V U)) : ℝ)
t : ℝ := (↑(G.edgeDensity U V) : ℝ)
hrs : |r - s| ≤ ε / 5
hst : ε ≤ |s - t|
hpr : |p - r| ≤ HPow.hPow (β := ℕ) ε 5 / 49
hqt : |q - t| ≤ HPow.hPow (β := ℕ) ε 5 / 49
⊢ 3 / 4 * ε ≤ |p - q|
have hε' : HPow.hPow (β := ℕ) ε 5 ≤ ε
Tactic: have hε' : ε ^ 5 ≤ ε := by
    simpa using pow_le_pow_of_le_one (by sz_positivity) hε₁ (show 1 ≤ 5 by simp)
-- 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
⊢ HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity U V) : ℝ) 2 - HPow.hPow (β := ℕ) ε 5 / 25 + HPow.hPow (β := ℕ) ε 4 / 3 ≤
    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
have bc : HPow.hPow (β := ℕ) ε 4 / 3 ≤
  HMul.hMul (α := ℝ) (↑(#(star hP G ε hU V)) : ℝ) (↑(#(star hP G ε hV U)) : ℝ) / HPow.hPow (α := ℝ) 16 #P.parts *
      (9 / 16) *
    HPow.hPow (β := ℕ) ε 2
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
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 (β := ℕ) ε 4 / 3 ≤
    HMul.hMul (α := ℝ) (↑(#(star hP G ε hU V)) : ℝ) (↑(#(star hP G ε hV U)) : ℝ) / HPow.hPow (α := ℝ) 16 #P.parts *
        (9 / 16) *
      HPow.hPow (β := ℕ) ε 2
have Ul : 4 / 5 * ε ≤ (↑(#(star hP G ε hU V)) : ℝ) / HPow.hPow (α := ℝ) 4 #P.parts
Tactic: have Ul : 4 / 5 * ε ≤ #(star hP G ε hU V) / _ :=
        eps_le_card_star_div hPα hPε hε₁ hU hV hUVne hUV
-- 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
Ul : 4 / 5 * ε ≤ (↑(#(star hP G ε hU V)) : ℝ) / HPow.hPow (α := ℝ) 4 #P.parts
⊢ HPow.hPow (β := ℕ) ε 4 / 3 ≤
    HMul.hMul (α := ℝ) (↑(#(star hP G ε hU V)) : ℝ) (↑(#(star hP G ε hV U)) : ℝ) / HPow.hPow (α := ℝ) 16 #P.parts *
        (9 / 16) *
      HPow.hPow (β := ℕ) ε 2
have Vl : 4 / 5 * ε ≤ (↑(#(star hP G ε hV U)) : ℝ) / HPow.hPow (α := ℝ) 4 #P.parts
Tactic: have Vl : 4 / 5 * ε ≤ #(star hP G ε hV U) / _ :=
        eps_le_card_star_div hPα hPε hε₁ hV hU hUVne.symm fun h => hUV h.symm
-- 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
⊢ HPow.hPow (β := ℕ) ε 4 / 3 ≤
    HMul.hMul (α := ℝ) (↑(#(star hP G ε hU V)) : ℝ) (↑(#(star hP G ε hV U)) : ℝ) / HPow.hPow (α := ℝ) 16 #P.parts *
        (9 / 16) *
      HPow.hPow (β := ℕ) ε 2
have bc : 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: rw [show (16 : ℝ) = ↑4 ^ 2 by norm_num, pow_right_comm, sq ((4 : ℝ) ^ _), ←
        _root_.div_mul_div_comm, mul_assoc]
-- 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
⊢ 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
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
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
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
⊢ 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)
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
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 < ε
⊢ 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)
have 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)
Tactic: have UVl := mul_le_mul Ul Vl (by 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
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)
⊢ 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)
have bc₁ : 0 ≤ (↑(#(star hP G ε hU V)) : ℝ) / HPow.hPow (α := ℝ) 4 #P.parts
Tactic: have UVl := mul_le_mul Ul Vl (by 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
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 ≤ (↑(#(star hP G ε hU V)) : ℝ) / HPow.hPow (α := ℝ) 4 #P.parts
have bc : LE.le (α := ℝ) 0 (↑(#(star hP G ε hU V)) : ℝ)
Tactic: apply div_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
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)) : ℝ)
⊢ 0 ≤ (↑(#(star hP G ε hU V)) : ℝ) / HPow.hPow (α := ℝ) 4 #P.parts
have bc₁ : 0 ≤ HPow.hPow (α := ℝ) 4 #P.parts
Tactic: apply div_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
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)
have bc : HPow.hPow (β := ℕ) ε 4 / 3 ≤ 4 / 5 * ε * (4 / 5 * ε) * (9 / HPow.hPow (α := ℝ) (β := ℕ) 4 2 * HPow.hPow (β := ℕ) ε 2)
Tactic: refine le_trans ?_ (mul_le_mul_of_nonneg_right UVl ?_)
-- 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)
bc :
  HPow.hPow (β := ℕ) ε 4 / 3 ≤ 4 / 5 * ε * (4 / 5 * ε) * (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)
have bc₁ : 0 ≤ 9 / HPow.hPow (α := ℝ) (β := ℕ) 4 2 * HPow.hPow (β := ℕ) ε 2
Tactic: refine le_trans ?_ (mul_le_mul_of_nonneg_right UVl ?_)
-- 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)
⊢ HPow.hPow (β := ℕ) ε 4 / 3 ≤ 4 / 5 * ε * (4 / 5 * ε) * (9 / HPow.hPow (α := ℝ) (β := ℕ) 4 2 * HPow.hPow (β := ℕ) ε 2)
have bc : HPow.hPow (β := ℕ) ε 4 / 3 ≤ 4 / 5 * ε * (4 / 5 * ε) * (9 / 16 * HPow.hPow (β := ℕ) ε 2)
Tactic: 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
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 ≤ 4 / 5 * ε * (4 / 5 * ε) * (9 / 16 * HPow.hPow (β := ℕ) ε 2)
have nlinarith : 4 / 5 * ε * (4 / 5 * ε) * (9 / 16 * HPow.hPow (β := ℕ) ε 2) < HPow.hPow (β := ℕ) ε 4 / 3 → 5 / 5 = 1
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)
nlinarith : 4 / 5 * ε * (4 / 5 * ε) * (9 / 16 * HPow.hPow (β := ℕ) ε 2) < HPow.hPow (β := ℕ) ε 4 / 3 → 5 / 5 = 1
⊢ 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 → HMul.hMul (α := ℝ) 1 5 = 5
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)
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
⊢ 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 → HMul.hMul (α := ℝ) 5 1 = 5
Tactic: nlinarith