awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
n d : ℕ
refine : (2 * d + 1) ^ n - 1 = HMul.hMul (α := ℕ) (∑ i : Fin n, d * (2 * d + 1) ^ (↑i : ℕ)) 2
⊢ ∑ i : Fin n, d * (2 * d + 1) ^ (↑i : ℕ) = ((2 * d + 1) ^ n - 1) / 2

Tactic:
refine (Nat.div_eq_of_eq_mul_left zero_lt_two ?_).symm

Premises used: Nat.div_eq_of_eq_mul_left, zero_lt_two, Eq.symm
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
n d : ℕ
rw : (2 * d + 1) ^ n - 1 = HMul.hMul (α := ℕ) (∑ i ∈ range n, d * (2 * d + 1) ^ i) 2
rw₁ : (2 * d + 1) ^ n - 1 = (d * ∑ i ∈ range n, (2 * d + 1) ^ i) * 2
rw₂ : (2 * d + 1) ^ n - 1 = d * 2 * ∑ i ∈ range n, (2 * d + 1) ^ i
rw₃ : (2 * d + 1) ^ n - 1 = 2 * d * ∑ i ∈ range n, (2 * d + 1) ^ i
rw₄ : (∑ i ∈ range n, (2 * d + 1) ^ i) * (2 * d) + 1 - 1 = 2 * d * ∑ i ∈ range n, (2 * d + 1) ^ i
rw₅ : (∑ i ∈ range n, (2 * d + 1) ^ i) * (2 * d) = 2 * d * ∑ i ∈ range n, (2 * d + 1) ^ i
rw₆ rw₇ : 2 * d * ∑ i ∈ range n, (2 * d + 1) ^ i = 2 * d * ∑ i ∈ range n, (2 * d + 1) ^ i
⊢ (2 * d + 1) ^ n - 1 = HMul.hMul (α := ℕ) (∑ i : Fin n, d * (2 * d + 1) ^ (↑i : ℕ)) 2

Tactic:
rw [← sum_range fun i => d * (2 * d + 1) ^ (i : ℕ), ← mul_sum, mul_right_comm, mul_comm d, ←
    geom_sum_mul_add, add_tsub_cancel_right, mul_comm]

Premises used: Finset.mul_sum, HMul.hMul, Finset.sum_range, HPow.hPow, HAdd.hAdd, mul_right_comm, geom_sum_mul_add, mul_comm, add_tsub_cancel_right, OfNat.ofNat
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
n d : ℕ
⊢ ∑ i : Fin n, d * (2 * d + 1) ^ (↑i : ℕ) < (2 * d + 1) ^ n

Tactic:
sum_eq.trans_lt <| (Nat.div_le_self _ 2).trans_lt <| pred_lt (pow_pos (succ_pos _) _).ne'

Premises used: pow_pos, Nat.div_le_self, LT.lt.ne', Nat.pred_lt, Nat.succ_pos, Eq.trans_lt, OfNat.ofNat, LE.le.trans_lt, Behrend.sum_eq
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
n d k : ℕ
zero : card (α := Fin 0 → ℕ) (sphere 0 d k) ≤ (rothNumberNat : (a : ℕ) → ℕ) (HPow.hPow (β := ℕ) (2 * d - 1) 0)
succ :
  ∀ (n : ℕ), card (α := Fin (n + 1) → ℕ) (sphere (n + 1) d k) ≤ (rothNumberNat : (a : ℕ) → ℕ) ((2 * d - 1) ^ (n + 1))
⊢ #(sphere n d k) ≤ (rothNumberNat : (a : ℕ) → ℕ) ((2 * d - 1) ^ n)

Tactic:
cases n
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
d k : ℕ
⊢ card (α := Fin 0 → ℕ) (sphere 0 d k) ≤ (rothNumberNat : (a : ℕ) → ℕ) 1

Tactic:
(card_le_univ _).trans_eq ?_

Premises used: LE.le.trans_eq, Finset.card_le_univ
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
d k : ℕ
zero : Fintype.card (Fin 0 → ℕ) = (rothNumberNat : (a : ℕ) → ℕ) 1
⊢ card (α := Fin 0 → ℕ) (sphere 0 d k) ≤ (rothNumberNat : (a : ℕ) → ℕ) 1

Tactic:
refine (card_le_univ _).trans_eq ?_

Premises used: LE.le.trans_eq, Finset.card_le_univ
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
d k : ℕ
⊢ Fintype.card (Fin 0 → ℕ) = (rothNumberNat : (a : ℕ) → ℕ) 1

Tactic:
rfl
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
d k n : ℕ
succ :
  card (α := Fin (n + 1) → ℕ) (sphere (n + 1) 0 k) ≤
    (rothNumberNat : (a : ℕ) → ℕ) ((HMul.hMul (α := ℕ) 2 0 - 1) ^ (n + 1))
