awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
n d_1 k N : ℕ
x : Fin n → ℕ
d : ℕ
a b : Fin n → ℕ
simp_rw :
  ∑ x : Fin n, (a x + b x) * d ^ (↑x : ℕ) =
    HAdd.hAdd (α := ℕ) (∑ i : Fin n, a i * d ^ (↑i : ℕ)) (∑ i : Fin n, b i * d ^ (↑i : ℕ))
simp_rw₁ :
  ∑ x : Fin n, (a x * d ^ (↑x : ℕ) + b x * d ^ (↑x : ℕ)) =
    HAdd.hAdd (α := ℕ) (∑ i : Fin n, a i * d ^ (↑i : ℕ)) (∑ i : Fin n, b i * d ^ (↑i : ℕ))
⊢ ∑ i : Fin n, (a + b) i * d ^ (↑i : ℕ) =
    HAdd.hAdd (α := ℕ) (∑ i : Fin n, a i * d ^ (↑i : ℕ)) (∑ i : Fin n, b i * d ^ (↑i : ℕ))

Tactic:
simp_rw [Pi.add_apply, add_mul, sum_add_distrib]

Premises used: add_mul, Finset.sum_add_distrib, Pi.add_apply
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
d : ℕ
a : Fin 0 → ℕ
⊢ Eq (α := ℕ) ((map d : (a : Fin 0 → ℕ) → ℕ) a : ℕ) (0 : ℕ)

Tactic:
simp [map]

Premises used: Behrend.map
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
n d : ℕ
a : Fin (n + 1) → ℕ
⊢ (map d : (a : Fin (n + 1) → ℕ) → ℕ) a = a 0 + (∑ x : Fin n, a x.succ * d ^ (↑x : ℕ)) * d

Tactic:
simp [map, Fin.sum_univ_succ, _root_.pow_succ, ← mul_assoc, ← sum_mul]

Premises used: pow_succ, mul_assoc, Finset.sum_mul, Fin.sum_univ_succ, Behrend.map
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
n d : ℕ
a : Fin (n + 1) → ℕ
⊢ (map d : (a : Fin (n + 1) → ℕ) → ℕ) a = a 0 + HMul.hMul (α := ℕ) ((map d : (a : Fin n → ℕ) → ℕ) (a ∘ Fin.succ) : ℕ) d

Tactic:
map_succ _

Premises used: Multiset.sum, Multiset.foldr, Behrend.map_succ, Finset.sum
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
n d : ℕ
x y : Fin n → ℕ
h : x ≤ y
dsimp : LE.le (α := ℕ) (∑ i : Fin n, x i * d ^ (↑i : ℕ)) (∑ i : Fin n, y i * d ^ (↑i : ℕ))
⊢ LE.le (α := ℕ) ((map d : (a : Fin n → ℕ) → ℕ) x : ℕ) ((map d : (a : Fin n → ℕ) → ℕ) y : ℕ)

Tactic:
dsimp
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
n d : ℕ
x y : Fin n → ℕ
h : x ≤ y
⊢ LE.le (α := ℕ) (∑ i : Fin n, x i * d ^ (↑i : ℕ)) (∑ i : Fin n, y i * d ^ (↑i : ℕ))

Tactic:
sum_le_sum fun i _ => Nat.mul_le_mul_right _ <| h i

Premises used: Nat.mul_le_mul_right, Fin.val, HPow.hPow, Finset.sum_le_sum
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
n d : ℕ
x y : Fin n → ℕ
h : x ≤ y
⊢ LE.le (α := ℕ) (∑ i : Fin n, x i * d ^ (↑i : ℕ)) (∑ i : Fin n, y i * d ^ (↑i : ℕ))

Tactic:
exact sum_le_sum fun i _ => Nat.mul_le_mul_right _ <| h i

Premises used: Nat.mul_le_mul_right, Finset.sum_le_sum
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
n d : ℕ
a : Fin n.succ → ℕ
rw : (a 0 + (∑ x : Fin n, a x.succ * d ^ (↑x : ℕ)) * d) % d = a 0 % d
rw₁ rw₂ : a 0 % d = a 0 % d
⊢ HMod.hMod (α := ℕ) ((map d : (a : Fin n.succ → ℕ) → ℕ) a : ℕ) d = a 0 % d

Tactic:
rw [map_succ, Nat.add_mul_mod_self_right]

Premises used: Behrend.map_succ, Nat.add_mul_mod_self_right
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
n d : ℕ
x₁ x₂ : Fin n.succ → ℕ
hx₁ : ∀ (i : Fin n.succ), x₁ i < d
hx₂ : ∀ (i : Fin n.succ), x₂ i < d
h :
  x₁ 0 = x₂ 0 ∧
    Eq (α := ℕ) ((map d : (a : Fin n → ℕ) → ℕ) (x₁ ∘ Fin.succ) : ℕ) ((map d : (a : Fin n → ℕ) → ℕ) (x₂ ∘ Fin.succ) : ℕ)
