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
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
hm : 0 ≤ HSub.hSub (α := ℝ) 1 (↑m : ℝ)⁻¹
hε : 0 ≤ 1 - ε / 10
hε₀ : 0 < ε
⊢ 4 / 5 * ε ≤ (↑(#(star hP G ε hU V)) : ℝ) / HPow.hPow (α := ℝ) 4 #P.parts
have ε₁ : 4 / 5 * ε = (1 - 1 / 10) * HSub.hSub (α := ℝ) 1 9⁻¹ * ε
Tactic: calc
    4 / 5 * ε = (1 - 1 / 10) * (1 - 9⁻¹) * ε := by norm_num
    _ ≤ (1 - ε / 10) * (1 - (↑m)⁻¹) * (#(G.nonuniformWitness ε U V) / #U) := by
        gcongr
        exacts [mod_cast (show 9 ≤ 100 by simp).trans (hundred_le_m hPα hPε hε₁),
          (le_div_iff₀' <| cast_pos.2 (P.nonempty_of_mem_parts hU).card_pos).2 <|
           G.le_card_nonuniformWitness hunif]
    _ = (1 - ε / 10) * #(G.nonuniformWitness ε U V) * ((1 - (↑m)⁻¹) / #U) := by
      rw [mul_assoc, mul_assoc, mul_div_left_comm]
    _ ≤ #((star hP G ε hU V).biUnion id) * ((1 - (↑m)⁻¹) / #U) := by
      gcongr
      exact one_sub_eps_mul_card_nonuniformWitness_le_card_star hV hUV hunif hPε hε₁
    _ ≤ #(star hP G ε hU V) * (m + 1) * ((1 - (↑m)⁻¹) / #U) := by
      gcongr
      exact card_biUnion_star_le_m_add_one_card_star_mul
    _ ≤ #(star hP G ε hU V) * (m + ↑1) * ((↑1 - (↑m)⁻¹) / (↑4 ^ #P.parts * m)) := by
      gcongr
      · sz_positivity
      · exact pow_mul_m_le_card_part hP hU
    _ ≤ #(star hP G ε hU V) / ↑4 ^ #P.parts := by
      rw [mul_assoc, mul_comm ((4 : ℝ) ^ #P.parts), ← div_div, ← mul_div_assoc, ← mul_comm_div]
      refine mul_le_of_le_one_right (by positivity) ?_
      have hm : (0 : ℝ) < m := by sz_positivity
      rw [mul_div_assoc', div_le_one hm, ← one_div, one_sub_div hm.ne', mul_div_assoc',
        div_le_iff₀ hm]
      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
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
hm : 0 ≤ HSub.hSub (α := ℝ) 1 (↑m : ℝ)⁻¹
hε : 0 ≤ 1 - ε / 10
hε₀ : 0 < ε
ε₁ : 4 / 5 * ε = (1 - 1 / 10) * HSub.hSub (α := ℝ) 1 9⁻¹ * ε
⊢ 4 / 5 * ε ≤ (↑(#(star hP G ε hU V)) : ℝ) / HPow.hPow (α := ℝ) 4 #P.parts
have ε₂ : (1 - 1 / 10) * HSub.hSub (α := ℝ) 1 9⁻¹ * ε ≤
  (1 - ε / 10) * HSub.hSub (α := ℝ) 1 (↑m : ℝ)⁻¹ * HDiv.hDiv (α := ℝ) (↑(#(G.nonuniformWitness ε U V)) : ℝ) (↑(#U) : ℝ)
Tactic: calc
    4 / 5 * ε = (1 - 1 / 10) * (1 - 9⁻¹) * ε := by norm_num
    _ ≤ (1 - ε / 10) * (1 - (↑m)⁻¹) * (#(G.nonuniformWitness ε U V) / #U) := by
        gcongr
        exacts [mod_cast (show 9 ≤ 100 by simp).trans (hundred_le_m hPα hPε hε₁),
          (le_div_iff₀' <| cast_pos.2 (P.nonempty_of_mem_parts hU).card_pos).2 <|
           G.le_card_nonuniformWitness hunif]
    _ = (1 - ε / 10) * #(G.nonuniformWitness ε U V) * ((1 - (↑m)⁻¹) / #U) := by
      rw [mul_assoc, mul_assoc, mul_div_left_comm]
    _ ≤ #((star hP G ε hU V).biUnion id) * ((1 - (↑m)⁻¹) / #U) := by
      gcongr
      exact one_sub_eps_mul_card_nonuniformWitness_le_card_star hV hUV hunif hPε hε₁
    _ ≤ #(star hP G ε hU V) * (m + 1) * ((1 - (↑m)⁻¹) / #U) := by
      gcongr
      exact card_biUnion_star_le_m_add_one_card_star_mul
    _ ≤ #(star hP G ε hU V) * (m + ↑1) * ((↑1 - (↑m)⁻¹) / (↑4 ^ #P.parts * m)) := by
      gcongr
      · sz_positivity
      · exact pow_mul_m_le_card_part hP hU
    _ ≤ #(star hP G ε hU V) / ↑4 ^ #P.parts := by
      rw [mul_assoc, mul_comm ((4 : ℝ) ^ #P.parts), ← div_div, ← mul_div_assoc, ← mul_comm_div]
      refine mul_le_of_le_one_right (by positivity) ?_
      have hm : (0 : ℝ) < m := by sz_positivity
      rw [mul_div_assoc', div_le_one hm, ← one_div, one_sub_div hm.ne', mul_div_assoc',
        div_le_iff₀ hm]
      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
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
hm : 0 ≤ HSub.hSub (α := ℝ) 1 (↑m : ℝ)⁻¹
hε : 0 ≤ 1 - ε / 10
hε₀ : 0 < ε
ε₁ : 4 / 5 * ε = (1 - 1 / 10) * HSub.hSub (α := ℝ) 1 9⁻¹ * ε
ε₂ :
  (1 - 1 / 10) * HSub.hSub (α := ℝ) 1 9⁻¹ * ε ≤
    (1 - ε / 10) * HSub.hSub (α := ℝ) 1 (↑m : ℝ)⁻¹ *
      HDiv.hDiv (α := ℝ) (↑(#(G.nonuniformWitness ε U V)) : ℝ) (↑(#U) : ℝ)
⊢ 4 / 5 * ε ≤ (↑(#(star hP G ε hU V)) : ℝ) / HPow.hPow (α := ℝ) 4 #P.parts
have ε₃ : (1 - ε / 10) * HSub.hSub (α := ℝ) 1 (↑m : ℝ)⁻¹ * HDiv.hDiv (α := ℝ) (↑(#(G.nonuniformWitness ε U V)) : ℝ) (↑(#U) : ℝ) =
  (1 - ε / 10) * (↑(#(G.nonuniformWitness ε U V)) : ℝ) * (HSub.hSub (α := ℝ) 1 (↑m : ℝ)⁻¹ / (↑(#U) : ℝ))
Tactic: calc
    4 / 5 * ε = (1 - 1 / 10) * (1 - 9⁻¹) * ε := by norm_num
    _ ≤ (1 - ε / 10) * (1 - (↑m)⁻¹) * (#(G.nonuniformWitness ε U V) / #U) := by
        gcongr
        exacts [mod_cast (show 9 ≤ 100 by simp).trans (hundred_le_m hPα hPε hε₁),
          (le_div_iff₀' <| cast_pos.2 (P.nonempty_of_mem_parts hU).card_pos).2 <|
           G.le_card_nonuniformWitness hunif]
    _ = (1 - ε / 10) * #(G.nonuniformWitness ε U V) * ((1 - (↑m)⁻¹) / #U) := by
      rw [mul_assoc, mul_assoc, mul_div_left_comm]
    _ ≤ #((star hP G ε hU V).biUnion id) * ((1 - (↑m)⁻¹) / #U) := by
      gcongr
      exact one_sub_eps_mul_card_nonuniformWitness_le_card_star hV hUV hunif hPε hε₁
    _ ≤ #(star hP G ε hU V) * (m + 1) * ((1 - (↑m)⁻¹) / #U) := by
      gcongr
      exact card_biUnion_star_le_m_add_one_card_star_mul
    _ ≤ #(star hP G ε hU V) * (m + ↑1) * ((↑1 - (↑m)⁻¹) / (↑4 ^ #P.parts * m)) := by
      gcongr
      · sz_positivity
      · exact pow_mul_m_le_card_part hP hU
    _ ≤ #(star hP G ε hU V) / ↑4 ^ #P.parts := by
      rw [mul_assoc, mul_comm ((4 : ℝ) ^ #P.parts), ← div_div, ← mul_div_assoc, ← mul_comm_div]
      refine mul_le_of_le_one_right (by positivity) ?_
      have hm : (0 : ℝ) < m := by sz_positivity
      rw [mul_div_assoc', div_le_one hm, ← one_div, one_sub_div hm.ne', mul_div_assoc',
        div_le_iff₀ hm]
      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
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
hm : 0 ≤ HSub.hSub (α := ℝ) 1 (↑m : ℝ)⁻¹
hε : 0 ≤ 1 - ε / 10
hε₀ : 0 < ε
ε₁ : 4 / 5 * ε = (1 - 1 / 10) * HSub.hSub (α := ℝ) 1 9⁻¹ * ε
ε₂ :
  (1 - 1 / 10) * HSub.hSub (α := ℝ) 1 9⁻¹ * ε ≤
    (1 - ε / 10) * HSub.hSub (α := ℝ) 1 (↑m : ℝ)⁻¹ *
      HDiv.hDiv (α := ℝ) (↑(#(G.nonuniformWitness ε U V)) : ℝ) (↑(#U) : ℝ)
ε₃ :
  (1 - ε / 10) * HSub.hSub (α := ℝ) 1 (↑m : ℝ)⁻¹ *
      HDiv.hDiv (α := ℝ) (↑(#(G.nonuniformWitness ε U V)) : ℝ) (↑(#U) : ℝ) =
    (1 - ε / 10) * (↑(#(G.nonuniformWitness ε U V)) : ℝ) * (HSub.hSub (α := ℝ) 1 (↑m : ℝ)⁻¹ / (↑(#U) : ℝ))
⊢ 4 / 5 * ε ≤ (↑(#(star hP G ε hU V)) : ℝ) / HPow.hPow (α := ℝ) 4 #P.parts
have ε₄ : (1 - ε / 10) * (↑(#(G.nonuniformWitness ε U V)) : ℝ) * (HSub.hSub (α := ℝ) 1 (↑m : ℝ)⁻¹ / (↑(#U) : ℝ)) ≤
  (↑(#((star hP G ε hU V).biUnion id)) : ℝ) * (HSub.hSub (α := ℝ) 1 (↑m : ℝ)⁻¹ / (↑(#U) : ℝ))
Tactic: calc
    4 / 5 * ε = (1 - 1 / 10) * (1 - 9⁻¹) * ε := by norm_num
    _ ≤ (1 - ε / 10) * (1 - (↑m)⁻¹) * (#(G.nonuniformWitness ε U V) / #U) := by
        gcongr
        exacts [mod_cast (show 9 ≤ 100 by simp).trans (hundred_le_m hPα hPε hε₁),
          (le_div_iff₀' <| cast_pos.2 (P.nonempty_of_mem_parts hU).card_pos).2 <|
           G.le_card_nonuniformWitness hunif]
    _ = (1 - ε / 10) * #(G.nonuniformWitness ε U V) * ((1 - (↑m)⁻¹) / #U) := by
      rw [mul_assoc, mul_assoc, mul_div_left_comm]
    _ ≤ #((star hP G ε hU V).biUnion id) * ((1 - (↑m)⁻¹) / #U) := by
      gcongr
      exact one_sub_eps_mul_card_nonuniformWitness_le_card_star hV hUV hunif hPε hε₁
    _ ≤ #(star hP G ε hU V) * (m + 1) * ((1 - (↑m)⁻¹) / #U) := by
      gcongr
      exact card_biUnion_star_le_m_add_one_card_star_mul
    _ ≤ #(star hP G ε hU V) * (m + ↑1) * ((↑1 - (↑m)⁻¹) / (↑4 ^ #P.parts * m)) := by
      gcongr
      · sz_positivity
      · exact pow_mul_m_le_card_part hP hU
    _ ≤ #(star hP G ε hU V) / ↑4 ^ #P.parts := by
      rw [mul_assoc, mul_comm ((4 : ℝ) ^ #P.parts), ← div_div, ← mul_div_assoc, ← mul_comm_div]
      refine mul_le_of_le_one_right (by positivity) ?_
      have hm : (0 : ℝ) < m := by sz_positivity
      rw [mul_div_assoc', div_le_one hm, ← one_div, one_sub_div hm.ne', mul_div_assoc',
        div_le_iff₀ hm]
      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
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
hm : 0 ≤ HSub.hSub (α := ℝ) 1 (↑m : ℝ)⁻¹
hε : 0 ≤ 1 - ε / 10
hε₀ : 0 < ε
ε₁ : 4 / 5 * ε = (1 - 1 / 10) * HSub.hSub (α := ℝ) 1 9⁻¹ * ε
ε₂ :
  (1 - 1 / 10) * HSub.hSub (α := ℝ) 1 9⁻¹ * ε ≤
    (1 - ε / 10) * HSub.hSub (α := ℝ) 1 (↑m : ℝ)⁻¹ *
      HDiv.hDiv (α := ℝ) (↑(#(G.nonuniformWitness ε U V)) : ℝ) (↑(#U) : ℝ)
ε₃ :
  (1 - ε / 10) * HSub.hSub (α := ℝ) 1 (↑m : ℝ)⁻¹ *
      HDiv.hDiv (α := ℝ) (↑(#(G.nonuniformWitness ε U V)) : ℝ) (↑(#U) : ℝ) =
    (1 - ε / 10) * (↑(#(G.nonuniformWitness ε U V)) : ℝ) * (HSub.hSub (α := ℝ) 1 (↑m : ℝ)⁻¹ / (↑(#U) : ℝ))
ε₄ :
  (1 - ε / 10) * (↑(#(G.nonuniformWitness ε U V)) : ℝ) * (HSub.hSub (α := ℝ) 1 (↑m : ℝ)⁻¹ / (↑(#U) : ℝ)) ≤
    (↑(#((star hP G ε hU V).biUnion id)) : ℝ) * (HSub.hSub (α := ℝ) 1 (↑m : ℝ)⁻¹ / (↑(#U) : ℝ))
⊢ 4 / 5 * ε ≤ (↑(#(star hP G ε hU V)) : ℝ) / HPow.hPow (α := ℝ) 4 #P.parts
have ε₅ : (↑(#((star hP G ε hU V).biUnion id)) : ℝ) * (HSub.hSub (α := ℝ) 1 (↑m : ℝ)⁻¹ / (↑(#U) : ℝ)) ≤
  (↑(#(star hP G ε hU V)) : ℝ) * HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 * (HSub.hSub (α := ℝ) 1 (↑m : ℝ)⁻¹ / (↑(#U) : ℝ))
Tactic: calc
    4 / 5 * ε = (1 - 1 / 10) * (1 - 9⁻¹) * ε := by norm_num
    _ ≤ (1 - ε / 10) * (1 - (↑m)⁻¹) * (#(G.nonuniformWitness ε U V) / #U) := by
        gcongr
        exacts [mod_cast (show 9 ≤ 100 by simp).trans (hundred_le_m hPα hPε hε₁),
          (le_div_iff₀' <| cast_pos.2 (P.nonempty_of_mem_parts hU).card_pos).2 <|
           G.le_card_nonuniformWitness hunif]
    _ = (1 - ε / 10) * #(G.nonuniformWitness ε U V) * ((1 - (↑m)⁻¹) / #U) := by
      rw [mul_assoc, mul_assoc, mul_div_left_comm]
    _ ≤ #((star hP G ε hU V).biUnion id) * ((1 - (↑m)⁻¹) / #U) := by
      gcongr
      exact one_sub_eps_mul_card_nonuniformWitness_le_card_star hV hUV hunif hPε hε₁
    _ ≤ #(star hP G ε hU V) * (m + 1) * ((1 - (↑m)⁻¹) / #U) := by
      gcongr
      exact card_biUnion_star_le_m_add_one_card_star_mul
    _ ≤ #(star hP G ε hU V) * (m + ↑1) * ((↑1 - (↑m)⁻¹) / (↑4 ^ #P.parts * m)) := by
      gcongr
      · sz_positivity
      · exact pow_mul_m_le_card_part hP hU
    _ ≤ #(star hP G ε hU V) / ↑4 ^ #P.parts := by
      rw [mul_assoc, mul_comm ((4 : ℝ) ^ #P.parts), ← div_div, ← mul_div_assoc, ← mul_comm_div]
      refine mul_le_of_le_one_right (by positivity) ?_
      have hm : (0 : ℝ) < m := by sz_positivity
      rw [mul_div_assoc', div_le_one hm, ← one_div, one_sub_div hm.ne', mul_div_assoc',
        div_le_iff₀ hm]
      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
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
hm : 0 ≤ HSub.hSub (α := ℝ) 1 (↑m : ℝ)⁻¹
hε : 0 ≤ 1 - ε / 10
hε₀ : 0 < ε
ε₁ : 4 / 5 * ε = (1 - 1 / 10) * HSub.hSub (α := ℝ) 1 9⁻¹ * ε
ε₂ :
  (1 - 1 / 10) * HSub.hSub (α := ℝ) 1 9⁻¹ * ε ≤
    (1 - ε / 10) * HSub.hSub (α := ℝ) 1 (↑m : ℝ)⁻¹ *
      HDiv.hDiv (α := ℝ) (↑(#(G.nonuniformWitness ε U V)) : ℝ) (↑(#U) : ℝ)
ε₃ :
  (1 - ε / 10) * HSub.hSub (α := ℝ) 1 (↑m : ℝ)⁻¹ *
      HDiv.hDiv (α := ℝ) (↑(#(G.nonuniformWitness ε U V)) : ℝ) (↑(#U) : ℝ) =
    (1 - ε / 10) * (↑(#(G.nonuniformWitness ε U V)) : ℝ) * (HSub.hSub (α := ℝ) 1 (↑m : ℝ)⁻¹ / (↑(#U) : ℝ))
ε₄ :
  (1 - ε / 10) * (↑(#(G.nonuniformWitness ε U V)) : ℝ) * (HSub.hSub (α := ℝ) 1 (↑m : ℝ)⁻¹ / (↑(#U) : ℝ)) ≤
    (↑(#((star hP G ε hU V).biUnion id)) : ℝ) * (HSub.hSub (α := ℝ) 1 (↑m : ℝ)⁻¹ / (↑(#U) : ℝ))
ε₅ :
  (↑(#((star hP G ε hU V).biUnion id)) : ℝ) * (HSub.hSub (α := ℝ) 1 (↑m : ℝ)⁻¹ / (↑(#U) : ℝ)) ≤
    (↑(#(star hP G ε hU V)) : ℝ) * HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 * (HSub.hSub (α := ℝ) 1 (↑m : ℝ)⁻¹ / (↑(#U) : ℝ))
⊢ 4 / 5 * ε ≤ (↑(#(star hP G ε hU V)) : ℝ) / HPow.hPow (α := ℝ) 4 #P.parts
have ε₆ : (↑(#(star hP G ε hU V)) : ℝ) * HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 * (HSub.hSub (α := ℝ) 1 (↑m : ℝ)⁻¹ / (↑(#U) : ℝ)) ≤
  (↑(#(star hP G ε hU V)) : ℝ) * HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 *
    (HSub.hSub (α := ℝ) 1 (↑m : ℝ)⁻¹ / (HPow.hPow (α := ℝ) 4 #P.parts * (↑m : ℝ)))
Tactic: calc
    4 / 5 * ε = (1 - 1 / 10) * (1 - 9⁻¹) * ε := by norm_num
    _ ≤ (1 - ε / 10) * (1 - (↑m)⁻¹) * (#(G.nonuniformWitness ε U V) / #U) := by
        gcongr
        exacts [mod_cast (show 9 ≤ 100 by simp).trans (hundred_le_m hPα hPε hε₁),
          (le_div_iff₀' <| cast_pos.2 (P.nonempty_of_mem_parts hU).card_pos).2 <|
           G.le_card_nonuniformWitness hunif]
    _ = (1 - ε / 10) * #(G.nonuniformWitness ε U V) * ((1 - (↑m)⁻¹) / #U) := by
      rw [mul_assoc, mul_assoc, mul_div_left_comm]
    _ ≤ #((star hP G ε hU V).biUnion id) * ((1 - (↑m)⁻¹) / #U) := by
      gcongr
      exact one_sub_eps_mul_card_nonuniformWitness_le_card_star hV hUV hunif hPε hε₁
    _ ≤ #(star hP G ε hU V) * (m + 1) * ((1 - (↑m)⁻¹) / #U) := by
      gcongr
      exact card_biUnion_star_le_m_add_one_card_star_mul
    _ ≤ #(star hP G ε hU V) * (m + ↑1) * ((↑1 - (↑m)⁻¹) / (↑4 ^ #P.parts * m)) := by
      gcongr
      · sz_positivity
      · exact pow_mul_m_le_card_part hP hU
    _ ≤ #(star hP G ε hU V) / ↑4 ^ #P.parts := by
      rw [mul_assoc, mul_comm ((4 : ℝ) ^ #P.parts), ← div_div, ← mul_div_assoc, ← mul_comm_div]
      refine mul_le_of_le_one_right (by positivity) ?_
      have hm : (0 : ℝ) < m := by sz_positivity
      rw [mul_div_assoc', div_le_one hm, ← one_div, one_sub_div hm.ne', mul_div_assoc',
        div_le_iff₀ hm]
      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
⊢ 3 / 4 * ε ≤
    |(∑ 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)) : ℝ) -
        (∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, (↑(G.edgeDensity ab.1 ab.2) : ℝ)) /
          HPow.hPow (α := ℝ) 16 #P.parts|
have rw : 3 / 4 * ε ≤
  |(∑ 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)) : ℝ) -
      (∑ 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)|
Tactic: rw [show (16 : ℝ) = ↑4 ^ 2 by norm_num, pow_right_comm, sq ((4 : ℝ) ^ _)]
-- 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) : ℝ)
⊢ 3 / 4 * ε ≤ |p - q|
have hrs : |r - s| ≤ ε / 5
Tactic: have hrs : |r - s| ≤ ε / 5 := abs_density_star_sub_density_le_eps hPε hε₁ 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
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
⊢ 3 / 4 * ε ≤ |p - q|
have hst : ε ≤ |s - t|
Tactic: have hst : ε ≤ |s - t| := by
    -- After https://github.com/leanprover/lean4/pull/2734, we need to do the zeta reduction before `mod_cast`.
    unfold s t
    exact mod_cast G.nonuniformWitness_spec 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
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|
⊢ 3 / 4 * ε ≤ |p - q|
have hpr : |p - r| ≤ HPow.hPow (β := ℕ) ε 5 / 49
Tactic: have hpr : |p - r| ≤ ε ^ 5 / 49 :=
    average_density_near_total_density hPα hPε hε₁ star_subset_chunk star_subset_chunk
-- 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
⊢ |q - t| ≤ HPow.hPow (β := ℕ) ε 5 / 49
have this : |(∑ 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) : ℝ) -
      (↑(G.edgeDensity ((chunk hP G ε hU).parts.biUnion id) ((chunk hP G ε hV).parts.biUnion id)) : ℝ)| ≤
  HPow.hPow (β := ℕ) ε 5 / 49
Tactic: have := average_density_near_total_density hPα hPε hε₁
      (Subset.refl (chunk hP G ε hU).parts) (Subset.refl (chunk hP G ε hV).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
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
⊢ 3 / 4 * ε ≤ |p - q|
have hqt : |q - t| ≤ HPow.hPow (β := ℕ) ε 5 / 49
Tactic: have hqt : |q - t| ≤ ε ^ 5 / 49 := by
    have := average_density_near_total_density hPα hPε hε₁
      (Subset.refl (chunk hP G ε hU).parts) (Subset.refl (chunk hP G ε hV).parts)
    simpa [← sup_eq_biUnion, sup_parts, card_chunk (m_pos hPα).ne']