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
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst_3 : Nonempty α
hP : P.IsEquipartition
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hU : U ∈ P.parts
hV : V ∈ P.parts
hGε : 0 ≤ (↑(G.edgeDensity U V) : ℝ) - HPow.hPow (β := ℕ) ε 5 / 50
this : 0 ≤ ε
⊢ HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity U V) : ℝ) 2 - (↑(G.edgeDensity U V) : ℝ) * HPow.hPow (β := ℕ) ε 5 / 25 +
      HPow.hPow (β := ℕ) ε 10 / 2500 =
    HPow.hPow (β := ℕ) ((↑(G.edgeDensity U V) : ℝ) - HPow.hPow (β := ℕ) ε 5 / 50) 2

Tactic:
ring
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst_3 : Nonempty α
hP : P.IsEquipartition
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hU : U ∈ P.parts
hV : V ∈ P.parts
hGε : 0 ≤ (↑(G.edgeDensity U V) : ℝ) - HPow.hPow (β := ℕ) ε 5 / 50
this : 0 ≤ ε
hab :
  (↑(G.edgeDensity U V) : ℝ) - HPow.hPow (β := ℕ) ε 5 / 50 ≤
    (∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, (↑(G.edgeDensity ab.1 ab.2) : ℝ)) /
      HPow.hPow (α := ℝ) 16 #P.parts