rw :
  x₁ 0 + HMul.hMul (α := ℕ) ((map d : (a : Fin n → ℕ) → ℕ) (x₁ ∘ Fin.succ) : ℕ) d =
    (map d : (a : Fin n.succ → ℕ) → ℕ) x₂
rw₁ :
  x₁ 0 + HMul.hMul (α := ℕ) ((map d : (a : Fin n → ℕ) → ℕ) (x₁ ∘ Fin.succ) : ℕ) d =
    x₂ 0 + HMul.hMul (α := ℕ) ((map d : (a : Fin n → ℕ) → ℕ) (x₂ ∘ Fin.succ) : ℕ) d
rw₂ :
  x₂ 0 + HMul.hMul (α := ℕ) ((map d : (a : Fin n → ℕ) → ℕ) (x₁ ∘ Fin.succ) : ℕ) d =
    x₂ 0 + HMul.hMul (α := ℕ) ((map d : (a : Fin n → ℕ) → ℕ) (x₂ ∘ Fin.succ) : ℕ) d
rw₃ rw₄ :
  x₂ 0 + HMul.hMul (α := ℕ) ((map d : (a : Fin n → ℕ) → ℕ) (x₂ ∘ Fin.succ) : ℕ) d =
    x₂ 0 + HMul.hMul (α := ℕ) ((map d : (a : Fin n → ℕ) → ℕ) (x₂ ∘ Fin.succ) : ℕ) d
⊢ Eq (α := ℕ) ((map d : (a : Fin n.succ → ℕ) → ℕ) x₁ : ℕ) ((map d : (a : Fin n.succ → ℕ) → ℕ) x₂ : ℕ)

Tactic:
rw [map_succ', map_succ', h.1, h.2]

Premises used: Behrend.map_succ', And.right, And.left
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
n d : ℕ
x₁ x₂ : Fin n.succ → ℕ
hx₁ : ∀ (i : Fin n.succ), x₁ i < d
hx₂ : ∀ (i : Fin n.succ), x₂ i < d
refine :
  ∀ (h : Eq (α := ℕ) ((map d : (a : Fin n.succ → ℕ) → ℕ) x₁ : ℕ) ((map d : (a : Fin n.succ → ℕ) → ℕ) x₂ : ℕ)),
    x₁ 0 = x₂ 0 ∧
      Eq (α := ℕ) ((map d : (a : Fin n → ℕ) → ℕ) (x₁ ∘ Fin.succ) : ℕ)
        ((map d : (a : Fin n → ℕ) → ℕ) (x₂ ∘ Fin.succ) : ℕ)
⊢ Eq (α := ℕ) ((map d : (a : Fin n.succ → ℕ) → ℕ) x₁ : ℕ) ((map d : (a : Fin n.succ → ℕ) → ℕ) x₂ : ℕ) ↔
    x₁ 0 = x₂ 0 ∧
      Eq (α := ℕ) ((map d : (a : Fin n → ℕ) → ℕ) (x₁ ∘ Fin.succ) : ℕ)
        ((map d : (a : Fin n → ℕ) → ℕ) (x₂ ∘ Fin.succ) : ℕ)

Tactic:
refine ⟨fun h => ?_, fun h => by rw [map_succ', map_succ', h.1, h.2]⟩
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
n d : ℕ
x₁ x₂ : Fin n.succ → ℕ
hx₁ : ∀ (i : Fin n.succ), x₁ i < d
hx₂ : ∀ (i : Fin n.succ), x₂ i < d
h : Eq (α := ℕ) ((map d : (a : Fin n.succ → ℕ) → ℕ) x₁ : ℕ) ((map d : (a : Fin n.succ → ℕ) → ℕ) x₂ : ℕ)
rw : x₁ 0 % d = x₂ 0
rw₁ : HMod.hMod (α := ℕ) ((map d : (a : Fin n.succ → ℕ) → ℕ) x₁ : ℕ) d = x₂ 0
rw₂ : HMod.hMod (α := ℕ) ((map d : (a : Fin n.succ → ℕ) → ℕ) x₁ : ℕ) d = x₂ 0 % d
rw₃ :
  HMod.hMod (α := ℕ) ((map d : (a : Fin n.succ → ℕ) → ℕ) x₁ : ℕ) d =
    HMod.hMod (α := ℕ) ((map d : (a : Fin n.succ → ℕ) → ℕ) x₂ : ℕ) d
rw₄ rw₅ :
  HMod.hMod (α := ℕ) ((map d : (a : Fin n.succ → ℕ) → ℕ) x₂ : ℕ) d =
    HMod.hMod (α := ℕ) ((map d : (a : Fin n.succ → ℕ) → ℕ) x₂ : ℕ) d
⊢ x₁ 0 = x₂ 0

Tactic:
rw [← mod_eq_of_lt (hx₁ _), ← map_mod, ← mod_eq_of_lt (hx₂ _), ← map_mod, h]

Premises used: Behrend.map_mod, Nat.mod_eq_of_lt
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
n d : ℕ
x₁ x₂ : Fin n.succ → ℕ
hx₁ : ∀ (i : Fin n.succ), x₁ i < d
hx₂ : ∀ (i : Fin n.succ), x₂ i < d
h : Eq (α := ℕ) ((map d : (a : Fin n.succ → ℕ) → ℕ) x₁ : ℕ) ((map d : (a : Fin n.succ → ℕ) → ℕ) x₂ : ℕ)
⊢ x₁ 0 = x₂ 0

