case intro.intro
α : Type ?u.568071
β : Type ?u.568074
n✝ d✝ k✝ N : ℕ
x : Fin n✝ → ℕ
n d k : ℕ
hk : ↑(d ^ n) / (↑(n * (d - 1) ^ 2) + 1) ≤ ↑(card (sphere n d k))
⊢ ∃ k, ↑d ^ ↑n / ↑(n * d ^ 2) ≤ ↑(card (sphere n d k))
α : Type ?u.568071
β : Type ?u.568074
n✝ d✝ k N : ℕ
x : Fin n✝ → ℕ
n d : ℕ
⊢ ∃ k, ↑d ^ ↑n / ↑(n * d ^ 2) ≤ ↑(card (sphere n d k))
obtain ⟨k, -, hk⟩ := exists_large_sphere_aux n d
case intro.intro
α : Type ?u.568071
β : Type ?u.568074
n✝ d✝ k✝ N : ℕ
x : Fin n✝ → ℕ
n d k : ℕ
hk : ↑(d ^ n) / (↑(n * (d - 1) ^ 2) + 1) ≤ ↑(card (sphere n d k))
⊢ ↑d ^ ↑n / ↑(n * d ^ 2) ≤ ↑(card (sphere n d k))
case intro.intro
α : Type ?u.568071
β : Type ?u.568074
n✝ d✝ k✝ N : ℕ
x : Fin n✝ → ℕ
n d k : ℕ
hk : ↑(d ^ n) / (↑(n * (d - 1) ^ 2) + 1) ≤ ↑(card (sphere n d k))
⊢ ∃ k, ↑d ^ ↑n / ↑(n * d ^ 2) ≤ ↑(card (sphere n d k))
refine' ⟨k, _⟩
case intro.intro.inl
α : Type ?u.568071
β : Type ?u.568074
n d✝ k✝ N : ℕ
x : Fin n → ℕ
d k : ℕ
hk : ↑(d ^ 0) / (↑(0 * (d - 1) ^ 2) + 1) ≤ ↑(card (sphere 0 d k))
⊢ ↑d ^ ↑0 / ↑(0 * d ^ 2) ≤ ↑(card (sphere 0 d k))

case intro.intro.inr
α : Type ?u.568071
β : Type ?u.568074
n✝ d✝ k✝ N : ℕ
x : Fin n✝ → ℕ
n d k : ℕ
hk : ↑(d ^ n) / (↑(n * (d - 1) ^ 2) + 1) ≤ ↑(card (sphere n d k))
hn : n > 0
⊢ ↑d ^ ↑n / ↑(n * d ^ 2) ≤ ↑(card (sphere n d k))
case intro.intro
α : Type ?u.568071
β : Type ?u.568074
n✝ d✝ k✝ N : ℕ
x : Fin n✝ → ℕ
n d k : ℕ
hk : ↑(d ^ n) / (↑(n * (d - 1) ^ 2) + 1) ≤ ↑(card (sphere n d k))
⊢ ↑d ^ ↑n / ↑(n * d ^ 2) ≤ ↑(card (sphere n d k))
obtain rfl | hn := n.eq_zero_or_pos
case intro.intro.inr.inl
α : Type ?u.568071
β : Type ?u.568074
n✝ d k✝ N : ℕ
x : Fin n✝ → ℕ
n k : ℕ
hn : n > 0
hk : ↑(0 ^ n) / (↑(n * (0 - 1) ^ 2) + 1) ≤ ↑(card (sphere n 0 k))
⊢ ↑0 ^ ↑n / ↑(n * 0 ^ 2) ≤ ↑(card (sphere n 0 k))

case intro.intro.inr.inr
α : Type ?u.568071
β : Type ?u.568074
n✝ d✝ k✝ N : ℕ
x : Fin n✝ → ℕ
n d k : ℕ
hk : ↑(d ^ n) / (↑(n * (d - 1) ^ 2) + 1) ≤ ↑(card (sphere n d k))
hn : n > 0
hd : d > 0
⊢ ↑d ^ ↑n / ↑(n * d ^ 2) ≤ ↑(card (sphere n d k))
case intro.intro.inr
α : Type ?u.568071
β : Type ?u.568074
n✝ d✝ k✝ N : ℕ
x : Fin n✝ → ℕ
n d k : ℕ
hk : ↑(d ^ n) / (↑(n * (d - 1) ^ 2) + 1) ≤ ↑(card (sphere n d k))
hn : n > 0
⊢ ↑d ^ ↑n / ↑(n * d ^ 2) ≤ ↑(card (sphere n d k))
obtain rfl | hd := d.eq_zero_or_pos
case intro.intro.inr.inr
α : Type ?u.568071
β : Type ?u.568074
n✝ d✝ k✝ N : ℕ
x : Fin n✝ → ℕ
n d k : ℕ
hk : ↑(d ^ n) / (↑(n * (d - 1) ^ 2) + 1) ≤ ↑(card (sphere n d k))
hn : n > 0
hd : d > 0
⊢ ↑(d ^ n) / ↑(n * d ^ 2) ≤ ↑(card (sphere n d k))
case intro.intro.inr.inr
α : Type ?u.568071
β : Type ?u.568074
n✝ d✝ k✝ N : ℕ
x : Fin n✝ → ℕ
n d k : ℕ
hk : ↑(d ^ n) / (↑(n * (d - 1) ^ 2) + 1) ≤ ↑(card (sphere n d k))
hn : n > 0
hd : d > 0
⊢ ↑d ^ ↑n / ↑(n * d ^ 2) ≤ ↑(card (sphere n d k))
rw [rpow_nat_cast, ← cast_pow]
case intro.intro.inr.inr.refine'_1
α : Type ?u.568071
β : Type ?u.568074
n✝ d✝ k✝ N : ℕ
x : Fin n✝ → ℕ
n d k : ℕ
hk : ↑(d ^ n) / (↑(n * (d - 1) ^ 2) + 1) ≤ ↑(card (sphere n d k))
hn : n > 0
hd : d > 0
⊢ 0 ≤ ↑(d ^ n)