⊢ HPow.hPow (β := ℕ) ((↑(G.edgeDensity U V) : ℝ) - HPow.hPow (β := ℕ) ε 5 / 50) 2 ≤
    HPow.hPow (β := ℕ)
      ((∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, (↑(G.edgeDensity ab.1 ab.2) : ℝ)) /
        HPow.hPow (α := ℝ) 16 #P.parts)
      2

Tactic:
gcongr
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst_3 : Nonempty α
hP : P.IsEquipartition
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hU : U ∈ P.parts
hV : V ∈ P.parts
hGε : 0 ≤ (↑(G.edgeDensity U V) : ℝ) - HPow.hPow (β := ℕ) ε 5 / 50
this : 0 ≤ ε
⊢ (chunk hP G ε hU).parts ⊆ (chunk hP G ε hU).parts

Tactic:
have rflU := Subset.refl (chunk hP G ε hU).parts
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst_3 : Nonempty α
hP : P.IsEquipartition
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hU : U ∈ P.parts
hV : V ∈ P.parts
hGε : 0 ≤ (↑(G.edgeDensity U V) : ℝ) - HPow.hPow (β := ℕ) ε 5 / 50
this : 0 ≤ ε
rflU : (chunk hP G ε hU).parts ⊆ (chunk hP G ε hU).parts
⊢ (chunk hP G ε hV).parts ⊆ (chunk hP G ε hV).parts

Tactic:
have rflV := Subset.refl (chunk hP G ε hV).parts
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst_3 : Nonempty α
hP : P.IsEquipartition
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hU : U ∈ P.parts
hV : V ∈ P.parts
hGε : 0 ≤ (↑(G.edgeDensity U V) : ℝ) - HPow.hPow (β := ℕ) ε 5 / 50
this : 0 ≤ ε
rflU : (chunk hP G ε hU).parts ⊆ (chunk hP G ε hU).parts
rflV : (chunk hP G ε hV).parts ⊆ (chunk hP G ε hV).parts
⊢ (↑(G.edgeDensity U V) : ℝ) - HPow.hPow (β := ℕ) ε 5 / 50 ≤
    (∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, (↑(G.edgeDensity ab.1 ab.2) : ℝ)) /
      HPow.hPow (α := ℝ) 16 #P.parts

Tactic:
(le_trans ?_ <| density_sub_eps_le_sum_density_div_card hPα hPε rflU rflV).trans ?_

Premises used: _private.0.SzemerediRegularity.density_sub_eps_le_sum_density_div_card, LE.le.trans, le_trans
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst_3 : Nonempty α
hP : P.IsEquipartition
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hU : U ∈ P.parts
hV : V ∈ P.parts
hGε : 0 ≤ (↑(G.edgeDensity U V) : ℝ) - HPow.hPow (β := ℕ) ε 5 / 50
this : 0 ≤ ε
rflU : (chunk hP G ε hU).parts ⊆ (chunk hP G ε hU).parts
rflV : (chunk hP G ε hV).parts ⊆ (chunk hP G ε hV).parts
hab :
  (↑(G.edgeDensity U V) : ℝ) - HPow.hPow (β := ℕ) ε 5 / 50 ≤
    (↑(G.edgeDensity ((chunk hP G ε hU).parts.biUnion id) ((chunk hP G ε hV).parts.biUnion id)) : ℝ) -
      HPow.hPow (β := ℕ) ε 5 / 50
hab₁ :
  (∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, (↑(G.edgeDensity ab.1 ab.2) : ℝ)) /
      HMul.hMul (α := ℝ) (↑(#(chunk hP G ε hU).parts) : ℝ) (↑(#(chunk hP G ε hV).parts) : ℝ) ≤
    (∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, (↑(G.edgeDensity ab.1 ab.2) : ℝ)) /
      HPow.hPow (α := ℝ) 16 #P.parts
⊢ (↑(G.edgeDensity U V) : ℝ) - HPow.hPow (β := ℕ) ε 5 / 50 ≤
    (∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, (↑(G.edgeDensity ab.1 ab.2) : ℝ)) /
      HPow.hPow (α := ℝ) 16 #P.parts

Tactic:
refine (le_trans ?_ <| density_sub_eps_le_sum_density_div_card hPα hPε rflU rflV).trans ?_

Premises used: _private.0.SzemerediRegularity.density_sub_eps_le_sum_density_div_card, LE.le.trans, le_trans
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst_3 : Nonempty α
hP : P.IsEquipartition
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hU : U ∈ P.parts
hV : V ∈ P.parts
hGε : 0 ≤ (↑(G.edgeDensity U V) : ℝ) - HPow.hPow (β := ℕ) ε 5 / 50
this : 0 ≤ ε
rflU : (chunk hP G ε hU).parts ⊆ (chunk hP G ε hU).parts
rflV : (chunk hP G ε hV).parts ⊆ (chunk hP G ε hV).parts
hab :
  (↑(G.edgeDensity U V) : ℝ) - HPow.hPow (β := ℕ) ε 5 / 50 ≤
    (↑(G.edgeDensity U ((chunk hP G ε hV).parts.biUnion id)) : ℝ) - HPow.hPow (β := ℕ) ε 5 / 50
hab₁ hab₂ :
  (↑(G.edgeDensity U V) : ℝ) - HPow.hPow (β := ℕ) ε 5 / 50 ≤ (↑(G.edgeDensity U V) : ℝ) - HPow.hPow (β := ℕ) ε 5 / 50
⊢ (↑(G.edgeDensity U V) : ℝ) - HPow.hPow (β := ℕ) ε 5 / 50 ≤
    (↑(G.edgeDensity ((chunk hP G ε hU).parts.biUnion id) ((chunk hP G ε hV).parts.biUnion id)) : ℝ) -
      HPow.hPow (β := ℕ) ε 5 / 50

Tactic:
rw [biUnion_parts, biUnion_parts]

Premises used: Finpartition.biUnion_parts
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst_3 : Nonempty α
hP : P.IsEquipartition
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hU : U ∈ P.parts
hV : V ∈ P.parts
hGε : 0 ≤ (↑(G.edgeDensity U V) : ℝ) - HPow.hPow (β := ℕ) ε 5 / 50
this : 0 ≤ ε
rflU : (chunk hP G ε hU).parts ⊆ (chunk hP G ε hU).parts
rflV : (chunk hP G ε hV).parts ⊆ (chunk hP G ε hV).parts
hab :
  (∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, (↑(G.edgeDensity ab.1 ab.2) : ℝ)) /
      HPow.hPow (α := ℝ) (↑(HMul.hMul (α := ℕ) 4 4) : ℝ) #P.parts ≤
    (∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, (↑(G.edgeDensity ab.1 ab.2) : ℝ)) /
      HPow.hPow (α := ℝ) 16 #P.parts
⊢ (∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, (↑(G.edgeDensity ab.1 ab.2) : ℝ)) /
      HMul.hMul (α := ℝ) (↑(#(chunk hP G ε hU).parts) : ℝ) (↑(#(chunk hP G ε hV).parts) : ℝ) ≤
    (∑ 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 [card_chunk (m_pos hPα).ne', card_chunk (m_pos hPα).ne', ← cast_mul, ← mul_pow, cast_pow]

Premises used: SzemerediRegularity.card_chunk, SzemerediRegularity.m_pos, LT.lt.ne', Nat.cast_mul, Nat.cast_pow, mul_pow
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst_3 : Nonempty α
hP : P.IsEquipartition
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hU : U ∈ P.parts
hV : V ∈ P.parts
hGε : 0 ≤ (↑(G.edgeDensity U V) : ℝ) - HPow.hPow (β := ℕ) ε 5 / 50
this : 0 ≤ ε
rflU : (chunk hP G ε hU).parts ⊆ (chunk hP G ε hU).parts
rflV : (chunk hP G ε hV).parts ⊆ (chunk hP G ε hV).parts
hab hab₁ hab₂ hab₃ :
  HDiv.hDiv (α := ℚ) (∑ i ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, G.edgeDensity i.1 i.2)
      (↑(HMul.hMul (α := ℕ) 4 4 ^ #P.parts) : ℚ) ≤
    HDiv.hDiv (α := ℚ) (∑ i ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, G.edgeDensity i.1 i.2)
      (↑(HMul.hMul (α := ℕ) 4 4 ^ #P.parts) : ℚ)
⊢ (∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, (↑(G.edgeDensity ab.1 ab.2) : ℝ)) /
      HPow.hPow (α := ℝ) (↑(HMul.hMul (α := ℕ) 4 4) : ℝ) #P.parts ≤
    (∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, (↑(G.edgeDensity ab.1 ab.2) : ℝ)) /
      HPow.hPow (α := ℝ) 16 #P.parts

Tactic:
norm_cast
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
P : Finpartition (α := Finset α) univ
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst_3 : Nonempty α
hP : P.IsEquipartition
hPα : #P.parts * HPow.hPow (α := ℕ) 16 #P.parts ≤ Fintype.card α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hU : U ∈ P.parts
hV : V ∈ P.parts
hGε : 0 ≤ (↑(G.edgeDensity U V) : ℝ) - HPow.hPow (β := ℕ) ε 5 / 50
this : 0 ≤ ε
_ :
  HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity U V) : ℝ) 2 - HPow.hPow (β := ℕ) ε 5 / 25 =
    HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity U V) : ℝ) 2 - 1 * HPow.hPow (β := ℕ) ε 5 / 25 +
      HPow.hPow (α := ℝ) (β := ℕ) 0 10 / 2500
_₁ :
  HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity U V) : ℝ) 2 - 1 * HPow.hPow (β := ℕ) ε 5 / 25 +
      HPow.hPow (α := ℝ) (β := ℕ) 0 10 / 2500 ≤
    HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity U V) : ℝ) 2 -
        (↑(G.edgeDensity U V) : ℝ) * HPow.hPow (β := ℕ) ε 5 / 25 +
      HPow.hPow (β := ℕ) ε 10 / 2500
_₂ :
  HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity U V) : ℝ) 2 - (↑(G.edgeDensity U V) : ℝ) * HPow.hPow (β := ℕ) ε 5 / 25 +
      HPow.hPow (β := ℕ) ε 10 / 2500 =
    HPow.hPow (β := ℕ) ((↑(G.edgeDensity U V) : ℝ) - HPow.hPow (β := ℕ) ε 5 / 50) 2