Tactic:
have : x₁ 0 = x₂ 0 := by
    rw [← mod_eq_of_lt (hx₁ _), ← map_mod, ← mod_eq_of_lt (hx₂ _), ← map_mod, h]
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
n d : ℕ
x₁ x₂ : Fin n.succ → ℕ
hx₁ : ∀ (i : Fin n.succ), x₁ i < d
hx₂ : ∀ (i : Fin n.succ), x₂ i < d
h : Eq (α := ℕ) ((map d : (a : Fin n.succ → ℕ) → ℕ) x₁ : ℕ) ((map d : (a : Fin n.succ → ℕ) → ℕ) x₂ : ℕ)
this : x₁ 0 = x₂ 0
⊢ Eq (α := ℕ) (∑ x : Fin n, x₁ x.succ * d ^ (↑x : ℕ)) (∑ x : Fin n, x₂ x.succ * d ^ (↑x : ℕ)) ∨ d = 0

Tactic:
rw [map_succ, map_succ, this, add_right_inj, mul_eq_mul_right_iff] at h

Premises used: Behrend.map_succ, mul_eq_mul_right_iff, add_right_inj
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
n d : ℕ
x₁ x₂ : Fin n.succ → ℕ
hx₁ : ∀ (i : Fin n.succ), x₁ i < d
hx₂ : ∀ (i : Fin n.succ), x₂ i < d
h : Eq (α := ℕ) ((map d : (a : Fin n.succ → ℕ) → ℕ) x₁ : ℕ) ((map d : (a : Fin n.succ → ℕ) → ℕ) x₂ : ℕ)
this : x₁ 0 = x₂ 0
h₁ : Eq (α := ℕ) (∑ x : Fin n, x₁ x.succ * d ^ (↑x : ℕ)) (∑ x : Fin n, x₂ x.succ * d ^ (↑x : ℕ)) ∨ d = 0
⊢ x₁ 0 = x₂ 0

Tactic:
rw [map_succ, map_succ, this, add_right_inj, mul_eq_mul_right_iff] at h

Premises used: Behrend.map_succ, mul_eq_mul_right_iff, add_right_inj
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
n d : ℕ
x₁ x₂ : Fin n.succ → ℕ
hx₁ : ∀ (i : Fin n.succ), x₁ i < d
hx₂ : ∀ (i : Fin n.succ), x₂ i < d
h : Eq (α := ℕ) (∑ x : Fin n, x₁ x.succ * d ^ (↑x : ℕ)) (∑ x : Fin n, x₂ x.succ * d ^ (↑x : ℕ)) ∨ d = 0
this : x₁ 0 = x₂ 0
⊢ x₁ 0 = x₂ 0 ∧
    Eq (α := ℕ) ((map d : (a : Fin n → ℕ) → ℕ) (x₁ ∘ Fin.succ) : ℕ) ((map d : (a : Fin n → ℕ) → ℕ) (x₂ ∘ Fin.succ) : ℕ)

Tactic:
⟨this, h.resolve_right (pos_of_gt (hx₁ 0)).ne'⟩

Premises used: pos_of_gt, LT.lt.ne', And.intro, Or.resolve_right, OfNat.ofNat
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
n d : ℕ
x₁ x₂ : Fin n.succ → ℕ
hx₁ : ∀ (i : Fin n.succ), x₁ i < d
hx₂ : ∀ (i : Fin n.succ), x₂ i < d
h : Eq (α := ℕ) (∑ x : Fin n, x₁ x.succ * d ^ (↑x : ℕ)) (∑ x : Fin n, x₂ x.succ * d ^ (↑x : ℕ)) ∨ d = 0
this : x₁ 0 = x₂ 0
⊢ x₁ 0 = x₂ 0 ∧
    Eq (α := ℕ) ((map d : (a : Fin n → ℕ) → ℕ) (x₁ ∘ Fin.succ) : ℕ) ((map d : (a : Fin n → ℕ) → ℕ) (x₂ ∘ Fin.succ) : ℕ)

Tactic:
exact ⟨this, h.resolve_right (pos_of_gt (hx₁ 0)).ne'⟩
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
n d : ℕ
x₁ : Fin 0 → ℕ
hx₁ : Membership.mem (γ := Set (Fin 0 → ℕ)) {x : Fin 0 → ℕ | ∀ (i : Fin 0), x i < d} x₁
x₂ : Fin 0 → ℕ
hx₂ : Membership.mem (γ := Set (Fin 0 → ℕ)) {x : Fin 0 → ℕ | ∀ (i : Fin 0), x i < d} x₂
h : Eq (α := ℕ) ((map d : (a : Fin 0 → ℕ) → ℕ) x₁ : ℕ) ((map d : (a : Fin 0 → ℕ) → ℕ) x₂ : ℕ)
⊢ x₁ = x₂

Tactic:
simp [eq_iff_true_of_subsingleton]