succ₁ :
  ∀ (n_1 : ℕ),
    card (α := Fin (n + 1) → ℕ) (sphere (n + 1) (n_1 + 1) k) ≤
      (rothNumberNat : (a : ℕ) → ℕ) ((2 * (n_1 + 1) - 1) ^ (n + 1))
⊢ card (α := Fin (n + 1) → ℕ) (sphere (n + 1) d k) ≤ (rothNumberNat : (a : ℕ) → ℕ) ((2 * d - 1) ^ (n + 1))

Tactic:
cases d
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
k n : ℕ
⊢ card (α := Fin (n + 1) → ℕ) (sphere (n + 1) 0 k) ≤
    (rothNumberNat : (a : ℕ) → ℕ) ((HMul.hMul (α := ℕ) 2 0 - 1) ^ (n + 1))

Tactic:
simp
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
k n n_1 : ℕ
apply :
  ∀ (x : ℕ),
    Membership.mem (γ := Finset ℕ)
        (image (α := Fin (n + 1) → ℕ) (⇑(map (2 * (n_1 + 1) - 1)) : (a : Fin (n + 1) → ℕ) → ℕ)
          (sphere (n + 1) (n_1 + 1) k))
        x →
      x < (2 * (n_1 + 1) - 1) ^ (n + 1)
apply₁ :
  Set.InjOn (β := ℕ) (⇑(map (2 * (n_1 + 1) - 1)) : (a : Fin (n + 1) → ℕ) → ℕ)
    (↑(sphere (n + 1) (n_1 + 1) k) : Set (Fin (n + 1) → ℕ))
⊢ card (α := Fin (n + 1) → ℕ) (sphere (n + 1) (n_1 + 1) k) ≤
    (rothNumberNat : (a : ℕ) → ℕ) ((2 * (n_1 + 1) - 1) ^ (n + 1))

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

Premises used: ThreeAPFree.le_rothNumberNat, Finset.card_image_of_injOn, Behrend.threeAPFree_image_sphere
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
k n n_1 : ℕ
simp :
  ∀ (x : ℕ) (x_1 : Fin (n + 1) → ℕ),
    Membership.mem (γ := Finset (Fin (n + 1) → ℕ)) (box (n + 1) (n_1 + 1)) x_1 →
      ∑ i : Fin (n + 1), HPow.hPow (β := ℕ) (x_1 i) 2 = k →
        (map (2 * (n_1 + 1) - 1) : (a : Fin (n + 1) → ℕ) → ℕ) x_1 = x → x < (2 * (n_1 + 1) - 1) ^ (n + 1)
⊢ ∀ (x : ℕ),
    Membership.mem (γ := Finset ℕ)
        (image (α := Fin (n + 1) → ℕ) (⇑(map (2 * (n_1 + 1) - 1)) : (a : Fin (n + 1) → ℕ) → ℕ)
          (sphere (n + 1) (n_1 + 1) k))
        x →
      x < (2 * (n_1 + 1) - 1) ^ (n + 1)

Tactic:
simp only [mem_image, and_imp, forall_exists_index,
      sphere, mem_filter]

Premises used: Finset.mem_image, Behrend.sphere, and_imp, forall_exists_index, Finset.mem_filter
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
k n n_1 : ℕ
x : Fin (n + 1) → ℕ
hx : Membership.mem (γ := Finset (Fin (n + 1) → ℕ)) (box (n + 1) (n_1 + 1)) x
h : ∑ i : Fin (n + 1), HPow.hPow (β := ℕ) (x i) 2 = k
⊢ (map (2 * (n_1 + 1) - 1) : (a : Fin (n + 1) → ℕ) → ℕ) x < (2 * (n_1 + 1) - 1) ^ (n + 1)

Tactic:
(map_le_of_mem_box hx).trans_lt sum_lt

Premises used: Behrend.sum_lt, Behrend.map_le_of_mem_box, LE.le.trans_lt
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
k n n_1 : ℕ
x : Fin (n + 1) → ℕ
hx : Membership.mem (γ := Finset (Fin (n + 1) → ℕ)) (box (n + 1) (n_1 + 1)) x
h : ∑ i : Fin (n + 1), HPow.hPow (β := ℕ) (x i) 2 = k
⊢ (map (2 * (n_1 + 1) - 1) : (a : Fin (n + 1) → ℕ) → ℕ) x < (2 * (n_1 + 1) - 1) ^ (n + 1)

Tactic:
exact (map_le_of_mem_box hx).trans_lt sum_lt

Premises used: Behrend.sum_lt, Behrend.map_le_of_mem_box, LE.le.trans_lt
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
k n n_1 : ℕ
apply :
  ∀ x ∈ (↑(sphere (n + 1) (n_1 + 1) k) : Set (Fin (n + 1) → ℕ)),
    Membership.mem (γ := Set (Fin (n + 1) → ℕ)) {x : Fin (n + 1) → ℕ | ∀ (i : Fin (n + 1)), x i < 2 * (n_1 + 1) - 1} x
