awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
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
⊢ (2 * d + 1) ^ n - 1 = HMul.hMul (α := ℕ) (∑ i : Fin n, d * (2 * d + 1) ^ (↑i : ℕ)) 2
have rw₃ : (2 * d + 1) ^ n - 1 = 2 * d * ∑ i ∈ range n, (2 * d + 1) ^ i
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]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
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
⊢ (2 * d + 1) ^ n - 1 = HMul.hMul (α := ℕ) (∑ i : Fin n, d * (2 * d + 1) ^ (↑i : ℕ)) 2
have rw₄ : (∑ i ∈ range n, (2 * d + 1) ^ i) * (2 * d) + 1 - 1 = 2 * d * ∑ i ∈ range n, (2 * d + 1) ^ i
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]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
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
⊢ (2 * d + 1) ^ n - 1 = HMul.hMul (α := ℕ) (∑ i : Fin n, d * (2 * d + 1) ^ (↑i : ℕ)) 2
have rw₅ : (∑ i ∈ range n, (2 * d + 1) ^ i) * (2 * d) = 2 * d * ∑ i ∈ range n, (2 * d + 1) ^ i
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]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
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
⊢ (2 * d + 1) ^ n - 1 = HMul.hMul (α := ℕ) (∑ i : Fin n, d * (2 * d + 1) ^ (↑i : ℕ)) 2
have rw₆ : 2 * d * ∑ i ∈ range n, (2 * d + 1) ^ i = 2 * d * ∑ i ∈ range n, (2 * d + 1) ^ i
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]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
n d k : ℕ
⊢ #(sphere n d k) ≤ (rothNumberNat : (a : ℕ) → ℕ) ((2 * d - 1) ^ n)
have zero : card (α := Fin 0 → ℕ) (sphere 0 d k) ≤ (rothNumberNat : (a : ℕ) → ℕ) (HPow.hPow (β := ℕ) (2 * d - 1) 0)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
n d k : ℕ
zero : card (α := Fin 0 → ℕ) (sphere 0 d k) ≤ (rothNumberNat : (a : ℕ) → ℕ) (HPow.hPow (β := ℕ) (2 * d - 1) 0)
⊢ #(sphere n d k) ≤ (rothNumberNat : (a : ℕ) → ℕ) ((2 * d - 1) ^ n)
have succ : ∀ (n : ℕ), card (α := Fin (n + 1) → ℕ) (sphere (n + 1) d k) ≤ (rothNumberNat : (a : ℕ) → ℕ) ((2 * d - 1) ^ (n + 1))
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
d k : ℕ
⊢ card (α := Fin 0 → ℕ) (sphere 0 d k) ≤ (rothNumberNat : (a : ℕ) → ℕ) 1
have zero : Fintype.card (Fin 0 → ℕ) = (rothNumberNat : (a : ℕ) → ℕ) 1
Tactic: refine (card_le_univ _).trans_eq ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
d k n : ℕ
⊢ card (α := Fin (n + 1) → ℕ) (sphere (n + 1) d k) ≤ (rothNumberNat : (a : ℕ) → ℕ) ((2 * d - 1) ^ (n + 1))
have succ : card (α := Fin (n + 1) → ℕ) (sphere (n + 1) 0 k) ≤
  (rothNumberNat : (a : ℕ) → ℕ) ((HMul.hMul (α := ℕ) 2 0 - 1) ^ (n + 1))
Tactic: cases d
Cleared hypotheses: d
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
d k n : ℕ
succ :
  card (α := Fin (n + 1) → ℕ) (sphere (n + 1) 0 k) ≤
    (rothNumberNat : (a : ℕ) → ℕ) ((HMul.hMul (α := ℕ) 2 0 - 1) ^ (n + 1))
⊢ card (α := Fin (n + 1) → ℕ) (sphere (n + 1) d k) ≤ (rothNumberNat : (a : ℕ) → ℕ) ((2 * d - 1) ^ (n + 1))
have succ₁ : ∀ (n_1 : ℕ),
  card (α := Fin (n + 1) → ℕ) (sphere (n + 1) (n_1 + 1) k) ≤
    (rothNumberNat : (a : ℕ) → ℕ) ((2 * (n_1 + 1) - 1) ^ (n + 1))
