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
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) : ℝ)) /
      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
have hab : HDiv.hDiv (α := ℚ) (∑ i ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, G.edgeDensity i.1 i.2)
    (↑(HMul.hMul (α := ℕ) 4 4 ^ #P.parts) : ℚ) ≤
  HDiv.hDiv (α := ℚ) (∑ i ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, G.edgeDensity i.1 i.2)
    (↑(HMul.hMul (α := ℕ) 4 4 ^ #P.parts) : ℚ)
Tactic: norm_cast
-- 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 - 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 _ : 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: calc
    _ = G.edgeDensity U V ^ 2 - 1 * ε ^ 5 / 25 + 0 ^ 10 / 2500 := by ring
    _ ≤ G.edgeDensity U V ^ 2 - G.edgeDensity U V * ε ^ 5 / 25 + ε ^ 10 / 2500 := by
      gcongr; exact mod_cast G.edgeDensity_le_one ..
    _ = (G.edgeDensity U V - ε ^ 5 / 50) ^ 2 := by ring
    _ ≤ _ := by
      gcongr
      have rflU := Subset.refl (chunk hP G ε hU).parts
      have rflV := Subset.refl (chunk hP G ε hV).parts
      refine (le_trans ?_ <| density_sub_eps_le_sum_density_div_card hPα hPε rflU rflV).trans ?_
      · rw [biUnion_parts, biUnion_parts]
      · rw [card_chunk (m_pos hPα).ne', card_chunk (m_pos hPα).ne', ← cast_mul, ← mul_pow, cast_pow]
        norm_cast
-- 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 - HPow.hPow (β := ℕ) ε 5 / 25 =
    HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity U V) : ℝ) 2 - 1 * HPow.hPow (β := ℕ) ε 5 / 25 +
      HPow.hPow (α := ℝ) (β := ℕ) 0 10 / 2500
⊢ 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 _₁ : 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: calc
    _ = G.edgeDensity U V ^ 2 - 1 * ε ^ 5 / 25 + 0 ^ 10 / 2500 := by ring
    _ ≤ G.edgeDensity U V ^ 2 - G.edgeDensity U V * ε ^ 5 / 25 + ε ^ 10 / 2500 := by
      gcongr; exact mod_cast G.edgeDensity_le_one ..
    _ = (G.edgeDensity U V - ε ^ 5 / 50) ^ 2 := by ring
    _ ≤ _ := by
      gcongr
      have rflU := Subset.refl (chunk hP G ε hU).parts
      have rflV := Subset.refl (chunk hP G ε hV).parts
      refine (le_trans ?_ <| density_sub_eps_le_sum_density_div_card hPα hPε rflU rflV).trans ?_
      · rw [biUnion_parts, biUnion_parts]
      · rw [card_chunk (m_pos hPα).ne', card_chunk (m_pos hPα).ne', ← cast_mul, ← mul_pow, cast_pow]
        norm_cast
-- 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 - HPow.hPow (β := ℕ) ε 5 / 25 =
    HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity U V) : ℝ) 2 - 1 * HPow.hPow (β := ℕ) ε 5 / 25 +
      HPow.hPow (α := ℝ) (β := ℕ) 0 10 / 2500
_₁ :
  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
⊢ 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 _₂ : HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity U V) : ℝ) 2 - (↑(G.edgeDensity U V) : ℝ) * HPow.hPow (β := ℕ) ε 5 / 25 +
    HPow.hPow (β := ℕ) ε 10 / 2500 =
  HPow.hPow (β := ℕ) ((↑(G.edgeDensity U V) : ℝ) - HPow.hPow (β := ℕ) ε 5 / 50) 2
Tactic: calc
    _ = G.edgeDensity U V ^ 2 - 1 * ε ^ 5 / 25 + 0 ^ 10 / 2500 := by ring
    _ ≤ G.edgeDensity U V ^ 2 - G.edgeDensity U V * ε ^ 5 / 25 + ε ^ 10 / 2500 := by
      gcongr; exact mod_cast G.edgeDensity_le_one ..
    _ = (G.edgeDensity U V - ε ^ 5 / 50) ^ 2 := by ring
    _ ≤ _ := by
      gcongr
      have rflU := Subset.refl (chunk hP G ε hU).parts
      have rflV := Subset.refl (chunk hP G ε hV).parts
      refine (le_trans ?_ <| density_sub_eps_le_sum_density_div_card hPα hPε rflU rflV).trans ?_
      · rw [biUnion_parts, biUnion_parts]
      · rw [card_chunk (m_pos hPα).ne', card_chunk (m_pos hPα).ne', ← cast_mul, ← mul_pow, cast_pow]
        norm_cast