case intro.intro.inr.inr.refine'_2
α : Type ?u.568071
β : Type ?u.568074
n✝ d✝ k✝ N : ℕ
x : Fin n✝ → ℕ
n d k : ℕ
hk : ↑(d ^ n) / (↑(n * (d - 1) ^ 2) + 1) ≤ ↑(card (sphere n d k))
hn : n > 0
hd : d > 0
⊢ 0 < ↑(n * (d - 1) ^ 2) + 1

case intro.intro.inr.inr.refine'_3
α : Type ?u.568071
β : Type ?u.568074
n✝ d✝ k✝ N : ℕ
x : Fin n✝ → ℕ
n d k : ℕ
hk : ↑(d ^ n) / (↑(n * (d - 1) ^ 2) + 1) ≤ ↑(card (sphere n d k))
hn : n > 0
hd : d > 0
⊢ ↑(n * (d - 1) ^ 2) + 1 ≤ ↑(n * d ^ 2)
case intro.intro.inr.inr
α : Type ?u.568071
β : Type ?u.568074
n✝ d✝ k✝ N : ℕ
x : Fin n✝ → ℕ
n d k : ℕ
hk : ↑(d ^ n) / (↑(n * (d - 1) ^ 2) + 1) ≤ ↑(card (sphere n d k))
hn : n > 0
hd : d > 0
⊢ ↑(d ^ n) / ↑(n * d ^ 2) ≤ ↑(card (sphere n d k))
refine' (div_le_div_of_le_left _ _ _).trans hk
case intro.intro.inr.inr.refine'_3
α : Type ?u.568071
β : Type ?u.568074
n✝ d✝ k✝ N : ℕ
x : Fin n✝ → ℕ
n d k : ℕ
hk : ↑(d ^ n) / (↑(n * (d - 1) ^ 2) + 1) ≤ ↑(card (sphere n d k))
hn : n > 0
hd : d > 0
⊢ 1 ≤ ↑n * (2 * ↑d * ↑(succ 0) - ↑(succ 0) ^ 2)
case intro.intro.inr.inr.refine'_3
α : Type ?u.568071
β : Type ?u.568074
n✝ d✝ k✝ N : ℕ
x : Fin n✝ → ℕ
n d k : ℕ
hk : ↑(d ^ n) / (↑(n * (d - 1) ^ 2) + 1) ≤ ↑(card (sphere n d k))
hn : n > 0
hd : d > 0
⊢ ↑(n * (d - 1) ^ 2) + 1 ≤ ↑(n * d ^ 2)
simp only [← le_sub_iff_add_le', cast_mul, ← mul_sub, cast_pow, cast_sub hd, sub_sq, one_pow,
  cast_one, mul_one, sub_add, sub_sub_self]
case intro.intro.inr.inr.refine'_3.ha
α : Type ?u.568071
β : Type ?u.568074
n✝ d✝ k✝ N : ℕ
x : Fin n✝ → ℕ
n d k : ℕ
hk : ↑(d ^ n) / (↑(n * (d - 1) ^ 2) + 1) ≤ ↑(card (sphere n d k))
hn : n > 0
hd : d > 0
⊢ 1 ≤ ↑n

