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
sz_positivity sz_positivity₁ sz_positivity₂ sz_positivity₃ : 0 < m → 0 < ε
⊢ 0 < ε
have sz_positivity₄ : 0 < m → 0 < ε → 0 < ε
Tactic: sz_positivity
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
hP : P.IsEquipartition
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst_3 : Nonempty α
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hε₁ : ε ≤ 1
hU : U ∈ P.parts
hV : V ∈ P.parts
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
hm : 0 ≤ HSub.hSub (α := ℝ) 1 (↑m : ℝ)⁻¹
hε : 0 ≤ 1 - ε / 10
⊢ 4 / 5 * ε ≤ (↑(#(star hP G ε hU V)) : ℝ) / HPow.hPow (α := ℝ) 4 #P.parts
have hε₀ : 0 < ε
Tactic: have hε₀ : 0 < ε := by sz_positivity
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
hP : P.IsEquipartition
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst_3 : Nonempty α
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hε₁ : ε ≤ 1
hU : U ∈ P.parts
hV : V ∈ P.parts
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
hm : 0 ≤ HSub.hSub (α := ℝ) 1 (↑m : ℝ)⁻¹
hε : 0 ≤ 1 - ε / 10
hε₀ : 0 < ε
⊢ (1 - 1 / 10) * HSub.hSub (α := ℝ) 1 9⁻¹ * ε ≤
    (1 - ε / 10) * HSub.hSub (α := ℝ) 1 (↑m : ℝ)⁻¹ *
      HDiv.hDiv (α := ℝ) (↑(#(G.nonuniformWitness ε U V)) : ℝ) (↑(#U) : ℝ)
have h₁ : LE.le (α := ℝ) 9 (↑m : ℝ)
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 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 < ε
h₁ : LE.le (α := ℝ) 9 (↑m : ℝ)
⊢ (1 - 1 / 10) * HSub.hSub (α := ℝ) 1 9⁻¹ * ε ≤
    (1 - ε / 10) * HSub.hSub (α := ℝ) 1 (↑m : ℝ)⁻¹ *
      HDiv.hDiv (α := ℝ) (↑(#(G.nonuniformWitness ε U V)) : ℝ) (↑(#U) : ℝ)
have h₂ : ε ≤ HDiv.hDiv (α := ℝ) (↑(#(G.nonuniformWitness ε U V)) : ℝ) (↑(#U) : ℝ)
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 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 < ε
⊢ (1 - ε / 10) * HSub.hSub (α := ℝ) 1 (↑m : ℝ)⁻¹ *
      HDiv.hDiv (α := ℝ) (↑(#(G.nonuniformWitness ε U V)) : ℝ) (↑(#U) : ℝ) =
    (1 - ε / 10) * (↑(#(G.nonuniformWitness ε U V)) : ℝ) * (HSub.hSub (α := ℝ) 1 (↑m : ℝ)⁻¹ / (↑(#U) : ℝ))
have rw : (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: rw [mul_assoc, mul_assoc, mul_div_left_comm]
-- 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 < ε
rw :
  (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) * HSub.hSub (α := ℝ) 1 (↑m : ℝ)⁻¹ *
      HDiv.hDiv (α := ℝ) (↑(#(G.nonuniformWitness ε U V)) : ℝ) (↑(#U) : ℝ) =
    (1 - ε / 10) * (↑(#(G.nonuniformWitness ε U V)) : ℝ) * (HSub.hSub (α := ℝ) 1 (↑m : ℝ)⁻¹ / (↑(#U) : ℝ))
have rw₁ : (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: rw [mul_assoc, mul_assoc, mul_div_left_comm]
-- 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 < ε
rw :
  (1 - ε / 10) *
      (HSub.hSub (α := ℝ) 1 (↑m : ℝ)⁻¹ * HDiv.hDiv (α := ℝ) (↑(#(G.nonuniformWitness ε U V)) : ℝ) (↑(#U) : ℝ)) =
    (1 - ε / 10) * (↑(#(G.nonuniformWitness ε U V)) : ℝ) * (HSub.hSub (α := ℝ) 1 (↑m : ℝ)⁻¹ / (↑(#U) : ℝ))
rw₁ :
  (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) * HSub.hSub (α := ℝ) 1 (↑m : ℝ)⁻¹ *
      HDiv.hDiv (α := ℝ) (↑(#(G.nonuniformWitness ε U V)) : ℝ) (↑(#U) : ℝ) =
    (1 - ε / 10) * (↑(#(G.nonuniformWitness ε U V)) : ℝ) * (HSub.hSub (α := ℝ) 1 (↑m : ℝ)⁻¹ / (↑(#U) : ℝ))
have rw₂ : (1 - ε / 10) * ((↑(#(G.nonuniformWitness ε U V)) : ℝ) * (HSub.hSub (α := ℝ) 1 (↑m : ℝ)⁻¹ / (↑(#U) : ℝ))) =
  (1 - ε / 10) * ((↑(#(G.nonuniformWitness ε U V)) : ℝ) * (HSub.hSub (α := ℝ) 1 (↑m : ℝ)⁻¹ / (↑(#U) : ℝ)))
Tactic: rw [mul_assoc, mul_assoc, mul_div_left_comm]
-- 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 < ε
⊢ (1 - ε / 10) * (↑(#(G.nonuniformWitness ε U V)) : ℝ) * (HSub.hSub (α := ℝ) 1 (↑m : ℝ)⁻¹ / (↑(#U) : ℝ)) ≤
    (↑(#((star hP G ε hU V).biUnion id)) : ℝ) * (HSub.hSub (α := ℝ) 1 (↑m : ℝ)⁻¹ / (↑(#U) : ℝ))
have hbc : (1 - ε / 10) * (↑(#(G.nonuniformWitness ε U V)) : ℝ) ≤ (↑(#((star hP G ε hU V).biUnion id)) : ℝ)
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 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 < ε
⊢ (↑(#((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) : ℝ))
have hbc : (↑(#((star hP G ε hU V).biUnion id)) : ℝ) ≤ (↑(#(star hP G ε hU V)) : ℝ) * HAdd.hAdd (α := ℝ) (↑m : ℝ) 1
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 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 < ε
⊢ (↑(#(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 : ℝ)))
have hbc : 0 < HPow.hPow (α := ℝ) 4 #P.parts * (↑m : ℝ)
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 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 < ε
hbc : 0 < HPow.hPow (α := ℝ) 4 #P.parts * (↑m : ℝ)
⊢ (↑(#(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 : ℝ)))
have hbc₁ : HPow.hPow (α := ℝ) 4 #P.parts * (↑m : ℝ) ≤ (↑(#U) : ℝ)
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 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 < ε
⊢ 0 < HPow.hPow (α := ℝ) 4 #P.parts * (↑m : ℝ)
have hbc : 0 < m → 0 < HPow.hPow (α := ℝ) 4 #P.parts * (↑m : ℝ)
Tactic: sz_positivity
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
hP : P.IsEquipartition
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst_3 : Nonempty α
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hε₁ : ε ≤ 1
hU : U ∈ P.parts
hV : V ∈ P.parts
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
hm : 0 ≤ HSub.hSub (α := ℝ) 1 (↑m : ℝ)⁻¹
hε : 0 ≤ 1 - ε / 10
hε₀ : 0 < ε
hbc hbc₁ hbc₂ hbc₃ : 0 < m → 0 < HPow.hPow (α := ℝ) 4 #P.parts * (↑m : ℝ)
⊢ 0 < HPow.hPow (α := ℝ) 4 #P.parts * (↑m : ℝ)
have hbc₄ : 0 < m → 0 < ε → 0 < HPow.hPow (α := ℝ) 4 #P.parts * (↑m : ℝ)
Tactic: sz_positivity
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
hP : P.IsEquipartition
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst_3 : Nonempty α
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hε₁ : ε ≤ 1
hU : U ∈ P.parts
hV : V ∈ P.parts
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
hm : 0 ≤ HSub.hSub (α := ℝ) 1 (↑m : ℝ)⁻¹
hε : 0 ≤ 1 - ε / 10
hε₀ : 0 < ε
⊢ (↑(#(star hP G ε hU V)) : ℝ) * HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 *
      (HSub.hSub (α := ℝ) 1 (↑m : ℝ)⁻¹ / (HPow.hPow (α := ℝ) 4 #P.parts * (↑m : ℝ))) ≤
    (↑(#(star hP G ε hU V)) : ℝ) / HPow.hPow (α := ℝ) 4 #P.parts
have rw : (↑(#(star hP G ε hU V)) : ℝ) / HPow.hPow (α := ℝ) 4 #P.parts *
    (HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 * (HSub.hSub (α := ℝ) 1 (↑m : ℝ)⁻¹ / (↑m : ℝ))) ≤
  (↑(#(star hP G ε hU V)) : ℝ) / HPow.hPow (α := ℝ) 4 #P.parts
Tactic: rw [mul_assoc, mul_comm ((4 : ℝ) ^ #P.parts), ← div_div, ← mul_div_assoc, ← mul_comm_div]
-- 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 < ε
⊢ (↑(#(star hP G ε hU V)) : ℝ) / HPow.hPow (α := ℝ) 4 #P.parts *
      (HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 * (HSub.hSub (α := ℝ) 1 (↑m : ℝ)⁻¹ / (↑m : ℝ))) ≤
    (↑(#(star hP G ε hU V)) : ℝ) / HPow.hPow (α := ℝ) 4 #P.parts
have refine : HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 * (HSub.hSub (α := ℝ) 1 (↑m : ℝ)⁻¹ / (↑m : ℝ)) ≤ 1
Tactic: refine mul_le_of_le_one_right (by positivity) ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
hP : P.IsEquipartition
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst_3 : Nonempty α
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hε₁ : ε ≤ 1
hU : U ∈ P.parts
hV : V ∈ P.parts
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
hm : 0 ≤ HSub.hSub (α := ℝ) 1 (↑m : ℝ)⁻¹
hε : 0 ≤ 1 - ε / 10
hε₀ : 0 < ε
⊢ LT.lt (α := ℝ) 0 (↑m : ℝ)
have sz_positivity : 0 < m → LT.lt (α := ℝ) 0 (↑m : ℝ)
Tactic: sz_positivity
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
hP : P.IsEquipartition
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst_3 : Nonempty α
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hε₁ : ε ≤ 1
hU : U ∈ P.parts
hV : V ∈ P.parts
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
hm : 0 ≤ HSub.hSub (α := ℝ) 1 (↑m : ℝ)⁻¹
hε : 0 ≤ 1 - ε / 10
hε₀ : 0 < ε
sz_positivity sz_positivity₁ sz_positivity₂ sz_positivity₃ : 0 < m → LT.lt (α := ℝ) 0 (↑m : ℝ)
⊢ LT.lt (α := ℝ) 0 (↑m : ℝ)
have sz_positivity₄ : 0 < m → 0 < ε → LT.lt (α := ℝ) 0 (↑m : ℝ)
Tactic: sz_positivity
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
hP : P.IsEquipartition
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst_3 : Nonempty α
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hε₁ : ε ≤ 1
hU : U ∈ P.parts
hV : V ∈ P.parts
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
hm : 0 ≤ HSub.hSub (α := ℝ) 1 (↑m : ℝ)⁻¹
hε : 0 ≤ 1 - ε / 10
hε₀ : 0 < ε
⊢ HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 * (HSub.hSub (α := ℝ) 1 (↑m : ℝ)⁻¹ / (↑m : ℝ)) ≤ 1
have hm₁ : LT.lt (α := ℝ) 0 (↑m : ℝ)
Tactic: have hm : (0 : ℝ) < m := by sz_positivity
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
hP : P.IsEquipartition
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst_3 : Nonempty α
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hε₁ : ε ≤ 1
hU : U ∈ P.parts
hV : V ∈ P.parts
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
hm_1 : 0 ≤ HSub.hSub (α := ℝ) 1 (↑m : ℝ)⁻¹
hε : 0 ≤ 1 - ε / 10
hε₀ : 0 < ε
hm : LT.lt (α := ℝ) 0 (↑m : ℝ)
⊢ HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 * (HSub.hSub (α := ℝ) 1 (↑m : ℝ)⁻¹ / (↑m : ℝ)) ≤ 1
have rw : HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 * HSub.hSub (α := ℝ) (↑m : ℝ) 1 ≤ HMul.hMul (α := ℝ) (↑m : ℝ) (↑m : ℝ)
Tactic: rw [mul_div_assoc', div_le_one hm, ← one_div, one_sub_div hm.ne', mul_div_assoc',
        div_le_iff₀ hm]
-- 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_1 : 0 ≤ HSub.hSub (α := ℝ) 1 (↑m : ℝ)⁻¹
hε : 0 ≤ 1 - ε / 10
hε₀ : 0 < ε
hm : LT.lt (α := ℝ) 0 (↑m : ℝ)
⊢ HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 * HSub.hSub (α := ℝ) (↑m : ℝ) 1 ≤ HMul.hMul (α := ℝ) (↑m : ℝ) (↑m : ℝ)
have linarith : HMul.hMul (α := ℝ) (↑m : ℝ) (↑m : ℝ) < HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 * HSub.hSub (α := ℝ) (↑m : ℝ) 1 →
  HMul.hMul (α := ℝ) 1 1 = 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 α
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_1 : 0 ≤ HSub.hSub (α := ℝ) 1 (↑m : ℝ)⁻¹
hε : 0 ≤ 1 - ε / 10
hε₀ : 0 < ε
hm : LT.lt (α := ℝ) 0 (↑m : ℝ)
linarith linarith₁ :
  HMul.hMul (α := ℝ) (↑m : ℝ) (↑m : ℝ) < HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 * HSub.hSub (α := ℝ) (↑m : ℝ) 1 →
    HMul.hMul (α := ℝ) 1 1 = 1
⊢ HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 * HSub.hSub (α := ℝ) (↑m : ℝ) 1 ≤ HMul.hMul (α := ℝ) (↑m : ℝ) (↑m : ℝ)
have linarith₂ : HMul.hMul (α := ℝ) (↑m : ℝ) (↑m : ℝ) < HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 * HSub.hSub (α := ℝ) (↑m : ℝ) 1 → 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 α
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_1 : 0 ≤ HSub.hSub (α := ℝ) 1 (↑m : ℝ)⁻¹
hε : 0 ≤ 1 - ε / 10
hε₀ : 0 < ε
hm : LT.lt (α := ℝ) 0 (↑m : ℝ)
linarith linarith₁ :
  HMul.hMul (α := ℝ) (↑m : ℝ) (↑m : ℝ) < HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 * HSub.hSub (α := ℝ) (↑m : ℝ) 1 →
    HMul.hMul (α := ℝ) 1 1 = 1
linarith₂ :
  HMul.hMul (α := ℝ) (↑m : ℝ) (↑m : ℝ) < HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 * HSub.hSub (α := ℝ) (↑m : ℝ) 1 → 10 / 10 = 1
⊢ HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 * HSub.hSub (α := ℝ) (↑m : ℝ) 1 ≤ HMul.hMul (α := ℝ) (↑m : ℝ) (↑m : ℝ)
have linarith₃ : HMul.hMul (α := ℝ) (↑m : ℝ) (↑m : ℝ) < HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 * HSub.hSub (α := ℝ) (↑m : ℝ) 1 →
  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 α
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_1 : 0 ≤ HSub.hSub (α := ℝ) 1 (↑m : ℝ)⁻¹
hε : 0 ≤ 1 - ε / 10
hε₀ : 0 < ε
hm : LT.lt (α := ℝ) 0 (↑m : ℝ)
linarith linarith₁ :
  HMul.hMul (α := ℝ) (↑m : ℝ) (↑m : ℝ) < HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 * HSub.hSub (α := ℝ) (↑m : ℝ) 1 →
    HMul.hMul (α := ℝ) 1 1 = 1
linarith₂ :
  HMul.hMul (α := ℝ) (↑m : ℝ) (↑m : ℝ) < HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 * HSub.hSub (α := ℝ) (↑m : ℝ) 1 → 10 / 10 = 1
linarith₃ :
  HMul.hMul (α := ℝ) (↑m : ℝ) (↑m : ℝ) < HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 * HSub.hSub (α := ℝ) (↑m : ℝ) 1 →
    HMul.hMul (α := ℝ) 1 10 = 10
⊢ HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 * HSub.hSub (α := ℝ) (↑m : ℝ) 1 ≤ HMul.hMul (α := ℝ) (↑m : ℝ) (↑m : ℝ)
have linarith₄ : HMul.hMul (α := ℝ) (↑m : ℝ) (↑m : ℝ) < HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 * HSub.hSub (α := ℝ) (↑m : ℝ) 1 →
  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 α
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_1 : 0 ≤ HSub.hSub (α := ℝ) 1 (↑m : ℝ)⁻¹
hε : 0 ≤ 1 - ε / 10
hε₀ : 0 < ε
hm : LT.lt (α := ℝ) 0 (↑m : ℝ)
linarith linarith₁ :
  HMul.hMul (α := ℝ) (↑m : ℝ) (↑m : ℝ) < HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 * HSub.hSub (α := ℝ) (↑m : ℝ) 1 →
    HMul.hMul (α := ℝ) 1 1 = 1
linarith₂ :
  HMul.hMul (α := ℝ) (↑m : ℝ) (↑m : ℝ) < HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 * HSub.hSub (α := ℝ) (↑m : ℝ) 1 → 10 / 10 = 1
linarith₃ :
  HMul.hMul (α := ℝ) (↑m : ℝ) (↑m : ℝ) < HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 * HSub.hSub (α := ℝ) (↑m : ℝ) 1 →
    HMul.hMul (α := ℝ) 1 10 = 10
linarith₄ :
  HMul.hMul (α := ℝ) (↑m : ℝ) (↑m : ℝ) < HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 * HSub.hSub (α := ℝ) (↑m : ℝ) 1 →
    GT.gt (α := ℝ) 10 0
⊢ HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 * HSub.hSub (α := ℝ) (↑m : ℝ) 1 ≤ HMul.hMul (α := ℝ) (↑m : ℝ) (↑m : ℝ)
have linarith₅ : HMul.hMul (α := ℝ) (↑m : ℝ) (↑m : ℝ) < HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 * HSub.hSub (α := ℝ) (↑m : ℝ) 1 →
  -1 +
      (HMul.hMul (α := ℝ) 1 (↑m : ℝ) * HMul.hMul (α := ℝ) 1 (↑m : ℝ) -
        (HMul.hMul (α := ℝ) 1 (↑m : ℝ) + HMul.hMul (α := ℝ) 1 1) *
          (HMul.hMul (α := ℝ) 1 (↑m : ℝ) - HMul.hMul (α := ℝ) 1 1)) =
    0
Tactic: linarith