α : Type ?u.461418
β : Type ?u.461421
n d k N : ℕ
x : Fin n → ℕ
⊢ AddSalemSpencer (↑(map (2 * d - 1)) '' ↑(sphere n d k))
α : Type ?u.461418
β : Type ?u.461421
n d k N : ℕ
x : Fin n → ℕ
⊢ AddSalemSpencer ↑(image (↑(map (2 * d - 1))) (sphere n d k))
rw [coe_image]
case refine'_1
α : Type ?u.461418
β : Type ?u.461421
n d k N : ℕ
x : Fin n → ℕ
⊢ Fin n → ℕ

case refine'_2
α : Type ?u.461418
β : Type ?u.461421
n d k N : ℕ
x : Fin n → ℕ
⊢ ↑(sphere n d k) + ↑(sphere n d k) ⊆ {x | ∀ (i : Fin n), x i < 2 * d - 1}
α : Type ?u.461418
β : Type ?u.461421
n d k N : ℕ
x : Fin n → ℕ
⊢ AddSalemSpencer (↑(map (2 * d - 1)) '' ↑(sphere n d k))
refine' @AddSalemSpencer.image _ (Fin n → ℕ) ℕ _ _ (sphere n d k) _ (map (2 * d - 1))
  (map_injOn.mono _) addSalemSpencer_sphere
case refine'_2
α : Type ?u.461418
β : Type ?u.461421
n d k N : ℕ
x : Fin n → ℕ
⊢ ∀ (x : Fin n → ℕ),
    x ∈ ↑(sphere n d k) → ∀ (y : Fin n → ℕ), y ∈ ↑(sphere n d k) → x + y ∈ {x | ∀ (i : Fin n), x i < 2 * d - 1}
case refine'_2
α : Type ?u.461418
β : Type ?u.461421
n d k N : ℕ
x : Fin n → ℕ
⊢ ↑(sphere n d k) + ↑(sphere n d k) ⊆ {x | ∀ (i : Fin n), x i < 2 * d - 1}
rw [Set.add_subset_iff]
case refine'_2
α : Type ?u.461418
β : Type ?u.461421
n d k N : ℕ
x a : Fin n → ℕ
ha : a ∈ ↑(sphere n d k)
b : Fin n → ℕ
hb : b ∈ ↑(sphere n d k)
i : Fin n
⊢ (a + b) i < 2 * d - 1
case refine'_2
α : Type ?u.461418
β : Type ?u.461421
n d k N : ℕ
x : Fin n → ℕ
⊢ ∀ (x : Fin n → ℕ),
    x ∈ ↑(sphere n d k) → ∀ (y : Fin n → ℕ), y ∈ ↑(sphere n d k) → x + y ∈ {x | ∀ (i : Fin n), x i < 2 * d - 1}
rintro a ha b hb i
case refine'_2
α : Type ?u.461418
β : Type ?u.461421
n d k N : ℕ
x a : Fin n → ℕ
ha : a ∈ ↑(sphere n d k)
b : Fin n → ℕ
hb : b ∈ ↑(sphere n d k)
i : Fin n
hai : a i < d
⊢ (a + b) i < 2 * d - 1
case refine'_2
α : Type ?u.461418
β : Type ?u.461421
n d k N : ℕ
x a : Fin n → ℕ
ha : a ∈ ↑(sphere n d k)
b : Fin n → ℕ
hb : b ∈ ↑(sphere n d k)
i : Fin n
⊢ (a + b) i < 2 * d - 1
have hai := mem_box.1 (sphere_subset_box ha) i
case refine'_2
α : Type ?u.461418
β : Type ?u.461421
n d k N : ℕ
x a : Fin n → ℕ
ha : a ∈ ↑(sphere n d k)
b : Fin n → ℕ
hb : b ∈ ↑(sphere n d k)
i : Fin n
hai : a i < d
hbi : b i < d
⊢ (a + b) i < 2 * d - 1
case refine'_2
α : Type ?u.461418
β : Type ?u.461421
n d k N : ℕ
x a : Fin n → ℕ
ha : a ∈ ↑(sphere n d k)
b : Fin n → ℕ
hb : b ∈ ↑(sphere n d k)
i : Fin n
hai : a i < d
⊢ (a + b) i < 2 * d - 1
have hbi := mem_box.1 (sphere_subset_box hb) i
case refine'_2
α : Type ?u.461418
β : Type ?u.461421
n d k N : ℕ
x a : Fin n → ℕ
ha : a ∈ ↑(sphere n d k)
b : Fin n → ℕ
hb : b ∈ ↑(sphere n d k)
i : Fin n
hai : a i < d
hbi : b i < d
⊢ succ ((a + b) i + 1) ≤ d + d
case refine'_2
α : Type ?u.461418
β : Type ?u.461421
n d k N : ℕ
x a : Fin n → ℕ
ha : a ∈ ↑(sphere n d k)
b : Fin n → ℕ
hb : b ∈ ↑(sphere n d k)
i : Fin n
hai : a i < d
hbi : b i < d
⊢ (a + b) i < 2 * d - 1
rw [lt_tsub_iff_right, ← succ_le_iff, two_mul]
no goals
case refine'_2
α : Type ?u.461418
β : Type ?u.461421
n d k N : ℕ
x a : Fin n → ℕ
ha : a ∈ ↑(sphere n d k)
b : Fin n → ℕ
hb : b ∈ ↑(sphere n d k)
i : Fin n
hai : a i < d
hbi : b i < d
⊢ succ ((a + b) i + 1) ≤ d + d
exact (add_add_add_comm _ _ 1 1).trans_le (_root_.add_le_add hai hbi)
no goals
case refine'_1
α : Type ?u.461418
β : Type ?u.461421
n d k N : ℕ
x : Fin n → ℕ
⊢ Fin n → ℕ
exact x