Premises used: eq_iff_true_of_subsingleton
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
n_1 d n : ℕ
ih :
  ∀ ⦃x₁ : Fin n → ℕ⦄ (hx₁ : Membership.mem (γ := Set (Fin n → ℕ)) {x : Fin n → ℕ | ∀ (i : Fin n), x i < d} x₁)
    ⦃x₂ : Fin n → ℕ⦄ (hx₂ : Membership.mem (γ := Set (Fin n → ℕ)) {x : Fin n → ℕ | ∀ (i : Fin n), x i < d} x₂)
    (h : Eq (α := ℕ) ((map d : (a : Fin n → ℕ) → ℕ) x₁ : ℕ) ((map d : (a : Fin n → ℕ) → ℕ) x₂ : ℕ)), x₁ = x₂
x₁ : Fin (n + 1) → ℕ
hx₁ : Membership.mem (γ := Set (Fin (n + 1) → ℕ)) {x : Fin (n + 1) → ℕ | ∀ (i : Fin (n + 1)), x i < d} x₁
x₂ : Fin (n + 1) → ℕ
hx₂ : Membership.mem (γ := Set (Fin (n + 1) → ℕ)) {x : Fin (n + 1) → ℕ | ∀ (i : Fin (n + 1)), x i < d} x₂
h : Eq (α := ℕ) ((map d : (a : Fin (n + 1) → ℕ) → ℕ) x₁ : ℕ) ((map d : (a : Fin (n + 1) → ℕ) → ℕ) x₂ : ℕ)
succ : ∀ (i : Fin (n + 1)), x₁ i = x₂ i
⊢ x₁ = x₂

Tactic:
ext i
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
n_1 d n : ℕ
ih :
  ∀ ⦃x₁ : Fin n → ℕ⦄ (hx₁ : Membership.mem (γ := Set (Fin n → ℕ)) {x : Fin n → ℕ | ∀ (i : Fin n), x i < d} x₁)
    ⦃x₂ : Fin n → ℕ⦄ (hx₂ : Membership.mem (γ := Set (Fin n → ℕ)) {x : Fin n → ℕ | ∀ (i : Fin n), x i < d} x₂)
    (h : Eq (α := ℕ) ((map d : (a : Fin n → ℕ) → ℕ) x₁ : ℕ) ((map d : (a : Fin n → ℕ) → ℕ) x₂ : ℕ)), x₁ = x₂
x₁ : Fin (n + 1) → ℕ
hx₁ : Membership.mem (γ := Set (Fin (n + 1) → ℕ)) {x : Fin (n + 1) → ℕ | ∀ (i : Fin (n + 1)), x i < d} x₁
x₂ : Fin (n + 1) → ℕ
hx₂ : Membership.mem (γ := Set (Fin (n + 1) → ℕ)) {x : Fin (n + 1) → ℕ | ∀ (i : Fin (n + 1)), x i < d} x₂
h : Eq (α := ℕ) ((map d : (a : Fin (n + 1) → ℕ) → ℕ) x₁ : ℕ) ((map d : (a : Fin (n + 1) → ℕ) → ℕ) x₂ : ℕ)
i : Fin (n + 1)
⊢ x₁ 0 = x₂ 0 ∧
    Eq (α := ℕ) ((map d : (a : Fin n → ℕ) → ℕ) (x₁ ∘ Fin.succ) : ℕ) ((map d : (a : Fin n → ℕ) → ℕ) (x₂ ∘ Fin.succ) : ℕ)

Tactic:
have x := (map_eq_iff hx₁ hx₂).1 h
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
n_1 d n : ℕ
ih :
  ∀ ⦃x₁ : Fin n → ℕ⦄ (hx₁ : Membership.mem (γ := Set (Fin n → ℕ)) {x : Fin n → ℕ | ∀ (i : Fin n), x i < d} x₁)
    ⦃x₂ : Fin n → ℕ⦄ (hx₂ : Membership.mem (γ := Set (Fin n → ℕ)) {x : Fin n → ℕ | ∀ (i : Fin n), x i < d} x₂)
    (h : Eq (α := ℕ) ((map d : (a : Fin n → ℕ) → ℕ) x₁ : ℕ) ((map d : (a : Fin n → ℕ) → ℕ) x₂ : ℕ)), x₁ = x₂
x₁ : Fin (n + 1) → ℕ
hx₁ : Membership.mem (γ := Set (Fin (n + 1) → ℕ)) {x : Fin (n + 1) → ℕ | ∀ (i : Fin (n + 1)), x i < d} x₁
x₂ : Fin (n + 1) → ℕ
hx₂ : Membership.mem (γ := Set (Fin (n + 1) → ℕ)) {x : Fin (n + 1) → ℕ | ∀ (i : Fin (n + 1)), x i < d} x₂
h : Eq (α := ℕ) ((map d : (a : Fin (n + 1) → ℕ) → ℕ) x₁ : ℕ) ((map d : (a : Fin (n + 1) → ℕ) → ℕ) x₂ : ℕ)
i : Fin (n + 1)
x :
  x₁ 0 = x₂ 0 ∧
    Eq (α := ℕ) ((map d : (a : Fin n → ℕ) → ℕ) (x₁ ∘ Fin.succ) : ℕ) ((map d : (a : Fin n → ℕ) → ℕ) (x₂ ∘ Fin.succ) : ℕ)
