case zero
α : Type ?u.508512
β : Type ?u.508515
n d✝ k✝ N : ℕ
x : Fin n → ℕ
d k : ℕ
⊢ card (sphere zero d k) ≤ ↑rothNumberNat ((2 * d - 1) ^ zero)

case succ
α : Type ?u.508512
β : Type ?u.508515
n d✝ k✝ N : ℕ
x : Fin n → ℕ
d k n✝ : ℕ
⊢ card (sphere (succ n✝) d k) ≤ ↑rothNumberNat ((2 * d - 1) ^ succ n✝)
α : Type ?u.508512
β : Type ?u.508515
n✝ d✝ k✝ N : ℕ
x : Fin n✝ → ℕ
n d k : ℕ
⊢ card (sphere n d k) ≤ ↑rothNumberNat ((2 * d - 1) ^ n)
cases n
case succ.zero
α : Type ?u.508512
β : Type ?u.508515
n d k✝ N : ℕ
x : Fin n → ℕ
k n✝ : ℕ
⊢ card (sphere (succ n✝) zero k) ≤ ↑rothNumberNat ((2 * zero - 1) ^ succ n✝)

case succ.succ
α : Type ?u.508512
β : Type ?u.508515
n d k✝ N : ℕ
x : Fin n → ℕ
k n✝¹ n✝ : ℕ
⊢ card (sphere (succ n✝¹) (succ n✝) k) ≤ ↑rothNumberNat ((2 * succ n✝ - 1) ^ succ n✝¹)
case succ
α : Type ?u.508512
β : Type ?u.508515
n d✝ k✝ N : ℕ
x : Fin n → ℕ
d k n✝ : ℕ
⊢ card (sphere (succ n✝) d k) ≤ ↑rothNumberNat ((2 * d - 1) ^ succ n✝)
cases d
case succ.succ.refine'_1
α : Type ?u.508512
β : Type ?u.508515
n d k✝ N : ℕ
x : Fin n → ℕ
k n✝¹ n✝ : ℕ
⊢ Fin (succ n✝¹) → ℕ

case succ.succ.refine'_2
α : Type ?u.508512
β : Type ?u.508515
n d k✝ N : ℕ
x : Fin n → ℕ
k n✝¹ n✝ : ℕ
⊢ ∀ (x : ℕ), x ∈ image (↑(map (2 * succ n✝ - 1))) (sphere (succ n✝¹) (succ n✝) k) → x < (2 * succ n✝ - 1) ^ succ n✝¹

case succ.succ.refine'_3
α : Type ?u.508512
β : Type ?u.508515
n d k✝ N : ℕ
x : Fin n → ℕ
k n✝¹ n✝ : ℕ
⊢ Set.InjOn ↑(map (2 * succ n✝ - 1)) ↑(sphere (succ n✝¹) (succ n✝) k)
case succ.succ
α : Type ?u.508512
β : Type ?u.508515
n d k✝ N : ℕ
x : Fin n → ℕ
k n✝¹ n✝ : ℕ
⊢ card (sphere (succ n✝¹) (succ n✝) k) ≤ ↑rothNumberNat ((2 * succ n✝ - 1) ^ succ n✝¹)
refine' addSalemSpencer_image_sphere.le_rothNumberNat _ _ (card_image_of_injOn _)
case succ.succ.refine'_3.refine'_1
α : Type ?u.508512
β : Type ?u.508515
n d k✝ N : ℕ
x : Fin n → ℕ
k n✝¹ n✝ : ℕ
⊢ Fin (succ n✝¹) → ℕ

