-- Mathlib/Combinatorics/Additive/AP/Three/Behrend.lean
theorem card_sphere_le_rothNumberNat (n d k : ℕ) :
    #(sphere n d k) ≤ rothNumberNat ((2 * d - 1) ^ n)

Proof state:
case succ
d k n✝ : ℕ
⊢ #(sphere (n✝ + 1) d k) ≤ rothNumberNat ((2 * d - 1) ^ (n✝ + 1))

Tactic:
cases d

Result:
case succ.zero
k n✝ : ℕ
⊢ #(sphere (n✝ + 1) 0 k) ≤ rothNumberNat ((2 * 0 - 1) ^ (n✝ + 1))

case succ.succ
k n✝¹ n✝ : ℕ
⊢ #(sphere (n✝¹ + 1) (n✝ + 1) k) ≤ rothNumberNat ((2 * (n✝ + 1) - 1) ^ (n✝¹ + 1))

Proof state:
case zero
d k : ℕ
⊢ #(sphere 0 d k) ≤ rothNumberNat 1

Tactic:
refine (card_le_univ _).trans_eq ?_

Result:
case zero
d k : ℕ
⊢ Fintype.card (Fin 0 → ℕ) = rothNumberNat 1

Proof state:
case zero
d k : ℕ
⊢ Fintype.card (Fin 0 → ℕ) = rothNumberNat 1

Tactic:
rfl

Result:
no goals

Proof state:
case succ.zero
k n✝ : ℕ
⊢ #(sphere (n✝ + 1) 0 k) ≤ rothNumberNat ((2 * 0 - 1) ^ (n✝ + 1))

Tactic:
simp

Result:
no goals

Proof state:
k n✝¹ n✝ : ℕ
x : Fin (n✝¹ + 1) → ℕ
hx : x ∈ box (n✝¹ + 1) (n✝ + 1)
a✝ : ∑ i : Fin (n✝¹ + 1), x i ^ 2 = k
⊢ (map (2 * (n✝ + 1) - 1)) x < (2 * (n✝ + 1) - 1) ^ (n✝¹ + 1)

Tactic:
exact (map_le_of_mem_box hx).trans_lt sum_lt

Result:
no goals

Proof state:
n d k : ℕ
⊢ #(sphere n d k) ≤ rothNumberNat ((2 * d - 1) ^ n)

Tactic:
cases n

Result:
case zero
d k : ℕ
⊢ #(sphere 0 d k) ≤ rothNumberNat ((2 * d - 1) ^ 0)

case succ
d k n✝ : ℕ
⊢ #(sphere (n✝ + 1) d k) ≤ rothNumberNat ((2 * d - 1) ^ (n✝ + 1))

Proof state:
case zero
d k : ℕ
⊢ #(sphere 0 d k) ≤ rothNumberNat ((2 * d - 1) ^ 0)

Tactic:
dsimp

Result:
case zero
d k : ℕ
⊢ #(sphere 0 d k) ≤ rothNumberNat 1

Proof state:
k n✝¹ n✝ : ℕ
⊢ ∀ x ∈ image (⇑(map (2 * (n✝ + 1) - 1))) (sphere (n✝¹ + 1) (n✝ + 1) k), x < (2 * (n✝ + 1) - 1) ^ (n✝¹ + 1)

Tactic:
simp only [subset_iff, mem_image, and_imp, forall_exists_index, mem_range,
  forall_apply_eq_imp_iff₂, sphere, mem_filter]

Result:
k n✝¹ n✝ : ℕ
⊢ ∀ (x : ℕ),
    ∀ x_1 ∈ box (n✝¹ + 1) (n✝ + 1),
      ∑ i : Fin (n✝¹ + 1), x_1 i ^ 2 = k → (map (2 * (n✝ + 1) - 1)) x_1 = x → x < (2 * (n✝ + 1) - 1) ^ (n✝¹ + 1)

Proof state:
k n✝¹ n✝ : ℕ
x : Fin (n✝¹ + 1) → ℕ
⊢ x ∈ ↑(sphere (n✝¹ + 1) (n✝ + 1) k) → x ∈ {x | ∀ (i : Fin (n✝¹ + 1)), x i < 2 * (n✝ + 1) - 1}

Tactic:
simp only [mem_coe, sphere, mem_filter, mem_box, and_imp, two_mul]

Result:
k n✝¹ n✝ : ℕ
x : Fin (n✝¹ + 1) → ℕ
⊢ (∀ (i : Fin (n✝¹ + 1)), x i < n✝ + 1) →
    ∑ i : Fin (n✝¹ + 1), x i ^ 2 = k → x ∈ {x | ∀ (i : Fin (n✝¹ + 1)), x i < n✝ + 1 + (n✝ + 1) - 1}

Proof state:
case succ.succ
k n✝¹ n✝ : ℕ
⊢ #(sphere (n✝¹ + 1) (n✝ + 1) k) ≤ rothNumberNat ((2 * (n✝ + 1) - 1) ^ (n✝¹ + 1))

Tactic:
apply threeAPFree_image_sphere.le_rothNumberNat _ _ (card_image_of_injOn _)

Result:
k n✝¹ n✝ : ℕ
⊢ ∀ x ∈ image (⇑(map (2 * (n✝ + 1) - 1))) (sphere (n✝¹ + 1) (n✝ + 1) k), x < (2 * (n✝ + 1) - 1) ^ (n✝¹ + 1)

k n✝¹ n✝ : ℕ
⊢ Set.InjOn ⇑(map (2 * (n✝ + 1) - 1)) ↑(sphere (n✝¹ + 1) (n✝ + 1) k)

Proof state:
k n✝¹ n✝ : ℕ
⊢ ∀ (x : ℕ),
    ∀ x_1 ∈ box (n✝¹ + 1) (n✝ + 1),
      ∑ i : Fin (n✝¹ + 1), x_1 i ^ 2 = k → (map (2 * (n✝ + 1) - 1)) x_1 = x → x < (2 * (n✝ + 1) - 1) ^ (n✝¹ + 1)

Tactic:
rintro _ x hx _ rfl

Result:
k n✝¹ n✝ : ℕ
x : Fin (n✝¹ + 1) → ℕ
hx : x ∈ box (n✝¹ + 1) (n✝ + 1)
a✝ : ∑ i : Fin (n✝¹ + 1), x i ^ 2 = k
⊢ (map (2 * (n✝ + 1) - 1)) x < (2 * (n✝ + 1) - 1) ^ (n✝¹ + 1)

Proof state:
k n✝¹ n✝ : ℕ
x : Fin (n✝¹ + 1) → ℕ
⊢ (∀ (i : Fin (n✝¹ + 1)), x i < n✝ + 1) →
    ∑ i : Fin (n✝¹ + 1), x i ^ 2 = k → x ∈ {x | ∀ (i : Fin (n✝¹ + 1)), x i < n✝ + 1 + (n✝ + 1) - 1}

Tactic:
exact fun h _ i => (h i).trans_le le_self_add

Result:
no goals

Proof state:
k n✝¹ n✝ : ℕ
⊢ Set.InjOn ⇑(map (2 * (n✝ + 1) - 1)) ↑(sphere (n✝¹ + 1) (n✝ + 1) k)

Tactic:
apply map_injOn.mono fun x => ?_

Result:
k n✝¹ n✝ : ℕ
x : Fin (n✝¹ + 1) → ℕ
⊢ x ∈ ↑(sphere (n✝¹ + 1) (n✝ + 1) k) → x ∈ {x | ∀ (i : Fin (n✝¹ + 1)), x i < 2 * (n✝ + 1) - 1}