⊢ x₁ i = x₂ i

Tactic:
Fin.cases x.1 (congr_fun <| ih (fun _ => hx₁ _) (fun _ => hx₂ _) x.2) i

Premises used: Fin.cases
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
n_1 d n : ℕ
ih :
  ∀ ⦃x₁ : Fin n → ℕ⦄ (hx₁ : Membership.mem (γ := Set (Fin n → ℕ)) {x : Fin n → ℕ | ∀ (i : Fin n), x i < d} x₁)
    ⦃x₂ : Fin n → ℕ⦄ (hx₂ : Membership.mem (γ := Set (Fin n → ℕ)) {x : Fin n → ℕ | ∀ (i : Fin n), x i < d} x₂)
    (h : Eq (α := ℕ) ((map d : (a : Fin n → ℕ) → ℕ) x₁ : ℕ) ((map d : (a : Fin n → ℕ) → ℕ) x₂ : ℕ)), x₁ = x₂
x₁ : Fin (n + 1) → ℕ
hx₁ : Membership.mem (γ := Set (Fin (n + 1) → ℕ)) {x : Fin (n + 1) → ℕ | ∀ (i : Fin (n + 1)), x i < d} x₁
x₂ : Fin (n + 1) → ℕ
hx₂ : Membership.mem (γ := Set (Fin (n + 1) → ℕ)) {x : Fin (n + 1) → ℕ | ∀ (i : Fin (n + 1)), x i < d} x₂
h : Eq (α := ℕ) ((map d : (a : Fin (n + 1) → ℕ) → ℕ) x₁ : ℕ) ((map d : (a : Fin (n + 1) → ℕ) → ℕ) x₂ : ℕ)
i : Fin (n + 1)
x :
  x₁ 0 = x₂ 0 ∧
    Eq (α := ℕ) ((map d : (a : Fin n → ℕ) → ℕ) (x₁ ∘ Fin.succ) : ℕ) ((map d : (a : Fin n → ℕ) → ℕ) (x₂ ∘ Fin.succ) : ℕ)
⊢ x₁ i = x₂ i

Tactic:
exact Fin.cases x.1 (congr_fun <| ih (fun _ => hx₁ _) (fun _ => hx₂ _) x.2) i
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
n d : ℕ
x₁ : Fin n → ℕ
hx₁ : Membership.mem (γ := Set (Fin n → ℕ)) {x : Fin n → ℕ | ∀ (i : Fin n), x i < d} x₁
x₂ : Fin n → ℕ
hx₂ : Membership.mem (γ := Set (Fin n → ℕ)) {x : Fin n → ℕ | ∀ (i : Fin n), x i < d} x₂
h : Eq (α := ℕ) ((map d : (a : Fin n → ℕ) → ℕ) x₁ : ℕ) ((map d : (a : Fin n → ℕ) → ℕ) x₂ : ℕ)
zero :
  ∀ ⦃x₁ : Fin 0 → ℕ⦄ (hx₁ : Membership.mem (γ := Set (Fin 0 → ℕ)) {x : Fin 0 → ℕ | ∀ (i : Fin 0), x i < d} x₁)
    ⦃x₂ : Fin 0 → ℕ⦄ (hx₂ : Membership.mem (γ := Set (Fin 0 → ℕ)) {x : Fin 0 → ℕ | ∀ (i : Fin 0), x i < d} x₂)
    (h : Eq (α := ℕ) ((map d : (a : Fin 0 → ℕ) → ℕ) x₁ : ℕ) ((map d : (a : Fin 0 → ℕ) → ℕ) x₂ : ℕ)), x₁ = x₂
succ :
  ∀ (n : ℕ)
    (ih :
      ∀ ⦃x₁ : Fin n → ℕ⦄ (hx₁ : Membership.mem (γ := Set (Fin n → ℕ)) {x : Fin n → ℕ | ∀ (i : Fin n), x i < d} x₁)
        ⦃x₂ : Fin n → ℕ⦄ (hx₂ : Membership.mem (γ := Set (Fin n → ℕ)) {x : Fin n → ℕ | ∀ (i : Fin n), x i < d} x₂)
        (h : Eq (α := ℕ) ((map d : (a : Fin n → ℕ) → ℕ) x₁ : ℕ) ((map d : (a : Fin n → ℕ) → ℕ) x₂ : ℕ)), x₁ = x₂)
    ⦃x₁ : Fin (n + 1) → ℕ⦄
    (hx₁ : Membership.mem (γ := Set (Fin (n + 1) → ℕ)) {x : Fin (n + 1) → ℕ | ∀ (i : Fin (n + 1)), x i < d} x₁)
    ⦃x₂ : Fin (n + 1) → ℕ⦄
    (hx₂ : Membership.mem (γ := Set (Fin (n + 1) → ℕ)) {x : Fin (n + 1) → ℕ | ∀ (i : Fin (n + 1)), x i < d} x₂)
    (h : Eq (α := ℕ) ((map d : (a : Fin (n + 1) → ℕ) → ℕ) x₁ : ℕ) ((map d : (a : Fin (n + 1) → ℕ) → ℕ) x₂ : ℕ)), x₁ = x₂