Tactic: cases d
Cleared hypotheses: d
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
k n n_1 : ℕ
⊢ card (α := Fin (n + 1) → ℕ) (sphere (n + 1) (n_1 + 1) k) ≤
    (rothNumberNat : (a : ℕ) → ℕ) ((2 * (n_1 + 1) - 1) ^ (n + 1))
have 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)
Tactic: apply threeAPFree_image_sphere.le_rothNumberNat _ _ (card_image_of_injOn _)
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
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)
⊢ card (α := Fin (n + 1) → ℕ) (sphere (n + 1) (n_1 + 1) k) ≤
    (rothNumberNat : (a : ℕ) → ℕ) ((2 * (n_1 + 1) - 1) ^ (n + 1))
have apply₁ : 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 threeAPFree_image_sphere.le_rothNumberNat _ _ (card_image_of_injOn _)
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
k n 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)
have 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)
Tactic: simp only [mem_image, and_imp, forall_exists_index,
      sphere, mem_filter]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
k n n_1 : ℕ
⊢ Set.InjOn (β := ℕ) (⇑(map (2 * (n_1 + 1) - 1)) : (a : Fin (n + 1) → ℕ) → ℕ)
    (↑(sphere (n + 1) (n_1 + 1) k) : Set (Fin (n + 1) → ℕ))
