awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
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) : ℝ)
rw₂ 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) : ℝ)

Tactic:
rw [mul_pow, ← mul_div_assoc, mul_assoc]

Premises used: mul_assoc, mul_div_assoc, mul_pow
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
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
⊢ HMul.hMul (α := ℝ) 2 2 ^ #P.parts * (↑m : ℝ) / (↑(#U) : ℝ) = HPow.hPow (α := ℝ) 4 #P.parts * (↑m : ℝ) / (↑(#U) : ℝ)

Tactic:
norm_num
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
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 * (↑m : ℝ) / (↑(#U) : ℝ) ≤ 1

Tactic:
div_le_one_of_le₀ (pow_mul_m_le_card_part hP hU) (cast_nonneg _)

Premises used: div_le_one_of_le₀, Nat.cast_nonneg, SzemerediRegularity.pow_mul_m_le_card_part
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
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 ≤ HPow.hPow (α := ℝ) 2 #P.parts * HPow.hPow (β := ℕ) ε 2 / 10

Tactic:
positivity
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
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
refine : 1 ≤ HPow.hPow (β := ℕ) (HPow.hPow (α := ℝ) 2 #P.parts * HPow.hPow (β := ℕ) ε 2 / 10) 2
⊢ 1 ≤ HPow.hPow (α := ℝ) 2 #P.parts * HPow.hPow (β := ℕ) ε 2 / 10

Tactic:
refine (one_le_sq_iff₀ <| by positivity).1 ?_

Premises used: one_le_sq_iff₀, Iff.mp
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
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 < HPow.hPow (α := ℝ) (β := ℕ) 10 2

Tactic:
positivity
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
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 (α := ℝ) (β := ℕ) 10 2 ≤ HPow.hPow (α := ℝ) (β := ℕ) 2 2 ^ #P.parts * ε ^ HMul.hMul (α := ℕ) 2 2
⊢ 1 ≤ HPow.hPow (β := ℕ) (HPow.hPow (α := ℝ) 2 #P.parts * HPow.hPow (β := ℕ) ε 2 / 10) 2

Tactic:
rw [div_pow, mul_pow, pow_right_comm, ← pow_mul ε, one_le_div (by positivity)]

Premises used: pow_right_comm, pow_mul, div_pow, one_le_div, mul_pow
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
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 = 100

Tactic:
norm_num
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
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
⊢ 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5

Tactic:
hPε
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
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
hbc : HPow.hPow (β := ℕ) ε 5 ≤ HPow.hPow (β := ℕ) ε 4
⊢ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 4

Tactic:
gcongr _ * ?_
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
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
sz_positivity sz_positivity₁ sz_positivity₂ sz_positivity₃ : 0 < ε → 0 ≤ ε
⊢ 0 ≤ ε

Tactic:
sz_positivity
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
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
⊢ LE.le (α := ℕ) 4 5

Tactic:
decide
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
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 (β := ℕ) ε 5 ≤ HPow.hPow (β := ℕ) ε 4

Tactic:
exact pow_le_pow_of_le_one (by sz_positivity) hε₁ (by decide)

Premises used: pow_le_pow_of_le_one
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
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 (β := ℕ) ε 4 =
    HPow.hPow (α := ℝ) (β := ℕ) 2 2 ^ #P.parts * ε ^ HMul.hMul (α := ℕ) 2 2

Tactic:
norm_num
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
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
by₂ :
  HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 4 =
    HPow.hPow (α := ℝ) (β := ℕ) 2 2 ^ #P.parts * ε ^ HMul.hMul (α := ℕ) 2 2
⊢ HPow.hPow (α := ℝ) (β := ℕ) 10 2 ≤ 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

Premises used: HMul.hMul, Finpartition.parts, HPow.hPow, OfNat.ofNat
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
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))
rw₂ 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))

Tactic:
rw [mul_div_assoc, sq, mul_div_assoc]

Premises used: mul_div_assoc, sq
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
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
m₃ : HPow.hPow (α := ℝ) 2 #P.parts * HPow.hPow (β := ℕ) ε 2 / 10 = HPow.hPow (α := ℝ) 2 #P.parts * (ε * (ε / 10))
⊢ HPow.hPow (α := ℝ) 2 #P.parts * (HPow.hPow (α := ℝ) 2 #P.parts * (↑m : ℝ) / (↑(#U) : ℝ)) ≤
    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]

Premises used: div_le_one_of_le₀, HMul.hMul, Nat.cast_nonneg, HDiv.hDiv, Finpartition.parts, SzemerediRegularity.pow_mul_m_le_card_part, OfNat.ofNat
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
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 * (↑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]
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
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
ha : LE.le (α := ℝ) 0 (↑(#(G.nonuniformWitness ε U V)) : ℝ)
⊢ (1 - ε / 10) * (↑(#(G.nonuniformWitness ε U V)) : ℝ) ≤
    (1 - HPow.hPow (α := ℝ) 2 #P.parts * (↑m : ℝ) / ((↑(#U) : ℝ) * ε)) * (↑(#(G.nonuniformWitness ε U V)) : ℝ)

Tactic:
gcongr
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
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)) : ℝ)
rw₁ 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)) : ℝ)
⊢ (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)) : ℝ)

Tactic:
rw [sub_mul, one_mul]