⊢ x₁ = x₂

Tactic:
induction n with
  | zero => simp [eq_iff_true_of_subsingleton]
  | succ n ih =>
    ext i
    have x := (map_eq_iff hx₁ hx₂).1 h
    exact Fin.cases x.1 (congr_fun <| ih (fun _ => hx₁ _) (fun _ => hx₂ _) x.2) i

Premises used: Nat.zero, Nat.succ, eq_iff_true_of_subsingleton
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
n d : ℕ
x : Fin n → ℕ
hx : x ∈ box n d
⊢ LE.le (α := ℕ) ((map (2 * d - 1) : (a : Fin n → ℕ) → ℕ) x : ℕ) (∑ i : Fin n, (d - 1) * (2 * d - 1) ^ (↑i : ℕ) : ℕ)

Tactic:
map_monotone (2 * d - 1) fun _ => Nat.le_sub_one_of_lt <| mem_box.1 hx _

Premises used: Multiset.sum, Multiset.foldr, HMul.hMul, HSub.hSub, Nat.le_sub_one_of_lt, Behrend.mem_box, Iff.mp, OfNat.ofNat, Finset.sum, Behrend.map_monotone
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
n d k : ℕ
f : (Fin n → ℕ) →+ EuclideanSpace ℝ (Fin n) :=
  { toFun := fun (f : Fin n → ℕ) ↦ toLp 2 (Nat.cast ∘ f), map_zero' := ⋯, map_add' := ⋯ }
⊢ ThreeAPFree (↑(sphere n d k) : Set (Fin n → ℕ))

Tactic:
ThreeAPFree.of_image (AddHomClass.isAddFreimanHom f (Set.mapsTo_image _ _))
    ((toLp_injective 2).comp_injOn cast_injective.comp_left.injOn) (Set.subset_univ _) ?_

Premises used: Function.Injective.injOn, Set.subset_univ, ThreeAPFree.of_image, Set.mapsTo_image, Function.Injective.comp_injOn, AddHomClass.isAddFreimanHom, WithLp.toLp_injective, Function.Injective.comp_left, Nat.cast_injective, OfNat.ofNat
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
n d k : ℕ
f : (Fin n → ℕ) →+ EuclideanSpace ℝ (Fin n) :=
  { toFun := fun (f : Fin n → ℕ) ↦ toLp 2 (Nat.cast ∘ f), map_zero' := ⋯, map_add' := ⋯ }
refine :
  ThreeAPFree (α := EuclideanSpace ℝ (Fin n))
    ((⇑f : (a : Fin n → ℕ) → EuclideanSpace ℝ (Fin n)) '' (↑(sphere n d k) : Set (Fin n → ℕ)))
⊢ ThreeAPFree (↑(sphere n d k) : Set (Fin n → ℕ))

Tactic:
refine ThreeAPFree.of_image (AddHomClass.isAddFreimanHom f (Set.mapsTo_image _ _))
    ((toLp_injective 2).comp_injOn cast_injective.comp_left.injOn) (Set.subset_univ _) ?_

Premises used: Function.Injective.injOn, Set.subset_univ, ThreeAPFree.of_image, Set.mapsTo_image, Function.Injective.comp_injOn, AddHomClass.isAddFreimanHom, WithLp.toLp_injective, Function.Injective.comp_left, Nat.cast_injective, OfNat.ofNat
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
n d k : ℕ
f : (Fin n → ℕ) →+ EuclideanSpace ℝ (Fin n) :=
  { toFun := fun (f : Fin n → ℕ) ↦ toLp 2 (Nat.cast ∘ f), map_zero' := ⋯, map_add' := ⋯ }
⊢ ThreeAPFree (α := EuclideanSpace ℝ (Fin n))
    ((⇑f : (a : Fin n → ℕ) → EuclideanSpace ℝ (Fin n)) '' (↑(sphere n d k) : Set (Fin n → ℕ)))

Tactic:
(threeAPFree_sphere 0 (√↑k)).mono (Set.image_subset_iff.2 fun x => ?_)

Premises used: Iff.mpr, threeAPFree_sphere, ThreeAPFree.mono, Nat.cast, Real.sqrt, Set.image_subset_iff, OfNat.ofNat
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
n d k : ℕ
f : (Fin n → ℕ) →+ EuclideanSpace ℝ (Fin n) :=
  { toFun := fun (f : Fin n → ℕ) ↦ toLp 2 (Nat.cast ∘ f), map_zero' := ⋯, map_add' := ⋯ }
refine :
  ∀ x ∈ (↑(sphere n d k) : Set (Fin n → ℕ)),
    Membership.mem (γ := Set (Fin n → ℕ))
      (Set.preimage (β := EuclideanSpace ℝ (Fin n)) (⇑f : (a : Fin n → ℕ) → EuclideanSpace ℝ (Fin n))
        (Metric.sphere 0 √(↑k : ℝ)))
      x