have 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
Tactic: apply map_injOn.mono fun x => ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
k n n_1 : ℕ
x : Fin (n + 1) → ℕ
⊢ 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
have 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
Tactic: simp only [mem_coe, sphere, mem_filter, mem_box, and_imp, two_mul]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
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)) : ℝ)
have 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)
Tactic: refine exists_le_card_fiber_of_nsmul_le_card_of_maps_to (fun x hx => ?_) nonempty_range_add_one ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
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)
⊢ ∃ k ∈ range (n * HPow.hPow (β := ℕ) (d - 1) 2 + 1),
    (↑(d ^ n) : ℝ) / HAdd.hAdd (α := ℝ) (↑(n * HPow.hPow (β := ℕ) (d - 1) 2) : ℝ) 1 ≤ (↑(#(sphere n d k)) : ℝ)
have refine_2 : #(range (n * HPow.hPow (β := ℕ) (d - 1) 2 + 1)) •
    ((↑(d ^ n) : ℝ) / HAdd.hAdd (α := ℝ) (↑(n * HPow.hPow (β := ℕ) (d - 1) 2) : ℝ) 1) ≤
  (↑(#(box n d)) : ℝ)
Tactic: refine exists_le_card_fiber_of_nsmul_le_card_of_maps_to (fun x hx => ?_) nonempty_range_add_one ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
n d : ℕ
x : Fin n → ℕ
hx : x ∈ box n d
⊢ ∑ i : Fin n, HPow.hPow (β := ℕ) (x i) 2 ∈ range (n * HPow.hPow (β := ℕ) (d - 1) 2 + 1)
have refine_1 : ∑ i : Fin n, HPow.hPow (β := ℕ) (x i) 2 ≤ n * HPow.hPow (β := ℕ) (d - 1) 2
Tactic: rw [mem_range, Nat.lt_succ_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
n d : ℕ
⊢ #(range (n * HPow.hPow (β := ℕ) (d - 1) 2 + 1)) •
      ((↑(d ^ n) : ℝ) / HAdd.hAdd (α := ℝ) (↑(n * HPow.hPow (β := ℕ) (d - 1) 2) : ℝ) 1) ≤
    (↑(#(box n d)) : ℝ)
have refine_2 : HAdd.hAdd (α := ℝ) (↑(n * HPow.hPow (β := ℕ) (d - 1) 2) : ℝ) 1 ≠ 0
Tactic: rw [card_range, nsmul_eq_mul, mul_div_assoc', cast_add_one, mul_div_cancel_left₀, card_box]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
n d : ℕ
⊢ ∃ (k : ℕ), HDiv.hDiv (α := ℝ) (↑(d ^ n) : ℝ) (↑(n * HPow.hPow (β := ℕ) d 2) : ℝ) ≤ (↑(#(sphere n d k)) : ℝ)
have 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)) : ℝ)
Tactic: obtain ⟨k, -, hk⟩ := exists_large_sphere_aux n d
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
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)) : ℝ)
have refine : HDiv.hDiv (α := ℝ) (↑(d ^ n) : ℝ) (↑(n * HPow.hPow (β := ℕ) d 2) : ℝ) ≤ (↑(#(sphere n d k)) : ℝ)
Tactic: refine ⟨k, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
n d k : ℕ
hk : (↑(d ^ n) : ℝ) / HAdd.hAdd (α := ℝ) (↑(n * HPow.hPow (β := ℕ) (d - 1) 2) : ℝ) 1 ≤ (↑(#(sphere n d k)) : ℝ)
⊢ HDiv.hDiv (α := ℝ) (↑(d ^ n) : ℝ) (↑(n * HPow.hPow (β := ℕ) d 2) : ℝ) ≤ (↑(#(sphere n d k)) : ℝ)
have 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)) : ℝ)
Tactic: obtain rfl | hn := n.eq_zero_or_pos
Cleared hypotheses: n, hk
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
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)) : ℝ)
⊢ HDiv.hDiv (α := ℝ) (↑(d ^ n) : ℝ) (↑(n * HPow.hPow (β := ℕ) d 2) : ℝ) ≤ (↑(#(sphere n d k)) : ℝ)
have inr : ∀ (hn : n > 0), HDiv.hDiv (α := ℝ) (↑(d ^ n) : ℝ) (↑(n * HPow.hPow (β := ℕ) d 2) : ℝ) ≤ (↑(#(sphere n d k)) : ℝ)
Tactic: obtain rfl | hn := n.eq_zero_or_pos
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
n d k : ℕ
hk : (↑(d ^ n) : ℝ) / HAdd.hAdd (α := ℝ) (↑(n * HPow.hPow (β := ℕ) (d - 1) 2) : ℝ) 1 ≤ (↑(#(sphere n d k)) : ℝ)
hn : n > 0
⊢ HDiv.hDiv (α := ℝ) (↑(d ^ n) : ℝ) (↑(n * HPow.hPow (β := ℕ) d 2) : ℝ) ≤ (↑(#(sphere n d k)) : ℝ)
have 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)) : ℝ)
Tactic: obtain rfl | hd := d.eq_zero_or_pos
Cleared hypotheses: d, hk
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
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)) : ℝ)
⊢ HDiv.hDiv (α := ℝ) (↑(d ^ n) : ℝ) (↑(n * HPow.hPow (β := ℕ) d 2) : ℝ) ≤ (↑(#(sphere n d k)) : ℝ)
have inr₁ : ∀ (hd : d > 0), HDiv.hDiv (α := ℝ) (↑(d ^ n) : ℝ) (↑(n * HPow.hPow (β := ℕ) d 2) : ℝ) ≤ (↑(#(sphere n d k)) : ℝ)
Tactic: obtain rfl | hd := d.eq_zero_or_pos
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
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
⊢ HDiv.hDiv (α := ℝ) (↑(d ^ n) : ℝ) (↑(n * HPow.hPow (β := ℕ) d 2) : ℝ) ≤ (↑(#(sphere n d k)) : ℝ)
have inr : HAdd.hAdd (α := ℝ) (↑(n * HPow.hPow (β := ℕ) (d - 1) 2) : ℝ) 1 ≤ (↑(n * HPow.hPow (β := ℕ) d 2) : ℝ)
Tactic: refine (div_le_div_of_nonneg_left (by positivity) (by positivity) ?_).trans hk
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
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
⊢ HAdd.hAdd (α := ℝ) (↑(n * HPow.hPow (β := ℕ) (d - 1) 2) : ℝ) 1 ≤ (↑(n * HPow.hPow (β := ℕ) d 2) : ℝ)
have inr : 1 ≤ (↑n : ℝ) * (HMul.hMul (α := ℝ) 2 (↑d : ℝ) - 1)
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]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
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 ≤ (↑n : ℝ) * (HMul.hMul (α := ℝ) 2 (↑d : ℝ) - 1)
have inr : LE.le (α := ℝ) 1 (↑n : ℝ)
Tactic: apply one_le_mul_of_one_le_of_one_le
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
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 : ℝ)
⊢ 1 ≤ (↑n : ℝ) * (HMul.hMul (α := ℝ) 2 (↑d : ℝ) - 1)
have inr₁ : 1 ≤ HMul.hMul (α := ℝ) 2 (↑d : ℝ) - 1
Tactic: apply one_le_mul_of_one_le_of_one_le
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
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 (α := ℝ) 1 (↑n : ℝ)
have inr : 1 ≤ n
Tactic: rwa [one_le_cast]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
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 ≤ HMul.hMul (α := ℝ) 2 (↑d : ℝ) - 1
have inr : HAdd.hAdd (α := ℝ) 1 1 ≤ HMul.hMul (α := ℝ) 2 (↑d : ℝ)
Tactic: rw [_root_.le_sub_iff_add_le]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
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
⊢ HAdd.hAdd (α := ℝ) 1 1 ≤ HMul.hMul (α := ℝ) 2 (↑d : ℝ)
have inr : 1 ≤ d
Tactic: norm_num
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
n d : ℕ
hd : d ≠ 0
hn : 2 ≤ n
⊢ HPow.hPow (α := ℝ) (↑d : ℝ) (n - 2) / (↑n : ℝ) ≤ (↑((rothNumberNat : (a : ℕ) → ℕ) ((2 * d - 1) ^ n)) : ℝ)
have h : HPow.hPow (α := ℝ) (↑d : ℝ) (n - 2) / (↑n : ℝ) = HDiv.hDiv (α := ℝ) (↑(d ^ n) : ℝ) (↑(n * HPow.hPow (β := ℕ) d 2) : ℝ)
Tactic: convert! bound_aux' n d using 1
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
n d : ℕ
hd : d ≠ 0
hn : 2 ≤ n
⊢ HPow.hPow (α := ℝ) (↑d : ℝ) (n - 2) / (↑n : ℝ) = HDiv.hDiv (α := ℝ) (↑(d ^ n) : ℝ) (↑(n * HPow.hPow (β := ℕ) d 2) : ℝ)
have rw : Ne (α := ℝ) (↑d : ℝ) 0
Tactic: rw [cast_mul, cast_pow, mul_comm, ← div_div, pow_sub₀ _ _ hn, ← div_eq_mul_inv, cast_pow]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
⊢ log 2 * 2 ≤ √(log 8)
have rw : log 2 * 2 ≤ √(3 * log 2)
Tactic: rw [show (8 : ℝ) = 2 ^ 3 by norm_num1, Real.log_pow, Nat.cast_ofNat]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
⊢ log 2 * 2 ≤ √(3 * log 2)
have h : HPow.hPow (β := ℕ) (log 2 * 2) 2 ≤ 3 * log 2
Tactic: apply le_sqrt_of_sq_le
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
⊢ HPow.hPow (β := ℕ) (log 2 * 2) 2 ≤ 3 * log 2
have h : log 2 * HPow.hPow (α := ℝ) (β := ℕ) 2 2 * log 2 ≤ 3 * log 2
Tactic: rw [mul_pow, sq (log 2), mul_assoc, mul_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
⊢ log 2 * HPow.hPow (α := ℝ) (β := ℕ) 2 2 * log 2 ≤ 3 * log 2
have h : log 2 * HPow.hPow (α := ℝ) (β := ℕ) 2 2 ≤ 3
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
⊢ log 2 * HPow.hPow (α := ℝ) (β := ℕ) 2 2 ≤ 3
have linarith : 3 < log 2 * HPow.hPow (α := ℝ) (β := ℕ) 2 2 → 156250000 / 156250000 = 1
Tactic: linarith only [log_two_lt_d9.le]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
linarith : 3 < log 2 * HPow.hPow (α := ℝ) (β := ℕ) 2 2 → 156250000 / 156250000 = 1
⊢ log 2 * HPow.hPow (α := ℝ) (β := ℕ) 2 2 ≤ 3
have linarith₁ : 3 < log 2 * HPow.hPow (α := ℝ) (β := ℕ) 2 2 → HMul.hMul (α := ℝ) 1 156250000 = 156250000
Tactic: linarith only [log_two_lt_d9.le]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
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
⊢ log 2 * HPow.hPow (α := ℝ) (β := ℕ) 2 2 ≤ 3
have linarith₂ : 3 < log 2 * HPow.hPow (α := ℝ) (β := ℕ) 2 2 → GT.gt (α := ℝ) 156250000 0
Tactic: linarith only [log_two_lt_d9.le]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
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
⊢ log 2 * HPow.hPow (α := ℝ) (β := ℕ) 2 2 ≤ 3
have 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
Tactic: linarith only [log_two_lt_d9.le]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
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
⊢ log 2 * HPow.hPow (α := ℝ) (β := ℕ) 2 2 ≤ 3
have linarith₄ : 3 < log 2 * HPow.hPow (α := ℝ) (β := ℕ) 2 2 → GT.gt (α := ℝ) 8883253 0
Tactic: linarith only [log_two_lt_d9.le]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
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
⊢ log 2 * HPow.hPow (α := ℝ) (β := ℕ) 2 2 ≤ 3
have linarith₅ : 3 < log 2 * HPow.hPow (α := ℝ) (β := ℕ) 2 2 → GT.gt (α := ℝ) 39062500 0
Tactic: linarith only [log_two_lt_d9.le]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
⊢ 2 / (1 - 2 / rexp 1) ≤ 8
have rw : HMul.hMul (α := ℝ) 8 2 ≤ HSub.hSub (α := ℝ) 8 2 * rexp 1
Tactic: rw [div_le_iff₀, mul_sub, mul_one, mul_div_assoc', le_sub_comm, div_le_iff₀ (exp_pos _)]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
rw : HMul.hMul (α := ℝ) 8 2 ≤ HSub.hSub (α := ℝ) 8 2 * rexp 1
⊢ 2 / (1 - 2 / rexp 1) ≤ 8
have rw₁ : 0 < 1 - 2 / rexp 1
Tactic: rw [div_le_iff₀, mul_sub, mul_one, mul_div_assoc', le_sub_comm, div_le_iff₀ (exp_pos _)]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
⊢ HMul.hMul (α := ℝ) 8 2 ≤ HSub.hSub (α := ℝ) 8 2 * rexp 1
have linarith : HSub.hSub (α := ℝ) 8 2 * rexp 1 < HMul.hMul (α := ℝ) 8 2 → 10000000000 / 10000000000 = 1
Tactic: linarith [exp_one_gt_d9]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
linarith : HSub.hSub (α := ℝ) 8 2 * rexp 1 < HMul.hMul (α := ℝ) 8 2 → 10000000000 / 10000000000 = 1
⊢ HMul.hMul (α := ℝ) 8 2 ≤ HSub.hSub (α := ℝ) 8 2 * rexp 1
have linarith₁ : HSub.hSub (α := ℝ) 8 2 * rexp 1 < HMul.hMul (α := ℝ) 8 2 → HMul.hMul (α := ℝ) 1 10000000000 = 10000000000
Tactic: linarith [exp_one_gt_d9]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
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
⊢ HMul.hMul (α := ℝ) 8 2 ≤ HSub.hSub (α := ℝ) 8 2 * rexp 1
have linarith₂ : HSub.hSub (α := ℝ) 8 2 * rexp 1 < HMul.hMul (α := ℝ) 8 2 → GT.gt (α := ℝ) 10000000000 0
Tactic: linarith [exp_one_gt_d9]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
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
⊢ HMul.hMul (α := ℝ) 8 2 ≤ HSub.hSub (α := ℝ) 8 2 * rexp 1
have 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
Tactic: linarith [exp_one_gt_d9]