Premises used: sub_mul, one_mul
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
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 : ℝ)

Tactic:
sub_le_sub_left ?_ _

Premises used: sub_le_sub_left
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
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
refine :
  HPow.hPow (α := ℝ) 2 (#P.parts - 1) * (↑m : ℝ) ≤
    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)) : ℝ) ≤
    (↑(#(G.nonuniformWitness ε U V)) : ℝ) - HPow.hPow (α := ℝ) 2 (#P.parts - 1) * (↑m : ℝ)

Tactic:
refine sub_le_sub_left ?_ _

Premises used: sub_le_sub_left
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
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)
rw₁ rw₂ : HPow.hPow (α := ℝ) 2 #P.parts = HPow.hPow (α := ℝ) 2 #P.parts
⊢ HPow.hPow (α := ℝ) 2 #P.parts = HPow.hPow (α := ℝ) 2 (#P.parts - 1) * 2

Tactic:
rw [← _root_.pow_succ, tsub_add_cancel_of_le (succ_le_iff.2 hP₁)]

Premises used: Iff.mpr, pow_succ, tsub_add_cancel_of_le, Nat.succ_le_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
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

Tactic:
have : (2 : ℝ) ^ #P.parts = ↑2 ^ (#P.parts - 1) * 2 := by
        rw [← _root_.pow_succ, tsub_add_cancel_of_le (succ_le_iff.2 hP₁)]
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
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_1 : HPow.hPow (α := ℝ) 2 #P.parts * (↑m : ℝ) / ((↑(#U) : ℝ) * ε) ≤ ε / 10
this : HPow.hPow (α := ℝ) 2 #P.parts = HPow.hPow (α := ℝ) 2 (#P.parts - 1) * 2
rw :
  HPow.hPow (α := ℝ) 2 (#P.parts - 1) * (↑m : ℝ) * ((↑(#U) : ℝ) * ε) ≤
    HPow.hPow (α := ℝ) 2 (#P.parts - 1) * (↑m : ℝ) * HMul.hMul (α := ℝ) 2 (↑(#(G.nonuniformWitness ε U V)) : ℝ)
rw₁ : 0 < (↑(#U) : ℝ) * ε
⊢ HPow.hPow (α := ℝ) 2 (#P.parts - 1) * (↑m : ℝ) ≤
    HPow.hPow (α := ℝ) 2 #P.parts * (↑m : ℝ) / ((↑(#U) : ℝ) * ε) * (↑(#(G.nonuniformWitness ε U V)) : ℝ)

Tactic:
rw [← mul_div_right_comm, this, mul_right_comm _ (2 : ℝ), mul_assoc, le_div_iff₀]

Premises used: mul_assoc, mul_div_right_comm, mul_right_comm, le_div_iff₀, OfNat.ofNat
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
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_1 : HPow.hPow (α := ℝ) 2 #P.parts * (↑m : ℝ) / ((↑(#U) : ℝ) * ε) ≤ ε / 10
this : HPow.hPow (α := ℝ) 2 #P.parts = HPow.hPow (α := ℝ) 2 (#P.parts - 1) * 2
hbc : (↑(#U) : ℝ) * ε ≤ HMul.hMul (α := ℝ) 2 (↑(#(G.nonuniformWitness ε U V)) : ℝ)
⊢ HPow.hPow (α := ℝ) 2 (#P.parts - 1) * (↑m : ℝ) * ((↑(#U) : ℝ) * ε) ≤
    HPow.hPow (α := ℝ) 2 (#P.parts - 1) * (↑m : ℝ) * HMul.hMul (α := ℝ) 2 (↑(#(G.nonuniformWitness ε U V)) : ℝ)

Tactic:
gcongr _ * ?_
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
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_1 : HPow.hPow (α := ℝ) 2 #P.parts * (↑m : ℝ) / ((↑(#U) : ℝ) * ε) ≤ ε / 10
this : HPow.hPow (α := ℝ) 2 #P.parts = HPow.hPow (α := ℝ) 2 (#P.parts - 1) * 2
⊢ (↑(#U) : ℝ) * ε ≤ HMul.hMul (α := ℝ) 2 (↑(#(G.nonuniformWitness ε U V)) : ℝ)

Tactic:
(G.le_card_nonuniformWitness hunif).trans
          (le_mul_of_one_le_left (cast_nonneg _) one_le_two)

Premises used: le_mul_of_one_le_left, Nat.cast_nonneg, SimpleGraph.le_card_nonuniformWitness, one_le_two, LE.le.trans
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
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_1 : HPow.hPow (α := ℝ) 2 #P.parts * (↑m : ℝ) / ((↑(#U) : ℝ) * ε) ≤ ε / 10
this : HPow.hPow (α := ℝ) 2 #P.parts = HPow.hPow (α := ℝ) 2 (#P.parts - 1) * 2
⊢ (↑(#U) : ℝ) * ε ≤ HMul.hMul (α := ℝ) 2 (↑(#(G.nonuniformWitness ε U V)) : ℝ)

Tactic:
exact (G.le_card_nonuniformWitness hunif).trans
          (le_mul_of_one_le_left (cast_nonneg _) one_le_two)

Premises used: le_mul_of_one_le_left, Nat.cast_nonneg, SimpleGraph.le_card_nonuniformWitness, one_le_two, LE.le.trans