awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.SmallTripling (goal)
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) : ℝ)
⊢ (↑(#(A ^ δ 0 * A ^ δ 1 * A ^ δ 2)) : ℝ) ≤ HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ)
have inr₇ : ∀ (hδ₀ : δ 0 = -1) (hδ₁ : δ 1 = -1) (hδ₂ : δ 2 = -1),
  (↑(#(A ^ δ 0 * A ^ δ 1 * A ^ δ 2)) : ℝ) ≤ HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ)
Tactic: obtain ⟨hδ₀ | hδ₀, hδ₁ | hδ₁, hδ₂ | hδ₂⟩ := hδ
Cleared hypotheses: hδ
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.SmallTripling (goal)
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 ^ δ 0 * A ^ δ 1 * A ^ δ 2)) : ℝ) ≤ HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ)
have inr : (↑(#(A * A * A)) : ℝ) ≤ HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ)
Tactic: simp [hδ₀, hδ₁, hδ₂]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.SmallTripling (goal)
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 ^ δ 0 * A ^ δ 1 * A ^ δ 2)) : ℝ) ≤ HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ)
have inr : (↑(#(A * A * A⁻¹)) : ℝ) ≤ HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ)
Tactic: simp [hδ₀, hδ₁, hδ₂]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.SmallTripling (goal)
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 ^ δ 0 * A ^ δ 1 * A ^ δ 2)) : ℝ) ≤ HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ)
have inr : (↑(#(A * A⁻¹ * A)) : ℝ) ≤ HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ)
Tactic: simp [hδ₀, hδ₁, hδ₂]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.SmallTripling (goal)
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 ^ δ 0 * A ^ δ 1 * A ^ δ 2)) : ℝ) ≤ HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ)
have inr : (↑(#(A * A⁻¹ * A⁻¹)) : ℝ) ≤ HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ)
Tactic: simp [hδ₀, hδ₁, hδ₂]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.SmallTripling (goal)
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 ^ δ 0 * A ^ δ 1 * A ^ δ 2)) : ℝ) ≤ HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ)
have inr : (↑(#(A⁻¹ * A * A)) : ℝ) ≤ HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ)
Tactic: simp [hδ₀, hδ₁, hδ₂]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.SmallTripling (goal)
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 ^ δ 0 * A ^ δ 1 * A ^ δ 2)) : ℝ) ≤ HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ)
have inr : (↑(#(A⁻¹ * A * A⁻¹)) : ℝ) ≤ HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ)
Tactic: simp [hδ₀, hδ₁, hδ₂]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.SmallTripling (goal)
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 ^ δ 0 * A ^ δ 1 * A ^ δ 2)) : ℝ) ≤ HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ)
have inr : (↑(#(A⁻¹ * A⁻¹ * A)) : ℝ) ≤ HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ)
Tactic: simp [hδ₀, hδ₁, hδ₂]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.SmallTripling (goal)
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 ^ δ 0 * A ^ δ 1 * A ^ δ 2)) : ℝ) ≤ HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ)
have inr : (↑(#(A⁻¹ * A⁻¹ * A⁻¹)) : ℝ) ≤ HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ)
Tactic: simp [hδ₀, hδ₁, hδ₂]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.SmallTripling (hypothesis)
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)) : ℝ) ≤ HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ)
have hA₁ : (↑(#(A * A * A)) : ℝ) ≤ K * (↑(#A) : ℝ)
Tactic: simp [pow_succ] at hA
Cleared hypotheses: hA
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.SmallTripling (goal)
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) : ℝ)
⊢ (↑(#(A * A * A)) : ℝ) ≤ HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ)
have 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
Tactic: nlinarith
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.SmallTripling (goal)
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⁻¹)) : ℝ) ≤ HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ)
have nlinarith : HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ) < (↑(#(A * A * A⁻¹)) : ℝ) → 1 * HPow.hPow (α := ℝ) (β := ℕ) 1 2 = 1
Tactic: nlinarith [small_pos_pos_neg_mul hA]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.SmallTripling (goal)
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
⊢ (↑(#(A * A * A⁻¹)) : ℝ) ≤ HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ)
have nlinarith₁ : HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ) < (↑(#(A * A * A⁻¹)) : ℝ) → HMul.hMul (α := ℝ) 1 1 = 1
Tactic: nlinarith [small_pos_pos_neg_mul hA]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.SmallTripling (goal)
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
⊢ (↑(#(A * A * A⁻¹)) : ℝ) ≤ HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ)
have nlinarith₂ : HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ) < (↑(#(A * A * A⁻¹)) : ℝ) → 1 * HPow.hPow (α := ℝ) (β := ℕ) 1 3 = 1
Tactic: nlinarith [small_pos_pos_neg_mul hA]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.SmallTripling (goal)
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
⊢ (↑(#(A * A * A⁻¹)) : ℝ) ≤ HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ)
have 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
Tactic: nlinarith [small_pos_pos_neg_mul hA]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.SmallTripling (goal)
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)) : ℝ) ≤ HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ)
have nlinarith : HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ) < (↑(#(A * A⁻¹ * A)) : ℝ) → 1 * HPow.hPow (α := ℝ) (β := ℕ) 1 3 = 1
Tactic: nlinarith [small_pos_neg_pos_mul hA]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.SmallTripling (goal)
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
⊢ (↑(#(A * A⁻¹ * A)) : ℝ) ≤ HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ)
have nlinarith₁ : HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ) < (↑(#(A * A⁻¹ * A)) : ℝ) → HMul.hMul (α := ℝ) 1 1 = 1
Tactic: nlinarith [small_pos_neg_pos_mul hA]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.SmallTripling (goal)
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
⊢ (↑(#(A * A⁻¹ * A)) : ℝ) ≤ HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ)
have 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
Tactic: nlinarith [small_pos_neg_pos_mul hA]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.SmallTripling (goal)
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⁻¹)) : ℝ) ≤ HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ)
have nlinarith : HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ) < (↑(#(A * A⁻¹ * A⁻¹)) : ℝ) → 1 * HPow.hPow (α := ℝ) (β := ℕ) 1 2 = 1
Tactic: nlinarith [small_pos_neg_neg_mul hA]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.SmallTripling (goal)
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
⊢ (↑(#(A * A⁻¹ * A⁻¹)) : ℝ) ≤ HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ)
have nlinarith₁ : HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ) < (↑(#(A * A⁻¹ * A⁻¹)) : ℝ) → HMul.hMul (α := ℝ) 1 1 = 1
Tactic: nlinarith [small_pos_neg_neg_mul hA]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.SmallTripling (goal)
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
⊢ (↑(#(A * A⁻¹ * A⁻¹)) : ℝ) ≤ HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ)
have nlinarith₂ : HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ) < (↑(#(A * A⁻¹ * A⁻¹)) : ℝ) → 1 * HPow.hPow (α := ℝ) (β := ℕ) 1 3 = 1
Tactic: nlinarith [small_pos_neg_neg_mul hA]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.SmallTripling (goal)
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
⊢ (↑(#(A * A⁻¹ * A⁻¹)) : ℝ) ≤ HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ)
have 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
Tactic: nlinarith [small_pos_neg_neg_mul hA]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.SmallTripling (goal)
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)) : ℝ) ≤ HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ)
have nlinarith : HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ) < (↑(#(A⁻¹ * A * A)) : ℝ) → 1 * HPow.hPow (α := ℝ) (β := ℕ) 1 2 = 1
Tactic: nlinarith [small_neg_pos_pos_mul hA]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.SmallTripling (goal)
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
⊢ (↑(#(A⁻¹ * A * A)) : ℝ) ≤ HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ)
have nlinarith₁ : HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ) < (↑(#(A⁻¹ * A * A)) : ℝ) → HMul.hMul (α := ℝ) 1 1 = 1
Tactic: nlinarith [small_neg_pos_pos_mul hA]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.SmallTripling (goal)
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
⊢ (↑(#(A⁻¹ * A * A)) : ℝ) ≤ HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ)
have nlinarith₂ : HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ) < (↑(#(A⁻¹ * A * A)) : ℝ) → 1 * HPow.hPow (α := ℝ) (β := ℕ) 1 3 = 1
Tactic: nlinarith [small_neg_pos_pos_mul hA]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.SmallTripling (goal)
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
⊢ (↑(#(A⁻¹ * A * A)) : ℝ) ≤ HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ)
have 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
Tactic: nlinarith [small_neg_pos_pos_mul hA]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.SmallTripling (goal)
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⁻¹)) : ℝ) ≤ HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ)
have nlinarith : HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ) < (↑(#(A⁻¹ * A * A⁻¹)) : ℝ) → 1 * HPow.hPow (α := ℝ) (β := ℕ) 1 3 = 1
Tactic: nlinarith [small_neg_pos_neg_mul hA]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.SmallTripling (goal)
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
⊢ (↑(#(A⁻¹ * A * A⁻¹)) : ℝ) ≤ HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ)
have nlinarith₁ : HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ) < (↑(#(A⁻¹ * A * A⁻¹)) : ℝ) → HMul.hMul (α := ℝ) 1 1 = 1
Tactic: nlinarith [small_neg_pos_neg_mul hA]