-- 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 - HPow.hPow (β := ℕ) ε 5 / 25 =
    HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity U V) : ℝ) 2 - 1 * HPow.hPow (β := ℕ) ε 5 / 25 +
      HPow.hPow (α := ℝ) (β := ℕ) 0 10 / 2500
_₁ :
  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
_₂ :
  HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity U V) : ℝ) 2 - (↑(G.edgeDensity U V) : ℝ) * HPow.hPow (β := ℕ) ε 5 / 25 +
      HPow.hPow (β := ℕ) ε 10 / 2500 =
    HPow.hPow (β := ℕ) ((↑(G.edgeDensity U V) : ℝ) - HPow.hPow (β := ℕ) ε 5 / 50) 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 _₃ : 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
Tactic: calc
    _ = G.edgeDensity U V ^ 2 - 1 * ε ^ 5 / 25 + 0 ^ 10 / 2500 := by ring
    _ ≤ G.edgeDensity U V ^ 2 - G.edgeDensity U V * ε ^ 5 / 25 + ε ^ 10 / 2500 := by
      gcongr; exact mod_cast G.edgeDensity_le_one ..
    _ = (G.edgeDensity U V - ε ^ 5 / 50) ^ 2 := by ring
    _ ≤ _ := by
      gcongr
      have rflU := Subset.refl (chunk hP G ε hU).parts
      have rflV := Subset.refl (chunk hP G ε hV).parts
      refine (le_trans ?_ <| density_sub_eps_le_sum_density_div_card hPα hPε rflU rflV).trans ?_
      · rw [biUnion_parts, biUnion_parts]
      · rw [card_chunk (m_pos hPα).ne', card_chunk (m_pos hPα).ne', ← cast_mul, ← mul_pow, cast_pow]
        norm_cast
-- 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 α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hε₁ : ε ≤ 1
hU : U ∈ P.parts
hV : V ∈ P.parts
hUV' : U ≠ V
hUV : ¬G.IsUniform ε U V
⊢ 0 ≤ ε / 10
have sz_positivity : 0 < ε → 0 ≤ ε / 10
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 α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hε₁ : ε ≤ 1
hU : U ∈ P.parts
hV : V ∈ P.parts
hUV' : U ≠ V
hUV : ¬G.IsUniform ε U V
⊢ |HSub.hSub (α := ℝ) (↑(G.edgeDensity ((star hP G ε hU V).biUnion id) ((star hP G ε hV U).biUnion id)) : ℝ)
        (↑(G.edgeDensity (G.nonuniformWitness ε U V) (G.nonuniformWitness ε V U)) : ℝ)| ≤
    ε / 5
