awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
n d k : ℕ
x : Fin n → ℕ
hx : x ∈ (↑(sphere n d k) : Set (Fin n → ℕ))
rw : Membership.mem (γ := Set (WithLp 2 (Fin n → ℝ))) (Metric.sphere 0 √(↑k : ℝ)) (toLp 2 (Nat.cast ∘ x))
rw₁ : Norm.norm (E := WithLp 2 (Fin n → ℝ)) (toLp 2 (Nat.cast ∘ x)) = √(↑k : ℝ)
⊢ Membership.mem (γ := Set (Fin n → ℕ))
    (Set.preimage (β := WithLp 2 (Fin n → ℝ)) (fun (x : Fin n → ℕ) ↦ toLp 2 (Nat.cast ∘ x)) (Metric.sphere 0 √(↑k : ℝ)))
    x
have rw₂ : √(↑k : ℝ) = √(↑k : ℝ)
Tactic: rw [Set.mem_preimage, mem_sphere_zero_iff_norm, norm_of_mem_sphere hx]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
n d_1 k N : ℕ
x : Fin n → ℕ
d : ℕ
⊢ Eq (α := ℕ) (∑ i : Fin n, 0 i * d ^ (↑i : ℕ)) 0
have simp_rw : Eq (α := ℕ) (∑ x : Fin n, 0 * d ^ (↑x : ℕ)) 0
Tactic: simp_rw [Pi.zero_apply, zero_mul, sum_const_zero]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
n d_1 k N : ℕ
x : Fin n → ℕ
d : ℕ
simp_rw : Eq (α := ℕ) (∑ x : Fin n, 0 * d ^ (↑x : ℕ)) 0
⊢ Eq (α := ℕ) (∑ i : Fin n, 0 i * d ^ (↑i : ℕ)) 0
have simp_rw₁ : Eq (α := ℕ) (∑ x : Fin n, 0) 0
Tactic: simp_rw [Pi.zero_apply, zero_mul, sum_const_zero]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
n d_1 k N : ℕ
x : Fin n → ℕ
d : ℕ
a b : Fin n → ℕ
⊢ ∑ i : Fin n, (a + b) i * d ^ (↑i : ℕ) =
    HAdd.hAdd (α := ℕ) (∑ i : Fin n, a i * d ^ (↑i : ℕ)) (∑ i : Fin n, b i * d ^ (↑i : ℕ))
have 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 : ℕ))
Tactic: simp_rw [Pi.add_apply, add_mul, sum_add_distrib]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
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 : ℕ))
⊢ ∑ i : Fin n, (a + b) i * d ^ (↑i : ℕ) =
    HAdd.hAdd (α := ℕ) (∑ i : Fin n, a i * d ^ (↑i : ℕ)) (∑ i : Fin n, b i * d ^ (↑i : ℕ))
