-- Mathlib/Combinatorics/Additive/SmallTripling.lean
/-- If `A` has small tripling, say with constant `K`, then `A` has small alternating powers, in the
sense that `|A^±1 * ... * A^±1|` is at most `|A|` times a constant exponential in the number of
terms in the product.

When `A` is symmetric (`A⁻¹ = A`), the base of the exponential can be lowered from `K ^ 3` to `K`,
where `K` is the tripling constant. See `Finset.small_pow_of_small_tripling`. -/
@[to_additive
"If `A` has small tripling, say with constant `K`, then `A` has small alternating powers, in the
sense that `|±A ± ... ± A|` is at most `|A|` times a constant exponential in the number of
terms in the product.

When `A` is symmetric (`-A = A`), the base of the exponential can be lowered from `K ^ 3` to `K`,
where `K` is the tripling constant. See `Finset.small_nsmul_of_small_tripling`."]
lemma small_alternating_pow_of_small_tripling (hm : 3 ≤ m) (hA : #(A ^ 3) ≤ K * #A) (ε : Fin m → ℤ)
    (hε : ∀ i, |ε i| = 1) :
    #((finRange m).map fun i ↦ A ^ ε i).prod ≤ K ^ (3 * (m - 2)) * #A

Proof state:
case inr.intro.inr.intro.inl.inl
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
K : ℝ
m : ℕ
hm : 3 ≤ m
hA : ↑(#(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✝ : K ≤ K ^ 3
this : K ^ 2 ≤ K ^ 3
hδ₀ : δ 0 = -1
hδ₁ : δ 1 = 1
hδ₂ : δ 2 = 1
⊢ ↑(#(A⁻¹ * A * A)) ≤ K ^ 3 * ↑(#A)

Tactic:
nlinarith [small_neg_pos_pos_mul hA]

Result:
no goals

Proof state:
case inr
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
K : ℝ
m : ℕ
hm : 3 ≤ m
hA : ↑(#(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
⊢ ↑(#(A ^ δ 0 * A ^ δ 1 * A ^ δ 2)) ≤ K ^ 3 * ↑(#A)

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δ

Result:
case inr
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
K : ℝ
m : ℕ
hm : 3 ≤ m
hA : ↑(#(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)
⊢ ↑(#(A ^ δ 0 * A ^ δ 1 * A ^ δ 2)) ≤ K ^ 3 * ↑(#A)

Proof state:
case inr.intro.inl.intro.inl.inl
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : 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✝ : K ≤ K ^ 3
this : K ^ 2 ≤ K ^ 3
hδ₀ : δ 0 = 1
hδ₁ : δ 1 = 1
hδ₂ : δ 2 = 1
hA : ↑(#(A * A * A)) ≤ K * ↑(#A)
⊢ ↑(#(A * A * A)) ≤ K ^ 3 * ↑(#A)

Tactic:
nlinarith

Result:
no goals

Proof state:
case hmn
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
K : ℝ
m : ℕ
hm : 3 ≤ m
hA : ↑(#(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 : K ≤ K ^ 3
⊢ 2 ≤ 3

Tactic:
norm_num

Result:
no goals

Proof state:
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
K : ℝ
m : ℕ
hm : 3 ≤ m
hA : ↑(#(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 : K ≤ K ^ 3
⊢ K ^ 2 ≤ K ^ 3

Tactic:
gcongr

Result:
case ha
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
K : ℝ
m : ℕ
hm : 3 ≤ m
hA : ↑(#(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 : K ≤ K ^ 3
⊢ 1 ≤ K

case hmn
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
K : ℝ
m : ℕ
hm : 3 ≤ m
hA : ↑(#(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 : K ≤ K ^ 3
⊢ 2 ≤ 3

Proof state:
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
K : ℝ
m : ℕ
hm : 3 ≤ m
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
ε : Fin m → ℤ
hε : ∀ (i : Fin m), |ε i| = 1
⊢ ↑(#(List.map (fun i => A ^ ε i) (finRange m)).prod) ≤ K ^ (3 * (m - 2)) * ↑(#A)

Tactic:
have hm₀ : m ≠ 0 := by positivity

Result:
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
K : ℝ
m : ℕ
hm : 3 ≤ m
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
ε : Fin m → ℤ
hε : ∀ (i : Fin m), |ε i| = 1
hm₀ : m ≠ 0
⊢ ↑(#(List.map (fun i => A ^ ε i) (finRange m)).prod) ≤ K ^ (3 * (m - 2)) * ↑(#A)