⊢ ThreeAPFree (α := EuclideanSpace ℝ (Fin n))
    ((⇑f : (a : Fin n → ℕ) → EuclideanSpace ℝ (Fin n)) '' (↑(sphere n d k) : Set (Fin n → ℕ)))

Tactic:
refine (threeAPFree_sphere 0 (√↑k)).mono (Set.image_subset_iff.2 fun x => ?_)
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
n d k : ℕ
f : (Fin n → ℕ) →+ EuclideanSpace ℝ (Fin n) :=
  { toFun := fun (f : Fin n → ℕ) ↦ toLp 2 (Nat.cast ∘ f), map_zero' := ⋯, map_add' := ⋯ }
x : Fin n → ℕ
rw :
  x ∈ (↑(sphere n d k) : Set (Fin n → ℕ)) →
    Norm.norm (E := EuclideanSpace ℝ (Fin n))
        ((f : (a : Fin n → ℕ) → EuclideanSpace ℝ (Fin n)) x : EuclideanSpace ℝ (Fin n)) =
      √(↑k : ℝ)
⊢ x ∈ (↑(sphere n d k) : Set (Fin n → ℕ)) →
    Membership.mem (γ := Set (Fin n → ℕ))
      (Set.preimage (β := EuclideanSpace ℝ (Fin n)) (⇑f : (a : Fin n → ℕ) → EuclideanSpace ℝ (Fin n))
        (Metric.sphere 0 √(↑k : ℝ)))
      x

Tactic:
rw [Set.mem_preimage, mem_sphere_zero_iff_norm]

Premises used: mem_sphere_zero_iff_norm, Set.mem_preimage
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
n d k : ℕ
f : (Fin n → ℕ) →+ EuclideanSpace ℝ (Fin n) :=
  { toFun := fun (f : Fin n → ℕ) ↦ toLp 2 (Nat.cast ∘ f), map_zero' := ⋯, map_add' := ⋯ }
x : Fin n → ℕ
⊢ x ∈ (↑(sphere n d k) : Set (Fin n → ℕ)) →
    Norm.norm (E := EuclideanSpace ℝ (Fin n))
        ((f : (a : Fin n → ℕ) → EuclideanSpace ℝ (Fin n)) x : EuclideanSpace ℝ (Fin n)) =
      √(↑k : ℝ)

Tactic:
norm_of_mem_sphere

Premises used: setOf, Behrend.norm_of_mem_sphere
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
n d k : ℕ
f : (Fin n → ℕ) →+ EuclideanSpace ℝ (Fin n) :=
  { toFun := fun (f : Fin n → ℕ) ↦ toLp 2 (Nat.cast ∘ f), map_zero' := ⋯, map_add' := ⋯ }
x : Fin n → ℕ
⊢ x ∈ (↑(sphere n d k) : Set (Fin n → ℕ)) →
    Norm.norm (E := EuclideanSpace ℝ (Fin n))
        ((f : (a : Fin n → ℕ) → EuclideanSpace ℝ (Fin n)) x : EuclideanSpace ℝ (Fin n)) =
      √(↑k : ℝ)

Tactic:
exact norm_of_mem_sphere

Premises used: Behrend.norm_of_mem_sphere
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
n d k : ℕ
rw : ThreeAPFree (α := ℕ) ((⇑(map (2 * d - 1)) : (a : Fin n → ℕ) → ℕ) '' (↑(sphere n d k) : Set (Fin n → ℕ)))
⊢ ThreeAPFree (↑(image (⇑(map (2 * d - 1)) : (a : Fin n → ℕ) → ℕ) (sphere n d k)) : Set ℕ)

Tactic:
rw [coe_image]

Premises used: Finset.coe_image
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
n d k : ℕ
apply :
  (↑(sphere n d k) : Set (Fin n → ℕ)) + (↑(sphere n d k) : Set (Fin n → ℕ)) ⊆
    {x : Fin n → ℕ | ∀ (i : Fin n), x i < 2 * d - 1}
⊢ ThreeAPFree (α := ℕ) ((⇑(map (2 * d - 1)) : (a : Fin n → ℕ) → ℕ) '' (↑(sphere n d k) : Set (Fin n → ℕ)))

Tactic:
apply ThreeAPFree.image' (α := Fin n → ℕ) (β := ℕ) (s := sphere n d k) (map (2 * d - 1))
    (map_injOn.mono _) threeAPFree_sphere

Premises used: HMul.hMul, HSub.hSub, Behrend.map_injOn, Set.InjOn.mono, OfNat.ofNat, Behrend.threeAPFree_sphere, ThreeAPFree.image', Behrend.map
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
n d k : ℕ
rw :
  ∀ x ∈ (↑(sphere n d k) : Set (Fin n → ℕ)),
    ∀ y ∈ (↑(sphere n d k) : Set (Fin n → ℕ)),
      Membership.mem (γ := Set (Fin n → ℕ)) {x : Fin n → ℕ | ∀ (i : Fin n), x i < 2 * d - 1} (x + y)