have 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 : ℕ))
Tactic: simp_rw [Pi.add_apply, add_mul, sum_add_distrib]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
n d : ℕ
x y : Fin n → ℕ
h : x ≤ y
⊢ LE.le (α := ℕ) ((map d : (a : Fin n → ℕ) → ℕ) x : ℕ) ((map d : (a : Fin n → ℕ) → ℕ) y : ℕ)
have dsimp : LE.le (α := ℕ) (∑ i : Fin n, x i * d ^ (↑i : ℕ)) (∑ i : Fin n, y i * d ^ (↑i : ℕ))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
n d : ℕ
a : Fin n.succ → ℕ
⊢ HMod.hMod (α := ℕ) ((map d : (a : Fin n.succ → ℕ) → ℕ) a : ℕ) d = a 0 % d
have rw : (a 0 + (∑ x : Fin n, a x.succ * d ^ (↑x : ℕ)) * d) % d = a 0 % d
Tactic: rw [map_succ, Nat.add_mul_mod_self_right]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
n d : ℕ
a : Fin n.succ → ℕ
rw : (a 0 + (∑ x : Fin n, a x.succ * d ^ (↑x : ℕ)) * d) % d = a 0 % d
⊢ HMod.hMod (α := ℕ) ((map d : (a : Fin n.succ → ℕ) → ℕ) a : ℕ) d = a 0 % d
have rw₁ : a 0 % d = a 0 % d
Tactic: rw [map_succ, Nat.add_mul_mod_self_right]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
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) : ℕ)
⊢ Eq (α := ℕ) ((map d : (a : Fin n.succ → ℕ) → ℕ) x₁ : ℕ) ((map d : (a : Fin n.succ → ℕ) → ℕ) x₂ : ℕ)
have rw : x₁ 0 + HMul.hMul (α := ℕ) ((map d : (a : Fin n → ℕ) → ℕ) (x₁ ∘ Fin.succ) : ℕ) d = (map d : (a : Fin n.succ → ℕ) → ℕ) x₂
Tactic: rw [map_succ', map_succ', h.1, h.2]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
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₂
⊢ Eq (α := ℕ) ((map d : (a : Fin n.succ → ℕ) → ℕ) x₁ : ℕ) ((map d : (a : Fin n.succ → ℕ) → ℕ) x₂ : ℕ)
have 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
Tactic: rw [map_succ', map_succ', h.1, h.2]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
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
⊢ Eq (α := ℕ) ((map d : (a : Fin n.succ → ℕ) → ℕ) x₁ : ℕ) ((map d : (a : Fin n.succ → ℕ) → ℕ) x₂ : ℕ)
have 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
Tactic: rw [map_succ', map_succ', h.1, h.2]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
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
⊢ Eq (α := ℕ) ((map d : (a : Fin n.succ → ℕ) → ℕ) x₁ : ℕ) ((map d : (a : Fin n.succ → ℕ) → ℕ) x₂ : ℕ)
have 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
Tactic: rw [map_succ', map_succ', h.1, h.2]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
n d : ℕ
x₁ x₂ : Fin n.succ → ℕ
hx₁ : ∀ (i : Fin n.succ), x₁ i < d
hx₂ : ∀ (i : Fin n.succ), x₂ i < d
⊢ 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) : ℕ)
have 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) : ℕ)
Tactic: refine ⟨fun h => ?_, fun h => by rw [map_succ', map_succ', h.1, h.2]⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
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
have rw : x₁ 0 % d = x₂ 0
Tactic: rw [← mod_eq_of_lt (hx₁ _), ← map_mod, ← mod_eq_of_lt (hx₂ _), ← map_mod, h]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
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
⊢ x₁ 0 = x₂ 0
have rw₁ : HMod.hMod (α := ℕ) ((map d : (a : Fin n.succ → ℕ) → ℕ) x₁ : ℕ) d = x₂ 0
Tactic: rw [← mod_eq_of_lt (hx₁ _), ← map_mod, ← mod_eq_of_lt (hx₂ _), ← map_mod, h]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
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
⊢ x₁ 0 = x₂ 0
have rw₂ : HMod.hMod (α := ℕ) ((map d : (a : Fin n.succ → ℕ) → ℕ) x₁ : ℕ) d = x₂ 0 % d
Tactic: rw [← mod_eq_of_lt (hx₁ _), ← map_mod, ← mod_eq_of_lt (hx₂ _), ← map_mod, h]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
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
⊢ x₁ 0 = x₂ 0
have rw₃ : HMod.hMod (α := ℕ) ((map d : (a : Fin n.succ → ℕ) → ℕ) x₁ : ℕ) d =
  HMod.hMod (α := ℕ) ((map d : (a : Fin n.succ → ℕ) → ℕ) x₂ : ℕ) d
Tactic: rw [← mod_eq_of_lt (hx₁ _), ← map_mod, ← mod_eq_of_lt (hx₂ _), ← map_mod, h]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
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
⊢ x₁ 0 = x₂ 0
have rw₄ : HMod.hMod (α := ℕ) ((map d : (a : Fin n.succ → ℕ) → ℕ) x₂ : ℕ) d =
  HMod.hMod (α := ℕ) ((map d : (a : Fin n.succ → ℕ) → ℕ) x₂ : ℕ) d
Tactic: rw [← mod_eq_of_lt (hx₁ _), ← map_mod, ← mod_eq_of_lt (hx₂ _), ← map_mod, h]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (hypothesis)
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 ∧
    Eq (α := ℕ) ((map d : (a : Fin n → ℕ) → ℕ) (x₁ ∘ Fin.succ) : ℕ) ((map d : (a : Fin n → ℕ) → ℕ) (x₂ ∘ Fin.succ) : ℕ)
have this : 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]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (hypothesis)
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
⊢ x₁ 0 = x₂ 0 ∧
    Eq (α := ℕ) ((map d : (a : Fin n → ℕ) → ℕ) (x₁ ∘ Fin.succ) : ℕ) ((map d : (a : Fin n → ℕ) → ℕ) (x₂ ∘ Fin.succ) : ℕ)
have h₁ : 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
Cleared hypotheses: h, this
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
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₂ : ℕ)
⊢ x₁ = x₂
have succ : ∀ (i : Fin (n + 1)), x₁ i = x₂ i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (hypothesis)
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₁ i = x₂ i
have x : 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
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
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₂ : ℕ)
⊢ x₁ = x₂
have 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₂
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
Cleared hypotheses: x₁, hx₁, x₂, hx₂, h
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
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₂
⊢ x₁ = x₂
have 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₂
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
Cleared hypotheses: x₁, hx₁, x₂, hx₂, h
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
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 → ℕ))
have refine : ThreeAPFree (α := EuclideanSpace ℝ (Fin n))
  ((⇑f : (a : Fin n → ℕ) → EuclideanSpace ℝ (Fin n)) '' (↑(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 _) ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
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 → ℕ)))
have 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
Tactic: refine (threeAPFree_sphere 0 (√↑k)).mono (Set.image_subset_iff.2 fun x => ?_)
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
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 → ℕ)) →
    Membership.mem (γ := Set (Fin n → ℕ))
      (Set.preimage (β := EuclideanSpace ℝ (Fin n)) (⇑f : (a : Fin n → ℕ) → EuclideanSpace ℝ (Fin n))
        (Metric.sphere 0 √(↑k : ℝ)))
      x
