α : Type ?u.502797
β : Type ?u.502800
n d k N : ℕ
x : Fin n → ℕ
hx : ∀ (i : Fin n), x i < d
⊢ ∑ i : Fin n, x i ^ 2 ≤ n * (d - 1) ^ 2
α : Type ?u.502797
β : Type ?u.502800
n d k N : ℕ
x : Fin n → ℕ
hx : x ∈ box n d
⊢ ∑ i : Fin n, x i ^ 2 ≤ n * (d - 1) ^ 2
rw [mem_box] at hx
α : Type ?u.502797
β : Type ?u.502800
n d k N : ℕ
x : Fin n → ℕ
hx : ∀ (i : Fin n), x i < d
this : ∀ (i : Fin n), x i ^ 2 ≤ (d - 1) ^ 2
⊢ ∑ i : Fin n, x i ^ 2 ≤ n * (d - 1) ^ 2
α : Type ?u.502797
β : Type ?u.502800
n d k N : ℕ
x : Fin n → ℕ
hx : ∀ (i : Fin n), x i < d
⊢ ∑ i : Fin n, x i ^ 2 ≤ n * (d - 1) ^ 2
have : ∀ i, x i ^ 2 ≤ (d - 1) ^ 2 := fun i =>
  Nat.pow_le_pow_of_le_left (Nat.le_pred_of_lt (hx i)) _
no goals
α : Type ?u.502797
β : Type ?u.502800
n d k N : ℕ
x : Fin n → ℕ
hx : ∀ (i : Fin n), x i < d
this : ∀ (i : Fin n), x i ^ 2 ≤ (d - 1) ^ 2
⊢ ∑ i : Fin n, x i ^ 2 ≤ n * (d - 1) ^ 2
exact (sum_le_card_nsmul univ _ _ fun i _ => this i).trans (by rw [card_fin, smul_eq_mul])
no goals
α : Type ?u.502797
β : Type ?u.502800
n d k N : ℕ
x : Fin n → ℕ
hx : ∀ (i : Fin n), x i < d
this : ∀ (i : Fin n), x i ^ 2 ≤ (d - 1) ^ 2
⊢ card univ • (d - 1) ^ 2 ≤ n * (d - 1) ^ 2
rw [card_fin, smul_eq_mul]