case succ.succ.refine'_3.refine'_2
α : Type ?u.508512
β : Type ?u.508515
n d k✝ N : ℕ
x✝ : Fin n → ℕ
k n✝¹ n✝ : ℕ
x : Fin (succ n✝¹) → ℕ
⊢ x ∈ ↑(sphere (succ n✝¹) (succ n✝) k) → x ∈ {x | ∀ (i : Fin (succ n✝¹)), x i < 2 * succ n✝ - 1}
case succ.succ.refine'_3
α : Type ?u.508512
β : Type ?u.508515
n d k✝ N : ℕ
x : Fin n → ℕ
k n✝¹ n✝ : ℕ
⊢ Set.InjOn ↑(map (2 * succ n✝ - 1)) ↑(sphere (succ n✝¹) (succ n✝) k)
refine' map_injOn.mono fun x => _
case succ.succ.refine'_3.refine'_2
α : Type ?u.508512
β : Type ?u.508515
n d k✝ N : ℕ
x✝ : Fin n → ℕ
k n✝¹ n✝ : ℕ
x : Fin (succ n✝¹) → ℕ
⊢ (∀ (i : Fin (succ n✝¹)), x i < succ n✝) →
    ∑ i : Fin (succ n✝¹), x i ^ 2 = k → x ∈ {x | ∀ (i : Fin (succ n✝¹)), x i < succ n✝ + succ n✝ - 1}
case succ.succ.refine'_3.refine'_2
α : Type ?u.508512
β : Type ?u.508515
n d k✝ N : ℕ
x✝ : Fin n → ℕ
k n✝¹ n✝ : ℕ
x : Fin (succ n✝¹) → ℕ
⊢ x ∈ ↑(sphere (succ n✝¹) (succ n✝) k) → x ∈ {x | ∀ (i : Fin (succ n✝¹)), x i < 2 * succ n✝ - 1}
simp only [mem_coe, sphere, mem_filter, mem_box, and_imp, two_mul]
no goals
case succ.succ.refine'_3.refine'_2
α : Type ?u.508512
β : Type ?u.508515
n d k✝ N : ℕ
x✝ : Fin n → ℕ
k n✝¹ n✝ : ℕ
x : Fin (succ n✝¹) → ℕ
⊢ (∀ (i : Fin (succ n✝¹)), x i < succ n✝) →
    ∑ i : Fin (succ n✝¹), x i ^ 2 = k → x ∈ {x | ∀ (i : Fin (succ n✝¹)), x i < succ n✝ + succ n✝ - 1}
exact fun h _ i => (h i).trans_le le_self_add
case zero
α : Type ?u.508512
β : Type ?u.508515
n d✝ k✝ N : ℕ
x : Fin n → ℕ
d k : ℕ
⊢ card (sphere 0 d k) ≤ ↑rothNumberNat 1
case zero
α : Type ?u.508512
β : Type ?u.508515
n d✝ k✝ N : ℕ
x : Fin n → ℕ
d k : ℕ
⊢ card (sphere zero d k) ≤ ↑rothNumberNat ((2 * d - 1) ^ zero)
dsimp
case zero
α : Type ?u.508512
β : Type ?u.508515
n d✝ k✝ N : ℕ
x : Fin n → ℕ
d k : ℕ
⊢ Fintype.card (Fin 0 → ℕ) = ↑rothNumberNat 1
case zero
α : Type ?u.508512
β : Type ?u.508515
n d✝ k✝ N : ℕ
x : Fin n → ℕ
d k : ℕ
⊢ card (sphere 0 d k) ≤ ↑rothNumberNat 1
refine' (card_le_univ _).trans_eq _
no goals
case zero
α : Type ?u.508512
β : Type ?u.508515
n d✝ k✝ N : ℕ
x : Fin n → ℕ
d k : ℕ
⊢ Fintype.card (Fin 0 → ℕ) = ↑rothNumberNat 1
simp
no goals
case succ.zero
α : Type ?u.508512
β : Type ?u.508515
n d k✝ N : ℕ
x : Fin n → ℕ
k n✝ : ℕ
⊢ card (sphere (succ n✝) zero k) ≤ ↑rothNumberNat ((2 * zero - 1) ^ succ n✝)
simp
case succ.succ.refine'_1
α : Type ?u.508512
β : Type ?u.508515
n d k✝ N : ℕ
x : Fin n → ℕ
k n✝¹ n✝ : ℕ
a✝ : Fin (succ n✝¹)
⊢ ℕ
case succ.succ.refine'_1
α : Type ?u.508512
β : Type ?u.508515
n d k✝ N : ℕ
x : Fin n → ℕ
k n✝¹ n✝ : ℕ
⊢ Fin (succ n✝¹) → ℕ
intro
no goals
case succ.succ.refine'_1
α : Type ?u.508512
β : Type ?u.508515
n d k✝ N : ℕ
x : Fin n → ℕ
k n✝¹ n✝ : ℕ
a✝ : Fin (succ n✝¹)
⊢ ℕ
assumption
case succ.succ.refine'_2
α : Type ?u.508512
β : Type ?u.508515
n d k✝ N : ℕ
x : Fin n → ℕ
k n✝¹ n✝ : ℕ
⊢ ∀ (x : ℕ) (x_1 : Fin (succ n✝¹) → ℕ),
    x_1 ∈ box (succ n✝¹) (succ n✝) →
      ∑ i : Fin (succ n✝¹), x_1 i ^ 2 = k → ↑(map (2 * succ n✝ - 1)) x_1 = x → x < (2 * succ n✝ - 1) ^ succ n✝¹
