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 : Finset α
hU : U ∈ P.parts
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hε₁ : ε ≤ 1
hP₁ : 0 < #P.parts
rw :
  HPow.hPow (α := ℝ) 2 #P.parts * (HPow.hPow (α := ℝ) 2 #P.parts * (↑m : ℝ) / (↑(#U) : ℝ)) =
    HPow.hPow (α := ℝ) 2 #P.parts * HPow.hPow (α := ℝ) 2 #P.parts * (↑m : ℝ) / (↑(#U) : ℝ)
rw₁ :
  HPow.hPow (α := ℝ) 2 #P.parts * (HPow.hPow (α := ℝ) 2 #P.parts * (↑m : ℝ)) / (↑(#U) : ℝ) =
    HPow.hPow (α := ℝ) 2 #P.parts * HPow.hPow (α := ℝ) 2 #P.parts * (↑m : ℝ) / (↑(#U) : ℝ)
⊢ HPow.hPow (α := ℝ) 2 #P.parts * (HPow.hPow (α := ℝ) 2 #P.parts * (↑m : ℝ) / (↑(#U) : ℝ)) =
    HMul.hMul (α := ℝ) 2 2 ^ #P.parts * (↑m : ℝ) / (↑(#U) : ℝ)
have rw₂ : HPow.hPow (α := ℝ) 2 #P.parts * (HPow.hPow (α := ℝ) 2 #P.parts * (↑m : ℝ)) / (↑(#U) : ℝ) =
  HPow.hPow (α := ℝ) 2 #P.parts * (HPow.hPow (α := ℝ) 2 #P.parts * (↑m : ℝ)) / (↑(#U) : ℝ)