have 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 : ℝ)
Tactic: rw [Set.mem_preimage, mem_sphere_zero_iff_norm]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
n d k : ℕ
⊢ ThreeAPFree (↑(image (⇑(map (2 * d - 1)) : (a : Fin n → ℕ) → ℕ) (sphere n d k)) : Set ℕ)
have rw : ThreeAPFree (α := ℕ) ((⇑(map (2 * d - 1)) : (a : Fin n → ℕ) → ℕ) '' (↑(sphere n d k) : Set (Fin n → ℕ)))
Tactic: rw [coe_image]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
n d k : ℕ
⊢ ThreeAPFree (α := ℕ) ((⇑(map (2 * d - 1)) : (a : Fin n → ℕ) → ℕ) '' (↑(sphere n d k) : Set (Fin n → ℕ)))
have 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}
Tactic: apply ThreeAPFree.image' (α := Fin n → ℕ) (β := ℕ) (s := sphere n d k) (map (2 * d - 1))
    (map_injOn.mono _) threeAPFree_sphere
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
n d k : ℕ
⊢ (↑(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}
have 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)
Tactic: rw [Set.add_subset_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (hypothesis)
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 + b) i < 2 * d - 1
have hai : a i < d
Tactic: have hai := mem_box.1 (sphere_subset_box ha) i
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (hypothesis)
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
⊢ (a + b) i < 2 * d - 1
have hbi : b i < d
Tactic: have hbi := mem_box.1 (sphere_subset_box hb) i
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
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 < 2 * d - 1
have rw : ((a + b) i + 1).succ ≤ d + d
Tactic: rw [lt_tsub_iff_right, ← succ_le_iff, two_mul]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (hypothesis)
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
have hx₁ : ∀ (i : Fin n), x i < d
Tactic: rw [mem_box] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (hypothesis)
Goal:
n d : ℕ
x : Fin n → ℕ
hx : ∀ (i : Fin n), x i < d
⊢ ∑ i : Fin n, HPow.hPow (β := ℕ) (x i) 2 ≤ n * HPow.hPow (β := ℕ) (d - 1) 2
have this : ∀ (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)) _
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
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
⊢ card (α := Fin n) univ • HPow.hPow (β := ℕ) (d - 1) 2 ≤ n * HPow.hPow (β := ℕ) (d - 1) 2
have rw : n • HPow.hPow (β := ℕ) (d - 1) 2 ≤ n * HPow.hPow (β := ℕ) (d - 1) 2
Tactic: rw [Finset.card_fin, smul_eq_mul]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
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
⊢ card (α := Fin n) univ • HPow.hPow (β := ℕ) (d - 1) 2 ≤ n * HPow.hPow (β := ℕ) (d - 1) 2
have rw₁ : n * HPow.hPow (β := ℕ) (d - 1) 2 ≤ n * HPow.hPow (β := ℕ) (d - 1) 2
Tactic: rw [Finset.card_fin, smul_eq_mul]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
n d : ℕ
⊢ ∑ i : Fin n, d * (2 * d + 1) ^ (↑i : ℕ) = ((2 * d + 1) ^ n - 1) / 2
have refine : (2 * d + 1) ^ n - 1 = HMul.hMul (α := ℕ) (∑ i : Fin n, d * (2 * d + 1) ^ (↑i : ℕ)) 2
Tactic: refine (Nat.div_eq_of_eq_mul_left zero_lt_two ?_).symm
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.AP.Three.Behrend (goal)
Goal:
n d : ℕ
⊢ (2 * d + 1) ^ n - 1 = HMul.hMul (α := ℕ) (∑ i : Fin n, d * (2 * d + 1) ^ (↑i : ℕ)) 2
have rw : (2 * d + 1) ^ n - 1 = HMul.hMul (α := ℕ) (∑ i ∈ range 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]
-- 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
⊢ (2 * d + 1) ^ n - 1 = HMul.hMul (α := ℕ) (∑ i : Fin n, d * (2 * d + 1) ^ (↑i : ℕ)) 2
have rw₁ : (2 * d + 1) ^ n - 1 = (d * ∑ i ∈ range n, (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]
-- 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
⊢ (2 * d + 1) ^ n - 1 = HMul.hMul (α := ℕ) (∑ i : Fin n, d * (2 * d + 1) ^ (↑i : ℕ)) 2
have rw₂ : (2 * d + 1) ^ n - 1 = d * 2 * ∑ 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]