case succ.succ.refine'_2
α : Type ?u.508512
β : Type ?u.508515
n d k✝ N : ℕ
x : Fin n → ℕ
k n✝¹ n✝ : ℕ
⊢ ∀ (x : ℕ), x ∈ image (↑(map (2 * succ n✝ - 1))) (sphere (succ n✝¹) (succ n✝) k) → x < (2 * succ n✝ - 1) ^ succ n✝¹
simp only [subset_iff, mem_image, and_imp, forall_exists_index, mem_range,
  forall_apply_eq_imp_iff₂, sphere, mem_filter]
case succ.succ.refine'_2
α : Type ?u.508512
β : Type ?u.508515
n d k✝ N : ℕ
x✝ : Fin n → ℕ
k n✝¹ n✝ : ℕ
x : Fin (succ n✝¹) → ℕ
hx : x ∈ box (succ n✝¹) (succ n✝)
a✝ : ∑ i : Fin (succ n✝¹), x i ^ 2 = k
⊢ ↑(map (2 * succ n✝ - 1)) x < (2 * succ n✝ - 1) ^ succ n✝¹
case succ.succ.refine'_2
α : Type ?u.508512
β : Type ?u.508515
n d k✝ N : ℕ
x : Fin n → ℕ
k n✝¹ n✝ : ℕ
⊢ ∀ (x : ℕ) (x_1 : Fin (succ n✝¹) → ℕ),
    x_1 ∈ box (succ n✝¹) (succ n✝) →
      ∑ i : Fin (succ n✝¹), x_1 i ^ 2 = k → ↑(map (2 * succ n✝ - 1)) x_1 = x → x < (2 * succ n✝ - 1) ^ succ n✝¹
rintro _ x hx _ rfl
no goals
case succ.succ.refine'_2
α : Type ?u.508512
β : Type ?u.508515
n d k✝ N : ℕ
x✝ : Fin n → ℕ
k n✝¹ n✝ : ℕ
x : Fin (succ n✝¹) → ℕ
hx : x ∈ box (succ n✝¹) (succ n✝)
a✝ : ∑ i : Fin (succ n✝¹), x i ^ 2 = k
⊢ ↑(map (2 * succ n✝ - 1)) x < (2 * succ n✝ - 1) ^ succ n✝¹
exact (map_le_of_mem_box hx).trans_lt sum_lt
case succ.succ.refine'_3.refine'_1
α : Type ?u.508512
β : Type ?u.508515
n d k✝ N : ℕ
x : Fin n → ℕ
k n✝¹ n✝ : ℕ
a✝ : Fin (succ n✝¹)
⊢ ℕ
case succ.succ.refine'_3.refine'_1
α : Type ?u.508512
β : Type ?u.508515
n d k✝ N : ℕ
x : Fin n → ℕ
k n✝¹ n✝ : ℕ
⊢ Fin (succ n✝¹) → ℕ
intro
no goals
case succ.succ.refine'_3.refine'_1
α : Type ?u.508512
β : Type ?u.508515
n d k✝ N : ℕ
x : Fin n → ℕ
k n✝¹ n✝ : ℕ
a✝ : Fin (succ n✝¹)
⊢ ℕ
assumption