case refine'_1
α : Type ?u.566246
β : Type ?u.566249
n✝ d✝ k N : ℕ
x✝ : Fin n✝ → ℕ
n d : ℕ
x : Fin n → ℕ
hx : x ∈ box n d
⊢ ∑ i : Fin n, x i ^ 2 ∈ range (n * (d - 1) ^ 2 + 1)

case refine'_2
α : Type ?u.566246
β : Type ?u.566249
n✝ d✝ k N : ℕ
x : Fin n✝ → ℕ
n d : ℕ
⊢ card (range (n * (d - 1) ^ 2 + 1)) • (↑(d ^ n) / (↑(n * (d - 1) ^ 2) + 1)) ≤ ↑(card (box n d))
α : Type ?u.566246
β : Type ?u.566249
n✝ d✝ k N : ℕ
x : Fin n✝ → ℕ
n d : ℕ
⊢ ∃ k, k ∈ range (n * (d - 1) ^ 2 + 1) ∧ ↑(d ^ n) / (↑(n * (d - 1) ^ 2) + 1) ≤ ↑(card (sphere n d k))
refine' exists_le_card_fiber_of_nsmul_le_card_of_maps_to (fun x hx => _) nonempty_range_succ _
case refine'_1
α : Type ?u.566246
β : Type ?u.566249
n✝ d✝ k N : ℕ
x✝ : Fin n✝ → ℕ
n d : ℕ
x : Fin n → ℕ
hx : x ∈ box n d
⊢ ∑ i : Fin n, x i ^ 2 ≤ n * (d - 1) ^ 2
case refine'_1
α : Type ?u.566246
β : Type ?u.566249
n✝ d✝ k N : ℕ
x✝ : Fin n✝ → ℕ
n d : ℕ
x : Fin n → ℕ
hx : x ∈ box n d
⊢ ∑ i : Fin n, x i ^ 2 ∈ range (n * (d - 1) ^ 2 + 1)
rw [mem_range, lt_succ_iff]
no goals
case refine'_1
α : Type ?u.566246
β : Type ?u.566249
n✝ d✝ k N : ℕ
x✝ : Fin n✝ → ℕ
n d : ℕ
x : Fin n → ℕ
hx : x ∈ box n d
⊢ ∑ i : Fin n, x i ^ 2 ≤ n * (d - 1) ^ 2
exact sum_sq_le_of_mem_box hx
case refine'_2.ha
α : Type ?u.566246
β : Type ?u.566249
n✝ d✝ k N : ℕ
x : Fin n✝ → ℕ
n d : ℕ
⊢ ↑(n * (d - 1) ^ 2) + 1 ≠ 0
case refine'_2
α : Type ?u.566246
β : Type ?u.566249
n✝ d✝ k N : ℕ
x : Fin n✝ → ℕ
n d : ℕ
⊢ card (range (n * (d - 1) ^ 2 + 1)) • (↑(d ^ n) / (↑(n * (d - 1) ^ 2) + 1)) ≤ ↑(card (box n d))
rw [card_range, _root_.nsmul_eq_mul, mul_div_assoc', cast_add_one, mul_div_cancel_left,
  card_box]
no goals
case refine'_2.ha
α : Type ?u.566246
β : Type ?u.566249
n✝ d✝ k N : ℕ
x : Fin n✝ → ℕ
n d : ℕ
⊢ ↑(n * (d - 1) ^ 2) + 1 ≠ 0
exact (cast_add_one_pos _).ne'