case intro.intro.inr.inr.refine'_3.hb
α : Type ?u.568071
β : Type ?u.568074
n✝ d✝ k✝ N : ℕ
x : Fin n✝ → ℕ
n d k : ℕ
hk : ↑(d ^ n) / (↑(n * (d - 1) ^ 2) + 1) ≤ ↑(card (sphere n d k))
hn : n > 0
hd : d > 0
⊢ 1 ≤ 2 * ↑d * ↑(succ 0) - ↑(succ 0) ^ 2
case intro.intro.inr.inr.refine'_3
α : Type ?u.568071
β : Type ?u.568074
n✝ d✝ k✝ N : ℕ
x : Fin n✝ → ℕ
n d k : ℕ
hk : ↑(d ^ n) / (↑(n * (d - 1) ^ 2) + 1) ≤ ↑(card (sphere n d k))
hn : n > 0
hd : d > 0
⊢ 1 ≤ ↑n * (2 * ↑d * ↑(succ 0) - ↑(succ 0) ^ 2)
apply one_le_mul_of_one_le_of_one_le
case intro.intro.inr.inr.refine'_3.hb
α : Type ?u.568071
β : Type ?u.568074
n✝ d✝ k✝ N : ℕ
x : Fin n✝ → ℕ
n d k : ℕ
hk : ↑(d ^ n) / (↑(n * (d - 1) ^ 2) + 1) ≤ ↑(card (sphere n d k))
hn : n > 0
hd : d > 0
⊢ 1 + ↑1 ^ 2 ≤ 2 * ↑d * ↑1
case intro.intro.inr.inr.refine'_3.hb
α : Type ?u.568071
β : Type ?u.568074
n✝ d✝ k✝ N : ℕ
x : Fin n✝ → ℕ
n d k : ℕ
hk : ↑(d ^ n) / (↑(n * (d - 1) ^ 2) + 1) ≤ ↑(card (sphere n d k))
hn : n > 0
hd : d > 0
⊢ 1 ≤ 2 * ↑d * ↑(succ 0) - ↑(succ 0) ^ 2
rw [← one_eq_succ_zero, _root_.le_sub_iff_add_le]
case intro.intro.inr.inr.refine'_3.hb
α : Type ?u.568071
β : Type ?u.568074
n✝ d✝ k✝ N : ℕ
x : Fin n✝ → ℕ
n d k : ℕ
hk : ↑(d ^ n) / (↑(n * (d - 1) ^ 2) + 1) ≤ ↑(card (sphere n d k))
hn : n > 0
hd : d > 0
⊢ 1 ≤ d
case intro.intro.inr.inr.refine'_3.hb
α : Type ?u.568071
β : Type ?u.568074
n✝ d✝ k✝ N : ℕ
x : Fin n✝ → ℕ
n d k : ℕ
hk : ↑(d ^ n) / (↑(n * (d - 1) ^ 2) + 1) ≤ ↑(card (sphere n d k))
hn : n > 0
hd : d > 0
⊢ 1 + ↑1 ^ 2 ≤ 2 * ↑d * ↑1
norm_num
no goals
case intro.intro.inr.inr.refine'_3.hb
α : Type ?u.568071
β : Type ?u.568074
n✝ d✝ k✝ N : ℕ
x : Fin n✝ → ℕ
n d k : ℕ
hk : ↑(d ^ n) / (↑(n * (d - 1) ^ 2) + 1) ≤ ↑(card (sphere n d k))
hn : n > 0
hd : d > 0
⊢ 1 ≤ d
exact one_le_cast.2 hd
no goals
case intro.intro.inl
α : Type ?u.568071
β : Type ?u.568074
n d✝ k✝ N : ℕ
x : Fin n → ℕ
d k : ℕ
hk : ↑(d ^ 0) / (↑(0 * (d - 1) ^ 2) + 1) ≤ ↑(card (sphere 0 d k))
⊢ ↑d ^ ↑0 / ↑(0 * d ^ 2) ≤ ↑(card (sphere 0 d k))
simp
no goals
case intro.intro.inr.inl
α : Type ?u.568071
β : Type ?u.568074
n✝ d k✝ N : ℕ
x : Fin n✝ → ℕ
n k : ℕ
hn : n > 0
hk : ↑(0 ^ n) / (↑(n * (0 - 1) ^ 2) + 1) ≤ ↑(card (sphere n 0 k))
⊢ ↑0 ^ ↑n / ↑(n * 0 ^ 2) ≤ ↑(card (sphere n 0 k))
simp
no goals
case intro.intro.inr.inr.refine'_1
α : Type ?u.568071
β : Type ?u.568074
n✝ d✝ k✝ N : ℕ
x : Fin n✝ → ℕ
n d k : ℕ
hk : ↑(d ^ n) / (↑(n * (d - 1) ^ 2) + 1) ≤ ↑(card (sphere n d k))
hn : n > 0
hd : d > 0
⊢ 0 ≤ ↑(d ^ n)
exact cast_nonneg _
no goals
case intro.intro.inr.inr.refine'_2
α : Type ?u.568071
β : Type ?u.568074
n✝ d✝ k✝ N : ℕ
x : Fin n✝ → ℕ
n d k : ℕ
hk : ↑(d ^ n) / (↑(n * (d - 1) ^ 2) + 1) ≤ ↑(card (sphere n d k))
hn : n > 0
hd : d > 0
⊢ 0 < ↑(n * (d - 1) ^ 2) + 1
exact cast_add_one_pos _
no goals
case intro.intro.inr.inr.refine'_3.ha
α : Type ?u.568071
β : Type ?u.568074
n✝ d✝ k✝ N : ℕ
x : Fin n✝ → ℕ
n d k : ℕ
hk : ↑(d ^ n) / (↑(n * (d - 1) ^ 2) + 1) ≤ ↑(card (sphere n d k))
hn : n > 0
hd : d > 0
⊢ 1 ≤ ↑n
rwa [one_le_cast]