have h : ε / 5 = 2 * (ε / 10)
Tactic: convert!
    abs_edgeDensity_sub_edgeDensity_le_two_mul G.Adj
      (biUnion_star_subset_nonuniformWitness hP G ε hU V)
      (biUnion_star_subset_nonuniformWitness hP G ε hV U) (by sz_positivity)
      (one_sub_eps_mul_card_nonuniformWitness_le_card_star hV hUV' hUV hPε hε₁)
      (one_sub_eps_mul_card_nonuniformWitness_le_card_star hU hUV'.symm (fun hVU => hUV hVU.symm)
        hPε hε₁) using 1
-- 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 α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hε₁ : ε ≤ 1
hU : U ∈ P.parts
hV : V ∈ P.parts
hUV' : U ≠ V
hUV : ¬G.IsUniform ε U V
⊢ ε / 5 = 2 * (ε / 10)
have linarith : ε / 5 < 2 * (ε / 10) → 5 / 5 = 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 α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hε₁ : ε ≤ 1
hU : U ∈ P.parts
hV : V ∈ P.parts
hUV' : U ≠ V
hUV : ¬G.IsUniform ε U V
linarith : ε / 5 < 2 * (ε / 10) → 5 / 5 = 1
⊢ ε / 5 = 2 * (ε / 10)
have linarith₁ : ε / 5 < 2 * (ε / 10) → HMul.hMul (α := ℝ) 2 5 = 10
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 α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hε₁ : ε ≤ 1
hU : U ∈ P.parts
hV : V ∈ P.parts
hUV' : U ≠ V
hUV : ¬G.IsUniform ε U V
linarith : ε / 5 < 2 * (ε / 10) → 5 / 5 = 1
linarith₁ : ε / 5 < 2 * (ε / 10) → HMul.hMul (α := ℝ) 2 5 = 10
⊢ ε / 5 = 2 * (ε / 10)
have linarith₂ : ε / 5 < 2 * (ε / 10) → 10 / 10 = 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 α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hε₁ : ε ≤ 1
hU : U ∈ P.parts
hV : V ∈ P.parts
hUV' : U ≠ V
hUV : ¬G.IsUniform ε U V
linarith : ε / 5 < 2 * (ε / 10) → 5 / 5 = 1
linarith₁ : ε / 5 < 2 * (ε / 10) → HMul.hMul (α := ℝ) 2 5 = 10
linarith₂ : ε / 5 < 2 * (ε / 10) → 10 / 10 = 1
⊢ ε / 5 = 2 * (ε / 10)
have linarith₃ : ε / 5 < 2 * (ε / 10) → HMul.hMul (α := ℝ) 1 10 = 10
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 α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hε₁ : ε ≤ 1
hU : U ∈ P.parts
hV : V ∈ P.parts
hUV' : U ≠ V
hUV : ¬G.IsUniform ε U V
linarith : ε / 5 < 2 * (ε / 10) → 5 / 5 = 1
linarith₁ : ε / 5 < 2 * (ε / 10) → HMul.hMul (α := ℝ) 2 5 = 10
linarith₂ : ε / 5 < 2 * (ε / 10) → 10 / 10 = 1
linarith₃ linarith₄ : ε / 5 < 2 * (ε / 10) → HMul.hMul (α := ℝ) 1 10 = 10
⊢ ε / 5 = 2 * (ε / 10)
have linarith₅ : ε / 5 < 2 * (ε / 10) → GT.gt (α := ℝ) 10 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 α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hε₁ : ε ≤ 1
hU : U ∈ P.parts
hV : V ∈ P.parts
hUV' : U ≠ V
hUV : ¬G.IsUniform ε U V
linarith : ε / 5 < 2 * (ε / 10) → 5 / 5 = 1
linarith₁ : ε / 5 < 2 * (ε / 10) → HMul.hMul (α := ℝ) 2 5 = 10
linarith₂ : ε / 5 < 2 * (ε / 10) → 10 / 10 = 1
linarith₃ linarith₄ : ε / 5 < 2 * (ε / 10) → HMul.hMul (α := ℝ) 1 10 = 10
linarith₅ : ε / 5 < 2 * (ε / 10) → GT.gt (α := ℝ) 10 0
⊢ ε / 5 = 2 * (ε / 10)
have linarith₆ : ε / 5 < 2 * (ε / 10) → 2 * ε - HMul.hMul (α := ℝ) 1 2 * (1 * ε) = 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 α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hε₁ : ε ≤ 1
hU : U ∈ P.parts
hV : V ∈ P.parts
hUV' : U ≠ V
hUV : ¬G.IsUniform ε U V
linarith : ε / 5 < 2 * (ε / 10) → 5 / 5 = 1
linarith₁ : ε / 5 < 2 * (ε / 10) → HMul.hMul (α := ℝ) 2 5 = 10
linarith₂ : ε / 5 < 2 * (ε / 10) → 10 / 10 = 1
linarith₃ linarith₄ : ε / 5 < 2 * (ε / 10) → HMul.hMul (α := ℝ) 1 10 = 10
linarith₅ : ε / 5 < 2 * (ε / 10) → GT.gt (α := ℝ) 10 0
linarith₆ : ε / 5 < 2 * (ε / 10) → 2 * ε - HMul.hMul (α := ℝ) 1 2 * (1 * ε) = 0
⊢ ε / 5 = 2 * (ε / 10)
have linarith₇ : 2 * (ε / 10) < ε / 5 → 10 / 10 = 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 α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hε₁ : ε ≤ 1
hU : U ∈ P.parts
hV : V ∈ P.parts
hUV' : U ≠ V
hUV : ¬G.IsUniform ε U V
linarith : ε / 5 < 2 * (ε / 10) → 5 / 5 = 1
linarith₁ : ε / 5 < 2 * (ε / 10) → HMul.hMul (α := ℝ) 2 5 = 10
linarith₂ : ε / 5 < 2 * (ε / 10) → 10 / 10 = 1
linarith₃ linarith₄ : ε / 5 < 2 * (ε / 10) → HMul.hMul (α := ℝ) 1 10 = 10
linarith₅ : ε / 5 < 2 * (ε / 10) → GT.gt (α := ℝ) 10 0
linarith₆ : ε / 5 < 2 * (ε / 10) → 2 * ε - HMul.hMul (α := ℝ) 1 2 * (1 * ε) = 0
linarith₇ : 2 * (ε / 10) < ε / 5 → 10 / 10 = 1
⊢ ε / 5 = 2 * (ε / 10)
have linarith₈ : 2 * (ε / 10) < ε / 5 → HMul.hMul (α := ℝ) 1 10 = 10
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 α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hε₁ : ε ≤ 1
hU : U ∈ P.parts
hV : V ∈ P.parts
hUV' : U ≠ V
hUV : ¬G.IsUniform ε U V
linarith : ε / 5 < 2 * (ε / 10) → 5 / 5 = 1
linarith₁ : ε / 5 < 2 * (ε / 10) → HMul.hMul (α := ℝ) 2 5 = 10
linarith₂ : ε / 5 < 2 * (ε / 10) → 10 / 10 = 1
linarith₃ linarith₄ : ε / 5 < 2 * (ε / 10) → HMul.hMul (α := ℝ) 1 10 = 10
linarith₅ : ε / 5 < 2 * (ε / 10) → GT.gt (α := ℝ) 10 0
linarith₆ : ε / 5 < 2 * (ε / 10) → 2 * ε - HMul.hMul (α := ℝ) 1 2 * (1 * ε) = 0
linarith₇ : 2 * (ε / 10) < ε / 5 → 10 / 10 = 1
linarith₈ linarith₉ : 2 * (ε / 10) < ε / 5 → HMul.hMul (α := ℝ) 1 10 = 10
⊢ ε / 5 = 2 * (ε / 10)
have linarith₁₀ : 2 * (ε / 10) < ε / 5 → 5 / 5 = 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 α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hε₁ : ε ≤ 1
hU : U ∈ P.parts
hV : V ∈ P.parts
hUV' : U ≠ V
hUV : ¬G.IsUniform ε U V
linarith : ε / 5 < 2 * (ε / 10) → 5 / 5 = 1
linarith₁ : ε / 5 < 2 * (ε / 10) → HMul.hMul (α := ℝ) 2 5 = 10
linarith₂ : ε / 5 < 2 * (ε / 10) → 10 / 10 = 1
linarith₃ linarith₄ : ε / 5 < 2 * (ε / 10) → HMul.hMul (α := ℝ) 1 10 = 10
linarith₅ : ε / 5 < 2 * (ε / 10) → GT.gt (α := ℝ) 10 0
linarith₆ : ε / 5 < 2 * (ε / 10) → 2 * ε - HMul.hMul (α := ℝ) 1 2 * (1 * ε) = 0
linarith₇ : 2 * (ε / 10) < ε / 5 → 10 / 10 = 1
linarith₈ linarith₉ : 2 * (ε / 10) < ε / 5 → HMul.hMul (α := ℝ) 1 10 = 10
linarith₁₀ : 2 * (ε / 10) < ε / 5 → 5 / 5 = 1
⊢ ε / 5 = 2 * (ε / 10)
have linarith₁₁ : 2 * (ε / 10) < ε / 5 → HMul.hMul (α := ℝ) 2 5 = 10
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 α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hε₁ : ε ≤ 1
hU : U ∈ P.parts
hV : V ∈ P.parts
hUV' : U ≠ V
hUV : ¬G.IsUniform ε U V
linarith : ε / 5 < 2 * (ε / 10) → 5 / 5 = 1
linarith₁ : ε / 5 < 2 * (ε / 10) → HMul.hMul (α := ℝ) 2 5 = 10
linarith₂ : ε / 5 < 2 * (ε / 10) → 10 / 10 = 1
linarith₃ linarith₄ : ε / 5 < 2 * (ε / 10) → HMul.hMul (α := ℝ) 1 10 = 10
linarith₅ : ε / 5 < 2 * (ε / 10) → GT.gt (α := ℝ) 10 0
linarith₆ : ε / 5 < 2 * (ε / 10) → 2 * ε - HMul.hMul (α := ℝ) 1 2 * (1 * ε) = 0
linarith₇ : 2 * (ε / 10) < ε / 5 → 10 / 10 = 1
linarith₈ linarith₉ : 2 * (ε / 10) < ε / 5 → HMul.hMul (α := ℝ) 1 10 = 10
linarith₁₀ : 2 * (ε / 10) < ε / 5 → 5 / 5 = 1
linarith₁₁ : 2 * (ε / 10) < ε / 5 → HMul.hMul (α := ℝ) 2 5 = 10
⊢ ε / 5 = 2 * (ε / 10)
have linarith₁₂ : 2 * (ε / 10) < ε / 5 → GT.gt (α := ℝ) 10 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 α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hε₁ : ε ≤ 1
hU : U ∈ P.parts
hV : V ∈ P.parts
hUV' : U ≠ V
hUV : ¬G.IsUniform ε U V
linarith : ε / 5 < 2 * (ε / 10) → 5 / 5 = 1
linarith₁ : ε / 5 < 2 * (ε / 10) → HMul.hMul (α := ℝ) 2 5 = 10
linarith₂ : ε / 5 < 2 * (ε / 10) → 10 / 10 = 1
linarith₃ linarith₄ : ε / 5 < 2 * (ε / 10) → HMul.hMul (α := ℝ) 1 10 = 10
linarith₅ : ε / 5 < 2 * (ε / 10) → GT.gt (α := ℝ) 10 0
linarith₆ : ε / 5 < 2 * (ε / 10) → 2 * ε - HMul.hMul (α := ℝ) 1 2 * (1 * ε) = 0
linarith₇ : 2 * (ε / 10) < ε / 5 → 10 / 10 = 1
linarith₈ linarith₉ : 2 * (ε / 10) < ε / 5 → HMul.hMul (α := ℝ) 1 10 = 10
linarith₁₀ : 2 * (ε / 10) < ε / 5 → 5 / 5 = 1
linarith₁₁ : 2 * (ε / 10) < ε / 5 → HMul.hMul (α := ℝ) 2 5 = 10
linarith₁₂ : 2 * (ε / 10) < ε / 5 → GT.gt (α := ℝ) 10 0
⊢ ε / 5 = 2 * (ε / 10)
have linarith₁₃ : 2 * (ε / 10) < ε / 5 → HMul.hMul (α := ℝ) 1 2 * (1 * ε) - 2 * ε = 0
Tactic: 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
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
⊢ 4 / 5 * ε ≤ (↑(#(star hP G ε hU V)) : ℝ) / HPow.hPow (α := ℝ) 4 #P.parts
have hm : 0 ≤ HSub.hSub (α := ℝ) 1 (↑m : ℝ)⁻¹
Tactic: have hm : (0 : ℝ) ≤ 1 - (↑m)⁻¹ := sub_nonneg_of_le (inv_le_one_of_one_le₀ <| one_le_m_coe hPα)
-- 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
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
hm : 0 ≤ HSub.hSub (α := ℝ) 1 (↑m : ℝ)⁻¹
⊢ 4 / 5 * ε ≤ (↑(#(star hP G ε hU V)) : ℝ) / HPow.hPow (α := ℝ) 4 #P.parts
have hε : 0 ≤ 1 - ε / 10
Tactic: have hε : 0 ≤ 1 - ε / 10 :=
    sub_nonneg_of_le (div_le_one_of_le₀ (hε₁.trans <| by simp) <| by 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
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
hm : 0 ≤ HSub.hSub (α := ℝ) 1 (↑m : ℝ)⁻¹
hε : 0 ≤ 1 - ε / 10
⊢ 0 < ε
have sz_positivity : 0 < m → 0 < ε
Tactic: sz_positivity