⊢ Set.InjOn (β := ℕ) (⇑(map (2 * (n_1 + 1) - 1)) : (a : Fin (n + 1) → ℕ) → ℕ)
    (↑(sphere (n + 1) (n_1 + 1) k) : Set (Fin (n + 1) → ℕ))

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

Premises used: Behrend.map_injOn, Set.InjOn.mono
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
k n n_1 : ℕ
x : Fin (n + 1) → ℕ
simp :
  (∀ (i : Fin (n + 1)), x i < n_1 + 1) →
    ∑ i : Fin (n + 1), HPow.hPow (β := ℕ) (x i) 2 = k →
      Membership.mem (γ := Set (Fin (n + 1) → ℕ))
        {x : Fin (n + 1) → ℕ | ∀ (i : Fin (n + 1)), x i < n_1 + 1 + (n_1 + 1) - 1} x
⊢ x ∈ (↑(sphere (n + 1) (n_1 + 1) k) : Set (Fin (n + 1) → ℕ)) →
    Membership.mem (γ := Set (Fin (n + 1) → ℕ)) {x : Fin (n + 1) → ℕ | ∀ (i : Fin (n + 1)), x i < 2 * (n_1 + 1) - 1} x

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

Premises used: Behrend.sphere, and_imp, two_mul, Behrend.mem_box, Finset.mem_filter, Finset.mem_coe
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
k n n_1 : ℕ
x : Fin (n + 1) → ℕ
⊢ (∀ (i : Fin (n + 1)), x i < n_1 + 1) →
    ∑ i : Fin (n + 1), HPow.hPow (β := ℕ) (x i) 2 = k →
      Membership.mem (γ := Set (Fin (n + 1) → ℕ))
        {x : Fin (n + 1) → ℕ | ∀ (i : Fin (n + 1)), x i < n_1 + 1 + (n_1 + 1) - 1} x

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

Premises used: Set.Mem, setOf, LT.lt.trans_le, le_self_add
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
k n n_1 : ℕ
x : Fin (n + 1) → ℕ
⊢ (∀ (i : Fin (n + 1)), x i < n_1 + 1) →
    ∑ i : Fin (n + 1), HPow.hPow (β := ℕ) (x i) 2 = k →
      Membership.mem (γ := Set (Fin (n + 1) → ℕ))
        {x : Fin (n + 1) → ℕ | ∀ (i : Fin (n + 1)), x i < n_1 + 1 + (n_1 + 1) - 1} x

