-- Mathlib/Combinatorics/Additive/AP/Three/Behrend.lean
theorem exists_large_sphere (n d : ℕ) :
    ∃ k, ((d ^ n :) / (n * d ^ 2 :) : ℝ) ≤ #(sphere n d k)

Proof state:
case intro.intro
n d k : ℕ
hk : ↑(d ^ n) / (↑(n * (d - 1) ^ 2) + 1) ≤ ↑(#(sphere n d k))
⊢ ↑(d ^ n) / ↑(n * d ^ 2) ≤ ↑(#(sphere n d k))

Tactic:
obtain rfl | hn := n.eq_zero_or_pos

Result:
case intro.intro.inl
d k : ℕ
hk : ↑(d ^ 0) / (↑(0 * (d - 1) ^ 2) + 1) ≤ ↑(#(sphere 0 d k))
⊢ ↑(d ^ 0) / ↑(0 * d ^ 2) ≤ ↑(#(sphere 0 d k))

case intro.intro.inr
n d k : ℕ
hk : ↑(d ^ n) / (↑(n * (d - 1) ^ 2) + 1) ≤ ↑(#(sphere n d k))
hn : n > 0
⊢ ↑(d ^ n) / ↑(n * d ^ 2) ≤ ↑(#(sphere n d k))

Proof state:
case intro.intro.inr.inr.refine_3.hb
n d k : ℕ
hk : ↑(d ^ n) / (↑(n * (d - 1) ^ 2) + 1) ≤ ↑(#(sphere n d k))
hn : n > 0
hd : d > 0
⊢ 1 ≤ 2 * ↑d - 1

Tactic:
rw [_root_.le_sub_iff_add_le]

Result:
case intro.intro.inr.inr.refine_3.hb
n d k : ℕ
hk : ↑(d ^ n) / (↑(n * (d - 1) ^ 2) + 1) ≤ ↑(#(sphere n d k))
hn : n > 0
hd : d > 0
⊢ 1 + 1 ≤ 2 * ↑d

Proof state:
case intro.intro
n d k : ℕ
hk : ↑(d ^ n) / (↑(n * (d - 1) ^ 2) + 1) ≤ ↑(#(sphere n d k))
⊢ ∃ k, ↑(d ^ n) / ↑(n * d ^ 2) ≤ ↑(#(sphere n d k))

Tactic:
refine ⟨k, ?_⟩

Result:
case intro.intro
n d k : ℕ
hk : ↑(d ^ n) / (↑(n * (d - 1) ^ 2) + 1) ≤ ↑(#(sphere n d k))
⊢ ↑(d ^ n) / ↑(n * d ^ 2) ≤ ↑(#(sphere n d k))

Proof state:
case intro.intro.inr.inr.refine_2
n d k : ℕ
hk : ↑(d ^ n) / (↑(n * (d - 1) ^ 2) + 1) ≤ ↑(#(sphere n d k))
hn : n > 0
hd : d > 0
⊢ 0 < ↑(n * (d - 1) ^ 2) + 1

Tactic:
exact cast_add_one_pos _

Result:
no goals

Proof state:
case intro.intro.inr.inr.refine_3.hb
n d k : ℕ
hk : ↑(d ^ n) / (↑(n * (d - 1) ^ 2) + 1) ≤ ↑(#(sphere n d k))
hn : n > 0
hd : d > 0
⊢ 1 + 1 ≤ 2 * ↑d

Tactic:
norm_num

Result:
case intro.intro.inr.inr.refine_3.hb
n d k : ℕ
hk : ↑(d ^ n) / (↑(n * (d - 1) ^ 2) + 1) ≤ ↑(#(sphere n d k))
hn : n > 0
hd : d > 0
⊢ 1 ≤ d

Proof state:
case intro.intro.inr.inr.refine_1
n d k : ℕ
hk : ↑(d ^ n) / (↑(n * (d - 1) ^ 2) + 1) ≤ ↑(#(sphere n d k))
hn : n > 0
hd : d > 0
⊢ 0 ≤ ↑(d ^ n)

Tactic:
exact cast_nonneg _

Result:
no goals

Proof state:
case intro.intro.inr.inr.refine_3.ha
n d k : ℕ
hk : ↑(d ^ n) / (↑(n * (d - 1) ^ 2) + 1) ≤ ↑(#(sphere n d k))
hn : n > 0
hd : d > 0
⊢ 1 ≤ ↑n

Tactic:
rwa [one_le_cast]

Result:
no goals

Proof state:
case intro.intro.inr.inr.refine_3
n d k : ℕ
hk : ↑(d ^ n) / (↑(n * (d - 1) ^ 2) + 1) ≤ ↑(#(sphere n d k))
hn : n > 0
hd : d > 0
⊢ ↑(n * (d - 1) ^ 2) + 1 ≤ ↑(n * d ^ 2)

Tactic:
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]

Result:
case intro.intro.inr.inr.refine_3
n d k : ℕ
hk : ↑(d ^ n) / (↑(n * (d - 1) ^ 2) + 1) ≤ ↑(#(sphere n d k))
hn : n > 0
hd : d > 0
⊢ 1 ≤ ↑n * (2 * ↑d - 1)

Proof state:
n d : ℕ
⊢ ∃ k, ↑(d ^ n) / ↑(n * d ^ 2) ≤ ↑(#(sphere n d k))

Tactic:
obtain ⟨k, -, hk⟩ := exists_large_sphere_aux n d

Result:
case intro.intro
n d k : ℕ
hk : ↑(d ^ n) / (↑(n * (d - 1) ^ 2) + 1) ≤ ↑(#(sphere n d k))
⊢ ∃ k, ↑(d ^ n) / ↑(n * d ^ 2) ≤ ↑(#(sphere n d k))

Proof state:
case intro.intro.inr
n d k : ℕ
hk : ↑(d ^ n) / (↑(n * (d - 1) ^ 2) + 1) ≤ ↑(#(sphere n d k))
hn : n > 0
⊢ ↑(d ^ n) / ↑(n * d ^ 2) ≤ ↑(#(sphere n d k))

Tactic:
obtain rfl | hd := d.eq_zero_or_pos

Result:
case intro.intro.inr.inl
n k : ℕ
hn : n > 0
hk : ↑(0 ^ n) / (↑(n * (0 - 1) ^ 2) + 1) ≤ ↑(#(sphere n 0 k))
⊢ ↑(0 ^ n) / ↑(n * 0 ^ 2) ≤ ↑(#(sphere n 0 k))

case intro.intro.inr.inr
n d k : ℕ
hk : ↑(d ^ n) / (↑(n * (d - 1) ^ 2) + 1) ≤ ↑(#(sphere n d k))
hn : n > 0
hd : d > 0
⊢ ↑(d ^ n) / ↑(n * d ^ 2) ≤ ↑(#(sphere n d k))

Proof state:
case intro.intro.inr.inr.refine_3.hb
n d k : ℕ
hk : ↑(d ^ n) / (↑(n * (d - 1) ^ 2) + 1) ≤ ↑(#(sphere n d k))
hn : n > 0
hd : d > 0
⊢ 1 ≤ d

Tactic:
exact one_le_cast.2 hd

Result:
no goals

Proof state:
case intro.intro.inr.inl
n k : ℕ
hn : n > 0
hk : ↑(0 ^ n) / (↑(n * (0 - 1) ^ 2) + 1) ≤ ↑(#(sphere n 0 k))
⊢ ↑(0 ^ n) / ↑(n * 0 ^ 2) ≤ ↑(#(sphere n 0 k))

Tactic:
simp

Result:
no goals

Proof state:
case intro.intro.inr.inr.refine_3
n d k : ℕ
hk : ↑(d ^ n) / (↑(n * (d - 1) ^ 2) + 1) ≤ ↑(#(sphere n d k))
hn : n > 0
hd : d > 0
⊢ 1 ≤ ↑n * (2 * ↑d - 1)

Tactic:
apply one_le_mul_of_one_le_of_one_le

Result:
case intro.intro.inr.inr.refine_3.ha
n d k : ℕ
hk : ↑(d ^ n) / (↑(n * (d - 1) ^ 2) + 1) ≤ ↑(#(sphere n d k))
hn : n > 0
hd : d > 0
⊢ 1 ≤ ↑n

case intro.intro.inr.inr.refine_3.hb
n d k : ℕ
hk : ↑(d ^ n) / (↑(n * (d - 1) ^ 2) + 1) ≤ ↑(#(sphere n d k))
hn : n > 0
hd : d > 0
⊢ 1 ≤ 2 * ↑d - 1

Proof state:
case intro.intro.inr.inr
n d k : ℕ
hk : ↑(d ^ n) / (↑(n * (d - 1) ^ 2) + 1) ≤ ↑(#(sphere n d k))
hn : n > 0
hd : d > 0
⊢ ↑(d ^ n) / ↑(n * d ^ 2) ≤ ↑(#(sphere n d k))

Tactic:
refine (div_le_div_of_nonneg_left ?_ ?_ ?_).trans hk

Result:
case intro.intro.inr.inr.refine_1
n d k : ℕ
hk : ↑(d ^ n) / (↑(n * (d - 1) ^ 2) + 1) ≤ ↑(#(sphere n d k))
hn : n > 0
hd : d > 0
⊢ 0 ≤ ↑(d ^ n)

case intro.intro.inr.inr.refine_2
n d k : ℕ
hk : ↑(d ^ n) / (↑(n * (d - 1) ^ 2) + 1) ≤ ↑(#(sphere n d k))
hn : n > 0
hd : d > 0
⊢ 0 < ↑(n * (d - 1) ^ 2) + 1

case intro.intro.inr.inr.refine_3
n d k : ℕ
hk : ↑(d ^ n) / (↑(n * (d - 1) ^ 2) + 1) ≤ ↑(#(sphere n d k))
hn : n > 0
hd : d > 0
⊢ ↑(n * (d - 1) ^ 2) + 1 ≤ ↑(n * d ^ 2)

Proof state:
case intro.intro.inl
d k : ℕ
hk : ↑(d ^ 0) / (↑(0 * (d - 1) ^ 2) + 1) ≤ ↑(#(sphere 0 d k))
⊢ ↑(d ^ 0) / ↑(0 * d ^ 2) ≤ ↑(#(sphere 0 d k))

Tactic:
simp

Result:
no goals