_₃ :
  HPow.hPow (β := ℕ) ((↑(G.edgeDensity U V) : ℝ) - HPow.hPow (β := ℕ) ε 5 / 50) 2 ≤
    HPow.hPow (β := ℕ)
      ((∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, (↑(G.edgeDensity ab.1 ab.2) : ℝ)) /
        HPow.hPow (α := ℝ) 16 #P.parts)
      2
⊢ HPow.hPow (α := ℝ) (β := ℕ) (↑(G.edgeDensity U V) : ℝ) 2 - HPow.hPow (β := ℕ) ε 5 / 25 ≤
    HPow.hPow (β := ℕ)
      ((∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, (↑(G.edgeDensity ab.1 ab.2) : ℝ)) /
        HPow.hPow (α := ℝ) 16 #P.parts)
      2

Tactic:
calc
    _ = G.edgeDensity U V ^ 2 - 1 * ε ^ 5 / 25 + 0 ^ 10 / 2500 := by ring
    _ ≤ G.edgeDensity U V ^ 2 - G.edgeDensity U V * ε ^ 5 / 25 + ε ^ 10 / 2500 := by
      gcongr; exact mod_cast G.edgeDensity_le_one ..
    _ = (G.edgeDensity U V - ε ^ 5 / 50) ^ 2 := by ring
    _ ≤ _ := by
      gcongr
      have rflU := Subset.refl (chunk hP G ε hU).parts
      have rflV := Subset.refl (chunk hP G ε hV).parts
      refine (le_trans ?_ <| density_sub_eps_le_sum_density_div_card hPα hPε rflU rflV).trans ?_
      · rw [biUnion_parts, biUnion_parts]
      · rw [card_chunk (m_pos hPα).ne', card_chunk (m_pos hPα).ne', ← cast_mul, ← mul_pow, cast_pow]
        norm_cast

Premises used: SimpleGraph.edgeDensity, HSub.hSub, HDiv.hDiv, Rat.cast, 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 α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hε₁ : ε ≤ 1
hU : U ∈ P.parts
hV : V ∈ P.parts
hUV' : U ≠ V
hUV : ¬G.IsUniform ε U V
sz_positivity sz_positivity₁ sz_positivity₂ sz_positivity₃ : 0 < ε → 0 ≤ ε / 10
⊢ 0 ≤ ε / 10

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 α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hε₁ : ε ≤ 1
hU : U ∈ P.parts
hV : V ∈ P.parts
hUV' : U ≠ V
hUV : ¬G.IsUniform ε U V
h : ε / 5 = 2 * (ε / 10)
⊢ |HSub.hSub (α := ℝ) (↑(G.edgeDensity ((star hP G ε hU V).biUnion id) ((star hP G ε hV U).biUnion id)) : ℝ)
        (↑(G.edgeDensity (G.nonuniformWitness ε U V) (G.nonuniformWitness ε V U)) : ℝ)| ≤
    ε / 5

Tactic:
convert!
    abs_edgeDensity_sub_edgeDensity_le_two_mul G.Adj
      (biUnion_star_subset_nonuniformWitness hP G ε hU V)
      (biUnion_star_subset_nonuniformWitness hP G ε hV U) (by sz_positivity)
      (one_sub_eps_mul_card_nonuniformWitness_le_card_star hV hUV' hUV hPε hε₁)
      (one_sub_eps_mul_card_nonuniformWitness_le_card_star hU hUV'.symm (fun hVU => hUV hVU.symm)
        hPε hε₁) using 1

Premises used: _private.0.SzemerediRegularity.one_sub_eps_mul_card_nonuniformWitness_le_card_star, SimpleGraph.Adj, Rel.abs_edgeDensity_sub_edgeDensity_le_two_mul, SzemerediRegularity.biUnion_star_subset_nonuniformWitness, Ne.symm, SimpleGraph.IsUniform.symm
-- 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 α
hPε : 100 ≤ HPow.hPow (α := ℝ) 4 #P.parts * HPow.hPow (β := ℕ) ε 5
hε₁ : ε ≤ 1
hU : U ∈ P.parts
hV : V ∈ P.parts
hUV' : U ≠ V
hUV : ¬G.IsUniform ε U V
linarith : ε / 5 < 2 * (ε / 10) → 5 / 5 = 1
linarith₁ : ε / 5 < 2 * (ε / 10) → HMul.hMul (α := ℝ) 2 5 = 10
linarith₂ : ε / 5 < 2 * (ε / 10) → 10 / 10 = 1
linarith₃ linarith₄ : ε / 5 < 2 * (ε / 10) → HMul.hMul (α := ℝ) 1 10 = 10
linarith₅ : ε / 5 < 2 * (ε / 10) → GT.gt (α := ℝ) 10 0
linarith₆ : ε / 5 < 2 * (ε / 10) → 2 * ε - HMul.hMul (α := ℝ) 1 2 * (1 * ε) = 0
linarith₇ : 2 * (ε / 10) < ε / 5 → 10 / 10 = 1
linarith₈ linarith₉ : 2 * (ε / 10) < ε / 5 → HMul.hMul (α := ℝ) 1 10 = 10
linarith₁₀ : 2 * (ε / 10) < ε / 5 → 5 / 5 = 1
linarith₁₁ : 2 * (ε / 10) < ε / 5 → HMul.hMul (α := ℝ) 2 5 = 10
linarith₁₂ : 2 * (ε / 10) < ε / 5 → GT.gt (α := ℝ) 10 0
linarith₁₃ : 2 * (ε / 10) < ε / 5 → HMul.hMul (α := ℝ) 1 2 * (1 * ε) - 2 * ε = 0
⊢ ε / 5 = 2 * (ε / 10)

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
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
⊢ 0 ≤ HSub.hSub (α := ℝ) 1 (↑m : ℝ)⁻¹

Tactic:
have hm : (0 : ℝ) ≤ 1 - (↑m)⁻¹ := sub_nonneg_of_le (inv_le_one_of_one_le₀ <| one_le_m_coe 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 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 : ℝ)⁻¹
⊢ LE.le (α := ℝ) 1 10

Tactic:
simp
-- 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 : ℝ)⁻¹
⊢ LE.le (α := ℝ) 0 10

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
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
hm : 0 ≤ HSub.hSub (α := ℝ) 1 (↑m : ℝ)⁻¹
⊢ 0 ≤ 1 - ε / 10

Tactic:
have hε : 0 ≤ 1 - ε / 10 :=
    sub_nonneg_of_le (div_le_one_of_le₀ (hε₁.trans <| by simp) <| by 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
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 < ε
sz_positivity₄ sz_positivity₅ : 0 < m → 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 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
⊢ 0 < ε

Tactic:
have hε₀ : 0 < ε := 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 : 0 ≤ HSub.hSub (α := ℝ) 1 (↑m : ℝ)⁻¹
hε : 0 ≤ 1 - ε / 10
hε₀ : 0 < ε
⊢ 4 / 5 * ε = (1 - 1 / 10) * HSub.hSub (α := ℝ) 1 9⁻¹ * ε

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
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 : ℝ)
h₂ : ε ≤ HDiv.hDiv (α := ℝ) (↑(#(G.nonuniformWitness ε U V)) : ℝ) (↑(#U) : ℝ)
⊢ (1 - 1 / 10) * HSub.hSub (α := ℝ) 1 9⁻¹ * ε ≤
    (1 - ε / 10) * HSub.hSub (α := ℝ) 1 (↑m : ℝ)⁻¹ *
      HDiv.hDiv (α := ℝ) (↑(#(G.nonuniformWitness ε U V)) : ℝ) (↑(#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 < ε
⊢ LE.le (α := ℕ) 9 100

Tactic:
simp
-- 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 < ε
⊢ ε ≤ HDiv.hDiv (α := ℝ) (↑(#(G.nonuniformWitness ε U V)) : ℝ) (↑(#U) : ℝ)

Tactic:
(le_div_iff₀' <| cast_pos.2 (P.nonempty_of_mem_parts hU).card_pos).2 <|
           G.le_card_nonuniformWitness hunif

Premises used: Iff.mpr, le_div_iff₀', SimpleGraph.le_card_nonuniformWitness
-- 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 < ε
⊢ LE.le (α := ℝ) 9 (↑m : ℝ)

Tactic:
exacts [mod_cast (show 9 ≤ 100 by simp).trans (hundred_le_m hPα hPε hε₁),
          (le_div_iff₀' <| cast_pos.2 (P.nonempty_of_mem_parts hU).card_pos).2 <|
           G.le_card_nonuniformWitness hunif]

Premises used: Iff.mpr, le_div_iff₀', SimpleGraph.le_card_nonuniformWitness, LE.le.trans, SzemerediRegularity.hundred_le_m