Tactic:
exact fun h _ i => (h i).trans_le le_self_add
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
n d : ℕ
⊢ ∃ k ∈ range (n * HPow.hPow (β := ℕ) (d - 1) 2 + 1),
    (↑(d ^ n) : ℝ) / HAdd.hAdd (α := ℝ) (↑(n * HPow.hPow (β := ℕ) (d - 1) 2) : ℝ) 1 ≤ (↑(#(sphere n d k)) : ℝ)

Tactic:
exists_le_card_fiber_of_nsmul_le_card_of_maps_to (fun x hx => ?_) nonempty_range_add_one ?_

Premises used: Behrend.sphere, Finset.nonempty_range_add_one, Finset.exists_le_card_fiber_of_nsmul_le_card_of_maps_to
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
n d : ℕ
refine_1 :
  ∀ (x : Fin n → ℕ) (hx : x ∈ box n d),
    ∑ i : Fin n, HPow.hPow (β := ℕ) (x i) 2 ∈ range (n * HPow.hPow (β := ℕ) (d - 1) 2 + 1)
refine_2 :
  #(range (n * HPow.hPow (β := ℕ) (d - 1) 2 + 1)) •
      ((↑(d ^ n) : ℝ) / HAdd.hAdd (α := ℝ) (↑(n * HPow.hPow (β := ℕ) (d - 1) 2) : ℝ) 1) ≤
    (↑(#(box n d)) : ℝ)
⊢ ∃ k ∈ range (n * HPow.hPow (β := ℕ) (d - 1) 2 + 1),
    (↑(d ^ n) : ℝ) / HAdd.hAdd (α := ℝ) (↑(n * HPow.hPow (β := ℕ) (d - 1) 2) : ℝ) 1 ≤ (↑(#(sphere n d k)) : ℝ)

Tactic:
refine exists_le_card_fiber_of_nsmul_le_card_of_maps_to (fun x hx => ?_) nonempty_range_add_one ?_

Premises used: Finset.nonempty_range_add_one, Finset.exists_le_card_fiber_of_nsmul_le_card_of_maps_to
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
n d : ℕ
x : Fin n → ℕ
hx : x ∈ box n d
refine_1 : ∑ i : Fin n, HPow.hPow (β := ℕ) (x i) 2 ≤ n * HPow.hPow (β := ℕ) (d - 1) 2
⊢ ∑ i : Fin n, HPow.hPow (β := ℕ) (x i) 2 ∈ range (n * HPow.hPow (β := ℕ) (d - 1) 2 + 1)

Tactic:
rw [mem_range, Nat.lt_succ_iff]

Premises used: Finset.mem_range, Nat.lt_succ_iff
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
n d : ℕ
x : Fin n → ℕ
hx : x ∈ box n d
⊢ ∑ i : Fin n, HPow.hPow (β := ℕ) (x i) 2 ≤ n * HPow.hPow (β := ℕ) (d - 1) 2

Tactic:
sum_sq_le_of_mem_box hx

Premises used: Behrend.sum_sq_le_of_mem_box
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
n d : ℕ
x : Fin n → ℕ
hx : x ∈ box n d
⊢ ∑ i : Fin n, HPow.hPow (β := ℕ) (x i) 2 ≤ n * HPow.hPow (β := ℕ) (d - 1) 2

Tactic:
exact sum_sq_le_of_mem_box hx

Premises used: Behrend.sum_sq_le_of_mem_box
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
n d : ℕ
refine_2 : HAdd.hAdd (α := ℝ) (↑(n * HPow.hPow (β := ℕ) (d - 1) 2) : ℝ) 1 ≠ 0
⊢ #(range (n * HPow.hPow (β := ℕ) (d - 1) 2 + 1)) •
      ((↑(d ^ n) : ℝ) / HAdd.hAdd (α := ℝ) (↑(n * HPow.hPow (β := ℕ) (d - 1) 2) : ℝ) 1) ≤
    (↑(#(box n d)) : ℝ)

Tactic:
rw [card_range, nsmul_eq_mul, mul_div_assoc', cast_add_one, mul_div_cancel_left₀, card_box]

Premises used: Finset.card_range, mul_div_assoc', mul_div_cancel_left₀, Behrend.card_box, nsmul_eq_mul, Nat.cast_add_one
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
n d : ℕ
⊢ HAdd.hAdd (α := ℝ) (↑(n * HPow.hPow (β := ℕ) (d - 1) 2) : ℝ) 1 ≠ 0

Tactic:
(cast_add_one_pos _).ne'

Premises used: Nat.cast_add_one_pos, LT.lt.ne'
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
n d : ℕ
⊢ HAdd.hAdd (α := ℝ) (↑(n * HPow.hPow (β := ℕ) (d - 1) 2) : ℝ) 1 ≠ 0

Tactic:
exact (cast_add_one_pos _).ne'

Premises used: Nat.cast_add_one_pos, LT.lt.ne'
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
n d : ℕ
obtain :
  ∀ (k : ℕ)
    (hk : (↑(d ^ n) : ℝ) / HAdd.hAdd (α := ℝ) (↑(n * HPow.hPow (β := ℕ) (d - 1) 2) : ℝ) 1 ≤ (↑(#(sphere n d k)) : ℝ)),
    ∃ (k : ℕ), HDiv.hDiv (α := ℝ) (↑(d ^ n) : ℝ) (↑(n * HPow.hPow (β := ℕ) d 2) : ℝ) ≤ (↑(#(sphere n d k)) : ℝ)
⊢ ∃ (k : ℕ), HDiv.hDiv (α := ℝ) (↑(d ^ n) : ℝ) (↑(n * HPow.hPow (β := ℕ) d 2) : ℝ) ≤ (↑(#(sphere n d k)) : ℝ)

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

Premises used: Behrend.exists_large_sphere_aux
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
n d k : ℕ
hk : (↑(d ^ n) : ℝ) / HAdd.hAdd (α := ℝ) (↑(n * HPow.hPow (β := ℕ) (d - 1) 2) : ℝ) 1 ≤ (↑(#(sphere n d k)) : ℝ)
⊢ ∃ (k : ℕ), HDiv.hDiv (α := ℝ) (↑(d ^ n) : ℝ) (↑(n * HPow.hPow (β := ℕ) d 2) : ℝ) ≤ (↑(#(sphere n d k)) : ℝ)

Tactic:
⟨k, ?_⟩

Premises used: Exists.intro
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
n d k : ℕ
hk : (↑(d ^ n) : ℝ) / HAdd.hAdd (α := ℝ) (↑(n * HPow.hPow (β := ℕ) (d - 1) 2) : ℝ) 1 ≤ (↑(#(sphere n d k)) : ℝ)
refine : HDiv.hDiv (α := ℝ) (↑(d ^ n) : ℝ) (↑(n * HPow.hPow (β := ℕ) d 2) : ℝ) ≤ (↑(#(sphere n d k)) : ℝ)
⊢ ∃ (k : ℕ), HDiv.hDiv (α := ℝ) (↑(d ^ n) : ℝ) (↑(n * HPow.hPow (β := ℕ) d 2) : ℝ) ≤ (↑(#(sphere n d k)) : ℝ)

Tactic:
refine ⟨k, ?_⟩
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
n d k : ℕ
hk : (↑(d ^ n) : ℝ) / HAdd.hAdd (α := ℝ) (↑(n * HPow.hPow (β := ℕ) (d - 1) 2) : ℝ) 1 ≤ (↑(#(sphere n d k)) : ℝ)
inl :
  ∀
    (hk :
      (↑(HPow.hPow (β := ℕ) d 0) : ℝ) / HAdd.hAdd (α := ℝ) (↑(0 * HPow.hPow (β := ℕ) (d - 1) 2) : ℝ) 1 ≤
        (↑(card (α := Fin 0 → ℕ) (sphere 0 d k)) : ℝ)),
    HDiv.hDiv (α := ℝ) (↑(HPow.hPow (β := ℕ) d 0) : ℝ) (↑(0 * HPow.hPow (β := ℕ) d 2) : ℝ) ≤
      (↑(card (α := Fin 0 → ℕ) (sphere 0 d k)) : ℝ)
inr : ∀ (hn : n > 0), HDiv.hDiv (α := ℝ) (↑(d ^ n) : ℝ) (↑(n * HPow.hPow (β := ℕ) d 2) : ℝ) ≤ (↑(#(sphere n d k)) : ℝ)
⊢ HDiv.hDiv (α := ℝ) (↑(d ^ n) : ℝ) (↑(n * HPow.hPow (β := ℕ) d 2) : ℝ) ≤ (↑(#(sphere n d k)) : ℝ)

Tactic:
obtain rfl | hn := n.eq_zero_or_pos

Premises used: Nat.eq_zero_or_pos, rfl
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
d k : ℕ
hk :
  (↑(HPow.hPow (β := ℕ) d 0) : ℝ) / HAdd.hAdd (α := ℝ) (↑(0 * HPow.hPow (β := ℕ) (d - 1) 2) : ℝ) 1 ≤
    (↑(card (α := Fin 0 → ℕ) (sphere 0 d k)) : ℝ)
⊢ HDiv.hDiv (α := ℝ) (↑(HPow.hPow (β := ℕ) d 0) : ℝ) (↑(0 * HPow.hPow (β := ℕ) d 2) : ℝ) ≤
    (↑(card (α := Fin 0 → ℕ) (sphere 0 d k)) : ℝ)

Tactic:
simp
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
n d k : ℕ
hk : (↑(d ^ n) : ℝ) / HAdd.hAdd (α := ℝ) (↑(n * HPow.hPow (β := ℕ) (d - 1) 2) : ℝ) 1 ≤ (↑(#(sphere n d k)) : ℝ)
hn : n > 0
inr :
  ∀
    (hk :
      (↑(HPow.hPow (α := ℕ) 0 n) : ℝ) /
          HAdd.hAdd (α := ℝ) (↑(n * HPow.hPow (β := ℕ) (HSub.hSub (α := ℕ) 0 1) 2) : ℝ) 1 ≤
        (↑(#(sphere n 0 k)) : ℝ)),
    HDiv.hDiv (α := ℝ) (↑(HPow.hPow (α := ℕ) 0 n) : ℝ) (↑(n * HPow.hPow (α := ℕ) (β := ℕ) 0 2) : ℝ) ≤
      (↑(#(sphere n 0 k)) : ℝ)
inr₁ : ∀ (hd : d > 0), HDiv.hDiv (α := ℝ) (↑(d ^ n) : ℝ) (↑(n * HPow.hPow (β := ℕ) d 2) : ℝ) ≤ (↑(#(sphere n d k)) : ℝ)
⊢ HDiv.hDiv (α := ℝ) (↑(d ^ n) : ℝ) (↑(n * HPow.hPow (β := ℕ) d 2) : ℝ) ≤ (↑(#(sphere n d k)) : ℝ)

Tactic:
obtain rfl | hd := d.eq_zero_or_pos

Premises used: Nat.eq_zero_or_pos, rfl
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
n k : ℕ
hn : n > 0
hk :
  (↑(HPow.hPow (α := ℕ) 0 n) : ℝ) / HAdd.hAdd (α := ℝ) (↑(n * HPow.hPow (β := ℕ) (HSub.hSub (α := ℕ) 0 1) 2) : ℝ) 1 ≤
    (↑(#(sphere n 0 k)) : ℝ)
⊢ HDiv.hDiv (α := ℝ) (↑(HPow.hPow (α := ℕ) 0 n) : ℝ) (↑(n * HPow.hPow (α := ℕ) (β := ℕ) 0 2) : ℝ) ≤
    (↑(#(sphere n 0 k)) : ℝ)

Tactic:
simp
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
n d k : ℕ
hk : (↑(d ^ n) : ℝ) / HAdd.hAdd (α := ℝ) (↑(n * HPow.hPow (β := ℕ) (d - 1) 2) : ℝ) 1 ≤ (↑(#(sphere n d k)) : ℝ)
hn : n > 0
hd : d > 0
⊢ LE.le (α := ℝ) 0 (↑(d ^ n) : ℝ)

Tactic:
positivity
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
n d k : ℕ
hk : (↑(d ^ n) : ℝ) / HAdd.hAdd (α := ℝ) (↑(n * HPow.hPow (β := ℕ) (d - 1) 2) : ℝ) 1 ≤ (↑(#(sphere n d k)) : ℝ)
hn : n > 0
hd : d > 0
⊢ 0 < HAdd.hAdd (α := ℝ) (↑(n * HPow.hPow (β := ℕ) (d - 1) 2) : ℝ) 1

Tactic:
positivity
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
n d k : ℕ
hk : (↑(d ^ n) : ℝ) / HAdd.hAdd (α := ℝ) (↑(n * HPow.hPow (β := ℕ) (d - 1) 2) : ℝ) 1 ≤ (↑(#(sphere n d k)) : ℝ)
hn : n > 0
hd : d > 0
inr : HAdd.hAdd (α := ℝ) (↑(n * HPow.hPow (β := ℕ) (d - 1) 2) : ℝ) 1 ≤ (↑(n * HPow.hPow (β := ℕ) d 2) : ℝ)
⊢ HDiv.hDiv (α := ℝ) (↑(d ^ n) : ℝ) (↑(n * HPow.hPow (β := ℕ) d 2) : ℝ) ≤ (↑(#(sphere n d k)) : ℝ)

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

Premises used: div_le_div_of_nonneg_left, LE.le.trans
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
n d k : ℕ
hk : (↑(d ^ n) : ℝ) / HAdd.hAdd (α := ℝ) (↑(n * HPow.hPow (β := ℕ) (d - 1) 2) : ℝ) 1 ≤ (↑(#(sphere n d k)) : ℝ)
hn : n > 0
hd : d > 0
inr : 1 ≤ (↑n : ℝ) * (HMul.hMul (α := ℝ) 2 (↑d : ℝ) - 1)
⊢ HAdd.hAdd (α := ℝ) (↑(n * HPow.hPow (β := ℕ) (d - 1) 2) : ℝ) 1 ≤ (↑(n * HPow.hPow (β := ℕ) 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]

Premises used: sub_add, one_pow, sub_sq, mul_sub, Nat.cast_sub, le_sub_iff_add_le', Nat.cast_mul, Nat.cast_pow, mul_one, Nat.cast_one, sub_sub_self
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
n d k : ℕ
hk : (↑(d ^ n) : ℝ) / HAdd.hAdd (α := ℝ) (↑(n * HPow.hPow (β := ℕ) (d - 1) 2) : ℝ) 1 ≤ (↑(#(sphere n d k)) : ℝ)
hn : n > 0
hd : d > 0
inr : LE.le (α := ℝ) 1 (↑n : ℝ)
inr₁ : 1 ≤ HMul.hMul (α := ℝ) 2 (↑d : ℝ) - 1
⊢ 1 ≤ (↑n : ℝ) * (HMul.hMul (α := ℝ) 2 (↑d : ℝ) - 1)

Tactic:
apply one_le_mul_of_one_le_of_one_le

Premises used: one_le_mul_of_one_le_of_one_le
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
n d k : ℕ
hk : (↑(d ^ n) : ℝ) / HAdd.hAdd (α := ℝ) (↑(n * HPow.hPow (β := ℕ) (d - 1) 2) : ℝ) 1 ≤ (↑(#(sphere n d k)) : ℝ)
hn : n > 0
hd : d > 0
inr inr₁ inr₂ inr₃ : 1 ≤ n
⊢ LE.le (α := ℝ) 1 (↑n : ℝ)

Tactic:
rwa [one_le_cast]

Premises used: Nat.one_le_cast
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
n d k : ℕ
hk : (↑(d ^ n) : ℝ) / HAdd.hAdd (α := ℝ) (↑(n * HPow.hPow (β := ℕ) (d - 1) 2) : ℝ) 1 ≤ (↑(#(sphere n d k)) : ℝ)
hn : n > 0
hd : d > 0
inr : HAdd.hAdd (α := ℝ) 1 1 ≤ HMul.hMul (α := ℝ) 2 (↑d : ℝ)
⊢ 1 ≤ HMul.hMul (α := ℝ) 2 (↑d : ℝ) - 1

Tactic:
rw [_root_.le_sub_iff_add_le]

Premises used: le_sub_iff_add_le
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
n d k : ℕ
hk : (↑(d ^ n) : ℝ) / HAdd.hAdd (α := ℝ) (↑(n * HPow.hPow (β := ℕ) (d - 1) 2) : ℝ) 1 ≤ (↑(#(sphere n d k)) : ℝ)
hn : n > 0
hd : d > 0
inr : 1 ≤ d
⊢ HAdd.hAdd (α := ℝ) 1 1 ≤ HMul.hMul (α := ℝ) 2 (↑d : ℝ)

Tactic:
norm_num
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
n d k : ℕ
hk : (↑(d ^ n) : ℝ) / HAdd.hAdd (α := ℝ) (↑(n * HPow.hPow (β := ℕ) (d - 1) 2) : ℝ) 1 ≤ (↑(#(sphere n d k)) : ℝ)
hn : n > 0
hd : d > 0
⊢ 1 ≤ d

Tactic:
one_le_cast.2 hd

Premises used: Iff.mpr, Nat.one_le_cast
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
n d k : ℕ
hk : (↑(d ^ n) : ℝ) / HAdd.hAdd (α := ℝ) (↑(n * HPow.hPow (β := ℕ) (d - 1) 2) : ℝ) 1 ≤ (↑(#(sphere n d k)) : ℝ)
hn : n > 0
hd : d > 0
⊢ 1 ≤ d

Tactic:
exact one_le_cast.2 hd

Premises used: Iff.mpr, Nat.one_le_cast
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
n d : ℕ
⊢ HDiv.hDiv (α := ℝ) (↑(d ^ n) : ℝ) (↑(n * HPow.hPow (β := ℕ) d 2) : ℝ) ≤
    (↑((rothNumberNat : (a : ℕ) → ℕ) ((2 * d - 1) ^ n)) : ℝ)

Tactic:
let ⟨_, h⟩ := exists_large_sphere n d
  h.trans <| cast_le.2 <| card_sphere_le_rothNumberNat _ _ _

Premises used: Iff.mpr, HMul.hMul, HSub.hSub, HDiv.hDiv, rothNumberNat, LE.le, Nat.cast, Behrend.card_sphere_le_rothNumberNat, HPow.hPow, Nat.cast_le, LE.le.trans, OfNat.ofNat, DFunLike.coe, _private.0.Behrend.bound_aux'.match_1, Behrend.exists_large_sphere
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
n d : ℕ
hd : d ≠ 0
hn : 2 ≤ n
⊢ HDiv.hDiv (α := ℝ) (↑(d ^ n) : ℝ) (↑(n * HPow.hPow (β := ℕ) d 2) : ℝ) ≤
    (↑((rothNumberNat : (a : ℕ) → ℕ) ((2 * d - 1) ^ n)) : ℝ)

Tactic:
bound_aux' n d

Premises used: Behrend.bound_aux'
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
n d : ℕ
hd : d ≠ 0
hn : 2 ≤ n
h :
  HPow.hPow (α := ℝ) (↑d : ℝ) (n - 2) / (↑n : ℝ) = HDiv.hDiv (α := ℝ) (↑(d ^ n) : ℝ) (↑(n * HPow.hPow (β := ℕ) d 2) : ℝ)
⊢ HPow.hPow (α := ℝ) (↑d : ℝ) (n - 2) / (↑n : ℝ) ≤ (↑((rothNumberNat : (a : ℕ) → ℕ) ((2 * d - 1) ^ n)) : ℝ)

Tactic:
convert! bound_aux' n d using 1

Premises used: Behrend.bound_aux'
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
n d : ℕ
hd : d ≠ 0
hn : 2 ≤ n
rw : Ne (α := ℝ) (↑d : ℝ) 0
⊢ HPow.hPow (α := ℝ) (↑d : ℝ) (n - 2) / (↑n : ℝ) = HDiv.hDiv (α := ℝ) (↑(d ^ n) : ℝ) (↑(n * HPow.hPow (β := ℕ) d 2) : ℝ)

Tactic:
rw [cast_mul, cast_pow, mul_comm, ← div_div, pow_sub₀ _ _ hn, ← div_eq_mul_inv, cast_pow]

Premises used: div_eq_mul_inv, Nat.cast_mul, mul_comm, pow_sub₀, Nat.cast_pow, div_div
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
n d : ℕ
hd : d ≠ 0
hn : 2 ≤ n
rwa rwa₁ rwa₂ rwa₃ : d ≠ 0
⊢ Ne (α := ℝ) (↑d : ℝ) 0

Tactic:
rwa [cast_ne_zero]

Premises used: Nat.cast_ne_zero
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
⊢ 8 = HPow.hPow (α := ℝ) (β := ℕ) 2 3

Tactic:
norm_num1
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
rw : log 2 * 2 ≤ √(3 * log 2)
⊢ log 2 * 2 ≤ √(log 8)

Tactic:
rw [show (8 : ℝ) = 2 ^ 3 by norm_num1, Real.log_pow, Nat.cast_ofNat]

Premises used: Nat.cast_ofNat, Real.log_pow
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
h : HPow.hPow (β := ℕ) (log 2 * 2) 2 ≤ 3 * log 2
⊢ log 2 * 2 ≤ √(3 * log 2)

Tactic:
apply le_sqrt_of_sq_le

Premises used: Real.le_sqrt_of_sq_le
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
h : log 2 * HPow.hPow (α := ℝ) (β := ℕ) 2 2 * log 2 ≤ 3 * log 2
⊢ HPow.hPow (β := ℕ) (log 2 * 2) 2 ≤ 3 * log 2

Tactic:
rw [mul_pow, sq (log 2), mul_assoc, mul_comm]

Premises used: mul_assoc, sq, Real.log, mul_comm, OfNat.ofNat, mul_pow
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
h : log 2 * HPow.hPow (α := ℝ) (β := ℕ) 2 2 ≤ 3
⊢ log 2 * HPow.hPow (α := ℝ) (β := ℕ) 2 2 * log 2 ≤ 3 * log 2

Tactic:
gcongr
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
linarith : 3 < log 2 * HPow.hPow (α := ℝ) (β := ℕ) 2 2 → 156250000 / 156250000 = 1
linarith₁ : 3 < log 2 * HPow.hPow (α := ℝ) (β := ℕ) 2 2 → HMul.hMul (α := ℝ) 1 156250000 = 156250000
linarith₂ : 3 < log 2 * HPow.hPow (α := ℝ) (β := ℕ) 2 2 → GT.gt (α := ℝ) 156250000 0
linarith₃ :
  3 < log 2 * HPow.hPow (α := ℝ) (β := ℕ) 2 2 →
    HMul.hMul (α := ℝ) 8883253 (-1) + 39062500 * (3 - log 2 * HPow.hPow (α := ℝ) (β := ℕ) 2 2) +
        (156250000 * log 2 - HMul.hMul (α := ℝ) 1 108304247) =
      0
linarith₄ : 3 < log 2 * HPow.hPow (α := ℝ) (β := ℕ) 2 2 → GT.gt (α := ℝ) 8883253 0
linarith₅ : 3 < log 2 * HPow.hPow (α := ℝ) (β := ℕ) 2 2 → GT.gt (α := ℝ) 39062500 0
⊢ log 2 * HPow.hPow (α := ℝ) (β := ℕ) 2 2 ≤ 3

Tactic:
linarith only [log_two_lt_d9.le]

Premises used: LT.lt.le, Real.log_two_lt_d9
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
rw : HMul.hMul (α := ℝ) 8 2 ≤ HSub.hSub (α := ℝ) 8 2 * rexp 1
rw₁ : 0 < 1 - 2 / rexp 1
⊢ 2 / (1 - 2 / rexp 1) ≤ 8

Tactic:
rw [div_le_iff₀, mul_sub, mul_one, mul_div_assoc', le_sub_comm, div_le_iff₀ (exp_pos _)]

Premises used: div_le_iff₀, mul_sub, mul_div_assoc', mul_one, le_sub_comm, Real.exp_pos
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
linarith : HSub.hSub (α := ℝ) 8 2 * rexp 1 < HMul.hMul (α := ℝ) 8 2 → 10000000000 / 10000000000 = 1
linarith₁ : HSub.hSub (α := ℝ) 8 2 * rexp 1 < HMul.hMul (α := ℝ) 8 2 → HMul.hMul (α := ℝ) 1 10000000000 = 10000000000
linarith₂ : HSub.hSub (α := ℝ) 8 2 * rexp 1 < HMul.hMul (α := ℝ) 8 2 → GT.gt (α := ℝ) 10000000000 0
linarith₃ :
  HSub.hSub (α := ℝ) 8 2 * rexp 1 < HMul.hMul (α := ℝ) 8 2 →
    HMul.hMul (α := ℝ) 1548454849 (-1) + 5000000000 * (HSub.hSub (α := ℝ) 8 2 * rexp 1 - HMul.hMul (α := ℝ) 8 2) +
        3 * (HMul.hMul (α := ℝ) 1 27182818283 - 10000000000 * rexp 1) =
      0
linarith₄ : HSub.hSub (α := ℝ) 8 2 * rexp 1 < HMul.hMul (α := ℝ) 8 2 → GT.gt (α := ℝ) 1548454849 0
linarith₅ : HSub.hSub (α := ℝ) 8 2 * rexp 1 < HMul.hMul (α := ℝ) 8 2 → GT.gt (α := ℝ) 5000000000 0
linarith₆ : HSub.hSub (α := ℝ) 8 2 * rexp 1 < HMul.hMul (α := ℝ) 8 2 → GT.gt (α := ℝ) 3 0
⊢ HMul.hMul (α := ℝ) 8 2 ≤ HSub.hSub (α := ℝ) 8 2 * rexp 1

Tactic:
linarith [exp_one_gt_d9]

Premises used: Real.exp_one_gt_d9
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
rw : 2 < rexp 1
rw₁ : 0 < rexp 1
⊢ 0 < 1 - 2 / rexp 1

Tactic:
rw [sub_pos, div_lt_one]

Premises used: sub_pos, div_lt_one
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
⊢ LT.lt (α := ℝ) 2 2.7182818283

Tactic:
norm_num
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
⊢ 2 < rexp 1

Tactic:
exact exp_one_gt_d9.trans' (by norm_num)

Premises used: Real.exp_one_gt_d9, LT.lt.trans'