α : Type ?u.783410
β : Type ?u.783413
n d k N : ℕ
x : Fin n → ℕ
hN : 2 ≤ N
this : (2 * dValue N - 1) ^ nValue N ≤ (2 * dValue N) ^ nValue N
⊢ (2 * dValue N - 1) ^ nValue N ≤ N
α : Type ?u.783410
β : Type ?u.783413
n d k N : ℕ
x : Fin n → ℕ
hN : 2 ≤ N
⊢ (2 * dValue N - 1) ^ nValue N ≤ N
have : (2 * dValue N - 1) ^ nValue N ≤ (2 * dValue N) ^ nValue N :=
  Nat.pow_le_pow_of_le_left (Nat.sub_le _ _) _
α : Type ?u.783410
β : Type ?u.783413
n d k N : ℕ
x : Fin n → ℕ
hN : 2 ≤ N
this : (2 * dValue N - 1) ^ nValue N ≤ (2 * dValue N) ^ nValue N
⊢ (2 * dValue N) ^ nValue N ≤ N
α : Type ?u.783410
β : Type ?u.783413
n d k N : ℕ
x : Fin n → ℕ
hN : 2 ≤ N
this : (2 * dValue N - 1) ^ nValue N ≤ (2 * dValue N) ^ nValue N
⊢ (2 * dValue N - 1) ^ nValue N ≤ N
apply this.trans
α : Type ?u.783410
β : Type ?u.783413
n d k N : ℕ
x : Fin n → ℕ
hN : 2 ≤ N
this : (2 * dValue N - 1) ^ nValue N ≤ (2 * dValue N) ^ nValue N
⊢ (2 * ↑(dValue N)) ^ ↑(nValue N) ≤ ↑N
α : Type ?u.783410
β : Type ?u.783413
n d k N : ℕ
x : Fin n → ℕ
hN : 2 ≤ N
this : (2 * dValue N - 1) ^ nValue N ≤ (2 * dValue N) ^ nValue N
⊢ (2 * dValue N) ^ nValue N ≤ N
suffices ((2 * dValue N) ^ nValue N : ℝ) ≤ N by exact_mod_cast this
α : Type ?u.783410
β : Type ?u.783413
n d k N : ℕ
x : Fin n → ℕ
hN : 2 ≤ N
this : (2 * dValue N - 1) ^ nValue N ≤ (2 * dValue N) ^ nValue N
i : 2 * ↑(dValue N) ≤ ↑N ^ (1 / ↑(nValue N))
⊢ (2 * ↑(dValue N)) ^ ↑(nValue N) ≤ ↑N

case i
α : Type ?u.783410
β : Type ?u.783413
n d k N : ℕ
x : Fin n → ℕ
hN : 2 ≤ N
this : (2 * dValue N - 1) ^ nValue N ≤ (2 * dValue N) ^ nValue N
⊢ 2 * ↑(dValue N) ≤ ↑N ^ (1 / ↑(nValue N))
α : Type ?u.783410
β : Type ?u.783413
n d k N : ℕ
x : Fin n → ℕ
hN : 2 ≤ N
this : (2 * dValue N - 1) ^ nValue N ≤ (2 * dValue N) ^ nValue N
⊢ (2 * ↑(dValue N)) ^ ↑(nValue N) ≤ ↑N
suffices i : (2 * dValue N : ℝ) ≤ (N : ℝ) ^ (1 / nValue N : ℝ)
case i
α : Type ?u.783410
β : Type ?u.783413
n d k N : ℕ
x : Fin n → ℕ
hN : 2 ≤ N
this : (2 * dValue N - 1) ^ nValue N ≤ (2 * dValue N) ^ nValue N
⊢ ↑(dValue N) ≤ ↑N ^ (1 / ↑(nValue N)) / 2