Tactic: rw [mul_pow, ← mul_div_assoc, 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 : Finset α
hU : U ∈ P.parts
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hε₁ : ε ≤ 1
hP₁ : 0 < #P.parts
⊢ 1 ≤ HPow.hPow (α := ℝ) 2 #P.parts * HPow.hPow (β := ℕ) ε 2 / 10
have refine : 1 ≤ HPow.hPow (β := ℕ) (HPow.hPow (α := ℝ) 2 #P.parts * HPow.hPow (β := ℕ) ε 2 / 10) 2
Tactic: refine (one_le_sq_iff₀ <| by positivity).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 : Finset α
hU : U ∈ P.parts
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hε₁ : ε ≤ 1
hP₁ : 0 < #P.parts
⊢ 1 ≤ HPow.hPow (β := ℕ) (HPow.hPow (α := ℝ) 2 #P.parts * HPow.hPow (β := ℕ) ε 2 / 10) 2
have rw : HPow.hPow (α := ℝ) (β := ℕ) 10 2 ≤ HPow.hPow (α := ℝ) (β := ℕ) 2 2 ^ #P.parts * ε ^ HMul.hMul (α := ℕ) 2 2
Tactic: rw [div_pow, mul_pow, pow_right_comm, ← pow_mul ε, one_le_div (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 : Finset α
hU : U ∈ P.parts
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hε₁ : ε ≤ 1
hP₁ : 0 < #P.parts
⊢ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 4
have hbc : HPow.hPow (β := ℕ) ε 5 ≤ HPow.hPow (β := ℕ) ε 4
Tactic: gcongr _ * ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
hP : P.IsEquipartition
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
U : Finset α
hU : U ∈ P.parts
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hε₁ : ε ≤ 1
hP₁ : 0 < #P.parts
⊢ 0 ≤ ε
have sz_positivity : 0 < ε → 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 : Finset α
hU : U ∈ P.parts
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hε₁ : ε ≤ 1
hP₁ : 0 < #P.parts
⊢ HPow.hPow (α := ℝ) (β := ℕ) 10 2 ≤ HPow.hPow (α := ℝ) (β := ℕ) 2 2 ^ #P.parts * ε ^ HMul.hMul (α := ℕ) 2 2
have by : HPow.hPow (α := ℝ) (β := ℕ) 10 2 = 100
Tactic: calc
          (↑10 ^ 2) = 100 := by norm_num
          _ ≤ ↑4 ^ #P.parts * ε ^ 5 := hPε
          _ ≤ ↑4 ^ #P.parts * ε ^ 4 := by
            gcongr _ * ?_
            exact pow_le_pow_of_le_one (by sz_positivity) hε₁ (by decide)
          _ = (↑2 ^ 2) ^ #P.parts * ε ^ (2 * 2) := 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 : Finset α
hU : U ∈ P.parts
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hε₁ : ε ≤ 1
hP₁ : 0 < #P.parts
by : HPow.hPow (α := ℝ) (β := ℕ) 10 2 = 100
⊢ HPow.hPow (α := ℝ) (β := ℕ) 10 2 ≤ HPow.hPow (α := ℝ) (β := ℕ) 2 2 ^ #P.parts * ε ^ HMul.hMul (α := ℕ) 2 2
have by₁ : HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 4
Tactic: calc
          (↑10 ^ 2) = 100 := by norm_num
          _ ≤ ↑4 ^ #P.parts * ε ^ 5 := hPε
          _ ≤ ↑4 ^ #P.parts * ε ^ 4 := by
            gcongr _ * ?_
            exact pow_le_pow_of_le_one (by sz_positivity) hε₁ (by decide)
          _ = (↑2 ^ 2) ^ #P.parts * ε ^ (2 * 2) := 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 : Finset α
hU : U ∈ P.parts
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hε₁ : ε ≤ 1
hP₁ : 0 < #P.parts
by : HPow.hPow (α := ℝ) (β := ℕ) 10 2 = 100
by₁ : HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 4
⊢ HPow.hPow (α := ℝ) (β := ℕ) 10 2 ≤ HPow.hPow (α := ℝ) (β := ℕ) 2 2 ^ #P.parts * ε ^ HMul.hMul (α := ℕ) 2 2
have by₂ : HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 4 =
  HPow.hPow (α := ℝ) (β := ℕ) 2 2 ^ #P.parts * ε ^ HMul.hMul (α := ℕ) 2 2
Tactic: calc
          (↑10 ^ 2) = 100 := by norm_num
          _ ≤ ↑4 ^ #P.parts * ε ^ 5 := hPε
          _ ≤ ↑4 ^ #P.parts * ε ^ 4 := by
            gcongr _ * ?_
            exact pow_le_pow_of_le_one (by sz_positivity) hε₁ (by decide)
          _ = (↑2 ^ 2) ^ #P.parts * ε ^ (2 * 2) := 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 : Finset α
hU : U ∈ P.parts
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hε₁ : ε ≤ 1
hP₁ : 0 < #P.parts
⊢ HPow.hPow (α := ℝ) 2 #P.parts * HPow.hPow (β := ℕ) ε 2 / 10 = HPow.hPow (α := ℝ) 2 #P.parts * (ε * (ε / 10))
have rw : HPow.hPow (α := ℝ) 2 #P.parts * (HPow.hPow (β := ℕ) ε 2 / 10) = HPow.hPow (α := ℝ) 2 #P.parts * (ε * (ε / 10))
Tactic: rw [mul_div_assoc, sq, mul_div_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 : Finset α
hU : U ∈ P.parts
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hε₁ : ε ≤ 1
hP₁ : 0 < #P.parts
rw : HPow.hPow (α := ℝ) 2 #P.parts * (HPow.hPow (β := ℕ) ε 2 / 10) = HPow.hPow (α := ℝ) 2 #P.parts * (ε * (ε / 10))
⊢ HPow.hPow (α := ℝ) 2 #P.parts * HPow.hPow (β := ℕ) ε 2 / 10 = HPow.hPow (α := ℝ) 2 #P.parts * (ε * (ε / 10))
have rw₁ : HPow.hPow (α := ℝ) 2 #P.parts * (ε * ε / 10) = HPow.hPow (α := ℝ) 2 #P.parts * (ε * (ε / 10))
Tactic: rw [mul_div_assoc, sq, mul_div_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 : Finset α
hU : U ∈ P.parts
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hε₁ : ε ≤ 1
hP₁ : 0 < #P.parts
rw : HPow.hPow (α := ℝ) 2 #P.parts * (HPow.hPow (β := ℕ) ε 2 / 10) = HPow.hPow (α := ℝ) 2 #P.parts * (ε * (ε / 10))
rw₁ : HPow.hPow (α := ℝ) 2 #P.parts * (ε * ε / 10) = HPow.hPow (α := ℝ) 2 #P.parts * (ε * (ε / 10))
⊢ HPow.hPow (α := ℝ) 2 #P.parts * HPow.hPow (β := ℕ) ε 2 / 10 = HPow.hPow (α := ℝ) 2 #P.parts * (ε * (ε / 10))
have rw₂ : HPow.hPow (α := ℝ) 2 #P.parts * (ε * (ε / 10)) = HPow.hPow (α := ℝ) 2 #P.parts * (ε * (ε / 10))
Tactic: rw [mul_div_assoc, sq, mul_div_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 : Finset α
hU : U ∈ P.parts
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hε₁ : ε ≤ 1
hP₁ : 0 < #P.parts
⊢ HPow.hPow (α := ℝ) 2 #P.parts * (HPow.hPow (α := ℝ) 2 #P.parts * (↑m : ℝ) / (↑(#U) : ℝ)) ≤
    HPow.hPow (α := ℝ) 2 #P.parts * (ε * (ε / 10))
have m : HPow.hPow (α := ℝ) 2 #P.parts * (HPow.hPow (α := ℝ) 2 #P.parts * (↑m : ℝ) / (↑(#U) : ℝ)) =
  HMul.hMul (α := ℝ) 2 2 ^ #P.parts * (↑m : ℝ) / (↑(#U) : ℝ)
Tactic: calc
      ↑2 ^ #P.parts * ((↑2 ^ #P.parts * m : ℝ) / #U) =
          ((2 : ℝ) * 2) ^ #P.parts * m / #U := by
        rw [mul_pow, ← mul_div_assoc, mul_assoc]
      _ = ↑4 ^ #P.parts * m / #U := by norm_num
      _ ≤ 1 := div_le_one_of_le₀ (pow_mul_m_le_card_part hP hU) (cast_nonneg _)
      _ ≤ ↑2 ^ #P.parts * ε ^ 2 / 10 := by
        refine (one_le_sq_iff₀ <| by positivity).1 ?_
        rw [div_pow, mul_pow, pow_right_comm, ← pow_mul ε, one_le_div (by positivity)]
        calc
          (↑10 ^ 2) = 100 := by norm_num
          _ ≤ ↑4 ^ #P.parts * ε ^ 5 := hPε
          _ ≤ ↑4 ^ #P.parts * ε ^ 4 := by
            gcongr _ * ?_
            exact pow_le_pow_of_le_one (by sz_positivity) hε₁ (by decide)
          _ = (↑2 ^ 2) ^ #P.parts * ε ^ (2 * 2) := by norm_num
      _ = ↑2 ^ #P.parts * (ε * (ε / 10)) := by rw [mul_div_assoc, sq, mul_div_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 : Finset α
hU : U ∈ P.parts
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hε₁ : ε ≤ 1
hP₁ : 0 < #P.parts
m :
  HPow.hPow (α := ℝ) 2 #P.parts * (HPow.hPow (α := ℝ) 2 #P.parts * (↑m : ℝ) / (↑(#U) : ℝ)) =
    HMul.hMul (α := ℝ) 2 2 ^ #P.parts * (↑m : ℝ) / (↑(#U) : ℝ)
⊢ HPow.hPow (α := ℝ) 2 #P.parts * (HPow.hPow (α := ℝ) 2 #P.parts * (↑m : ℝ) / (↑(#U) : ℝ)) ≤
    HPow.hPow (α := ℝ) 2 #P.parts * (ε * (ε / 10))
have m₁ : HMul.hMul (α := ℝ) 2 2 ^ #P.parts * (↑m : ℝ) / (↑(#U) : ℝ) = HPow.hPow (α := ℝ) 4 #P.parts * (↑m : ℝ) / (↑(#U) : ℝ)
Tactic: calc
      ↑2 ^ #P.parts * ((↑2 ^ #P.parts * m : ℝ) / #U) =
          ((2 : ℝ) * 2) ^ #P.parts * m / #U := by
        rw [mul_pow, ← mul_div_assoc, mul_assoc]
      _ = ↑4 ^ #P.parts * m / #U := by norm_num
      _ ≤ 1 := div_le_one_of_le₀ (pow_mul_m_le_card_part hP hU) (cast_nonneg _)
      _ ≤ ↑2 ^ #P.parts * ε ^ 2 / 10 := by
        refine (one_le_sq_iff₀ <| by positivity).1 ?_
        rw [div_pow, mul_pow, pow_right_comm, ← pow_mul ε, one_le_div (by positivity)]
        calc
          (↑10 ^ 2) = 100 := by norm_num
          _ ≤ ↑4 ^ #P.parts * ε ^ 5 := hPε
          _ ≤ ↑4 ^ #P.parts * ε ^ 4 := by
            gcongr _ * ?_
            exact pow_le_pow_of_le_one (by sz_positivity) hε₁ (by decide)
          _ = (↑2 ^ 2) ^ #P.parts * ε ^ (2 * 2) := by norm_num
      _ = ↑2 ^ #P.parts * (ε * (ε / 10)) := by rw [mul_div_assoc, sq, mul_div_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 : Finset α
hU : U ∈ P.parts
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hε₁ : ε ≤ 1
hP₁ : 0 < #P.parts
m :
  HPow.hPow (α := ℝ) 2 #P.parts * (HPow.hPow (α := ℝ) 2 #P.parts * (↑m : ℝ) / (↑(#U) : ℝ)) =
    HMul.hMul (α := ℝ) 2 2 ^ #P.parts * (↑m : ℝ) / (↑(#U) : ℝ)
m₁ : HMul.hMul (α := ℝ) 2 2 ^ #P.parts * (↑m : ℝ) / (↑(#U) : ℝ) = HPow.hPow (α := ℝ) 4 #P.parts * (↑m : ℝ) / (↑(#U) : ℝ)
⊢ HPow.hPow (α := ℝ) 2 #P.parts * (HPow.hPow (α := ℝ) 2 #P.parts * (↑m : ℝ) / (↑(#U) : ℝ)) ≤
    HPow.hPow (α := ℝ) 2 #P.parts * (ε * (ε / 10))
have m₂ : 1 ≤ HPow.hPow (α := ℝ) 2 #P.parts * HPow.hPow (β := ℕ) ε 2 / 10
Tactic: calc
      ↑2 ^ #P.parts * ((↑2 ^ #P.parts * m : ℝ) / #U) =
          ((2 : ℝ) * 2) ^ #P.parts * m / #U := by
        rw [mul_pow, ← mul_div_assoc, mul_assoc]
      _ = ↑4 ^ #P.parts * m / #U := by norm_num
      _ ≤ 1 := div_le_one_of_le₀ (pow_mul_m_le_card_part hP hU) (cast_nonneg _)
      _ ≤ ↑2 ^ #P.parts * ε ^ 2 / 10 := by
        refine (one_le_sq_iff₀ <| by positivity).1 ?_
        rw [div_pow, mul_pow, pow_right_comm, ← pow_mul ε, one_le_div (by positivity)]
        calc
          (↑10 ^ 2) = 100 := by norm_num
          _ ≤ ↑4 ^ #P.parts * ε ^ 5 := hPε
          _ ≤ ↑4 ^ #P.parts * ε ^ 4 := by
            gcongr _ * ?_
            exact pow_le_pow_of_le_one (by sz_positivity) hε₁ (by decide)
          _ = (↑2 ^ 2) ^ #P.parts * ε ^ (2 * 2) := by norm_num
      _ = ↑2 ^ #P.parts * (ε * (ε / 10)) := by rw [mul_div_assoc, sq, mul_div_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 : Finset α
hU : U ∈ P.parts
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hε₁ : ε ≤ 1
hP₁ : 0 < #P.parts
m :
  HPow.hPow (α := ℝ) 2 #P.parts * (HPow.hPow (α := ℝ) 2 #P.parts * (↑m : ℝ) / (↑(#U) : ℝ)) =
    HMul.hMul (α := ℝ) 2 2 ^ #P.parts * (↑m : ℝ) / (↑(#U) : ℝ)
m₁ : HMul.hMul (α := ℝ) 2 2 ^ #P.parts * (↑m : ℝ) / (↑(#U) : ℝ) = HPow.hPow (α := ℝ) 4 #P.parts * (↑m : ℝ) / (↑(#U) : ℝ)
m₂ : 1 ≤ HPow.hPow (α := ℝ) 2 #P.parts * HPow.hPow (β := ℕ) ε 2 / 10
⊢ HPow.hPow (α := ℝ) 2 #P.parts * (HPow.hPow (α := ℝ) 2 #P.parts * (↑m : ℝ) / (↑(#U) : ℝ)) ≤
    HPow.hPow (α := ℝ) 2 #P.parts * (ε * (ε / 10))
have m₃ : HPow.hPow (α := ℝ) 2 #P.parts * HPow.hPow (β := ℕ) ε 2 / 10 = HPow.hPow (α := ℝ) 2 #P.parts * (ε * (ε / 10))
Tactic: calc
      ↑2 ^ #P.parts * ((↑2 ^ #P.parts * m : ℝ) / #U) =
          ((2 : ℝ) * 2) ^ #P.parts * m / #U := by
        rw [mul_pow, ← mul_div_assoc, mul_assoc]
      _ = ↑4 ^ #P.parts * m / #U := by norm_num
      _ ≤ 1 := div_le_one_of_le₀ (pow_mul_m_le_card_part hP hU) (cast_nonneg _)
      _ ≤ ↑2 ^ #P.parts * ε ^ 2 / 10 := by
        refine (one_le_sq_iff₀ <| by positivity).1 ?_
        rw [div_pow, mul_pow, pow_right_comm, ← pow_mul ε, one_le_div (by positivity)]
        calc
          (↑10 ^ 2) = 100 := by norm_num
          _ ≤ ↑4 ^ #P.parts * ε ^ 5 := hPε
          _ ≤ ↑4 ^ #P.parts * ε ^ 4 := by
            gcongr _ * ?_
            exact pow_le_pow_of_le_one (by sz_positivity) hε₁ (by decide)
          _ = (↑2 ^ 2) ^ #P.parts * ε ^ (2 * 2) := by norm_num
      _ = ↑2 ^ #P.parts * (ε * (ε / 10)) := by rw [mul_div_assoc, sq, mul_div_assoc]
-- 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 : Finset α
hU : U ∈ P.parts
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hε₁ : ε ≤ 1
hP₁ : 0 < #P.parts
⊢ (1 - ε / 10) * (↑(#(G.nonuniformWitness ε U V)) : ℝ) ≤ (↑(#((star hP G ε hU V).biUnion id)) : ℝ)
have this : HPow.hPow (α := ℝ) 2 #P.parts * (↑m : ℝ) / ((↑(#U) : ℝ) * ε) ≤ ε / 10
Tactic: have : (↑2 ^ #P.parts : ℝ) * m / (#U * ε) ≤ ε / 10 := by
    rw [← div_div, div_le_iff₀']
    swap
    · sz_positivity
    refine le_of_mul_le_mul_left ?_ (pow_pos zero_lt_two #P.parts)
    calc
      ↑2 ^ #P.parts * ((↑2 ^ #P.parts * m : ℝ) / #U) =
          ((2 : ℝ) * 2) ^ #P.parts * m / #U := by
        rw [mul_pow, ← mul_div_assoc, mul_assoc]
      _ = ↑4 ^ #P.parts * m / #U := by norm_num
      _ ≤ 1 := div_le_one_of_le₀ (pow_mul_m_le_card_part hP hU) (cast_nonneg _)
      _ ≤ ↑2 ^ #P.parts * ε ^ 2 / 10 := by
        refine (one_le_sq_iff₀ <| by positivity).1 ?_
        rw [div_pow, mul_pow, pow_right_comm, ← pow_mul ε, one_le_div (by positivity)]
        calc
          (↑10 ^ 2) = 100 := by norm_num
          _ ≤ ↑4 ^ #P.parts * ε ^ 5 := hPε
          _ ≤ ↑4 ^ #P.parts * ε ^ 4 := by
            gcongr _ * ?_
            exact pow_le_pow_of_le_one (by sz_positivity) hε₁ (by decide)
          _ = (↑2 ^ 2) ^ #P.parts * ε ^ (2 * 2) := by norm_num
      _ = ↑2 ^ #P.parts * (ε * (ε / 10)) := by rw [mul_div_assoc, sq, mul_div_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 : Finset α
hU : U ∈ P.parts
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hε₁ : ε ≤ 1
hP₁ : 0 < #P.parts
this : HPow.hPow (α := ℝ) 2 #P.parts * (↑m : ℝ) / ((↑(#U) : ℝ) * ε) ≤ ε / 10
⊢ (1 - ε / 10) * (↑(#(G.nonuniformWitness ε U V)) : ℝ) ≤
    (1 - HPow.hPow (α := ℝ) 2 #P.parts * (↑m : ℝ) / ((↑(#U) : ℝ) * ε)) * (↑(#(G.nonuniformWitness ε U V)) : ℝ)
have ha : LE.le (α := ℝ) 0 (↑(#(G.nonuniformWitness ε U V)) : ℝ)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
hP : P.IsEquipartition
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
U : Finset α
hU : U ∈ P.parts
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hε₁ : ε ≤ 1
hP₁ : 0 < #P.parts
this : HPow.hPow (α := ℝ) 2 #P.parts * (↑m : ℝ) / ((↑(#U) : ℝ) * ε) ≤ ε / 10
⊢ (1 - HPow.hPow (α := ℝ) 2 #P.parts * (↑m : ℝ) / ((↑(#U) : ℝ) * ε)) * (↑(#(G.nonuniformWitness ε U V)) : ℝ) =
    (↑(#(G.nonuniformWitness ε U V)) : ℝ) -
      HPow.hPow (α := ℝ) 2 #P.parts * (↑m : ℝ) / ((↑(#U) : ℝ) * ε) * (↑(#(G.nonuniformWitness ε U V)) : ℝ)
have rw : HMul.hMul (α := ℝ) 1 (↑(#(G.nonuniformWitness ε U V)) : ℝ) -
    HPow.hPow (α := ℝ) 2 #P.parts * (↑m : ℝ) / ((↑(#U) : ℝ) * ε) * (↑(#(G.nonuniformWitness ε U V)) : ℝ) =
  (↑(#(G.nonuniformWitness ε U V)) : ℝ) -
    HPow.hPow (α := ℝ) 2 #P.parts * (↑m : ℝ) / ((↑(#U) : ℝ) * ε) * (↑(#(G.nonuniformWitness ε U V)) : ℝ)
Tactic: rw [sub_mul, one_mul]
-- 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 : Finset α
hU : U ∈ P.parts
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hε₁ : ε ≤ 1
hP₁ : 0 < #P.parts
this : HPow.hPow (α := ℝ) 2 #P.parts * (↑m : ℝ) / ((↑(#U) : ℝ) * ε) ≤ ε / 10
rw :
  HMul.hMul (α := ℝ) 1 (↑(#(G.nonuniformWitness ε U V)) : ℝ) -
      HPow.hPow (α := ℝ) 2 #P.parts * (↑m : ℝ) / ((↑(#U) : ℝ) * ε) * (↑(#(G.nonuniformWitness ε U V)) : ℝ) =
    (↑(#(G.nonuniformWitness ε U V)) : ℝ) -
      HPow.hPow (α := ℝ) 2 #P.parts * (↑m : ℝ) / ((↑(#U) : ℝ) * ε) * (↑(#(G.nonuniformWitness ε U V)) : ℝ)
⊢ (1 - HPow.hPow (α := ℝ) 2 #P.parts * (↑m : ℝ) / ((↑(#U) : ℝ) * ε)) * (↑(#(G.nonuniformWitness ε U V)) : ℝ) =
    (↑(#(G.nonuniformWitness ε U V)) : ℝ) -
      HPow.hPow (α := ℝ) 2 #P.parts * (↑m : ℝ) / ((↑(#U) : ℝ) * ε) * (↑(#(G.nonuniformWitness ε U V)) : ℝ)
have rw₁ : (↑(#(G.nonuniformWitness ε U V)) : ℝ) -
    HPow.hPow (α := ℝ) 2 #P.parts * (↑m : ℝ) / ((↑(#U) : ℝ) * ε) * (↑(#(G.nonuniformWitness ε U V)) : ℝ) =
  (↑(#(G.nonuniformWitness ε U V)) : ℝ) -
    HPow.hPow (α := ℝ) 2 #P.parts * (↑m : ℝ) / ((↑(#U) : ℝ) * ε) * (↑(#(G.nonuniformWitness ε U V)) : ℝ)
Tactic: rw [sub_mul, one_mul]
-- 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 : Finset α
hU : U ∈ P.parts
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hε₁ : ε ≤ 1
hP₁ : 0 < #P.parts
this : HPow.hPow (α := ℝ) 2 #P.parts * (↑m : ℝ) / ((↑(#U) : ℝ) * ε) ≤ ε / 10
⊢ (↑(#(G.nonuniformWitness ε U V)) : ℝ) -
      HPow.hPow (α := ℝ) 2 #P.parts * (↑m : ℝ) / ((↑(#U) : ℝ) * ε) * (↑(#(G.nonuniformWitness ε U V)) : ℝ) ≤
    (↑(#(G.nonuniformWitness ε U V)) : ℝ) - HPow.hPow (α := ℝ) 2 (#P.parts - 1) * (↑m : ℝ)
have refine : HPow.hPow (α := ℝ) 2 (#P.parts - 1) * (↑m : ℝ) ≤
  HPow.hPow (α := ℝ) 2 #P.parts * (↑m : ℝ) / ((↑(#U) : ℝ) * ε) * (↑(#(G.nonuniformWitness ε U V)) : ℝ)
Tactic: refine sub_le_sub_left ?_ _
-- 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 : Finset α
hU : U ∈ P.parts
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hε₁ : ε ≤ 1
hP₁ : 0 < #P.parts
this : HPow.hPow (α := ℝ) 2 #P.parts * (↑m : ℝ) / ((↑(#U) : ℝ) * ε) ≤ ε / 10
⊢ HPow.hPow (α := ℝ) 2 #P.parts = HPow.hPow (α := ℝ) 2 (#P.parts - 1) * 2
have rw : HPow.hPow (α := ℝ) 2 #P.parts = HPow.hPow (α := ℝ) 2 (#P.parts - 1 + 1)
Tactic: rw [← _root_.pow_succ, tsub_add_cancel_of_le (succ_le_iff.2 hP₁)]
-- 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 : Finset α
hU : U ∈ P.parts
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hε₁ : ε ≤ 1
hP₁ : 0 < #P.parts
this : HPow.hPow (α := ℝ) 2 #P.parts * (↑m : ℝ) / ((↑(#U) : ℝ) * ε) ≤ ε / 10
rw : HPow.hPow (α := ℝ) 2 #P.parts = HPow.hPow (α := ℝ) 2 (#P.parts - 1 + 1)
⊢ HPow.hPow (α := ℝ) 2 #P.parts = HPow.hPow (α := ℝ) 2 (#P.parts - 1) * 2
have rw₁ : HPow.hPow (α := ℝ) 2 #P.parts = HPow.hPow (α := ℝ) 2 #P.parts
Tactic: rw [← _root_.pow_succ, tsub_add_cancel_of_le (succ_le_iff.2 hP₁)]