⊢ (↑(sphere n d k) : Set (Fin n → ℕ)) + (↑(sphere n d k) : Set (Fin n → ℕ)) ⊆
    {x : Fin n → ℕ | ∀ (i : Fin n), x i < 2 * d - 1}

Tactic:
rw [Set.add_subset_iff]

Premises used: Set.add_subset_iff
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
n d k : ℕ
a : Fin n → ℕ
ha : a ∈ (↑(sphere n d k) : Set (Fin n → ℕ))
b : Fin n → ℕ
hb : b ∈ (↑(sphere n d k) : Set (Fin n → ℕ))
i : Fin n
⊢ a i < d

Tactic:
have hai := mem_box.1 (sphere_subset_box ha) i
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
n d k : ℕ
a : Fin n → ℕ
ha : a ∈ (↑(sphere n d k) : Set (Fin n → ℕ))
b : Fin n → ℕ
hb : b ∈ (↑(sphere n d k) : Set (Fin n → ℕ))
i : Fin n
hai : a i < d
⊢ b i < d

Tactic:
have hbi := mem_box.1 (sphere_subset_box hb) i
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
n d k : ℕ
a : Fin n → ℕ
ha : a ∈ (↑(sphere n d k) : Set (Fin n → ℕ))
b : Fin n → ℕ
hb : b ∈ (↑(sphere n d k) : Set (Fin n → ℕ))
i : Fin n
hai : a i < d
hbi : b i < d
rw : ((a + b) i + 1).succ ≤ d + d
⊢ (a + b) i < 2 * d - 1

Tactic:
rw [lt_tsub_iff_right, ← succ_le_iff, two_mul]

Premises used: lt_tsub_iff_right, two_mul, Nat.succ_le_iff
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
n d k : ℕ
a : Fin n → ℕ
ha : a ∈ (↑(sphere n d k) : Set (Fin n → ℕ))
b : Fin n → ℕ
hb : b ∈ (↑(sphere n d k) : Set (Fin n → ℕ))
i : Fin n
hai : a i < d
hbi : b i < d
⊢ ((a + b) i + 1).succ ≤ d + d

Tactic:
(add_add_add_comm _ _ 1 1).trans_le (_root_.add_le_add hai hbi)

Premises used: add_le_add, Eq.trans_le, add_add_add_comm, OfNat.ofNat
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
n d k : ℕ
a : Fin n → ℕ
ha : a ∈ (↑(sphere n d k) : Set (Fin n → ℕ))
b : Fin n → ℕ
hb : b ∈ (↑(sphere n d k) : Set (Fin n → ℕ))
i : Fin n
hai : a i < d
hbi : b i < d
⊢ ((a + b) i + 1).succ ≤ d + d

Tactic:
exact (add_add_add_comm _ _ 1 1).trans_le (_root_.add_le_add hai hbi)

Premises used: add_le_add, Eq.trans_le, add_add_add_comm, OfNat.ofNat
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
n d : ℕ
x : Fin n → ℕ
hx : x ∈ box n d
⊢ ∀ (i : Fin n), x i < d

Tactic:
rw [mem_box] at hx

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

Tactic:
have : ∀ i, x i ^ 2 ≤ (d - 1) ^ 2 := fun i =>
    Nat.pow_le_pow_left (Nat.le_sub_one_of_lt (hx i)) _
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
n d : ℕ
x : Fin n → ℕ
hx : ∀ (i : Fin n), x i < d
this : ∀ (i : Fin n), HPow.hPow (β := ℕ) (x i) 2 ≤ HPow.hPow (β := ℕ) (d - 1) 2
rw : n • HPow.hPow (β := ℕ) (d - 1) 2 ≤ n * HPow.hPow (β := ℕ) (d - 1) 2
rw₁ rw₂ : n * HPow.hPow (β := ℕ) (d - 1) 2 ≤ n * HPow.hPow (β := ℕ) (d - 1) 2
⊢ card (α := Fin n) univ • HPow.hPow (β := ℕ) (d - 1) 2 ≤ n * HPow.hPow (β := ℕ) (d - 1) 2

Tactic:
rw [Finset.card_fin, smul_eq_mul]

Premises used: Finset.card_fin, smul_eq_mul
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
n d : ℕ
x : Fin n → ℕ
hx : ∀ (i : Fin n), x i < d
this : ∀ (i : Fin n), HPow.hPow (β := ℕ) (x i) 2 ≤ HPow.hPow (β := ℕ) (d - 1) 2
⊢ ∑ i : Fin n, HPow.hPow (β := ℕ) (x i) 2 ≤ n * HPow.hPow (β := ℕ) (d - 1) 2

Tactic:
exact (sum_le_card_nsmul univ _ _ fun i _ => this i).trans (by rw [Finset.card_fin, smul_eq_mul])

Premises used: Finset.univ, Finset.sum_le_card_nsmul, LE.le.trans
-- Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend
Goal:
n d : ℕ
⊢ ∑ i : Fin n, d * (2 * d + 1) ^ (↑i : ℕ) = ((2 * d + 1) ^ n - 1) / 2

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