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 : ℝ
hA : (↑(#(HPow.hPow (β := ℕ) A 3)) : ℝ) ≤ K * (↑(#A) : ℝ)
hA₀ : A.Nonempty
⊢ (↑(#(HPow.hPow (β := ℕ) A 2)) : ℝ) ≤ K * (↑(#A) : ℝ)

Tactic:
calc
        (#(A ^ 2) : ℝ) ≤ #(A ^ 3) := mod_cast hA₀.card_pow_mono (by simp)
        _ ≤ K * #A := hA

Premises used: Nat.cast, Finset.Nonempty.card_pow_mono, HPow.hPow, Finset.card, OfNat.ofNat
-- Module: Mathlib.Combinatorics.Additive.SmallTripling
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : Group G
A : Finset G
K : ℝ
hA : (↑(#(HPow.hPow (β := ℕ) A 3)) : ℝ) ≤ K * (↑(#A) : ℝ)
hA₀ : A.Nonempty
⊢ HPow.hPow (β := ℕ) K 2 * (↑(#A) : ℝ) * (K * (↑(#A) : ℝ)) = (↑(#A) : ℝ) * (HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ))

Tactic:
ring
-- Module: Mathlib.Combinatorics.Additive.SmallTripling
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : Group G
A : Finset G
K : ℝ
hA : (↑(#(HPow.hPow (β := ℕ) A 3)) : ℝ) ≤ K * (↑(#A) : ℝ)
hA₀ : A.Nonempty
simpa :
  HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#(A * A⁻¹ * A)) : ℝ) ≤
    HMul.hMul (α := ℝ) (↑(#(A * (A * A⁻¹))) : ℝ) (↑(#(A * A)) : ℝ)
simpa₁ :
  HMul.hMul (α := ℝ) (↑(#(A * (A * A⁻¹))) : ℝ) (↑(#(A * A)) : ℝ) =
    HMul.hMul (α := ℝ) (↑(#(A * A * A⁻¹)) : ℝ) (↑(#(HPow.hPow (β := ℕ) A 2)) : ℝ)
simpa₂ :
  HMul.hMul (α := ℝ) (↑(#(A * A * A⁻¹)) : ℝ) (↑(#(HPow.hPow (β := ℕ) A 2)) : ℝ) ≤
    HPow.hPow (β := ℕ) K 2 * (↑(#A) : ℝ) * (K * (↑(#A) : ℝ))
simpa₃ : HPow.hPow (β := ℕ) K 2 * (↑(#A) : ℝ) * (K * (↑(#A) : ℝ)) = (↑(#A) : ℝ) * (HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ))
⊢ HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#(A * A⁻¹ * A)) : ℝ) ≤ (↑(#A) : ℝ) * (HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ))

Tactic:
calc
    (#A * #(A * A⁻¹ * A) : ℝ) ≤ #(A * (A * A⁻¹)) * #(A * A) := by
      norm_cast; simpa using ruzsa_triangle_inequality_invMul_mul_mul (A * A⁻¹) A A
    _ = #(A * A * A⁻¹) * #(A ^ 2) := by simp [pow_succ, mul_assoc]
    _ ≤ (K ^ 2 * #A) * (K * #A) := by
      gcongr
      · exact small_pos_pos_neg_mul hA
      calc
        (#(A ^ 2) : ℝ) ≤ #(A ^ 3) := mod_cast hA₀.card_pow_mono (by simp)
        _ ≤ K * #A := hA
    _ = #A * (K ^ 3 * #A) := by ring

Premises used: HMul.hMul, Nat.cast, Inv.inv, HPow.hPow, Finset.card, OfNat.ofNat
-- Module: Mathlib.Combinatorics.Additive.SmallTripling
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : Group G
A : Finset G
K : ℝ
hA : (↑(#(HPow.hPow (β := ℕ) A 3)) : ℝ) ≤ K * (↑(#A) : ℝ)
rw : (↑(#(A⁻¹ * A * A⁻¹)⁻¹) : ℝ) ≤ HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ)
⊢ (↑(#(A⁻¹ * A * A⁻¹)) : ℝ) ≤ HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ)

Tactic:
rw [← card_inv]

Premises used: Finset.card_inv
-- Module: Mathlib.Combinatorics.Additive.SmallTripling
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : Group G
A : Finset G
K : ℝ
hA : (↑(#(HPow.hPow (β := ℕ) A 3)) : ℝ) ≤ K * (↑(#A) : ℝ)
⊢ (↑(#(A⁻¹ * A * A⁻¹)⁻¹) : ℝ) ≤ HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ)

Tactic:
simpa [mul_assoc] using small_pos_neg_pos_mul (A := A) (K := K) (by simpa)

Premises used: mul_assoc, _private.0.Finset.small_pos_neg_pos_mul
-- Module: Mathlib.Combinatorics.Additive.SmallTripling
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : Group G
A : Finset G
K : ℝ
m : ℕ
hm : 3 ≤ m
hA : (↑(#(HPow.hPow (β := ℕ) A 3)) : ℝ) ≤ K * (↑(#A) : ℝ)
ε : Fin m → ℤ
hε : ∀ (i : Fin m), |ε i| = 1
⊢ m ≠ 0

Tactic:
positivity
-- Module: Mathlib.Combinatorics.Additive.SmallTripling
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : Group G
A : Finset G
K : ℝ
m : ℕ
hm : 3 ≤ m
hA : (↑(#(HPow.hPow (β := ℕ) A 3)) : ℝ) ≤ K * (↑(#A) : ℝ)
ε : Fin m → ℤ
hε : ∀ (i : Fin m), |ε i| = 1
⊢ m ≠ 0

Tactic:
have hm₀ : m ≠ 0 := by positivity
-- Module: Mathlib.Combinatorics.Additive.SmallTripling
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : Group G
A : Finset G
K : ℝ
m : ℕ
hm : 3 ≤ m
hA : (↑(#(HPow.hPow (β := ℕ) A 3)) : ℝ) ≤ K * (↑(#A) : ℝ)
ε : Fin m → ℤ
hε : ∀ (i : Fin m), |ε i| = 1
hm₀ : m ≠ 0
i : Fin m
h : ε i = 0
⊢ False

Tactic:
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 : ℕ
hm : 3 ≤ m
hA : (↑(#(HPow.hPow (β := ℕ) A 3)) : ℝ) ≤ K * (↑(#A) : ℝ)
ε : Fin m → ℤ
hε : ∀ (i : Fin m), |ε i| = 1
hm₀ : m ≠ 0
⊢ ∀ (i : Fin m), ε 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 : ℕ
hm : 3 ≤ m
hA : (↑(#(HPow.hPow (β := ℕ) A 3)) : ℝ) ≤ K * (↑(#A) : ℝ)
ε : Fin m → ℤ
hε : ∀ (i : Fin m), |ε i| = 1
hm₀ : m ≠ 0
hε₀ : ∀ (i : Fin m), ε i ≠ 0
inl :
  ∀ (hA : (↑(#(HPow.hPow (α := Finset G) (β := ℕ) ∅ 3)) : ℝ) ≤ K * (↑(card.{u_1} (α := G) ∅) : ℝ)),
    (↑(card.{u_1} (α := G) (prod (List.map (fun (i : Fin m) ↦ HPow.hPow (α := Finset G) ∅ (ε i)) (finRange m)))) : ℝ) ≤
      K ^ (3 * (m - 2)) * (↑(card.{u_1} (α := G) ∅) : ℝ)
inr :
  ∀ (hA₀ : A.Nonempty),
    (↑(card.{u_1} (α := G) (prod (List.map (fun (i : Fin m) ↦ A ^ ε i) (finRange m)))) : ℝ) ≤
      K ^ (3 * (m - 2)) * (↑(#A) : ℝ)
⊢ (↑(card.{u_1} (α := G) (prod (List.map (fun (i : Fin m) ↦ A ^ ε i) (finRange m)))) : ℝ) ≤
    K ^ (3 * (m - 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 : ℕ
hm : 3 ≤ m
ε : Fin m → ℤ
hε : ∀ (i : Fin m), |ε i| = 1
hm₀ : m ≠ 0
hε₀ : ∀ (i : Fin m), ε i ≠ 0
hA : (↑(#(HPow.hPow (α := Finset G) (β := ℕ) ∅ 3)) : ℝ) ≤ K * (↑(card.{u_1} (α := G) ∅) : ℝ)
⊢ (↑(card.{u_1} (α := G) (prod (List.map (fun (i : Fin m) ↦ HPow.hPow (α := Finset G) ∅ (ε i)) (finRange m)))) : ℝ) ≤
    K ^ (3 * (m - 2)) * (↑(card.{u_1} (α := G) ∅) : ℝ)

Tactic:
simp [hm₀, hε₀]
-- Module: Mathlib.Combinatorics.Additive.SmallTripling
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : Group G
A : Finset G
K : ℝ
m : ℕ
hm : 3 ≤ m
hA : (↑(#(HPow.hPow (β := ℕ) A 3)) : ℝ) ≤ K * (↑(#A) : ℝ)
ε : Fin m → ℤ
hε : ∀ (i : Fin m), |ε i| = 1
hm₀ : m ≠ 0
hε₀ : ∀ (i : Fin m), ε 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 : ℕ
hm : 3 ≤ m
hA : (↑(#(HPow.hPow (β := ℕ) A 3)) : ℝ) ≤ K * (↑(#A) : ℝ)
ε : Fin m → ℤ
hε : ∀ (i : Fin m), |ε i| = 1
hm₀ : m ≠ 0
hε₀ : ∀ (i : Fin m), ε i ≠ 0
hA₀ : A.Nonempty
norm_cast : #A ≤ #(HPow.hPow (β := ℕ) A 3)
⊢ LE.le (α := ℝ) (↑(#A) : ℝ) (↑(#(HPow.hPow (β := ℕ) A 3)) : ℝ)

Tactic:
norm_cast
-- Module: Mathlib.Combinatorics.Additive.SmallTripling
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : Group G
A : Finset G
K : ℝ
m : ℕ
hm : 3 ≤ m
hA : (↑(#(HPow.hPow (β := ℕ) A 3)) : ℝ) ≤ K * (↑(#A) : ℝ)
ε : Fin m → ℤ
hε : ∀ (i : Fin m), |ε i| = 1
hm₀ : m ≠ 0
hε₀ : ∀ (i : Fin m), ε i ≠ 0
hA₀ : A.Nonempty
⊢ Ne (α := ℕ) 3 0

Tactic:
simp
-- Module: Mathlib.Combinatorics.Additive.SmallTripling
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : Group G
A : Finset G
K : ℝ
m : ℕ
hm : 3 ≤ m
hA : (↑(#(HPow.hPow (β := ℕ) A 3)) : ℝ) ≤ K * (↑(#A) : ℝ)
ε : Fin m → ℤ
hε : ∀ (i : Fin m), |ε i| = 1
hm₀ : m ≠ 0
hε₀ : ∀ (i : Fin m), ε i ≠ 0
hA₀ : A.Nonempty
⊢ #A ≤ #(HPow.hPow (β := ℕ) A 3)

Tactic:
exact card_le_card_pow (by simp)

Premises used: Finset.card_le_card_pow
-- Module: Mathlib.Combinatorics.Additive.SmallTripling
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : Group G
A : Finset G
K : ℝ
m : ℕ
hm : 3 ≤ m
hA : (↑(#(HPow.hPow (β := ℕ) A 3)) : ℝ) ≤ K * (↑(#A) : ℝ)
ε : Fin m → ℤ
hε : ∀ (i : Fin m), |ε i| = 1
hm₀ : m ≠ 0
hε₀ : ∀ (i : Fin m), ε i ≠ 0
hA₀ : A.Nonempty
⊢ 1 ≤ K

Tactic:
have hK₁ : 1 ≤ K :=
    one_le_of_le_mul_right₀ (by positivity)
      (hA.trans' <| by norm_cast; exact card_le_card_pow (by simp))
-- Module: Mathlib.Combinatorics.Additive.SmallTripling
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : Group G
A : Finset G
K : ℝ
m : ℕ
hm : 3 ≤ m
hA : (↑(#(HPow.hPow (β := ℕ) A 3)) : ℝ) ≤ K * (↑(#A) : ℝ)
ε : Fin m → ℤ
hε : ∀ (i : Fin m), |ε i| = 1
hm₀ : m ≠ 0
hε₀ : ∀ (i : Fin m), ε i ≠ 0
hA₀ : A.Nonempty
hK₁ : 1 ≤ K
inr :
  (↑(card.{u_1} (α := G) (prod (List.map (fun (i : Fin m) ↦ A ^ ε i) (finRange m)))) : ℝ) ≤
    HPow.hPow (β := ℕ) K 3 ^ (m - 2) * (↑(#A) : ℝ)
⊢ (↑(card.{u_1} (α := G) (prod (List.map (fun (i : Fin m) ↦ A ^ ε i) (finRange m)))) : ℝ) ≤
    K ^ (3 * (m - 2)) * (↑(#A) : ℝ)

Tactic:
rw [pow_mul]

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

Tactic:
inductive_claim_mul hm (fun δ hδ ↦ ?_) ε hε

Premises used: _private.0.Finset.inductive_claim_mul
-- Module: Mathlib.Combinatorics.Additive.SmallTripling
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : Group G
A : Finset G
K : ℝ
m : ℕ
hm : 3 ≤ m
hA : (↑(#(HPow.hPow (β := ℕ) A 3)) : ℝ) ≤ K * (↑(#A) : ℝ)
ε : Fin m → ℤ
hε : ∀ (i : Fin m), |ε i| = 1
hm₀ : m ≠ 0
hε₀ : ∀ (i : Fin m), ε i ≠ 0
hA₀ : A.Nonempty
hK₁ : 1 ≤ K
inr :
  ∀ (δ : Fin 3 → ℤ) (hδ : ∀ (i : Fin 3), |δ i| = 1),
    (↑(card.{u_1} (α := G) (prod (List.map (fun (i : Fin 3) ↦ A ^ δ i) (finRange 3)))) : ℝ) ≤
      HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ)
⊢ (↑(card.{u_1} (α := G) (prod (List.map (fun (i : Fin m) ↦ A ^ ε i) (finRange m)))) : ℝ) ≤
    HPow.hPow (β := ℕ) K 3 ^ (m - 2) * (↑(#A) : ℝ)

Tactic:
refine inductive_claim_mul hm (fun δ hδ ↦ ?_) ε hε

Premises used: _private.0.Finset.inductive_claim_mul
-- Module: Mathlib.Combinatorics.Additive.SmallTripling
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : Group G
A : Finset G
K : ℝ
m : ℕ
hm : 3 ≤ m
hA : (↑(#(HPow.hPow (β := ℕ) A 3)) : ℝ) ≤ K * (↑(#A) : ℝ)
ε : Fin m → ℤ
hε : ∀ (i : Fin m), |ε i| = 1
hm₀ : m ≠ 0
hε₀ : ∀ (i : Fin m), ε i ≠ 0
hA₀ : A.Nonempty
hK₁ : 1 ≤ K
δ : Fin 3 → ℤ
hδ : ∀ (i : Fin 3), |δ i| = 1
inr : (↑(#(A ^ δ 0 * A ^ δ 1 * A ^ δ 2)) : ℝ) ≤ HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ)
⊢ (↑(card.{u_1} (α := G) (prod (List.map (fun (i : Fin 3) ↦ A ^ δ i) (finRange 3)))) : ℝ) ≤
    HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ)

Tactic:
simp only [finRange_succ, Nat.reduceAdd, isValue, finRange_zero, map_nil, List.map_cons,
    succ_zero_eq_one, succ_one_eq_two, List.prod_cons, prod_nil, mul_one, ← mul_assoc]

Premises used: List.map_cons, mul_assoc, List.finRange_succ, Nat.reduceAdd, Fin.succ_zero_eq_one, Fin.isValue, List.prod_nil, mul_one, List.prod_cons, List.finRange_zero, List.map_nil, Fin.succ_one_eq_two
-- Module: Mathlib.Combinatorics.Additive.SmallTripling
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : Group G
A : Finset G
K : ℝ
m : ℕ
hm : 3 ≤ m
hA : (↑(#(HPow.hPow (β := ℕ) A 3)) : ℝ) ≤ K * (↑(#A) : ℝ)
ε : Fin m → ℤ
hε : ∀ (i : Fin m), |ε i| = 1
hm₀ : m ≠ 0
hε₀ : ∀ (i : Fin m), ε i ≠ 0
hA₀ : A.Nonempty
hK₁ : 1 ≤ K
δ : Fin 3 → ℤ
hδ : ∀ (i : Fin 3), |δ i| = 1
⊢ (δ 0 = 1 ∨ δ 0 = -1) ∧ (δ 1 = 1 ∨ δ 1 = -1) ∧ (δ 2 = 1 ∨ δ 2 = -1)

Tactic:
simp only [zero_le_one, abs_eq, Int.reduceNeg, forall_iff_succ, isValue, succ_zero_eq_one,
    succ_one_eq_two, IsEmpty.forall_iff, and_true] at hδ

Premises used: and_true, Int.reduceNeg, abs_eq, Fin.succ_zero_eq_one, zero_le_one, Fin.forall_iff_succ, Fin.isValue, IsEmpty.forall_iff, Fin.succ_one_eq_two
-- Module: Mathlib.Combinatorics.Additive.SmallTripling
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : Group G
A : Finset G
K : ℝ
m : ℕ
hm : 3 ≤ m
hA : (↑(#(HPow.hPow (β := ℕ) A 3)) : ℝ) ≤ K * (↑(#A) : ℝ)
ε : Fin m → ℤ
hε : ∀ (i : Fin m), |ε i| = 1
hm₀ : m ≠ 0
hε₀ : ∀ (i : Fin m), ε i ≠ 0
hA₀ : A.Nonempty
hK₁ : 1 ≤ K
δ : Fin 3 → ℤ
hδ : (δ 0 = 1 ∨ δ 0 = -1) ∧ (δ 1 = 1 ∨ δ 1 = -1) ∧ (δ 2 = 1 ∨ δ 2 = -1)
hmn : LE.le (α := ℕ) 2 3
⊢ HPow.hPow (β := ℕ) K 2 ≤ HPow.hPow (β := ℕ) K 3

Tactic:
gcongr
-- Module: Mathlib.Combinatorics.Additive.SmallTripling
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : Group G
A : Finset G
K : ℝ
m : ℕ
hm : 3 ≤ m
hA : (↑(#(HPow.hPow (β := ℕ) A 3)) : ℝ) ≤ K * (↑(#A) : ℝ)
ε : Fin m → ℤ
hε : ∀ (i : Fin m), |ε i| = 1
hm₀ : m ≠ 0
hε₀ : ∀ (i : Fin m), ε i ≠ 0
hA₀ : A.Nonempty
hK₁ : 1 ≤ K
δ : Fin 3 → ℤ
hδ : (δ 0 = 1 ∨ δ 0 = -1) ∧ (δ 1 = 1 ∨ δ 1 = -1) ∧ (δ 2 = 1 ∨ δ 2 = -1)
⊢ LE.le (α := ℕ) 2 3

Tactic:
simp
-- Module: Mathlib.Combinatorics.Additive.SmallTripling
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : Group G
A : Finset G
K : ℝ
m : ℕ
hm : 3 ≤ m
hA : (↑(#(HPow.hPow (β := ℕ) A 3)) : ℝ) ≤ K * (↑(#A) : ℝ)
ε : Fin m → ℤ
hε : ∀ (i : Fin m), |ε i| = 1
hm₀ : m ≠ 0
hε₀ : ∀ (i : Fin m), ε i ≠ 0
hA₀ : A.Nonempty
hK₁ : 1 ≤ K
δ : Fin 3 → ℤ
hδ : (δ 0 = 1 ∨ δ 0 = -1) ∧ (δ 1 = 1 ∨ δ 1 = -1) ∧ (δ 2 = 1 ∨ δ 2 = -1)
⊢ HPow.hPow (β := ℕ) K 2 ≤ HPow.hPow (β := ℕ) K 3

Tactic:
have : K ^ 2 ≤ K ^ 3 := by gcongr; simp
-- Module: Mathlib.Combinatorics.Additive.SmallTripling
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : Group G
A : Finset G
K : ℝ
m : ℕ
hm : 3 ≤ m
hA : (↑(#(HPow.hPow (β := ℕ) A 3)) : ℝ) ≤ K * (↑(#A) : ℝ)
ε : Fin m → ℤ
hε : ∀ (i : Fin m), |ε i| = 1
hm₀ : m ≠ 0
hε₀ : ∀ (i : Fin m), ε i ≠ 0
hA₀ : A.Nonempty
hK₁ : 1 ≤ K
δ : Fin 3 → ℤ
hδ : (δ 0 = 1 ∨ δ 0 = -1) ∧ (δ 1 = 1 ∨ δ 1 = -1) ∧ (δ 2 = 1 ∨ δ 2 = -1)
this : HPow.hPow (β := ℕ) K 2 ≤ HPow.hPow (β := ℕ) K 3
inr :
  ∀ (hδ₀ : δ 0 = 1) (hδ₁ : δ 1 = 1) (hδ₂ : δ 2 = 1),
    (↑(#(A ^ δ 0 * A ^ δ 1 * A ^ δ 2)) : ℝ) ≤ HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ)
inr₁ :
  ∀ (hδ₀ : δ 0 = 1) (hδ₁ : δ 1 = 1) (hδ₂ : δ 2 = -1),
    (↑(#(A ^ δ 0 * A ^ δ 1 * A ^ δ 2)) : ℝ) ≤ HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ)
inr₂ :
  ∀ (hδ₀ : δ 0 = 1) (hδ₁ : δ 1 = -1) (hδ₂ : δ 2 = 1),
    (↑(#(A ^ δ 0 * A ^ δ 1 * A ^ δ 2)) : ℝ) ≤ HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ)
inr₃ :
  ∀ (hδ₀ : δ 0 = 1) (hδ₁ : δ 1 = -1) (hδ₂ : δ 2 = -1),
    (↑(#(A ^ δ 0 * A ^ δ 1 * A ^ δ 2)) : ℝ) ≤ HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ)
inr₄ :
  ∀ (hδ₀ : δ 0 = -1) (hδ₁ : δ 1 = 1) (hδ₂ : δ 2 = 1),
    (↑(#(A ^ δ 0 * A ^ δ 1 * A ^ δ 2)) : ℝ) ≤ HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ)
inr₅ :
  ∀ (hδ₀ : δ 0 = -1) (hδ₁ : δ 1 = 1) (hδ₂ : δ 2 = -1),
    (↑(#(A ^ δ 0 * A ^ δ 1 * A ^ δ 2)) : ℝ) ≤ HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ)
inr₆ :
  ∀ (hδ₀ : δ 0 = -1) (hδ₁ : δ 1 = -1) (hδ₂ : δ 2 = 1),
    (↑(#(A ^ δ 0 * A ^ δ 1 * A ^ δ 2)) : ℝ) ≤ HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ)
inr₇ :
  ∀ (hδ₀ : δ 0 = -1) (hδ₁ : δ 1 = -1) (hδ₂ : δ 2 = -1),
    (↑(#(A ^ δ 0 * A ^ δ 1 * A ^ δ 2)) : ℝ) ≤ HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ)
⊢ (↑(#(A ^ δ 0 * A ^ δ 1 * A ^ δ 2)) : ℝ) ≤ HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ)

Tactic:
obtain ⟨hδ₀ | hδ₀, hδ₁ | hδ₁, hδ₂ | hδ₂⟩ := hδ
-- Module: Mathlib.Combinatorics.Additive.SmallTripling
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : Group G
A : Finset G
K : ℝ
m : ℕ
hm : 3 ≤ m
hA : (↑(#(HPow.hPow (β := ℕ) A 3)) : ℝ) ≤ K * (↑(#A) : ℝ)
ε : Fin m → ℤ
hε : ∀ (i : Fin m), |ε i| = 1
hm₀ : m ≠ 0
hε₀ : ∀ (i : Fin m), ε i ≠ 0
hA₀ : A.Nonempty
hK₁ : 1 ≤ K
δ : Fin 3 → ℤ
this : HPow.hPow (β := ℕ) K 2 ≤ HPow.hPow (β := ℕ) K 3
hδ₀ : δ 0 = 1
hδ₁ : δ 1 = 1
hδ₂ : δ 2 = 1
inr : (↑(#(A * A * A)) : ℝ) ≤ HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ)
⊢ (↑(#(A ^ δ 0 * A ^ δ 1 * A ^ δ 2)) : ℝ) ≤ HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ)

Tactic:
simp [hδ₀, hδ₁, hδ₂]
-- Module: Mathlib.Combinatorics.Additive.SmallTripling
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : Group G
A : Finset G
K : ℝ
m : ℕ
hm : 3 ≤ m
hA : (↑(#(HPow.hPow (β := ℕ) A 3)) : ℝ) ≤ K * (↑(#A) : ℝ)
ε : Fin m → ℤ
hε : ∀ (i : Fin m), |ε i| = 1
hm₀ : m ≠ 0
hε₀ : ∀ (i : Fin m), ε i ≠ 0
hA₀ : A.Nonempty
hK₁ : 1 ≤ K
δ : Fin 3 → ℤ
this : HPow.hPow (β := ℕ) K 2 ≤ HPow.hPow (β := ℕ) K 3
hδ₀ : δ 0 = 1
hδ₁ : δ 1 = 1
hδ₂ : δ 2 = -1
inr : (↑(#(A * A * A⁻¹)) : ℝ) ≤ HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ)
⊢ (↑(#(A ^ δ 0 * A ^ δ 1 * A ^ δ 2)) : ℝ) ≤ HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ)

Tactic:
simp [hδ₀, hδ₁, hδ₂]
-- Module: Mathlib.Combinatorics.Additive.SmallTripling
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : Group G
A : Finset G
K : ℝ
m : ℕ
hm : 3 ≤ m
hA : (↑(#(HPow.hPow (β := ℕ) A 3)) : ℝ) ≤ K * (↑(#A) : ℝ)
ε : Fin m → ℤ
hε : ∀ (i : Fin m), |ε i| = 1
hm₀ : m ≠ 0
hε₀ : ∀ (i : Fin m), ε i ≠ 0
hA₀ : A.Nonempty
hK₁ : 1 ≤ K
δ : Fin 3 → ℤ
this : HPow.hPow (β := ℕ) K 2 ≤ HPow.hPow (β := ℕ) K 3
hδ₀ : δ 0 = 1
hδ₁ : δ 1 = -1
hδ₂ : δ 2 = 1
inr : (↑(#(A * A⁻¹ * A)) : ℝ) ≤ HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ)
⊢ (↑(#(A ^ δ 0 * A ^ δ 1 * A ^ δ 2)) : ℝ) ≤ HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ)

Tactic:
simp [hδ₀, hδ₁, hδ₂]
-- Module: Mathlib.Combinatorics.Additive.SmallTripling
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : Group G
A : Finset G
K : ℝ
m : ℕ
hm : 3 ≤ m
hA : (↑(#(HPow.hPow (β := ℕ) A 3)) : ℝ) ≤ K * (↑(#A) : ℝ)
ε : Fin m → ℤ
hε : ∀ (i : Fin m), |ε i| = 1
hm₀ : m ≠ 0
hε₀ : ∀ (i : Fin m), ε i ≠ 0
hA₀ : A.Nonempty
hK₁ : 1 ≤ K
δ : Fin 3 → ℤ
this : HPow.hPow (β := ℕ) K 2 ≤ HPow.hPow (β := ℕ) K 3
hδ₀ : δ 0 = 1
hδ₁ : δ 1 = -1
hδ₂ : δ 2 = -1
inr : (↑(#(A * A⁻¹ * A⁻¹)) : ℝ) ≤ HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ)
⊢ (↑(#(A ^ δ 0 * A ^ δ 1 * A ^ δ 2)) : ℝ) ≤ HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ)

Tactic:
simp [hδ₀, hδ₁, hδ₂]
-- Module: Mathlib.Combinatorics.Additive.SmallTripling
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : Group G
A : Finset G
K : ℝ
m : ℕ
hm : 3 ≤ m
hA : (↑(#(HPow.hPow (β := ℕ) A 3)) : ℝ) ≤ K * (↑(#A) : ℝ)
ε : Fin m → ℤ
hε : ∀ (i : Fin m), |ε i| = 1
hm₀ : m ≠ 0
hε₀ : ∀ (i : Fin m), ε i ≠ 0
hA₀ : A.Nonempty
hK₁ : 1 ≤ K
δ : Fin 3 → ℤ
this : HPow.hPow (β := ℕ) K 2 ≤ HPow.hPow (β := ℕ) K 3
hδ₀ : δ 0 = -1
hδ₁ : δ 1 = 1
hδ₂ : δ 2 = 1
inr : (↑(#(A⁻¹ * A * A)) : ℝ) ≤ HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ)
⊢ (↑(#(A ^ δ 0 * A ^ δ 1 * A ^ δ 2)) : ℝ) ≤ HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ)

Tactic:
simp [hδ₀, hδ₁, hδ₂]
-- Module: Mathlib.Combinatorics.Additive.SmallTripling
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : Group G
A : Finset G
K : ℝ
m : ℕ
hm : 3 ≤ m
hA : (↑(#(HPow.hPow (β := ℕ) A 3)) : ℝ) ≤ K * (↑(#A) : ℝ)
ε : Fin m → ℤ
hε : ∀ (i : Fin m), |ε i| = 1
hm₀ : m ≠ 0
hε₀ : ∀ (i : Fin m), ε i ≠ 0
hA₀ : A.Nonempty
hK₁ : 1 ≤ K
δ : Fin 3 → ℤ
this : HPow.hPow (β := ℕ) K 2 ≤ HPow.hPow (β := ℕ) K 3
hδ₀ : δ 0 = -1
hδ₁ : δ 1 = 1
hδ₂ : δ 2 = -1
inr : (↑(#(A⁻¹ * A * A⁻¹)) : ℝ) ≤ HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ)
⊢ (↑(#(A ^ δ 0 * A ^ δ 1 * A ^ δ 2)) : ℝ) ≤ HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ)

Tactic:
simp [hδ₀, hδ₁, hδ₂]
-- Module: Mathlib.Combinatorics.Additive.SmallTripling
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : Group G
A : Finset G
K : ℝ
m : ℕ
hm : 3 ≤ m
hA : (↑(#(HPow.hPow (β := ℕ) A 3)) : ℝ) ≤ K * (↑(#A) : ℝ)
ε : Fin m → ℤ
hε : ∀ (i : Fin m), |ε i| = 1
hm₀ : m ≠ 0
hε₀ : ∀ (i : Fin m), ε i ≠ 0
hA₀ : A.Nonempty
hK₁ : 1 ≤ K
δ : Fin 3 → ℤ
this : HPow.hPow (β := ℕ) K 2 ≤ HPow.hPow (β := ℕ) K 3
hδ₀ : δ 0 = -1
hδ₁ : δ 1 = -1
hδ₂ : δ 2 = 1
inr : (↑(#(A⁻¹ * A⁻¹ * A)) : ℝ) ≤ HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ)
⊢ (↑(#(A ^ δ 0 * A ^ δ 1 * A ^ δ 2)) : ℝ) ≤ HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ)

Tactic:
simp [hδ₀, hδ₁, hδ₂]
-- Module: Mathlib.Combinatorics.Additive.SmallTripling
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : Group G
A : Finset G
K : ℝ
m : ℕ
hm : 3 ≤ m
hA : (↑(#(HPow.hPow (β := ℕ) A 3)) : ℝ) ≤ K * (↑(#A) : ℝ)
ε : Fin m → ℤ
hε : ∀ (i : Fin m), |ε i| = 1
hm₀ : m ≠ 0
hε₀ : ∀ (i : Fin m), ε i ≠ 0
hA₀ : A.Nonempty
hK₁ : 1 ≤ K
δ : Fin 3 → ℤ
this : HPow.hPow (β := ℕ) K 2 ≤ HPow.hPow (β := ℕ) K 3
hδ₀ : δ 0 = -1
hδ₁ : δ 1 = -1
hδ₂ : δ 2 = -1
inr : (↑(#(A⁻¹ * A⁻¹ * A⁻¹)) : ℝ) ≤ HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ)
⊢ (↑(#(A ^ δ 0 * A ^ δ 1 * A ^ δ 2)) : ℝ) ≤ HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ)

Tactic:
simp [hδ₀, hδ₁, hδ₂]
-- Module: Mathlib.Combinatorics.Additive.SmallTripling
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : Group G
A : Finset G
K : ℝ
m : ℕ
hm : 3 ≤ m
hA : (↑(#(HPow.hPow (β := ℕ) A 3)) : ℝ) ≤ K * (↑(#A) : ℝ)
ε : Fin m → ℤ
hε : ∀ (i : Fin m), |ε i| = 1
hm₀ : m ≠ 0
hε₀ : ∀ (i : Fin m), ε i ≠ 0
hA₀ : A.Nonempty
hK₁ : 1 ≤ K
δ : Fin 3 → ℤ
this : HPow.hPow (β := ℕ) K 2 ≤ HPow.hPow (β := ℕ) K 3
hδ₀ : δ 0 = 1
hδ₁ : δ 1 = 1
hδ₂ : δ 2 = 1
⊢ (↑(#(A * A * A)) : ℝ) ≤ K * (↑(#A) : ℝ)

Tactic:
simp [pow_succ] at hA

Premises used: pow_succ
-- Module: Mathlib.Combinatorics.Additive.SmallTripling
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : Group G
A : Finset G
K : ℝ
m : ℕ
hm : 3 ≤ m
ε : Fin m → ℤ
hε : ∀ (i : Fin m), |ε i| = 1
hm₀ : m ≠ 0
hε₀ : ∀ (i : Fin m), ε i ≠ 0
hA₀ : A.Nonempty
hK₁ : 1 ≤ K
δ : Fin 3 → ℤ
this : HPow.hPow (β := ℕ) K 2 ≤ HPow.hPow (β := ℕ) K 3
hδ₀ : δ 0 = 1
hδ₁ : δ 1 = 1
hδ₂ : δ 2 = 1
hA : (↑(#(A * A * A)) : ℝ) ≤ K * (↑(#A) : ℝ)
nlinarith :
  HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ) < (↑(#(A * A * A)) : ℝ) →
    (↑(#(A * A * A)) : ℝ) - K * (↑(#A) : ℝ) + (HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ) - (↑(#(A * A * A)) : ℝ)) +
            (0 - HSub.hSub (α := ℝ) 0 (↑(#(A * A * A)) : ℝ) * (1 - K)) +
          (0 - HSub.hSub (α := ℝ) 0 (↑(#A) : ℝ) * (HPow.hPow (β := ℕ) K 2 - HPow.hPow (β := ℕ) K 3)) +
        (0 - (1 - K) * ((↑(#(A * A * A)) : ℝ) - K * (↑(#A) : ℝ))) =
      0
⊢ (↑(#(A * A * A)) : ℝ) ≤ HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ)

Tactic:
nlinarith
-- Module: Mathlib.Combinatorics.Additive.SmallTripling
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : Group G
A : Finset G
K : ℝ
m : ℕ
hm : 3 ≤ m
hA : (↑(#(HPow.hPow (β := ℕ) A 3)) : ℝ) ≤ K * (↑(#A) : ℝ)
ε : Fin m → ℤ
hε : ∀ (i : Fin m), |ε i| = 1
hm₀ : m ≠ 0
hε₀ : ∀ (i : Fin m), ε i ≠ 0
hA₀ : A.Nonempty
hK₁ : 1 ≤ K
δ : Fin 3 → ℤ
this : HPow.hPow (β := ℕ) K 2 ≤ HPow.hPow (β := ℕ) K 3
hδ₀ : δ 0 = 1
hδ₁ : δ 1 = 1
hδ₂ : δ 2 = -1
nlinarith : HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ) < (↑(#(A * A * A⁻¹)) : ℝ) → 1 * HPow.hPow (α := ℝ) (β := ℕ) 1 2 = 1
nlinarith₁ : HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ) < (↑(#(A * A * A⁻¹)) : ℝ) → HMul.hMul (α := ℝ) 1 1 = 1
nlinarith₂ : HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ) < (↑(#(A * A * A⁻¹)) : ℝ) → 1 * HPow.hPow (α := ℝ) (β := ℕ) 1 3 = 1
nlinarith₃ : HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ) < (↑(#(A * A * A⁻¹)) : ℝ) → HMul.hMul (α := ℝ) 1 1 = 1
nlinarith₄ :
  HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ) < (↑(#(A * A * A⁻¹)) : ℝ) →
    1 * HPow.hPow (β := ℕ) (1 * K) 3 * HMul.hMul (α := ℝ) 1 (↑(#A) : ℝ) - HMul.hMul (α := ℝ) 1 (↑(#(A * A * A⁻¹)) : ℝ) +
          (HMul.hMul (α := ℝ) 1 (↑(#(A * A * A⁻¹)) : ℝ) -
            1 * HPow.hPow (β := ℕ) (1 * K) 2 * HMul.hMul (α := ℝ) 1 (↑(#A) : ℝ)) +
        (0 - HSub.hSub (α := ℝ) 0 (↑(#A) : ℝ) * (HPow.hPow (β := ℕ) K 2 - HPow.hPow (β := ℕ) K 3)) =
      0
⊢ (↑(#(A * A * A⁻¹)) : ℝ) ≤ HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ)

Tactic:
nlinarith [small_pos_pos_neg_mul hA]

Premises used: _private.0.Finset.small_pos_pos_neg_mul
-- Module: Mathlib.Combinatorics.Additive.SmallTripling
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : Group G
A : Finset G
K : ℝ
m : ℕ
hm : 3 ≤ m
hA : (↑(#(HPow.hPow (β := ℕ) A 3)) : ℝ) ≤ K * (↑(#A) : ℝ)
ε : Fin m → ℤ
hε : ∀ (i : Fin m), |ε i| = 1
hm₀ : m ≠ 0
hε₀ : ∀ (i : Fin m), ε i ≠ 0
hA₀ : A.Nonempty
hK₁ : 1 ≤ K
δ : Fin 3 → ℤ
this : HPow.hPow (β := ℕ) K 2 ≤ HPow.hPow (β := ℕ) K 3
hδ₀ : δ 0 = 1
hδ₁ : δ 1 = -1
hδ₂ : δ 2 = 1
nlinarith : HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ) < (↑(#(A * A⁻¹ * A)) : ℝ) → 1 * HPow.hPow (α := ℝ) (β := ℕ) 1 3 = 1
nlinarith₁ : HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ) < (↑(#(A * A⁻¹ * A)) : ℝ) → HMul.hMul (α := ℝ) 1 1 = 1
nlinarith₂ : HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ) < (↑(#(A * A⁻¹ * A)) : ℝ) → 1 * HPow.hPow (α := ℝ) (β := ℕ) 1 3 = 1
nlinarith₃ : HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ) < (↑(#(A * A⁻¹ * A)) : ℝ) → HMul.hMul (α := ℝ) 1 1 = 1
nlinarith₄ :
  HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ) < (↑(#(A * A⁻¹ * A)) : ℝ) →
    1 * HPow.hPow (β := ℕ) (1 * K) 3 * HMul.hMul (α := ℝ) 1 (↑(#A) : ℝ) - HMul.hMul (α := ℝ) 1 (↑(#(A * A⁻¹ * A)) : ℝ) +
        (HMul.hMul (α := ℝ) 1 (↑(#(A * A⁻¹ * A)) : ℝ) -
          1 * HPow.hPow (β := ℕ) (1 * K) 3 * HMul.hMul (α := ℝ) 1 (↑(#A) : ℝ)) =
      0
⊢ (↑(#(A * A⁻¹ * A)) : ℝ) ≤ HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ)

Tactic:
nlinarith [small_pos_neg_pos_mul hA]

Premises used: _private.0.Finset.small_pos_neg_pos_mul