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 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) : ℝ)))
rw₂ rw₃ :
  (1 - ε / 10) * ((↑(#(G.nonuniformWitness ε U V)) : ℝ) * (HSub.hSub (α := ℝ) 1 (↑m : ℝ)⁻¹ / (↑(#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) : ℝ))

Tactic:
rw [mul_assoc, mul_assoc, mul_div_left_comm]

Premises used: mul_assoc, mul_div_left_comm
-- 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 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 : (1 - ε / 10) * (↑(#(G.nonuniformWitness ε U V)) : ℝ) ≤ (↑(#((star hP G ε hU V).biUnion id)) : ℝ)
⊢ (1 - ε / 10) * (↑(#(G.nonuniformWitness ε U V)) : ℝ) * (HSub.hSub (α := ℝ) 1 (↑m : ℝ)⁻¹ / (↑(#U) : ℝ)) ≤
    (↑(#((star hP G ε hU V).biUnion id)) : ℝ) * (HSub.hSub (α := ℝ) 1 (↑m : ℝ)⁻¹ / (↑(#U) : ℝ))

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 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)) : ℝ) ≤ (↑(#((star hP G ε hU V).biUnion id)) : ℝ)

Tactic:
one_sub_eps_mul_card_nonuniformWitness_le_card_star hV hUV hunif hPε hε₁

Premises used: _private.0.SzemerediRegularity.one_sub_eps_mul_card_nonuniformWitness_le_card_star
-- 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 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)) : ℝ) ≤ (↑(#((star hP G ε hU V).biUnion id)) : ℝ)

Tactic:
exact one_sub_eps_mul_card_nonuniformWitness_le_card_star hV hUV hunif hPε hε₁

Premises used: _private.0.SzemerediRegularity.one_sub_eps_mul_card_nonuniformWitness_le_card_star
-- 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 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 : (↑(#((star hP G ε hU V).biUnion id)) : ℝ) ≤ (↑(#(star hP G ε hU V)) : ℝ) * HAdd.hAdd (α := ℝ) (↑m : ℝ) 1
⊢ (↑(#((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:
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 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)) : ℝ) ≤ (↑(#(star hP G ε hU V)) : ℝ) * HAdd.hAdd (α := ℝ) (↑m : ℝ) 1

Tactic:
card_biUnion_star_le_m_add_one_card_star_mul

Premises used: SzemerediRegularity.card_biUnion_star_le_m_add_one_card_star_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 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)) : ℝ) ≤ (↑(#(star hP G ε hU V)) : ℝ) * HAdd.hAdd (α := ℝ) (↑m : ℝ) 1

Tactic:
exact card_biUnion_star_le_m_add_one_card_star_mul

Premises used: SzemerediRegularity.card_biUnion_star_le_m_add_one_card_star_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 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 : ℝ)
hbc₁ : HPow.hPow (α := ℝ) 4 #P.parts * (↑m : ℝ) ≤ (↑(#U) : ℝ)
⊢ (↑(#(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:
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 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 : ℝ)
hbc₄ hbc₅ : 0 < m → 0 < ε → 0 < HPow.hPow (α := ℝ) 4 #P.parts * (↑m : ℝ)
⊢ 0 < HPow.hPow (α := ℝ) 4 #P.parts * (↑m : ℝ)

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 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 < ε
⊢ HPow.hPow (α := ℝ) 4 #P.parts * (↑m : ℝ) ≤ (↑(#U) : ℝ)

Tactic:
pow_mul_m_le_card_part hP hU

Premises used: 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 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 < ε
⊢ HPow.hPow (α := ℝ) 4 #P.parts * (↑m : ℝ) ≤ (↑(#U) : ℝ)

Tactic:
exact pow_mul_m_le_card_part hP hU

Premises used: 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 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 :
  (↑(#(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
⊢ (↑(#(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

Tactic:
rw [mul_assoc, mul_comm ((4 : ℝ) ^ #P.parts), ← div_div, ← mul_div_assoc, ← mul_comm_div]

Premises used: mul_assoc, mul_div_assoc, Finpartition.parts, HPow.hPow, mul_comm_div, mul_comm, Finset.card, div_div, 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 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 ≤ (↑(#(star hP G ε hU V)) : ℝ) / HPow.hPow (α := ℝ) 4 #P.parts

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 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 < ε
refine : HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 * (HSub.hSub (α := ℝ) 1 (↑m : ℝ)⁻¹ / (↑m : ℝ)) ≤ 1
⊢ (↑(#(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:
refine mul_le_of_le_one_right (by positivity) ?_

Premises used: mul_le_of_le_one_right
-- 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 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 : ℝ)
sz_positivity₄ sz_positivity₅ : 0 < m → 0 < ε → LT.lt (α := ℝ) 0 (↑m : ℝ)
⊢ LT.lt (α := ℝ) 0 (↑m : ℝ)

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 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 : ℝ)

Tactic:
have hm : (0 : ℝ) < m := by 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 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 : ℝ)
rw : HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 * HSub.hSub (α := ℝ) (↑m : ℝ) 1 ≤ HMul.hMul (α := ℝ) (↑m : ℝ) (↑m : ℝ)
⊢ HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 * (HSub.hSub (α := ℝ) 1 (↑m : ℝ)⁻¹ / (↑m : ℝ)) ≤ 1

Tactic:
rw [mul_div_assoc', div_le_one hm, ← one_div, one_sub_div hm.ne', mul_div_assoc',
        div_le_iff₀ hm]

Premises used: div_le_iff₀, mul_div_assoc', LT.lt.ne', div_le_one, one_div, one_sub_div
-- 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 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
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
⊢ HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 * HSub.hSub (α := ℝ) (↑m : ℝ) 1 ≤ HMul.hMul (α := ℝ) (↑m : ℝ) (↑m : ℝ)

Tactic:
linarith
-- 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 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
⊢ 16 = HPow.hPow (α := ℝ) (β := ℕ) 4 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 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
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)|
⊢ 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|

Tactic:
rw [show (16 : ℝ) = ↑4 ^ 2 by norm_num, pow_right_comm, sq ((4 : ℝ) ^ _)]

Premises used: pow_right_comm, sq, 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 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
set :
  let 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)) : ℝ);
  3 / 4 * ε ≤
    |p -
        (∑ 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)|
⊢ 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:
set p : ℝ :=
    (∑ ab ∈ (star hP G ε hU V).product (star hP G ε hV U), (G.edgeDensity ab.1 ab.2 : ℝ)) /
      (#(star hP G ε hU V) * #(star hP G ε hV U))

Premises used: HMul.hMul, SimpleGraph.edgeDensity, Rat.cast, SzemerediRegularity.star, Prod.fst, Finset.card, Prod.snd, Finset.product, Finset.sum
-- 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 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)) : ℝ)
set :
  let 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);
  3 / 4 * ε ≤ |p - q|
⊢ 3 / 4 * ε ≤
    |p -
        (∑ 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:
set q : ℝ :=
    (∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts,
      (G.edgeDensity ab.1 ab.2 : ℝ)) / (↑4 ^ #P.parts * ↑4 ^ #P.parts)

Premises used: HMul.hMul, SimpleGraph.edgeDensity, Rat.cast, SzemerediRegularity.chunk, Finpartition.parts, Prod.fst, HPow.hPow, Finset.card, Prod.snd, Finset.product, Finset.sum
-- 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 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) : ℝ)
⊢ |r - s| ≤ ε / 5

Tactic:
have hrs : |r - s| ≤ ε / 5 := abs_density_star_sub_density_le_eps hPε hε₁ hUVne hUV
-- 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 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
unfold :
  ε ≤
    |HSub.hSub (α := ℝ) (↑(G.edgeDensity (G.nonuniformWitness ε U V) (G.nonuniformWitness ε V U)) : ℝ)
        (↑(G.edgeDensity U V) : ℝ)|
⊢ ε ≤ |s - t|

Tactic:
unfold s t