-- Mathlib/Combinatorics/SimpleGraph/Regularity/Bound.lean
theorem add_div_le_sum_sq_div_card (hst : s ⊆ t) (f : ι → 𝕜) (d : 𝕜) (hx : 0 ≤ x)
    (hs : x ≤ |(∑ i ∈ s, f i) / #s - (∑ i ∈ t, f i) / #t|) (ht : d ≤ ((∑ i ∈ t, f i) / #t) ^ 2) :
    d + #s / #t * x ^ 2 ≤ (∑ i ∈ t, f i ^ 2) / #t

Proof state:
case inr
ι : Type u_2
𝕜 : Type u_3
inst✝ : LinearOrderedField 𝕜
s t : Finset ι
x : 𝕜
hst : s ⊆ t
f : ι → 𝕜
d : 𝕜
hx : 0 ≤ x
hs : x ≤ |(∑ i ∈ s, f i) / ↑(#s) - (∑ i ∈ t, f i) / ↑(#t)|
ht : d ≤ ((∑ i ∈ t, f i) / ↑(#t)) ^ 2
hscard : 0 < ↑(#s)
htcard : 0 < ↑(#t)
h₁ : x ^ 2 ≤ ((∑ i ∈ s, f i) / ↑(#s) - (∑ i ∈ t, f i) / ↑(#t)) ^ 2
h₂ : x ^ 2 ≤ ((∑ i ∈ s, (f i - (∑ j ∈ t, f j) / ↑(#t))) / ↑(#s)) ^ 2
h₃ : ↑(#s) * x ^ 2 ≤ ∑ i ∈ t, (fun i => f i - (∑ j ∈ t, f j) / ↑(#t)) i ^ 2
⊢ ((∑ i ∈ t, f i) / ↑(#t)) ^ 2 * ↑(#t) + ∑ i ∈ t, (fun i => f i - (∑ j ∈ t, f j) / ↑(#t)) i ^ 2 ≤ ∑ i ∈ t, f i ^ 2

Tactic:
simp_rw [sub_div' htcard.ne']

Result:
case inr
ι : Type u_2
𝕜 : Type u_3
inst✝ : LinearOrderedField 𝕜
s t : Finset ι
x : 𝕜
hst : s ⊆ t
f : ι → 𝕜
d : 𝕜
hx : 0 ≤ x
hs : x ≤ |(∑ i ∈ s, f i) / ↑(#s) - (∑ i ∈ t, f i) / ↑(#t)|
ht : d ≤ ((∑ i ∈ t, f i) / ↑(#t)) ^ 2
hscard : 0 < ↑(#s)
htcard : 0 < ↑(#t)
h₁ : x ^ 2 ≤ ((∑ i ∈ s, f i) / ↑(#s) - (∑ i ∈ t, f i) / ↑(#t)) ^ 2
h₂ : x ^ 2 ≤ ((∑ i ∈ s, (f i - (∑ j ∈ t, f j) / ↑(#t))) / ↑(#s)) ^ 2
h₃ : ↑(#s) * x ^ 2 ≤ ∑ i ∈ t, (fun i => f i - (∑ j ∈ t, f j) / ↑(#t)) i ^ 2
⊢ ((∑ i ∈ t, f i) / ↑(#t)) ^ 2 * ↑(#t) + ∑ x ∈ t, ((f x * ↑(#t) - ∑ i ∈ t, f i) / ↑(#t)) ^ 2 ≤ ∑ i ∈ t, f i ^ 2

Proof state:
ι : Type u_2
𝕜 : Type u_3
inst✝ : LinearOrderedField 𝕜
s t : Finset ι
x : 𝕜
hst : s ⊆ t
f : ι → 𝕜
d : 𝕜
hx : 0 ≤ x
hs : x ≤ |(∑ i ∈ s, f i) / ↑(#s) - (∑ i ∈ t, f i) / ↑(#t)|
ht : d ≤ ((∑ i ∈ t, f i) / ↑(#t)) ^ 2
⊢ d + ↑(#s) / ↑(#t) * x ^ 2 ≤ (∑ i ∈ t, f i ^ 2) / ↑(#t)

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

Result:
case inl
ι : Type u_2
𝕜 : Type u_3
inst✝ : LinearOrderedField 𝕜
s t : Finset ι
x : 𝕜
hst : s ⊆ t
f : ι → 𝕜
d : 𝕜
hx : 0 ≤ x
hs : x ≤ |(∑ i ∈ s, f i) / ↑(#s) - (∑ i ∈ t, f i) / ↑(#t)|
ht : d ≤ ((∑ i ∈ t, f i) / ↑(#t)) ^ 2
hscard : 0 = ↑(#s)
⊢ d + ↑(#s) / ↑(#t) * x ^ 2 ≤ (∑ i ∈ t, f i ^ 2) / ↑(#t)

case inr
ι : Type u_2
𝕜 : Type u_3
inst✝ : LinearOrderedField 𝕜
s t : Finset ι
x : 𝕜
hst : s ⊆ t
f : ι → 𝕜
d : 𝕜
hx : 0 ≤ x
hs : x ≤ |(∑ i ∈ s, f i) / ↑(#s) - (∑ i ∈ t, f i) / ↑(#t)|
ht : d ≤ ((∑ i ∈ t, f i) / ↑(#t)) ^ 2
hscard : 0 < ↑(#s)
⊢ d + ↑(#s) / ↑(#t) * x ^ 2 ≤ (∑ i ∈ t, f i ^ 2) / ↑(#t)

Proof state:
case inr
ι : Type u_2
𝕜 : Type u_3
inst✝ : LinearOrderedField 𝕜
s t : Finset ι
x : 𝕜
hst : s ⊆ t
f : ι → 𝕜
d : 𝕜
hx : 0 ≤ x
hs : x ≤ |(∑ i ∈ s, f i) / ↑(#s) - (∑ i ∈ t, f i) / ↑(#t)|
ht : d ≤ ((∑ i ∈ t, f i) / ↑(#t)) ^ 2
hscard : 0 < ↑(#s)
htcard : 0 < ↑(#t)
h₁ : x ^ 2 ≤ ((∑ i ∈ s, f i) / ↑(#s) - (∑ i ∈ t, f i) / ↑(#t)) ^ 2
h₂ : x ^ 2 ≤ ((∑ i ∈ s, (f i - (∑ j ∈ t, f j) / ↑(#t))) / ↑(#s)) ^ 2
h₃ : ↑(#s) * x ^ 2 ≤ ∑ i ∈ t, (fun i => f i - (∑ j ∈ t, f j) / ↑(#t)) i ^ 2
⊢ (∑ i ∈ t, f i) ^ 2 * ↑(#t) + ∑ i ∈ t, (f i * ↑(#t) - ∑ i ∈ t, f i) ^ 2 ≤ (∑ i ∈ t, f i ^ 2) * ↑(#t) ^ 2

Tactic:
simp_rw [sub_sq, sum_add_distrib, sum_const, nsmul_eq_mul, sum_sub_distrib, mul_pow, ← sum_mul,
  ← mul_sum, ← sum_mul]

Result:
case inr
ι : Type u_2
𝕜 : Type u_3
inst✝ : LinearOrderedField 𝕜
s t : Finset ι
x : 𝕜
hst : s ⊆ t
f : ι → 𝕜
d : 𝕜
hx : 0 ≤ x
hs : x ≤ |(∑ i ∈ s, f i) / ↑(#s) - (∑ i ∈ t, f i) / ↑(#t)|
ht : d ≤ ((∑ i ∈ t, f i) / ↑(#t)) ^ 2
hscard : 0 < ↑(#s)
htcard : 0 < ↑(#t)
h₁ : x ^ 2 ≤ ((∑ i ∈ s, f i) / ↑(#s) - (∑ i ∈ t, f i) / ↑(#t)) ^ 2
h₂ : x ^ 2 ≤ ((∑ i ∈ s, (f i - (∑ j ∈ t, f j) / ↑(#t))) / ↑(#s)) ^ 2
h₃ : ↑(#s) * x ^ 2 ≤ ∑ i ∈ t, (fun i => f i - (∑ j ∈ t, f j) / ↑(#t)) i ^ 2
⊢ (∑ i ∈ t, f i) ^ 2 * ↑(#t) +
      ((∑ i ∈ t, f i ^ 2) * ↑(#t) ^ 2 - 2 * ((∑ i ∈ t, f i) * ↑(#t)) * ∑ i ∈ t, f i + ↑(#t) * (∑ i ∈ t, f i) ^ 2) ≤
    (∑ i ∈ t, f i ^ 2) * ↑(#t) ^ 2

Proof state:
case inr
ι : Type u_2
𝕜 : Type u_3
inst✝ : LinearOrderedField 𝕜
s t : Finset ι
x : 𝕜
hst : s ⊆ t
f : ι → 𝕜
d : 𝕜
hx : 0 ≤ x
hs : x ≤ |(∑ i ∈ s, f i) / ↑(#s) - (∑ i ∈ t, f i) / ↑(#t)|
ht : d ≤ ((∑ i ∈ t, f i) / ↑(#t)) ^ 2
hscard : 0 < ↑(#s)
htcard : 0 < ↑(#t)
h₁ : x ^ 2 ≤ ((∑ i ∈ s, f i) / ↑(#s) - (∑ i ∈ t, f i) / ↑(#t)) ^ 2
h₂ : x ^ 2 ≤ ((∑ i ∈ s, (f i - (∑ j ∈ t, f j) / ↑(#t))) / ↑(#s)) ^ 2
h₃ : ↑(#s) * x ^ 2 ≤ ∑ i ∈ t, (fun i => f i - (∑ j ∈ t, f j) / ↑(#t)) i ^ 2
⊢ (∑ i ∈ t, f i) ^ 2 * ↑(#t) +
      ((∑ i ∈ t, f i ^ 2) * ↑(#t) ^ 2 - 2 * ((∑ i ∈ t, f i) * ↑(#t)) * ∑ i ∈ t, f i + ↑(#t) * (∑ i ∈ t, f i) ^ 2) ≤
    (∑ i ∈ t, f i ^ 2) * ↑(#t) ^ 2

Tactic:
ring_nf

Result:
case inr
ι : Type u_2
𝕜 : Type u_3
inst✝ : LinearOrderedField 𝕜
s t : Finset ι
x : 𝕜
hst : s ⊆ t
f : ι → 𝕜
d : 𝕜
hx : 0 ≤ x
hs : x ≤ |(∑ i ∈ s, f i) / ↑(#s) - (∑ i ∈ t, f i) / ↑(#t)|
ht : d ≤ ((∑ i ∈ t, f i) / ↑(#t)) ^ 2
hscard : 0 < ↑(#s)
htcard : 0 < ↑(#t)
h₁ : x ^ 2 ≤ ((∑ i ∈ s, f i) / ↑(#s) - (∑ i ∈ t, f i) / ↑(#t)) ^ 2
h₂ : x ^ 2 ≤ ((∑ i ∈ s, (f i - (∑ j ∈ t, f j) / ↑(#t))) / ↑(#s)) ^ 2
h₃ : ↑(#s) * x ^ 2 ≤ ∑ i ∈ t, (fun i => f i - (∑ j ∈ t, f j) / ↑(#t)) i ^ 2
⊢ ↑(#t) ^ 2 * ∑ x ∈ t, f x ^ 2 ≤ ↑(#t) ^ 2 * ∑ x ∈ t, f x ^ 2

Proof state:
ι : Type u_2
𝕜 : Type u_3
inst✝ : LinearOrderedField 𝕜
s t : Finset ι
x : 𝕜
hst : s ⊆ t
f : ι → 𝕜
d : 𝕜
hx : 0 ≤ x
hs : x ≤ |(∑ i ∈ s, f i) / ↑(#s) - (∑ i ∈ t, f i) / ↑(#t)|
ht : d ≤ ((∑ i ∈ t, f i) / ↑(#t)) ^ 2
hscard : 0 < ↑(#s)
htcard : 0 < ↑(#t)
h₁ : x ^ 2 ≤ ((∑ i ∈ s, f i) / ↑(#s) - (∑ i ∈ t, f i) / ↑(#t)) ^ 2
⊢ ((∑ i ∈ s, f i) / ↑(#s) - (∑ i ∈ t, f i) / ↑(#t)) ^ 2 ≤ ((∑ i ∈ s, (f i - (∑ 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']

Result:
no goals

Proof state:
case inr
ι : Type u_2
𝕜 : Type u_3
inst✝ : LinearOrderedField 𝕜
s t : Finset ι
x : 𝕜
hst : s ⊆ t
f : ι → 𝕜
d : 𝕜
hx : 0 ≤ x
hs : x ≤ |(∑ i ∈ s, f i) / ↑(#s) - (∑ i ∈ t, f i) / ↑(#t)|
ht : d ≤ ((∑ i ∈ t, f i) / ↑(#t)) ^ 2
hscard : 0 < ↑(#s)
htcard : 0 < ↑(#t)
h₁ : x ^ 2 ≤ ((∑ i ∈ s, f i) / ↑(#s) - (∑ i ∈ t, f i) / ↑(#t)) ^ 2
h₂ : x ^ 2 ≤ ((∑ i ∈ s, (f i - (∑ j ∈ t, f j) / ↑(#t))) / ↑(#s)) ^ 2
⊢ ((∑ i ∈ t, f i) / ↑(#t)) ^ 2 * ↑(#t) + ↑(#s) * x ^ 2 ≤ ∑ i ∈ t, f i ^ 2

Tactic:
have h₃ := mul_sq_le_sum_sq hst (fun i => (f i - (∑ j ∈ t, f j) / #t)) h₂ hscard.ne'

Result:
case inr
ι : Type u_2
𝕜 : Type u_3
inst✝ : LinearOrderedField 𝕜
s t : Finset ι
x : 𝕜
hst : s ⊆ t
f : ι → 𝕜
d : 𝕜
hx : 0 ≤ x
hs : x ≤ |(∑ i ∈ s, f i) / ↑(#s) - (∑ i ∈ t, f i) / ↑(#t)|
ht : d ≤ ((∑ i ∈ t, f i) / ↑(#t)) ^ 2
hscard : 0 < ↑(#s)
htcard : 0 < ↑(#t)
h₁ : x ^ 2 ≤ ((∑ i ∈ s, f i) / ↑(#s) - (∑ i ∈ t, f i) / ↑(#t)) ^ 2
h₂ : x ^ 2 ≤ ((∑ i ∈ s, (f i - (∑ j ∈ t, f j) / ↑(#t))) / ↑(#s)) ^ 2
h₃ : ↑(#s) * x ^ 2 ≤ ∑ i ∈ t, (fun i => f i - (∑ j ∈ t, f j) / ↑(#t)) i ^ 2
⊢ ((∑ i ∈ t, f i) / ↑(#t)) ^ 2 * ↑(#t) + ↑(#s) * x ^ 2 ≤ ∑ i ∈ t, f i ^ 2

Proof state:
case inr
ι : Type u_2
𝕜 : Type u_3
inst✝ : LinearOrderedField 𝕜
s t : Finset ι
x : 𝕜
hst : s ⊆ t
f : ι → 𝕜
d : 𝕜
hx : 0 ≤ x
hs : x ≤ |(∑ i ∈ s, f i) / ↑(#s) - (∑ i ∈ t, f i) / ↑(#t)|
ht : d ≤ ((∑ i ∈ t, f i) / ↑(#t)) ^ 2
hscard : 0 < ↑(#s)
htcard : 0 < ↑(#t)
h₁ : x ^ 2 ≤ ((∑ i ∈ s, f i) / ↑(#s) - (∑ i ∈ t, f i) / ↑(#t)) ^ 2
⊢ d + ↑(#s) / ↑(#t) * x ^ 2 ≤ (∑ i ∈ t, f i ^ 2) / ↑(#t)

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']

Result:
case inr
ι : Type u_2
𝕜 : Type u_3
inst✝ : LinearOrderedField 𝕜
s t : Finset ι
x : 𝕜
hst : s ⊆ t
f : ι → 𝕜
d : 𝕜
hx : 0 ≤ x
hs : x ≤ |(∑ i ∈ s, f i) / ↑(#s) - (∑ i ∈ t, f i) / ↑(#t)|
ht : d ≤ ((∑ i ∈ t, f i) / ↑(#t)) ^ 2
hscard : 0 < ↑(#s)
htcard : 0 < ↑(#t)
h₁ : x ^ 2 ≤ ((∑ i ∈ s, f i) / ↑(#s) - (∑ i ∈ t, f i) / ↑(#t)) ^ 2
h₂ : x ^ 2 ≤ ((∑ i ∈ s, (f i - (∑ j ∈ t, f j) / ↑(#t))) / ↑(#s)) ^ 2
⊢ d + ↑(#s) / ↑(#t) * x ^ 2 ≤ (∑ i ∈ t, f i ^ 2) / ↑(#t)