case i
α : Type ?u.783410
β : Type ?u.783413
n d k N : ℕ
x : Fin n → ℕ
hN : 2 ≤ N
this : (2 * dValue N - 1) ^ nValue N ≤ (2 * dValue N) ^ nValue N
⊢ 0 < 2
case i
α : Type ?u.783410
β : Type ?u.783413
n d k N : ℕ
x : Fin n → ℕ
hN : 2 ≤ N
this : (2 * dValue N - 1) ^ nValue N ≤ (2 * dValue N) ^ nValue N
⊢ 2 * ↑(dValue N) ≤ ↑N ^ (1 / ↑(nValue N))
rw [← le_div_iff']
no goals
case i
α : Type ?u.783410
β : Type ?u.783413
n d k N : ℕ
x : Fin n → ℕ
hN : 2 ≤ N
this : (2 * dValue N - 1) ^ nValue N ≤ (2 * dValue N) ^ nValue N
⊢ 0 < 2
apply zero_lt_two
no goals
α : Type ?u.783410
β : Type ?u.783413
n d k N : ℕ
x : Fin n → ℕ
hN : 2 ≤ N
this✝ : (2 * dValue N - 1) ^ nValue N ≤ (2 * dValue N) ^ nValue N
this : (2 * ↑(dValue N)) ^ ↑(nValue N) ≤ ↑N
⊢ (2 * dValue N) ^ nValue N ≤ N
exact_mod_cast this
α : Type ?u.783410
β : Type ?u.783413
n d k N : ℕ
x : Fin n → ℕ
hN : 2 ≤ N
this : (2 * dValue N - 1) ^ nValue N ≤ (2 * dValue N) ^ nValue N
i : 2 * ↑(dValue N) ≤ ↑N ^ (1 / ↑(nValue N))
⊢ (↑N ^ (1 / ↑(nValue N))) ^ ↑(nValue N) ≤ ↑N
α : Type ?u.783410
β : Type ?u.783413
n d k N : ℕ
x : Fin n → ℕ
hN : 2 ≤ N
this : (2 * dValue N - 1) ^ nValue N ≤ (2 * dValue N) ^ nValue N
i : 2 * ↑(dValue N) ≤ ↑N ^ (1 / ↑(nValue N))
⊢ (2 * ↑(dValue N)) ^ ↑(nValue N) ≤ ↑N
apply (rpow_le_rpow (mul_nonneg zero_le_two (cast_nonneg _)) i (cast_nonneg _)).trans
α : Type ?u.783410
β : Type ?u.783413
n d k N : ℕ
x : Fin n → ℕ
hN : 2 ≤ N
this : (2 * dValue N - 1) ^ nValue N ≤ (2 * dValue N) ^ nValue N
i : 2 * ↑(dValue N) ≤ ↑N ^ (1 / ↑(nValue N))
⊢ ↑(nValue N) ≠ 0
α : Type ?u.783410
β : Type ?u.783413
n d k N : ℕ
x : Fin n → ℕ
hN : 2 ≤ N
this : (2 * dValue N - 1) ^ nValue N ≤ (2 * dValue N) ^ nValue N
i : 2 * ↑(dValue N) ≤ ↑N ^ (1 / ↑(nValue N))
⊢ (↑N ^ (1 / ↑(nValue N))) ^ ↑(nValue N) ≤ ↑N
rw [← rpow_mul (cast_nonneg _), one_div_mul_cancel, rpow_one]
α : Type ?u.783410
β : Type ?u.783413
n d k N : ℕ
x : Fin n → ℕ
hN : 2 ≤ N
this : (2 * dValue N - 1) ^ nValue N ≤ (2 * dValue N) ^ nValue N
i : 2 * ↑(dValue N) ≤ ↑N ^ (1 / ↑(nValue N))
⊢ nValue N ≠ 0
α : Type ?u.783410
β : Type ?u.783413
n d k N : ℕ
x : Fin n → ℕ
hN : 2 ≤ N
this : (2 * dValue N - 1) ^ nValue N ≤ (2 * dValue N) ^ nValue N
i : 2 * ↑(dValue N) ≤ ↑N ^ (1 / ↑(nValue N))
⊢ ↑(nValue N) ≠ 0
rw [cast_ne_zero]
no goals
α : Type ?u.783410
β : Type ?u.783413
n d k N : ℕ
x : Fin n → ℕ
hN : 2 ≤ N
this : (2 * dValue N - 1) ^ nValue N ≤ (2 * dValue N) ^ nValue N
i : 2 * ↑(dValue N) ≤ ↑N ^ (1 / ↑(nValue N))
⊢ nValue N ≠ 0
apply (nValue_pos hN).ne'
no goals
case i
α : Type ?u.783410
β : Type ?u.783413
n d k N : ℕ
x : Fin n → ℕ
hN : 2 ≤ N
this : (2 * dValue N - 1) ^ nValue N ≤ (2 * dValue N) ^ nValue N
⊢ ↑(dValue N) ≤ ↑N ^ (1 / ↑(nValue N)) / 2
exact floor_le (div_nonneg (rpow_nonneg_of_nonneg (cast_nonneg _) _) zero_le_two)