awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Bound
Goal:
ε : ℝ
l : ℕ
⊢ l ≤ bound ε l

Tactic:
(le_initialBound ε l).trans <| initialBound_le_bound ε l

Premises used: SzemerediRegularity.initialBound_le_bound, LE.le.trans, SzemerediRegularity.le_initialBound
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Bound
Goal:
ε : ℝ
l : ℕ
⊢ 0 < bound ε l

Tactic:
(initialBound_pos ε l).trans_le <| initialBound_le_bound ε l

Premises used: SzemerediRegularity.initialBound_le_bound, LT.lt.trans_le, SzemerediRegularity.initialBound_pos
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Bound
Goal:
ι : Type u_2
𝕜 : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s t : Finset ι
x : 𝕜
hst : s ⊆ t
f : ι → 𝕜
hs : HPow.hPow (β := ℕ) x 2 ≤ HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ s, f i) (↑(#s) : 𝕜)) 2
hs' : Ne.{u_3 + 1} (α := 𝕜) (↑(#s) : 𝕜) 0
hbc : HPow.hPow (β := ℕ) x 2 ≤ HDiv.hDiv (α := 𝕜) (∑ i ∈ s, HPow.hPow (β := ℕ) (f i) 2) (↑(#s) : 𝕜)
⊢ (↑(#s) : 𝕜) * HPow.hPow (β := ℕ) x 2 ≤
    (↑(#s) : 𝕜) * HDiv.hDiv (α := 𝕜) (∑ i ∈ s, HPow.hPow (β := ℕ) (f i) 2) (↑(#s) : 𝕜)

Tactic:
gcongr
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Bound
Goal:
ι : Type u_2
𝕜 : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s t : Finset ι
x : 𝕜
hst : s ⊆ t
f : ι → 𝕜
hs : HPow.hPow (β := ℕ) x 2 ≤ HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ s, f i) (↑(#s) : 𝕜)) 2
hs' : Ne.{u_3 + 1} (α := 𝕜) (↑(#s) : 𝕜) 0
⊢ HPow.hPow (β := ℕ) x 2 ≤ HDiv.hDiv (α := 𝕜) (∑ i ∈ s, HPow.hPow (β := ℕ) (f i) 2) (↑(#s) : 𝕜)

Tactic:
hs.trans sum_div_card_sq_le_sum_sq_div_card

Premises used: sum_div_card_sq_le_sum_sq_div_card, LE.le.trans
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Bound
Goal:
ι : Type u_2
𝕜 : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s t : Finset ι
x : 𝕜
hst : s ⊆ t
f : ι → 𝕜
hs : HPow.hPow (β := ℕ) x 2 ≤ HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ s, f i) (↑(#s) : 𝕜)) 2
hs' : Ne.{u_3 + 1} (α := 𝕜) (↑(#s) : 𝕜) 0
⊢ HPow.hPow (β := ℕ) x 2 ≤ HDiv.hDiv (α := 𝕜) (∑ i ∈ s, HPow.hPow (β := ℕ) (f i) 2) (↑(#s) : 𝕜)

Tactic:
exact hs.trans sum_div_card_sq_le_sum_sq_div_card

Premises used: sum_div_card_sq_le_sum_sq_div_card, LE.le.trans
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Bound
Goal:
ι : Type u_2
𝕜 : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s t : Finset ι
x : 𝕜
hst : s ⊆ t
f : ι → 𝕜
hs : HPow.hPow (β := ℕ) x 2 ≤ HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ s, f i) (↑(#s) : 𝕜)) 2
hs' : Ne.{u_3 + 1} (α := 𝕜) (↑(#s) : 𝕜) 0
hf : ∀ i ∈ t, i ∉ s → 0 ≤ HPow.hPow (β := ℕ) (f i) 2
⊢ LE.le.{u_3} (α := 𝕜) (∑ i ∈ s, HPow.hPow (β := ℕ) (f i) 2) (∑ i ∈ t, HPow.hPow (β := ℕ) (f i) 2)

Tactic:
gcongr
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Bound
Goal:
ι : Type u_2
𝕜 : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s t : Finset ι
x : 𝕜
hst : s ⊆ t
f : ι → 𝕜
d : 𝕜
hx : 0 ≤ x
hs : x ≤ |HDiv.hDiv (α := 𝕜) (∑ i ∈ s, f i) (↑(#s) : 𝕜) - HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)|
ht : d ≤ HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)) 2
inl :
  ∀ (hscard : Eq.{u_3 + 1} (α := 𝕜) 0 (↑(#s) : 𝕜)),
    d + HDiv.hDiv (α := 𝕜) (↑(#s) : 𝕜) (↑(#t) : 𝕜) * HPow.hPow (β := ℕ) x 2 ≤
      HDiv.hDiv (α := 𝕜) (∑ i ∈ t, HPow.hPow (β := ℕ) (f i) 2) (↑(#t) : 𝕜)
inr :
  ∀ (hscard : LT.lt.{u_3} (α := 𝕜) 0 (↑(#s) : 𝕜)),
    d + HDiv.hDiv (α := 𝕜) (↑(#s) : 𝕜) (↑(#t) : 𝕜) * HPow.hPow (β := ℕ) x 2 ≤
      HDiv.hDiv (α := 𝕜) (∑ i ∈ t, HPow.hPow (β := ℕ) (f i) 2) (↑(#t) : 𝕜)
⊢ d + HDiv.hDiv (α := 𝕜) (↑(#s) : 𝕜) (↑(#t) : 𝕜) * HPow.hPow (β := ℕ) x 2 ≤
    HDiv.hDiv (α := 𝕜) (∑ i ∈ t, HPow.hPow (β := ℕ) (f i) 2) (↑(#t) : 𝕜)

Tactic:
obtain hscard | hscard := ((#s).cast_nonneg : (0 : 𝕜) ≤ #s).eq_or_lt

Premises used: LE.le.eq_or_lt, Nat.cast_nonneg, Finset.card
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Bound
Goal:
ι : Type u_2
𝕜 : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s t : Finset ι
x : 𝕜
hst : s ⊆ t
f : ι → 𝕜
d : 𝕜
hx : 0 ≤ x
hs : x ≤ |HDiv.hDiv (α := 𝕜) (∑ i ∈ s, f i) (↑(#s) : 𝕜) - HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)|
ht : d ≤ HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)) 2
hscard : Eq.{u_3 + 1} (α := 𝕜) 0 (↑(#s) : 𝕜)
⊢ d + HDiv.hDiv (α := 𝕜) (↑(#s) : 𝕜) (↑(#t) : 𝕜) * HPow.hPow (β := ℕ) x 2 ≤
    HDiv.hDiv (α := 𝕜) (∑ i ∈ t, HPow.hPow (β := ℕ) (f i) 2) (↑(#t) : 𝕜)

Tactic:
simpa [← hscard] using ht.trans sum_div_card_sq_le_sum_sq_div_card

Premises used: sum_div_card_sq_le_sum_sq_div_card, LE.le.trans
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Bound
Goal:
ι : Type u_2
𝕜 : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s t : Finset ι
x : 𝕜
hst : s ⊆ t
f : ι → 𝕜
d : 𝕜
hx : 0 ≤ x
hs : x ≤ |HDiv.hDiv (α := 𝕜) (∑ i ∈ s, f i) (↑(#s) : 𝕜) - HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)|
ht : d ≤ HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)) 2
hscard : LT.lt.{u_3} (α := 𝕜) 0 (↑(#s) : 𝕜)
⊢ LT.lt.{u_3} (α := 𝕜) 0 (↑(#t) : 𝕜)

Tactic:
have htcard : (0 : 𝕜) < #t := hscard.trans_le (Nat.cast_le.2 (card_le_card hst))
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Bound
Goal:
ι : Type u_2
𝕜 : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s t : Finset ι
x : 𝕜
hst : s ⊆ t
f : ι → 𝕜
d : 𝕜
hx : 0 ≤ x
hs : x ≤ |HDiv.hDiv (α := 𝕜) (∑ i ∈ s, f i) (↑(#s) : 𝕜) - HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)|
ht : d ≤ HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)) 2
hscard : LT.lt.{u_3} (α := 𝕜) 0 (↑(#s) : 𝕜)
htcard : LT.lt.{u_3} (α := 𝕜) 0 (↑(#t) : 𝕜)
rwa rwa₁ rwa₂ rwa₃ : x ≤ |HDiv.hDiv (α := 𝕜) (∑ i ∈ s, f i) (↑(#s) : 𝕜) - HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)|
⊢ |x| ≤ |HDiv.hDiv (α := 𝕜) (∑ i ∈ s, f i) (↑(#s) : 𝕜) - HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)|

Tactic:
rwa [abs_of_nonneg hx]

Premises used: abs_of_nonneg
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Bound
Goal:
ι : Type u_2
𝕜 : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s t : Finset ι
x : 𝕜
hst : s ⊆ t
f : ι → 𝕜
d : 𝕜
hx : 0 ≤ x
hs : x ≤ |HDiv.hDiv (α := 𝕜) (∑ i ∈ s, f i) (↑(#s) : 𝕜) - HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)|
ht : d ≤ HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)) 2
hscard : LT.lt.{u_3} (α := 𝕜) 0 (↑(#s) : 𝕜)
htcard : LT.lt.{u_3} (α := 𝕜) 0 (↑(#t) : 𝕜)
⊢ HPow.hPow (β := ℕ) x 2 ≤
    HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ s, f i) (↑(#s) : 𝕜) - HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)) 2

Tactic:
have h₁ : x ^ 2 ≤ ((∑ i ∈ s, f i) / #s - (∑ i ∈ t, f i) / #t) ^ 2 :=
    sq_le_sq.2 (by rwa [abs_of_nonneg hx])
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Bound
Goal:
ι : Type u_2
𝕜 : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s t : Finset ι
x : 𝕜
hst : s ⊆ t
f : ι → 𝕜
d : 𝕜
hx : 0 ≤ x
hs : x ≤ |HDiv.hDiv (α := 𝕜) (∑ i ∈ s, f i) (↑(#s) : 𝕜) - HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)|
ht : d ≤ HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)) 2
hscard : LT.lt.{u_3} (α := 𝕜) 0 (↑(#s) : 𝕜)
htcard : LT.lt.{u_3} (α := 𝕜) 0 (↑(#t) : 𝕜)
h₁ :
  HPow.hPow (β := ℕ) x 2 ≤
    HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ s, f i) (↑(#s) : 𝕜) - HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)) 2
apply :
  HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ s, f i) (↑(#s) : 𝕜) - HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)) 2 ≤
    HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ s, (f i - HDiv.hDiv (α := 𝕜) (∑ j ∈ t, f j) (↑(#t) : 𝕜))) (↑(#s) : 𝕜))
      2
⊢ HPow.hPow (β := ℕ) x 2 ≤
    HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ s, (f i - HDiv.hDiv (α := 𝕜) (∑ j ∈ t, f j) (↑(#t) : 𝕜))) (↑(#s) : 𝕜))
      2

Tactic:
apply h₁.trans

Premises used: LE.le.trans
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Bound
Goal:
ι : Type u_2
𝕜 : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s t : Finset ι
x : 𝕜
hst : s ⊆ t
f : ι → 𝕜
d : 𝕜
hx : 0 ≤ x
hs : x ≤ |HDiv.hDiv (α := 𝕜) (∑ i ∈ s, f i) (↑(#s) : 𝕜) - HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)|
ht : d ≤ HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)) 2
hscard : LT.lt.{u_3} (α := 𝕜) 0 (↑(#s) : 𝕜)
htcard : LT.lt.{u_3} (α := 𝕜) 0 (↑(#t) : 𝕜)
h₁ :
  HPow.hPow (β := ℕ) x 2 ≤
    HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ s, f i) (↑(#s) : 𝕜) - HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)) 2
rw :
  HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ s, f i) (↑(#s) : 𝕜) - HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)) 2 ≤
    HPow.hPow (β := ℕ)
      (HSub.hSub (α := 𝕜) (∑ x ∈ s, f x) (∑ x ∈ s, HDiv.hDiv (α := 𝕜) (∑ j ∈ t, f j) (↑(#t) : 𝕜)) / (↑(#s) : 𝕜)) 2
rw₁ :
  HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ s, f i) (↑(#s) : 𝕜) - HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)) 2 ≤
    HPow.hPow (β := ℕ) ((∑ x ∈ s, f x - #s • HDiv.hDiv (α := 𝕜) (∑ j ∈ t, f j) (↑(#t) : 𝕜)) / (↑(#s) : 𝕜)) 2
rw₂ :
  HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ s, f i) (↑(#s) : 𝕜) - HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)) 2 ≤
    HPow.hPow (β := ℕ) ((∑ x ∈ s, f x - (↑(#s) : 𝕜) * HDiv.hDiv (α := 𝕜) (∑ j ∈ t, f j) (↑(#t) : 𝕜)) / (↑(#s) : 𝕜)) 2
rw₃ :
  HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ s, f i) (↑(#s) : 𝕜) - HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)) 2 ≤
    HPow.hPow (β := ℕ)
      (HDiv.hDiv (α := 𝕜) (∑ x ∈ s, f x) (↑(#s) : 𝕜) -
        (↑(#s) : 𝕜) * HDiv.hDiv (α := 𝕜) (∑ j ∈ t, f j) (↑(#t) : 𝕜) / (↑(#s) : 𝕜))
      2
rw₄ rw₅ :
  HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ s, f i) (↑(#s) : 𝕜) - HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)) 2 ≤
    HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ s, f i) (↑(#s) : 𝕜) - HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)) 2
⊢ HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ s, f i) (↑(#s) : 𝕜) - HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)) 2 ≤
    HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ s, (f i - HDiv.hDiv (α := 𝕜) (∑ j ∈ t, f j) (↑(#t) : 𝕜))) (↑(#s) : 𝕜))
      2

Tactic:
rw [sum_sub_distrib, sum_const, nsmul_eq_mul, sub_div, mul_div_cancel_left₀ _ hscard.ne']

Premises used: mul_div_cancel_left₀, sub_div, LT.lt.ne', Finset.sum_sub_distrib, nsmul_eq_mul, Finset.sum_const
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Bound
Goal:
ι : Type u_2
𝕜 : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s t : Finset ι
x : 𝕜
hst : s ⊆ t
f : ι → 𝕜
d : 𝕜
hx : 0 ≤ x
hs : x ≤ |HDiv.hDiv (α := 𝕜) (∑ i ∈ s, f i) (↑(#s) : 𝕜) - HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)|
ht : d ≤ HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)) 2
hscard : LT.lt.{u_3} (α := 𝕜) 0 (↑(#s) : 𝕜)
htcard : LT.lt.{u_3} (α := 𝕜) 0 (↑(#t) : 𝕜)
h₁ :
  HPow.hPow (β := ℕ) x 2 ≤
    HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ s, f i) (↑(#s) : 𝕜) - HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)) 2
⊢ HPow.hPow (β := ℕ) x 2 ≤
    HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ s, (f i - HDiv.hDiv (α := 𝕜) (∑ j ∈ t, f j) (↑(#t) : 𝕜))) (↑(#s) : 𝕜))
      2

Tactic:
have h₂ : x ^ 2 ≤ ((∑ i ∈ s, (f i - (∑ j ∈ t, f j) / #t)) / #s) ^ 2 := by
    apply h₁.trans
    rw [sum_sub_distrib, sum_const, nsmul_eq_mul, sub_div, mul_div_cancel_left₀ _ hscard.ne']
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Bound
Goal:
ι : Type u_2
𝕜 : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s t : Finset ι
x : 𝕜
hst : s ⊆ t
f : ι → 𝕜
d : 𝕜
hx : 0 ≤ x
hs : x ≤ |HDiv.hDiv (α := 𝕜) (∑ i ∈ s, f i) (↑(#s) : 𝕜) - HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)|
ht : d ≤ HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)) 2
hscard : LT.lt.{u_3} (α := 𝕜) 0 (↑(#s) : 𝕜)
htcard : LT.lt.{u_3} (α := 𝕜) 0 (↑(#t) : 𝕜)
h₁ :
  HPow.hPow (β := ℕ) x 2 ≤
    HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ s, f i) (↑(#s) : 𝕜) - HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)) 2
h₂ :
  HPow.hPow (β := ℕ) x 2 ≤
    HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ s, (f i - HDiv.hDiv (α := 𝕜) (∑ j ∈ t, f j) (↑(#t) : 𝕜))) (↑(#s) : 𝕜))
      2
inr :
  HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)) 2 +
      HDiv.hDiv (α := 𝕜) (↑(#s) : 𝕜) (↑(#t) : 𝕜) * HPow.hPow (β := ℕ) x 2 ≤
    HDiv.hDiv (α := 𝕜) (∑ i ∈ t, HPow.hPow (β := ℕ) (f i) 2) (↑(#t) : 𝕜)
⊢ d + HDiv.hDiv (α := 𝕜) (↑(#s) : 𝕜) (↑(#t) : 𝕜) * HPow.hPow (β := ℕ) x 2 ≤
    HDiv.hDiv (α := 𝕜) (∑ i ∈ t, HPow.hPow (β := ℕ) (f i) 2) (↑(#t) : 𝕜)

Tactic:
grw [ht]
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Bound
Goal:
ι : Type u_2
𝕜 : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s t : Finset ι
x : 𝕜
hst : s ⊆ t
f : ι → 𝕜
d : 𝕜
hx : 0 ≤ x
hs : x ≤ |HDiv.hDiv (α := 𝕜) (∑ i ∈ s, f i) (↑(#s) : 𝕜) - HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)|
ht : d ≤ HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)) 2
hscard : LT.lt.{u_3} (α := 𝕜) 0 (↑(#s) : 𝕜)
htcard : LT.lt.{u_3} (α := 𝕜) 0 (↑(#t) : 𝕜)
h₁ :
  HPow.hPow (β := ℕ) x 2 ≤
    HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ s, f i) (↑(#s) : 𝕜) - HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)) 2
h₂ :
  HPow.hPow (β := ℕ) x 2 ≤
    HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ s, (f i - HDiv.hDiv (α := 𝕜) (∑ j ∈ t, f j) (↑(#t) : 𝕜))) (↑(#s) : 𝕜))
      2
inr :
  HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)) 2 * (↑(#t) : 𝕜) +
      (↑(#s) : 𝕜) * HPow.hPow (β := ℕ) x 2 ≤
    ∑ i ∈ t, HPow.hPow (β := ℕ) (f i) 2
⊢ HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)) 2 +
      HDiv.hDiv (α := 𝕜) (↑(#s) : 𝕜) (↑(#t) : 𝕜) * HPow.hPow (β := ℕ) x 2 ≤
    HDiv.hDiv (α := 𝕜) (∑ i ∈ t, HPow.hPow (β := ℕ) (f i) 2) (↑(#t) : 𝕜)

Tactic:
rw [← mul_div_right_comm, le_div_iff₀ htcard, add_mul, div_mul_cancel₀ _ htcard.ne']

Premises used: add_mul, div_mul_cancel₀, mul_div_right_comm, LT.lt.ne', le_div_iff₀
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Bound
Goal:
ι : Type u_2
𝕜 : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s t : Finset ι
x : 𝕜
hst : s ⊆ t
f : ι → 𝕜
d : 𝕜
hx : 0 ≤ x
hs : x ≤ |HDiv.hDiv (α := 𝕜) (∑ i ∈ s, f i) (↑(#s) : 𝕜) - HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)|
ht : d ≤ HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)) 2
hscard : LT.lt.{u_3} (α := 𝕜) 0 (↑(#s) : 𝕜)
htcard : LT.lt.{u_3} (α := 𝕜) 0 (↑(#t) : 𝕜)
h₁ :
  HPow.hPow (β := ℕ) x 2 ≤
    HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ s, f i) (↑(#s) : 𝕜) - HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)) 2
h₂ :
  HPow.hPow (β := ℕ) x 2 ≤
    HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ s, (f i - HDiv.hDiv (α := 𝕜) (∑ j ∈ t, f j) (↑(#t) : 𝕜))) (↑(#s) : 𝕜))
      2
⊢ (↑(#s) : 𝕜) * HPow.hPow (β := ℕ) x 2 ≤
    ∑ i ∈ t, HPow.hPow (α := 𝕜) (β := ℕ) ((fun (i : ι) ↦ f i - HDiv.hDiv (α := 𝕜) (∑ j ∈ t, f j) (↑(#t) : 𝕜)) i) 2

Tactic:
have h₃ := mul_sq_le_sum_sq hst (fun i => (f i - (∑ j ∈ t, f j) / #t)) h₂ hscard.ne'
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Bound
Goal:
ι : Type u_2
𝕜 : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s t : Finset ι
x : 𝕜
hst : s ⊆ t
f : ι → 𝕜
d : 𝕜
hx : 0 ≤ x
hs : x ≤ |HDiv.hDiv (α := 𝕜) (∑ i ∈ s, f i) (↑(#s) : 𝕜) - HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)|
ht : d ≤ HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)) 2
hscard : LT.lt.{u_3} (α := 𝕜) 0 (↑(#s) : 𝕜)
htcard : LT.lt.{u_3} (α := 𝕜) 0 (↑(#t) : 𝕜)
h₁ :
  HPow.hPow (β := ℕ) x 2 ≤
    HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ s, f i) (↑(#s) : 𝕜) - HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)) 2
h₂ :
  HPow.hPow (β := ℕ) x 2 ≤
    HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ s, (f i - HDiv.hDiv (α := 𝕜) (∑ j ∈ t, f j) (↑(#t) : 𝕜))) (↑(#s) : 𝕜))
      2
h₃ :
  (↑(#s) : 𝕜) * HPow.hPow (β := ℕ) x 2 ≤
    ∑ i ∈ t, HPow.hPow (α := 𝕜) (β := ℕ) ((fun (i : ι) ↦ f i - HDiv.hDiv (α := 𝕜) (∑ j ∈ t, f j) (↑(#t) : 𝕜)) i) 2
inr :
  HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)) 2 * (↑(#t) : 𝕜) +
      ∑ i ∈ t, HPow.hPow (α := 𝕜) (β := ℕ) ((fun (i : ι) ↦ f i - HDiv.hDiv (α := 𝕜) (∑ j ∈ t, f j) (↑(#t) : 𝕜)) i) 2 ≤
    ∑ i ∈ t, HPow.hPow (β := ℕ) (f i) 2
⊢ HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)) 2 * (↑(#t) : 𝕜) +
      (↑(#s) : 𝕜) * HPow.hPow (β := ℕ) x 2 ≤
    ∑ i ∈ t, HPow.hPow (β := ℕ) (f i) 2

Tactic:
grw [h₃]
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Bound
Goal:
ι : Type u_2
𝕜 : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s t : Finset ι
x : 𝕜
hst : s ⊆ t
f : ι → 𝕜
d : 𝕜
hx : 0 ≤ x
hs : x ≤ |HDiv.hDiv (α := 𝕜) (∑ i ∈ s, f i) (↑(#s) : 𝕜) - HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)|
ht : d ≤ HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)) 2
hscard : LT.lt.{u_3} (α := 𝕜) 0 (↑(#s) : 𝕜)
htcard : LT.lt.{u_3} (α := 𝕜) 0 (↑(#t) : 𝕜)
h₁ :
  HPow.hPow (β := ℕ) x 2 ≤
    HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ s, f i) (↑(#s) : 𝕜) - HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)) 2
h₂ :
  HPow.hPow (β := ℕ) x 2 ≤
    HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ s, (f i - HDiv.hDiv (α := 𝕜) (∑ j ∈ t, f j) (↑(#t) : 𝕜))) (↑(#s) : 𝕜))
      2
h₃ :
  (↑(#s) : 𝕜) * HPow.hPow (β := ℕ) x 2 ≤
    ∑ i ∈ t, HPow.hPow (α := 𝕜) (β := ℕ) ((fun (i : ι) ↦ f i - HDiv.hDiv (α := 𝕜) (∑ j ∈ t, f j) (↑(#t) : 𝕜)) i) 2
inr :
  HPow.hPow (α := 𝕜) (β := ℕ) (∑ i ∈ t, f i) 2 * (↑(#t) : 𝕜) +
      ((∑ i ∈ t, HPow.hPow (β := ℕ) (f i) 2) * HPow.hPow (α := 𝕜) (β := ℕ) (↑(#t) : 𝕜) 2 -
          (HMul.hMul (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜) + HMul.hMul (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)) *
            ∑ i ∈ t, f i +
        (↑(#t) : 𝕜) * HPow.hPow (α := 𝕜) (β := ℕ) (∑ i ∈ t, f i) 2) ≤
    (∑ i ∈ t, HPow.hPow (β := ℕ) (f i) 2) * HPow.hPow (α := 𝕜) (β := ℕ) (↑(#t) : 𝕜) 2
⊢ HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)) 2 * (↑(#t) : 𝕜) +
      ∑ i ∈ t, HPow.hPow (α := 𝕜) (β := ℕ) ((fun (i : ι) ↦ f i - HDiv.hDiv (α := 𝕜) (∑ j ∈ t, f j) (↑(#t) : 𝕜)) i) 2 ≤
    ∑ i ∈ t, HPow.hPow (β := ℕ) (f i) 2

Tactic:
simp only [sub_div' htcard.ne', div_pow, ← sum_div, ← mul_div_right_comm _ (#t : 𝕜), ← add_div,
    div_le_iff₀ (sq_pos_of_ne_zero htcard.ne'), sub_sq, sum_add_distrib, sum_const,
    sum_sub_distrib, mul_pow, ← sum_mul, nsmul_eq_mul, two_mul]

Premises used: div_le_iff₀, sub_sq, Finset.sum_add_distrib, two_mul, Nat.cast, mul_div_right_comm, LT.lt.ne', Finset.sum_div, Finset.sum_sub_distrib, div_pow, Finset.card, nsmul_eq_mul, sq_pos_of_ne_zero, mul_pow, sub_div', Finset.sum_mul, Finset.sum_const, add_div
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Bound
Goal:
ι : Type u_2
𝕜 : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s t : Finset ι
x : 𝕜
hst : s ⊆ t
f : ι → 𝕜
d : 𝕜
hx : 0 ≤ x
hs : x ≤ |HDiv.hDiv (α := 𝕜) (∑ i ∈ s, f i) (↑(#s) : 𝕜) - HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)|
ht : d ≤ HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)) 2
hscard : LT.lt.{u_3} (α := 𝕜) 0 (↑(#s) : 𝕜)
htcard : LT.lt.{u_3} (α := 𝕜) 0 (↑(#t) : 𝕜)
h₁ :
  HPow.hPow (β := ℕ) x 2 ≤
    HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ s, f i) (↑(#s) : 𝕜) - HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)) 2
h₂ :
  HPow.hPow (β := ℕ) x 2 ≤
    HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ s, (f i - HDiv.hDiv (α := 𝕜) (∑ j ∈ t, f j) (↑(#t) : 𝕜))) (↑(#s) : 𝕜))
      2
h₃ :
  (↑(#s) : 𝕜) * HPow.hPow (β := ℕ) x 2 ≤
    ∑ i ∈ t, HPow.hPow (α := 𝕜) (β := ℕ) ((fun (i : ι) ↦ f i - HDiv.hDiv (α := 𝕜) (∑ j ∈ t, f j) (↑(#t) : 𝕜)) i) 2
inr :
  HPow.hPow (α := 𝕜) (β := ℕ) (↑(#t) : 𝕜) 2 * ∑ x ∈ t, HPow.hPow (β := ℕ) (f x) 2 ≤
    HPow.hPow (α := 𝕜) (β := ℕ) (↑(#t) : 𝕜) 2 * ∑ x ∈ t, HPow.hPow (β := ℕ) (f x) 2
⊢ HPow.hPow (α := 𝕜) (β := ℕ) (∑ i ∈ t, f i) 2 * (↑(#t) : 𝕜) +
      ((∑ i ∈ t, HPow.hPow (β := ℕ) (f i) 2) * HPow.hPow (α := 𝕜) (β := ℕ) (↑(#t) : 𝕜) 2 -
          (HMul.hMul (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜) + HMul.hMul (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)) *
            ∑ i ∈ t, f i +
        (↑(#t) : 𝕜) * HPow.hPow (α := 𝕜) (β := ℕ) (∑ i ∈ t, f i) 2) ≤
    (∑ i ∈ t, HPow.hPow (β := ℕ) (f i) 2) * HPow.hPow (α := 𝕜) (β := ℕ) (↑(#t) : 𝕜) 2

Tactic:
ring_nf
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Bound
Goal:
ι : Type u_2
𝕜 : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s t : Finset ι
x : 𝕜
hst : s ⊆ t
f : ι → 𝕜
d : 𝕜
hx : 0 ≤ x
hs : x ≤ |HDiv.hDiv (α := 𝕜) (∑ i ∈ s, f i) (↑(#s) : 𝕜) - HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)|
ht : d ≤ HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)) 2
hscard : LT.lt.{u_3} (α := 𝕜) 0 (↑(#s) : 𝕜)
htcard : LT.lt.{u_3} (α := 𝕜) 0 (↑(#t) : 𝕜)
h₁ :
  HPow.hPow (β := ℕ) x 2 ≤
    HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ s, f i) (↑(#s) : 𝕜) - HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)) 2
h₂ :
  HPow.hPow (β := ℕ) x 2 ≤
    HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ s, (f i - HDiv.hDiv (α := 𝕜) (∑ j ∈ t, f j) (↑(#t) : 𝕜))) (↑(#s) : 𝕜))
      2
h₃ :
  (↑(#s) : 𝕜) * HPow.hPow (β := ℕ) x 2 ≤
    ∑ i ∈ t, HPow.hPow (α := 𝕜) (β := ℕ) ((fun (i : ι) ↦ f i - HDiv.hDiv (α := 𝕜) (∑ j ∈ t, f j) (↑(#t) : 𝕜)) i) 2
⊢ HPow.hPow (α := 𝕜) (β := ℕ) (↑(#t) : 𝕜) 2 * ∑ x ∈ t, HPow.hPow (β := ℕ) (f x) 2 ≤
    HPow.hPow (α := 𝕜) (β := ℕ) (↑(#t) : 𝕜) 2 * ∑ x ∈ t, HPow.hPow (β := ℕ) (f x) 2

Tactic:
rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Bound
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
P : Finpartition (α := Finset α) univ
u : Finset α
ε_1 ε : ℝ
l : ℕ
⊢ 0 < initialBound ε l

Tactic:
positivity
-- Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Bound
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
P : Finpartition (α := Finset α) univ
u : Finset α
ε_1 ε : ℝ
l : ℕ
⊢ 0 < bound ε l

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 α
⊢ (star hP G ε hU V).biUnion id ⊆ G.nonuniformWitness ε U V

Tactic:
biUnion_subset_iff_forall_subset.2 fun _ hA => (mem_filter.1 hA).2

Premises used: Iff.mpr, Finset.biUnion_subset_iff_forall_subset, And.right, Iff.mp, Finset.mem_filter
-- 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
h₂ : ¬G.IsUniform ε U V
⊢ G.nonuniformWitness ε U V ∈ P.nonuniformWitnesses G ε U

Tactic:
have hX : G.nonuniformWitness ε U V ∈ P.nonuniformWitnesses G ε U :=
    nonuniformWitness_mem_nonuniformWitnesses h₂ hV 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 : Finset α
hU : U ∈ P.parts
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
h₂ : ¬G.IsUniform ε U V
hX : G.nonuniformWitness ε U V ∈ P.nonuniformWitnesses G ε U
x : α
hx : x ∈ G.nonuniformWitness ε U V \ (star hP G ε hU V).biUnion id
⊢ (∃ a ∈ {u ∈ parts (atomise U (P.nonuniformWitnesses G ε U)) | u ⊆ G.nonuniformWitness ε U V ∧ u.Nonempty}, x ∈ id a) ∧
    x ∉ {A ∈ (chunk hP G ε hU).parts | A ⊆ G.nonuniformWitness ε U V}.biUnion id

Tactic:
rw [← biUnion_filter_atomise hX (G.nonuniformWitness_subset h₂), star, mem_sdiff,
      mem_biUnion] at hx

Premises used: SzemerediRegularity.star, Finset.mem_sdiff, Finpartition.biUnion_filter_atomise, SimpleGraph.nonuniformWitness_subset, Finset.mem_biUnion