awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Additive.SmallTripling
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : Group G
A : Finset G
k : ℝ
m_1 : ℕ
h :
  ∀ (ε : Fin 3 → ℤ),
    (∀ (i : Fin 3), |ε i| = 1) →
      (↑(card.{u_1} (α := G) (prod (List.map (fun (i : Fin 3) ↦ A ^ ε i) (finRange 3)))) : ℝ) ≤ k * (↑(#A) : ℝ)
m : ℕ
hm : 3 ≤ m + 1
ih :
  ∀ (ε : Fin (m + 1) → ℤ) (hε : ∀ (i : Fin (m + 1)), |ε i| = 1),
    (↑(card.{u_1} (α := G) (prod (List.map (fun (i : Fin (m + 1)) ↦ A ^ ε i) (finRange (m + 1))))) : ℝ) ≤
      k ^ (m + 1 - 2) * (↑(#A) : ℝ)
ε : Fin (m + 1 + 1) → ℤ
hε : ∀ (i : Fin (m + 1 + 1)), |ε i| = 1
hm₀ : m ≠ 0
⊢ ∀ (i : Fin (m + 1 + 1)), ε i ≠ 0

Tactic:
have hε₀ i : ε i ≠ 0 := fun h ↦ by simpa [h] using hε i
-- Module: Mathlib.Combinatorics.Additive.SmallTripling
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : Group G
A : Finset G
k : ℝ
m_1 : ℕ
h :
  ∀ (ε : Fin 3 → ℤ),
    (∀ (i : Fin 3), |ε i| = 1) →
      (↑(card.{u_1} (α := G) (prod (List.map (fun (i : Fin 3) ↦ A ^ ε i) (finRange 3)))) : ℝ) ≤ k * (↑(#A) : ℝ)
m : ℕ
hm : 3 ≤ m + 1
ih :
  ∀ (ε : Fin (m + 1) → ℤ) (hε : ∀ (i : Fin (m + 1)), |ε i| = 1),
    (↑(card.{u_1} (α := G) (prod (List.map (fun (i : Fin (m + 1)) ↦ A ^ ε i) (finRange (m + 1))))) : ℝ) ≤
      k ^ (m + 1 - 2) * (↑(#A) : ℝ)
ε : Fin (m + 1 + 1) → ℤ
hε : ∀ (i : Fin (m + 1 + 1)), |ε i| = 1
hm₀ : m ≠ 0
hε₀ : ∀ (i : Fin (m + 1 + 1)), ε i ≠ 0
succ :
  ∀
    (h :
      ∀ (ε : Fin 3 → ℤ),
        (∀ (i : Fin 3), |ε i| = 1) →
          (↑(card.{u_1} (α := G) (prod (List.map (fun (i : Fin 3) ↦ HPow.hPow (α := Finset G) ∅ (ε i)) (finRange 3)))) :
              ℝ) ≤
            k * (↑(card.{u_1} (α := G) ∅) : ℝ))
    (ih :
      ∀ (ε : Fin (m + 1) → ℤ) (hε : ∀ (i : Fin (m + 1)), |ε i| = 1),
        (↑(card.{u_1} (α := G)
                (prod (List.map (fun (i : Fin (m + 1)) ↦ HPow.hPow (α := Finset G) ∅ (ε i)) (finRange (m + 1))))) :
            ℝ) ≤
          k ^ (m + 1 - 2) * (↑(card.{u_1} (α := G) ∅) : ℝ)),
    (↑(card.{u_1} (α := G)
            (prod (List.map (fun (i : Fin (m + 1 + 1)) ↦ HPow.hPow (α := Finset G) ∅ (ε i)) (finRange (m + 1 + 1))))) :
        ℝ) ≤
      k ^ (m + 1 + 1 - 2) * (↑(card.{u_1} (α := G) ∅) : ℝ)
succ₁ :
  ∀ (hA : A.Nonempty),
    (↑(card.{u_1} (α := G) (prod (List.map (fun (i : Fin (m + 1 + 1)) ↦ A ^ ε i) (finRange (m + 1 + 1))))) : ℝ) ≤
      k ^ (m + 1 + 1 - 2) * (↑(#A) : ℝ)
⊢ (↑(card.{u_1} (α := G) (prod (List.map (fun (i : Fin (m + 1 + 1)) ↦ A ^ ε i) (finRange (m + 1 + 1))))) : ℝ) ≤
    k ^ (m + 1 + 1 - 2) * (↑(#A) : ℝ)

Tactic:
obtain rfl | hA := A.eq_empty_or_nonempty

Premises used: rfl, Finset.eq_empty_or_nonempty
-- Module: Mathlib.Combinatorics.Additive.SmallTripling
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : Group G
k : ℝ
m_1 m : ℕ
hm : 3 ≤ m + 1
ε : Fin (m + 1 + 1) → ℤ
hε : ∀ (i : Fin (m + 1 + 1)), |ε i| = 1
hm₀ : m ≠ 0
hε₀ : ∀ (i : Fin (m + 1 + 1)), ε i ≠ 0
h :
  ∀ (ε : Fin 3 → ℤ),
    (∀ (i : Fin 3), |ε i| = 1) →
      (↑(card.{u_1} (α := G) (prod (List.map (fun (i : Fin 3) ↦ HPow.hPow (α := Finset G) ∅ (ε i)) (finRange 3)))) :
          ℝ) ≤
        k * (↑(card.{u_1} (α := G) ∅) : ℝ)
ih :
  ∀ (ε : Fin (m + 1) → ℤ) (hε : ∀ (i : Fin (m + 1)), |ε i| = 1),
    (↑(card.{u_1} (α := G)
            (prod (List.map (fun (i : Fin (m + 1)) ↦ HPow.hPow (α := Finset G) ∅ (ε i)) (finRange (m + 1))))) :
        ℝ) ≤
      k ^ (m + 1 - 2) * (↑(card.{u_1} (α := G) ∅) : ℝ)
⊢ (↑(card.{u_1} (α := G)
          (prod (List.map (fun (i : Fin (m + 1 + 1)) ↦ HPow.hPow (α := Finset G) ∅ (ε i)) (finRange (m + 1 + 1))))) :
      ℝ) ≤
    k ^ (m + 1 + 1 - 2) * (↑(card.{u_1} (α := G) ∅) : ℝ)

Tactic:
simp [hε₀]
-- Module: Mathlib.Combinatorics.Additive.SmallTripling
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : Group G
A : Finset G
k : ℝ
m_1 : ℕ
h :
  ∀ (ε : Fin 3 → ℤ),
    (∀ (i : Fin 3), |ε i| = 1) →
      (↑(card.{u_1} (α := G) (prod (List.map (fun (i : Fin 3) ↦ A ^ ε i) (finRange 3)))) : ℝ) ≤ k * (↑(#A) : ℝ)
m : ℕ
hm : 3 ≤ m + 1
ih :
  ∀ (ε : Fin (m + 1) → ℤ) (hε : ∀ (i : Fin (m + 1)), |ε i| = 1),
    (↑(card.{u_1} (α := G) (prod (List.map (fun (i : Fin (m + 1)) ↦ A ^ ε i) (finRange (m + 1))))) : ℝ) ≤
      k ^ (m + 1 - 2) * (↑(#A) : ℝ)
ε : Fin (m + 1 + 1) → ℤ
hε : ∀ (i : Fin (m + 1 + 1)), |ε i| = 1
hm₀ : m ≠ 0
hε₀ : ∀ (i : Fin (m + 1 + 1)), ε i ≠ 0
hA : A.Nonempty
⊢ ∀ (i : Fin 3), Eq (α := ℤ) |1 i| 1

Tactic:
simp
-- Module: Mathlib.Combinatorics.Additive.SmallTripling
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : Group G
A : Finset G
k : ℝ
m_1 : ℕ
h :
  ∀ (ε : Fin 3 → ℤ),
    (∀ (i : Fin 3), |ε i| = 1) →
      (↑(card.{u_1} (α := G) (prod (List.map (fun (i : Fin 3) ↦ A ^ ε i) (finRange 3)))) : ℝ) ≤ k * (↑(#A) : ℝ)
m : ℕ
hm : 3 ≤ m + 1
ih :
  ∀ (ε : Fin (m + 1) → ℤ) (hε : ∀ (i : Fin (m + 1)), |ε i| = 1),
    (↑(card.{u_1} (α := G) (prod (List.map (fun (i : Fin (m + 1)) ↦ A ^ ε i) (finRange (m + 1))))) : ℝ) ≤
      k ^ (m + 1 - 2) * (↑(#A) : ℝ)
ε : Fin (m + 1 + 1) → ℤ
hε : ∀ (i : Fin (m + 1 + 1)), |ε i| = 1
hm₀ : m ≠ 0
hε₀ : ∀ (i : Fin (m + 1 + 1)), ε i ≠ 0
hA : A.Nonempty
⊢ LE.le (α := ℝ) 0
    (↑(card.{u_1} (α := G) (prod (List.map (fun (i : Fin 3) ↦ HPow.hPow (β := ℤ) A (1 i)) (finRange 3)))) : ℝ)

Tactic:
positivity
-- Module: Mathlib.Combinatorics.Additive.SmallTripling
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : Group G
A : Finset G
k : ℝ
m_1 : ℕ
h :
  ∀ (ε : Fin 3 → ℤ),
    (∀ (i : Fin 3), |ε i| = 1) →
      (↑(card.{u_1} (α := G) (prod (List.map (fun (i : Fin 3) ↦ A ^ ε i) (finRange 3)))) : ℝ) ≤ k * (↑(#A) : ℝ)
m : ℕ
hm : 3 ≤ m + 1
ih :
  ∀ (ε : Fin (m + 1) → ℤ) (hε : ∀ (i : Fin (m + 1)), |ε i| = 1),
    (↑(card.{u_1} (α := G) (prod (List.map (fun (i : Fin (m + 1)) ↦ A ^ ε i) (finRange (m + 1))))) : ℝ) ≤
      k ^ (m + 1 - 2) * (↑(#A) : ℝ)
ε : Fin (m + 1 + 1) → ℤ
hε : ∀ (i : Fin (m + 1 + 1)), |ε i| = 1
hm₀ : m ≠ 0
hε₀ : ∀ (i : Fin (m + 1 + 1)), ε i ≠ 0
hA : A.Nonempty
⊢ LT.lt (α := ℝ) 0 (↑(#A) : ℝ)

Tactic:
positivity
-- Module: Mathlib.Combinatorics.Additive.SmallTripling
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : Group G
A : Finset G
k : ℝ
m_1 : ℕ
h :
  ∀ (ε : Fin 3 → ℤ),
    (∀ (i : Fin 3), |ε i| = 1) →
      (↑(card.{u_1} (α := G) (prod (List.map (fun (i : Fin 3) ↦ A ^ ε i) (finRange 3)))) : ℝ) ≤ k * (↑(#A) : ℝ)
m : ℕ
hm : 3 ≤ m + 1
ih :
  ∀ (ε : Fin (m + 1) → ℤ) (hε : ∀ (i : Fin (m + 1)), |ε i| = 1),
    (↑(card.{u_1} (α := G) (prod (List.map (fun (i : Fin (m + 1)) ↦ A ^ ε i) (finRange (m + 1))))) : ℝ) ≤
      k ^ (m + 1 - 2) * (↑(#A) : ℝ)
ε : Fin (m + 1 + 1) → ℤ
hε : ∀ (i : Fin (m + 1 + 1)), |ε i| = 1
hm₀ : m ≠ 0
hε₀ : ∀ (i : Fin (m + 1 + 1)), ε i ≠ 0
hA : A.Nonempty
⊢ 0 ≤ k

Tactic:
have hk : 0 ≤ k :=
      nonneg_of_mul_nonneg_left ((h 1 (by simp)).trans' (by positivity)) (by positivity)
-- Module: Mathlib.Combinatorics.Additive.SmallTripling
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : Group G
A : Finset G
k : ℝ
m_1 : ℕ
h :
  ∀ (ε : Fin 3 → ℤ),
    (∀ (i : Fin 3), |ε i| = 1) →
      (↑(card.{u_1} (α := G) (prod (List.map (fun (i : Fin 3) ↦ A ^ ε i) (finRange 3)))) : ℝ) ≤ k * (↑(#A) : ℝ)
m : ℕ
hm : 3 ≤ m + 1
ih :
  ∀ (ε : Fin (m + 1) → ℤ) (hε : ∀ (i : Fin (m + 1)), |ε i| = 1),
    (↑(card.{u_1} (α := G) (prod (List.map (fun (i : Fin (m + 1)) ↦ A ^ ε i) (finRange (m + 1))))) : ℝ) ≤
      k ^ (m + 1 - 2) * (↑(#A) : ℝ)
ε : Fin (m + 1 + 1) → ℤ
hε : ∀ (i : Fin (m + 1 + 1)), |ε i| = 1
hm₀ : m ≠ 0
hε₀ : ∀ (i : Fin (m + 1 + 1)), ε i ≠ 0
hA : A.Nonempty
hk : 0 ≤ k
π : {n : ℕ} → (δ : Fin n → ℤ) → Finset G :=
  fun {n : ℕ} (δ : Fin n → ℤ) ↦ prod (List.map (fun (i : Fin n) ↦ A ^ δ i) (finRange n))
V : Finset G := π ![-ε 1, -ε 0]
W : Finset G := π (tail (α := fun (i : Fin (m + 1)) ↦ ℤ) (tail (α := fun (i : Fin (m + 1 + 1)) ↦ ℤ) ε))
⊢ LT.lt (α := ℝ) 0 (↑(#A) : ℝ)

Tactic:
positivity
-- Module: Mathlib.Combinatorics.Additive.SmallTripling
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : Group G
A : Finset G
k : ℝ
m_1 : ℕ
h :
  ∀ (ε : Fin 3 → ℤ),
    (∀ (i : Fin 3), |ε i| = 1) →
      (↑(card.{u_1} (α := G) (prod (List.map (fun (i : Fin 3) ↦ A ^ ε i) (finRange 3)))) : ℝ) ≤ k * (↑(#A) : ℝ)
m : ℕ
hm : 3 ≤ m + 1
ih :
  ∀ (ε : Fin (m + 1) → ℤ) (hε : ∀ (i : Fin (m + 1)), |ε i| = 1),
    (↑(card.{u_1} (α := G) (prod (List.map (fun (i : Fin (m + 1)) ↦ A ^ ε i) (finRange (m + 1))))) : ℝ) ≤
      k ^ (m + 1 - 2) * (↑(#A) : ℝ)
ε : Fin (m + 1 + 1) → ℤ
hε : ∀ (i : Fin (m + 1 + 1)), |ε i| = 1
hm₀ : m ≠ 0
hε₀ : ∀ (i : Fin (m + 1 + 1)), ε i ≠ 0
hA : A.Nonempty
hk : 0 ≤ k
π : {n : ℕ} → (δ : Fin n → ℤ) → Finset G :=
  fun {n : ℕ} (δ : Fin n → ℤ) ↦ prod (List.map (fun (i : Fin n) ↦ A ^ δ i) (finRange n))
V : Finset G := π ![-ε 1, -ε 0]
W : Finset G := π (tail (α := fun (i : Fin (m + 1)) ↦ ℤ) (tail (α := fun (i : Fin (m + 1 + 1)) ↦ ℤ) ε))
succ :
  HMul.hMul (α := ℝ) (↑(#A) : ℝ)
      (↑(card.{u_1} (α := G) (prod (List.map (fun (i : Fin (m + 1 + 1)) ↦ A ^ ε i) (finRange (m + 1 + 1))))) : ℝ) ≤
    (↑(#A) : ℝ) * (k ^ (m + 1 + 1 - 2) * (↑(#A) : ℝ))
⊢ (↑(card.{u_1} (α := G) (prod (List.map (fun (i : Fin (m + 1 + 1)) ↦ A ^ ε i) (finRange (m + 1 + 1))))) : ℝ) ≤
    k ^ (m + 1 + 1 - 2) * (↑(#A) : ℝ)

Tactic:
refine le_of_mul_le_mul_left ?_ (by positivity : (0 : ℝ) < #A)

Premises used: le_of_mul_le_mul_left
-- Module: Mathlib.Combinatorics.Additive.SmallTripling
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : Group G
A : Finset G
k : ℝ
m_1 : ℕ
h :
  ∀ (ε : Fin 3 → ℤ),
    (∀ (i : Fin 3), |ε i| = 1) →
      (↑(card.{u_1} (α := G) (prod (List.map (fun (i : Fin 3) ↦ A ^ ε i) (finRange 3)))) : ℝ) ≤ k * (↑(#A) : ℝ)
m : ℕ
hm : 3 ≤ m + 1
ih :
  ∀ (ε : Fin (m + 1) → ℤ) (hε : ∀ (i : Fin (m + 1)), |ε i| = 1),
    (↑(card.{u_1} (α := G) (prod (List.map (fun (i : Fin (m + 1)) ↦ A ^ ε i) (finRange (m + 1))))) : ℝ) ≤
      k ^ (m + 1 - 2) * (↑(#A) : ℝ)
ε : Fin (m + 1 + 1) → ℤ
hε : ∀ (i : Fin (m + 1 + 1)), |ε i| = 1
hm₀ : m ≠ 0
hε₀ : ∀ (i : Fin (m + 1 + 1)), ε i ≠ 0
hA : A.Nonempty
hk : 0 ≤ k
π : {n : ℕ} → (δ : Fin n → ℤ) → Finset G :=
  fun {n : ℕ} (δ : Fin n → ℤ) ↦ prod (List.map (fun (i : Fin n) ↦ A ^ δ i) (finRange n))
V : Finset G := π ![-ε 1, -ε 0]
W : Finset G := π (tail (α := fun (i : Fin (m + 1)) ↦ ℤ) (tail (α := fun (i : Fin (m + 1 + 1)) ↦ ℤ) ε))
⊢ HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#(π ε)) : ℝ) = HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#(V⁻¹ * W)) : ℝ)

Tactic:
simp [π, V, W, List.finRange_succ, Fin.tail, Function.comp_def, mul_assoc]

Premises used: mul_assoc, List.finRange_succ, Function.comp_def, Fin.tail
-- Module: Mathlib.Combinatorics.Additive.SmallTripling
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : Group G
A : Finset G
k : ℝ
m_1 : ℕ
h :
  ∀ (ε : Fin 3 → ℤ),
    (∀ (i : Fin 3), |ε i| = 1) →
      (↑(card.{u_1} (α := G) (prod (List.map (fun (i : Fin 3) ↦ A ^ ε i) (finRange 3)))) : ℝ) ≤ k * (↑(#A) : ℝ)
m : ℕ
hm : 3 ≤ m + 1
ih :
  ∀ (ε : Fin (m + 1) → ℤ) (hε : ∀ (i : Fin (m + 1)), |ε i| = 1),
    (↑(card.{u_1} (α := G) (prod (List.map (fun (i : Fin (m + 1)) ↦ A ^ ε i) (finRange (m + 1))))) : ℝ) ≤
      k ^ (m + 1 - 2) * (↑(#A) : ℝ)
ε : Fin (m + 1 + 1) → ℤ
hε : ∀ (i : Fin (m + 1 + 1)), |ε i| = 1
hm₀ : m ≠ 0
hε₀ : ∀ (i : Fin (m + 1 + 1)), ε i ≠ 0
hA : A.Nonempty
hk : 0 ≤ k
π : {n : ℕ} → (δ : Fin n → ℤ) → Finset G :=
  fun {n : ℕ} (δ : Fin n → ℤ) ↦ prod (List.map (fun (i : Fin n) ↦ A ^ δ i) (finRange n))
V : Finset G := π ![-ε 1, -ε 0]
W : Finset G := π (tail (α := fun (i : Fin (m + 1)) ↦ ℤ) (tail (α := fun (i : Fin (m + 1 + 1)) ↦ ℤ) ε))
⊢ #A * #(V⁻¹ * W) ≤ #(A * V) * #(A * W)

Tactic:
ruzsa_triangle_inequality_invMul_mul_mul ..

Premises used: Finset.ruzsa_triangle_inequality_invMul_mul_mul
-- Module: Mathlib.Combinatorics.Additive.SmallTripling
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : Group G
A : Finset G
k : ℝ
m_1 : ℕ
h :
  ∀ (ε : Fin 3 → ℤ),
    (∀ (i : Fin 3), |ε i| = 1) →
      (↑(card.{u_1} (α := G) (prod (List.map (fun (i : Fin 3) ↦ A ^ ε i) (finRange 3)))) : ℝ) ≤ k * (↑(#A) : ℝ)
m : ℕ
hm : 3 ≤ m + 1
ih :
  ∀ (ε : Fin (m + 1) → ℤ) (hε : ∀ (i : Fin (m + 1)), |ε i| = 1),
    (↑(card.{u_1} (α := G) (prod (List.map (fun (i : Fin (m + 1)) ↦ A ^ ε i) (finRange (m + 1))))) : ℝ) ≤
      k ^ (m + 1 - 2) * (↑(#A) : ℝ)
ε : Fin (m + 1 + 1) → ℤ
hε : ∀ (i : Fin (m + 1 + 1)), |ε i| = 1
hm₀ : m ≠ 0
hε₀ : ∀ (i : Fin (m + 1 + 1)), ε i ≠ 0
hA : A.Nonempty
hk : 0 ≤ k
π : {n : ℕ} → (δ : Fin n → ℤ) → Finset G :=
  fun {n : ℕ} (δ : Fin n → ℤ) ↦ prod (List.map (fun (i : Fin n) ↦ A ^ δ i) (finRange n))
V : Finset G := π ![-ε 1, -ε 0]
W : Finset G := π (tail (α := fun (i : Fin (m + 1)) ↦ ℤ) (tail (α := fun (i : Fin (m + 1 + 1)) ↦ ℤ) ε))
⊢ #A * #(V⁻¹ * W) ≤ #(A * V) * #(A * W)

Tactic:
exact ruzsa_triangle_inequality_invMul_mul_mul ..

Premises used: Finset.ruzsa_triangle_inequality_invMul_mul_mul
-- Module: Mathlib.Combinatorics.Additive.SmallTripling
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : Group G
A : Finset G
k : ℝ
m_1 : ℕ
h :
  ∀ (ε : Fin 3 → ℤ),
    (∀ (i : Fin 3), |ε i| = 1) →
      (↑(card.{u_1} (α := G) (prod (List.map (fun (i : Fin 3) ↦ A ^ ε i) (finRange 3)))) : ℝ) ≤ k * (↑(#A) : ℝ)
m : ℕ
hm : 3 ≤ m + 1
ih :
  ∀ (ε : Fin (m + 1) → ℤ) (hε : ∀ (i : Fin (m + 1)), |ε i| = 1),
    (↑(card.{u_1} (α := G) (prod (List.map (fun (i : Fin (m + 1)) ↦ A ^ ε i) (finRange (m + 1))))) : ℝ) ≤
      k ^ (m + 1 - 2) * (↑(#A) : ℝ)
ε : Fin (m + 1 + 1) → ℤ
hε : ∀ (i : Fin (m + 1 + 1)), |ε i| = 1
hm₀ : m ≠ 0
hε₀ : ∀ (i : Fin (m + 1 + 1)), ε i ≠ 0
hA : A.Nonempty
hk : 0 ≤ k
π : {n : ℕ} → (δ : Fin n → ℤ) → Finset G :=
  fun {n : ℕ} (δ : Fin n → ℤ) ↦ prod (List.map (fun (i : Fin n) ↦ A ^ δ i) (finRange n))
V : Finset G := π ![-ε 1, -ε 0]
W : Finset G := π (tail (α := fun (i : Fin (m + 1)) ↦ ℤ) (tail (α := fun (i : Fin (m + 1 + 1)) ↦ ℤ) ε))
⊢ HMul.hMul (α := ℝ) (↑(#(A * V)) : ℝ) (↑(#(A * W)) : ℝ) =
    HMul.hMul (α := ℝ) (↑(#(π ![1, -ε 1, -ε 0])) : ℝ)
      (↑(#(π (n := m + 1)
              (Fin.cons (α := fun (a : Fin (m + 1)) ↦ ℤ) 1
                (tail (α := fun (i : Fin (m + 1)) ↦ ℤ) (tail (α := fun (i : Fin (m + 1 + 1)) ↦ ℤ) ε))))) :
        ℝ)

Tactic:
simp [π, V, W, List.finRange_succ, Fin.tail, Function.comp_def]

Premises used: List.finRange_succ, Function.comp_def, Fin.tail
-- Module: Mathlib.Combinatorics.Additive.SmallTripling
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : Group G
A : Finset G
k : ℝ
m_1 : ℕ
h :
  ∀ (ε : Fin 3 → ℤ),
    (∀ (i : Fin 3), |ε i| = 1) →
      (↑(card.{u_1} (α := G) (prod (List.map (fun (i : Fin 3) ↦ A ^ ε i) (finRange 3)))) : ℝ) ≤ k * (↑(#A) : ℝ)
m : ℕ
hm : 3 ≤ m + 1
ih :
  ∀ (ε : Fin (m + 1) → ℤ) (hε : ∀ (i : Fin (m + 1)), |ε i| = 1),
    (↑(card.{u_1} (α := G) (prod (List.map (fun (i : Fin (m + 1)) ↦ A ^ ε i) (finRange (m + 1))))) : ℝ) ≤
      k ^ (m + 1 - 2) * (↑(#A) : ℝ)
ε : Fin (m + 1 + 1) → ℤ
hε : ∀ (i : Fin (m + 1 + 1)), |ε i| = 1
hm₀ : m ≠ 0
hε₀ : ∀ (i : Fin (m + 1 + 1)), ε i ≠ 0
hA : A.Nonempty
hk : 0 ≤ k
π : {n : ℕ} → (δ : Fin n → ℤ) → Finset G :=
  fun {n : ℕ} (δ : Fin n → ℤ) ↦ prod (List.map (fun (i : Fin n) ↦ A ^ δ i) (finRange n))
V : Finset G := π ![-ε 1, -ε 0]
W : Finset G := π (tail (α := fun (i : Fin (m + 1)) ↦ ℤ) (tail (α := fun (i : Fin (m + 1 + 1)) ↦ ℤ) ε))
h₁ : (↑(#(π ![1, -ε 1, -ε 0])) : ℝ) ≤ k * (↑(#A) : ℝ)
h₂ :
  (↑(#(π (n := m + 1)
            (Fin.cons (α := fun (a : Fin (m + 1)) ↦ ℤ) 1
              (tail (α := fun (i : Fin (m + 1)) ↦ ℤ) (tail (α := fun (i : Fin (m + 1 + 1)) ↦ ℤ) ε))))) :
      ℝ) ≤
    k ^ (m - 1) * (↑(#A) : ℝ)
⊢ HMul.hMul (α := ℝ) (↑(#(π ![1, -ε 1, -ε 0])) : ℝ)
      (↑(#(π (n := m + 1)
              (Fin.cons (α := fun (a : Fin (m + 1)) ↦ ℤ) 1
                (tail (α := fun (i : Fin (m + 1)) ↦ ℤ) (tail (α := fun (i : Fin (m + 1 + 1)) ↦ ℤ) ε))))) :
        ℝ) ≤
    k * (↑(#A) : ℝ) * (k ^ (m - 1) * (↑(#A) : ℝ))

Tactic:
gcongr
-- Module: Mathlib.Combinatorics.Additive.SmallTripling
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : Group G
A : Finset G
k : ℝ
m_1 : ℕ
h :
  ∀ (ε : Fin 3 → ℤ),
    (∀ (i : Fin 3), |ε i| = 1) →
      (↑(card.{u_1} (α := G) (prod (List.map (fun (i : Fin 3) ↦ A ^ ε i) (finRange 3)))) : ℝ) ≤ k * (↑(#A) : ℝ)
m : ℕ
hm : 3 ≤ m + 1
ih :
  ∀ (ε : Fin (m + 1) → ℤ) (hε : ∀ (i : Fin (m + 1)), |ε i| = 1),
    (↑(card.{u_1} (α := G) (prod (List.map (fun (i : Fin (m + 1)) ↦ A ^ ε i) (finRange (m + 1))))) : ℝ) ≤
      k ^ (m + 1 - 2) * (↑(#A) : ℝ)
ε : Fin (m + 1 + 1) → ℤ
hε : ∀ (i : Fin (m + 1 + 1)), |ε i| = 1
hm₀ : m ≠ 0
hε₀ : ∀ (i : Fin (m + 1 + 1)), ε i ≠ 0
hA : A.Nonempty
hk : 0 ≤ k
π : {n : ℕ} → (δ : Fin n → ℤ) → Finset G :=
  fun {n : ℕ} (δ : Fin n → ℤ) ↦ prod (List.map (fun (i : Fin n) ↦ A ^ δ i) (finRange n))
V : Finset G := π ![-ε 1, -ε 0]
W : Finset G := π (tail (α := fun (i : Fin (m + 1)) ↦ ℤ) (tail (α := fun (i : Fin (m + 1 + 1)) ↦ ℤ) ε))
i : Fin 3
0 : |![1, -ε 1, -ε 0] ((fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3))| = 1
1 : |![1, -ε 1, -ε 0] ((fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3))| = 1
2 : |![1, -ε 1, -ε 0] ((fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3))| = 1
⊢ |![1, -ε 1, -ε 0] i| = 1

Tactic:
fin_cases i
-- Module: Mathlib.Combinatorics.Additive.SmallTripling
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : Group G
A : Finset G
k : ℝ
m_1 : ℕ
h :
  ∀ (ε : Fin 3 → ℤ),
    (∀ (i : Fin 3), |ε i| = 1) →
      (↑(card.{u_1} (α := G) (prod (List.map (fun (i : Fin 3) ↦ A ^ ε i) (finRange 3)))) : ℝ) ≤ k * (↑(#A) : ℝ)
m : ℕ
hm : 3 ≤ m + 1
ih :
  ∀ (ε : Fin (m + 1) → ℤ) (hε : ∀ (i : Fin (m + 1)), |ε i| = 1),
    (↑(card.{u_1} (α := G) (prod (List.map (fun (i : Fin (m + 1)) ↦ A ^ ε i) (finRange (m + 1))))) : ℝ) ≤
      k ^ (m + 1 - 2) * (↑(#A) : ℝ)
ε : Fin (m + 1 + 1) → ℤ
hε : ∀ (i : Fin (m + 1 + 1)), |ε i| = 1
hm₀ : m ≠ 0
hε₀ : ∀ (i : Fin (m + 1 + 1)), ε i ≠ 0
hA : A.Nonempty
hk : 0 ≤ k
π : {n : ℕ} → (δ : Fin n → ℤ) → Finset G :=
  fun {n : ℕ} (δ : Fin n → ℤ) ↦ prod (List.map (fun (i : Fin n) ↦ A ^ δ i) (finRange n))
V : Finset G := π ![-ε 1, -ε 0]
W : Finset G := π (tail (α := fun (i : Fin (m + 1)) ↦ ℤ) (tail (α := fun (i : Fin (m + 1 + 1)) ↦ ℤ) ε))
⊢ |![1, -ε 1, -ε 0] ((fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3))| = 1

Tactic:
simp [hε]
-- Module: Mathlib.Combinatorics.Additive.SmallTripling
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : Group G
A : Finset G
k : ℝ
m_1 : ℕ
h :
  ∀ (ε : Fin 3 → ℤ),
    (∀ (i : Fin 3), |ε i| = 1) →
      (↑(card.{u_1} (α := G) (prod (List.map (fun (i : Fin 3) ↦ A ^ ε i) (finRange 3)))) : ℝ) ≤ k * (↑(#A) : ℝ)
m : ℕ
hm : 3 ≤ m + 1
ih :
  ∀ (ε : Fin (m + 1) → ℤ) (hε : ∀ (i : Fin (m + 1)), |ε i| = 1),
    (↑(card.{u_1} (α := G) (prod (List.map (fun (i : Fin (m + 1)) ↦ A ^ ε i) (finRange (m + 1))))) : ℝ) ≤
      k ^ (m + 1 - 2) * (↑(#A) : ℝ)
ε : Fin (m + 1 + 1) → ℤ
hε : ∀ (i : Fin (m + 1 + 1)), |ε i| = 1
hm₀ : m ≠ 0
hε₀ : ∀ (i : Fin (m + 1 + 1)), ε i ≠ 0
hA : A.Nonempty
hk : 0 ≤ k
π : {n : ℕ} → (δ : Fin n → ℤ) → Finset G :=
  fun {n : ℕ} (δ : Fin n → ℤ) ↦ prod (List.map (fun (i : Fin n) ↦ A ^ δ i) (finRange n))
V : Finset G := π ![-ε 1, -ε 0]
W : Finset G := π (tail (α := fun (i : Fin (m + 1)) ↦ ℤ) (tail (α := fun (i : Fin (m + 1 + 1)) ↦ ℤ) ε))
⊢ |![1, -ε 1, -ε 0] ((fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3))| = 1

Tactic:
simp [hε]
-- Module: Mathlib.Combinatorics.Additive.SmallTripling
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : Group G
A : Finset G
k : ℝ
m_1 : ℕ
h :
  ∀ (ε : Fin 3 → ℤ),
    (∀ (i : Fin 3), |ε i| = 1) →
      (↑(card.{u_1} (α := G) (prod (List.map (fun (i : Fin 3) ↦ A ^ ε i) (finRange 3)))) : ℝ) ≤ k * (↑(#A) : ℝ)
m : ℕ
hm : 3 ≤ m + 1
ih :
  ∀ (ε : Fin (m + 1) → ℤ) (hε : ∀ (i : Fin (m + 1)), |ε i| = 1),
    (↑(card.{u_1} (α := G) (prod (List.map (fun (i : Fin (m + 1)) ↦ A ^ ε i) (finRange (m + 1))))) : ℝ) ≤
      k ^ (m + 1 - 2) * (↑(#A) : ℝ)
ε : Fin (m + 1 + 1) → ℤ
hε : ∀ (i : Fin (m + 1 + 1)), |ε i| = 1
hm₀ : m ≠ 0
hε₀ : ∀ (i : Fin (m + 1 + 1)), ε i ≠ 0
hA : A.Nonempty
hk : 0 ≤ k
π : {n : ℕ} → (δ : Fin n → ℤ) → Finset G :=
  fun {n : ℕ} (δ : Fin n → ℤ) ↦ prod (List.map (fun (i : Fin n) ↦ A ^ δ i) (finRange n))
V : Finset G := π ![-ε 1, -ε 0]
W : Finset G := π (tail (α := fun (i : Fin (m + 1)) ↦ ℤ) (tail (α := fun (i : Fin (m + 1 + 1)) ↦ ℤ) ε))
⊢ |![1, -ε 1, -ε 0] ((fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3))| = 1

Tactic:
simp [hε]
-- Module: Mathlib.Combinatorics.Additive.SmallTripling
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : Group G
A : Finset G
k : ℝ
m_1 : ℕ
h :
  ∀ (ε : Fin 3 → ℤ),
    (∀ (i : Fin 3), |ε i| = 1) →
      (↑(card.{u_1} (α := G) (prod (List.map (fun (i : Fin 3) ↦ A ^ ε i) (finRange 3)))) : ℝ) ≤ k * (↑(#A) : ℝ)
m : ℕ
hm : 3 ≤ m + 1
ih :
  ∀ (ε : Fin (m + 1) → ℤ) (hε : ∀ (i : Fin (m + 1)), |ε i| = 1),
    (↑(card.{u_1} (α := G) (prod (List.map (fun (i : Fin (m + 1)) ↦ A ^ ε i) (finRange (m + 1))))) : ℝ) ≤
      k ^ (m + 1 - 2) * (↑(#A) : ℝ)
ε : Fin (m + 1 + 1) → ℤ
hε : ∀ (i : Fin (m + 1 + 1)), |ε i| = 1
hm₀ : m ≠ 0
hε₀ : ∀ (i : Fin (m + 1 + 1)), ε i ≠ 0
hA : A.Nonempty
hk : 0 ≤ k
π : {n : ℕ} → (δ : Fin n → ℤ) → Finset G :=
  fun {n : ℕ} (δ : Fin n → ℤ) ↦ prod (List.map (fun (i : Fin n) ↦ A ^ δ i) (finRange n))
V : Finset G := π ![-ε 1, -ε 0]
W : Finset G := π (tail (α := fun (i : Fin (m + 1)) ↦ ℤ) (tail (α := fun (i : Fin (m + 1 + 1)) ↦ ℤ) ε))
⊢ (↑(#(π ![1, -ε 1, -ε 0])) : ℝ) ≤ k * (↑(#A) : ℝ)

Tactic:
exact h ![1, -ε 1, -ε 0] fun i ↦ by fin_cases i <;> simp [hε]

Premises used: Matrix.vecEmpty, OfNat.ofNat, Matrix.vecCons, Neg.neg
-- Module: Mathlib.Combinatorics.Additive.SmallTripling
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : Group G
A : Finset G
k : ℝ
m_1 : ℕ
h :
  ∀ (ε : Fin 3 → ℤ),
    (∀ (i : Fin 3), |ε i| = 1) →
      (↑(card.{u_1} (α := G) (prod (List.map (fun (i : Fin 3) ↦ A ^ ε i) (finRange 3)))) : ℝ) ≤ k * (↑(#A) : ℝ)
m : ℕ
hm : 3 ≤ m + 1
ih :
  ∀ (ε : Fin (m + 1) → ℤ) (hε : ∀ (i : Fin (m + 1)), |ε i| = 1),
    (↑(card.{u_1} (α := G) (prod (List.map (fun (i : Fin (m + 1)) ↦ A ^ ε i) (finRange (m + 1))))) : ℝ) ≤
      k ^ (m + 1 - 2) * (↑(#A) : ℝ)
ε : Fin (m + 1 + 1) → ℤ
hε : ∀ (i : Fin (m + 1 + 1)), |ε i| = 1
hm₀ : m ≠ 0
hε₀ : ∀ (i : Fin (m + 1 + 1)), ε i ≠ 0
hA : A.Nonempty
hk : 0 ≤ k
π : {n : ℕ} → (δ : Fin n → ℤ) → Finset G :=
  fun {n : ℕ} (δ : Fin n → ℤ) ↦ prod (List.map (fun (i : Fin n) ↦ A ^ δ i) (finRange n))
V : Finset G := π ![-ε 1, -ε 0]
W : Finset G := π (tail (α := fun (i : Fin (m + 1)) ↦ ℤ) (tail (α := fun (i : Fin (m + 1 + 1)) ↦ ℤ) ε))
⊢ Eq (α := ℤ)
    (|Fin.cons (α := fun (a : Fin (m + 1)) ↦ ℤ) 1
          (tail (α := fun (i : Fin (m + 1)) ↦ ℤ) (tail (α := fun (i : Fin (m + 1 + 1)) ↦ ℤ) ε)) 0| :
      ℤ)
    (1 : ℤ)

Tactic:
simp
-- Module: Mathlib.Combinatorics.Additive.SmallTripling
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : Group G
A : Finset G
k : ℝ
m_1 : ℕ
h :
  ∀ (ε : Fin 3 → ℤ),
    (∀ (i : Fin 3), |ε i| = 1) →
      (↑(card.{u_1} (α := G) (prod (List.map (fun (i : Fin 3) ↦ A ^ ε i) (finRange 3)))) : ℝ) ≤ k * (↑(#A) : ℝ)
m : ℕ
hm : 3 ≤ m + 1
ih :
  ∀ (ε : Fin (m + 1) → ℤ) (hε : ∀ (i : Fin (m + 1)), |ε i| = 1),
    (↑(card.{u_1} (α := G) (prod (List.map (fun (i : Fin (m + 1)) ↦ A ^ ε i) (finRange (m + 1))))) : ℝ) ≤
      k ^ (m + 1 - 2) * (↑(#A) : ℝ)
ε : Fin (m + 1 + 1) → ℤ
hε : ∀ (i : Fin (m + 1 + 1)), |ε i| = 1
hm₀ : m ≠ 0
hε₀ : ∀ (i : Fin (m + 1 + 1)), ε i ≠ 0
hA : A.Nonempty
hk : 0 ≤ k
π : {n : ℕ} → (δ : Fin n → ℤ) → Finset G :=
  fun {n : ℕ} (δ : Fin n → ℤ) ↦ prod (List.map (fun (i : Fin n) ↦ A ^ δ i) (finRange n))
V : Finset G := π ![-ε 1, -ε 0]
W : Finset G := π (tail (α := fun (i : Fin (m + 1)) ↦ ℤ) (tail (α := fun (i : Fin (m + 1 + 1)) ↦ ℤ) ε))
⊢ ∀ (i : Fin m),
    Eq (α := ℤ)
      (|Fin.cons (α := fun (a : Fin (m + 1)) ↦ ℤ) 1
            (tail (α := fun (i : Fin (m + 1)) ↦ ℤ) (tail (α := fun (i : Fin (m + 1 + 1)) ↦ ℤ) ε)) i.succ| :
        ℤ)
      (1 : ℤ)

Tactic:
simp [hε, Fin.tail]

Premises used: Fin.tail