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 : ℝ
hA : (↑(#(HPow.hPow (β := ℕ) A 3)) : ℝ) ≤ K * (↑(#A) : ℝ)
hA₀ : A.Nonempty
⊢ (↑(#(A * A⁻¹ * A)) : ℝ) ≤ HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ)
have inr : HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#(A * A⁻¹ * A)) : ℝ) ≤ (↑(#A) : ℝ) * (HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ))
Tactic: refine le_of_mul_le_mul_left ?_ (by positivity : (0 : ℝ) < #A)
-- 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 : ℝ
hA : (↑(#(HPow.hPow (β := ℕ) A 3)) : ℝ) ≤ K * (↑(#A) : ℝ)
hA₀ : A.Nonempty
⊢ HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#(A * A⁻¹ * A)) : ℝ) ≤
    HMul.hMul (α := ℝ) (↑(#(A * (A * A⁻¹))) : ℝ) (↑(#(A * A)) : ℝ)
have norm_cast : #A * #(A * A⁻¹ * A) ≤ #(A * (A * A⁻¹)) * #(A * A)
Tactic: norm_cast
-- 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 : ℝ
hA : (↑(#(HPow.hPow (β := ℕ) A 3)) : ℝ) ≤ K * (↑(#A) : ℝ)
hA₀ : A.Nonempty
⊢ HMul.hMul (α := ℝ) (↑(#(A * A * A⁻¹)) : ℝ) (↑(#(HPow.hPow (β := ℕ) A 2)) : ℝ) ≤
    HPow.hPow (β := ℕ) K 2 * (↑(#A) : ℝ) * (K * (↑(#A) : ℝ))
have h₁ : (↑(#(A * A * A⁻¹)) : ℝ) ≤ HPow.hPow (β := ℕ) K 2 * (↑(#A) : ℝ)
Tactic: gcongr
-- 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 : ℝ
hA : (↑(#(HPow.hPow (β := ℕ) A 3)) : ℝ) ≤ K * (↑(#A) : ℝ)
hA₀ : A.Nonempty
h₁ : (↑(#(A * A * A⁻¹)) : ℝ) ≤ HPow.hPow (β := ℕ) K 2 * (↑(#A) : ℝ)
⊢ HMul.hMul (α := ℝ) (↑(#(A * A * A⁻¹)) : ℝ) (↑(#(HPow.hPow (β := ℕ) A 2)) : ℝ) ≤
    HPow.hPow (β := ℕ) K 2 * (↑(#A) : ℝ) * (K * (↑(#A) : ℝ))
have h₂ : (↑(#(HPow.hPow (β := ℕ) A 2)) : ℝ) ≤ K * (↑(#A) : ℝ)
Tactic: gcongr
-- 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 : ℝ
hA : (↑(#(HPow.hPow (β := ℕ) A 3)) : ℝ) ≤ K * (↑(#A) : ℝ)
hA₀ : A.Nonempty
⊢ HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#(A * A⁻¹ * A)) : ℝ) ≤ (↑(#A) : ℝ) * (HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ))
have simpa : HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#(A * A⁻¹ * A)) : ℝ) ≤ HMul.hMul (α := ℝ) (↑(#(A * (A * A⁻¹))) : ℝ) (↑(#(A * 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
-- 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 : ℝ
hA : (↑(#(HPow.hPow (β := ℕ) A 3)) : ℝ) ≤ K * (↑(#A) : ℝ)
hA₀ : A.Nonempty
simpa :
  HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#(A * A⁻¹ * A)) : ℝ) ≤
    HMul.hMul (α := ℝ) (↑(#(A * (A * A⁻¹))) : ℝ) (↑(#(A * A)) : ℝ)
⊢ HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#(A * A⁻¹ * A)) : ℝ) ≤ (↑(#A) : ℝ) * (HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ))
have simpa₁ : HMul.hMul (α := ℝ) (↑(#(A * (A * A⁻¹))) : ℝ) (↑(#(A * A)) : ℝ) =
  HMul.hMul (α := ℝ) (↑(#(A * A * A⁻¹)) : ℝ) (↑(#(HPow.hPow (β := ℕ) A 2)) : ℝ)
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
-- 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 : ℝ
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)) : ℝ)
⊢ HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#(A * A⁻¹ * A)) : ℝ) ≤ (↑(#A) : ℝ) * (HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ))
have simpa₂ : HMul.hMul (α := ℝ) (↑(#(A * A * A⁻¹)) : ℝ) (↑(#(HPow.hPow (β := ℕ) A 2)) : ℝ) ≤
  HPow.hPow (β := ℕ) K 2 * (↑(#A) : ℝ) * (K * (↑(#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
-- 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 : ℝ
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) : ℝ))
⊢ HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#(A * A⁻¹ * A)) : ℝ) ≤ (↑(#A) : ℝ) * (HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ))
have simpa₃ : HPow.hPow (β := ℕ) K 2 * (↑(#A) : ℝ) * (K * (↑(#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
-- 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 : ℝ
hA : (↑(#(HPow.hPow (β := ℕ) A 3)) : ℝ) ≤ K * (↑(#A) : ℝ)
⊢ (↑(#(A⁻¹ * A * A⁻¹)) : ℝ) ≤ HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ)
have rw : (↑(#(A⁻¹ * A * A⁻¹)⁻¹) : ℝ) ≤ HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ)
Tactic: rw [← card_inv]
-- 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
⊢ (↑(card.{u_1} (α := G) (prod (List.map (fun (i : Fin m) ↦ A ^ ε i) (finRange m)))) : ℝ) ≤
    K ^ (3 * (m - 2)) * (↑(#A) : ℝ)
have hm₀ : m ≠ 0
Tactic: have hm₀ : m ≠ 0 := by positivity
-- 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
⊢ (↑(card.{u_1} (α := G) (prod (List.map (fun (i : Fin m) ↦ A ^ ε i) (finRange m)))) : ℝ) ≤
    K ^ (3 * (m - 2)) * (↑(#A) : ℝ)
have hε₀ : ∀ (i : Fin m), ε i ≠ 0
Tactic: have hε₀ i : ε i ≠ 0 := fun h ↦ by simpa [h] using hε i
-- 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
⊢ (↑(card.{u_1} (α := G) (prod (List.map (fun (i : Fin m) ↦ A ^ ε i) (finRange m)))) : ℝ) ≤
    K ^ (3 * (m - 2)) * (↑(#A) : ℝ)
have 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) ∅) : ℝ)
Tactic: obtain rfl | hA₀ := A.eq_empty_or_nonempty
Cleared hypotheses: A, 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
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) ∅) : ℝ)
⊢ (↑(card.{u_1} (α := G) (prod (List.map (fun (i : Fin m) ↦ A ^ ε i) (finRange m)))) : ℝ) ≤
    K ^ (3 * (m - 2)) * (↑(#A) : ℝ)
have inr : ∀ (hA₀ : A.Nonempty),
  (↑(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
-- 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
⊢ LE.le (α := ℝ) (↑(#A) : ℝ) (↑(#(HPow.hPow (β := ℕ) A 3)) : ℝ)
have norm_cast : #A ≤ #(HPow.hPow (β := ℕ) A 3)
Tactic: norm_cast
-- 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
⊢ (↑(card.{u_1} (α := G) (prod (List.map (fun (i : Fin m) ↦ A ^ ε i) (finRange m)))) : ℝ) ≤
    K ^ (3 * (m - 2)) * (↑(#A) : ℝ)
have hK₁ : 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))
-- 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
⊢ (↑(card.{u_1} (α := G) (prod (List.map (fun (i : Fin m) ↦ A ^ ε i) (finRange m)))) : ℝ) ≤
    K ^ (3 * (m - 2)) * (↑(#A) : ℝ)
have inr : (↑(card.{u_1} (α := G) (prod (List.map (fun (i : Fin m) ↦ A ^ ε i) (finRange m)))) : ℝ) ≤
  HPow.hPow (β := ℕ) K 3 ^ (m - 2) * (↑(#A) : ℝ)
Tactic: rw [pow_mul]
-- 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
⊢ (↑(card.{u_1} (α := G) (prod (List.map (fun (i : Fin m) ↦ A ^ ε i) (finRange m)))) : ℝ) ≤
    HPow.hPow (β := ℕ) K 3 ^ (m - 2) * (↑(#A) : ℝ)
have 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) : ℝ)
Tactic: refine inductive_claim_mul hm (fun δ 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 → ℤ
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) : ℝ)
have inr : (↑(#(A ^ δ 0 * A ^ δ 1 * A ^ δ 2)) : ℝ) ≤ 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]
-- 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 → ℤ
hδ : ∀ (i : Fin 3), |δ i| = 1
⊢ (↑(#(A ^ δ 0 * A ^ δ 1 * A ^ δ 2)) : ℝ) ≤ HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ)
have hδ₁ : (δ 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δ
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 → ℤ
hδ : (δ 0 = 1 ∨ δ 0 = -1) ∧ (δ 1 = 1 ∨ δ 1 = -1) ∧ (δ 2 = 1 ∨ δ 2 = -1)
⊢ HPow.hPow (β := ℕ) K 2 ≤ HPow.hPow (β := ℕ) K 3
have hmn : LE.le (α := ℕ) 2 3
Tactic: gcongr
-- 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 → ℤ
hδ : (δ 0 = 1 ∨ δ 0 = -1) ∧ (δ 1 = 1 ∨ δ 1 = -1) ∧ (δ 2 = 1 ∨ δ 2 = -1)
⊢ (↑(#(A ^ δ 0 * A ^ δ 1 * A ^ δ 2)) : ℝ) ≤ HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ)
have this : HPow.hPow (β := ℕ) K 2 ≤ HPow.hPow (β := ℕ) K 3
Tactic: have : K ^ 2 ≤ K ^ 3 := by gcongr; simp
-- 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
⊢ (↑(#(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 → ℤ
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) : ℝ)
⊢ (↑(#(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 → ℤ
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) : ℝ)
⊢ (↑(#(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 → ℤ
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) : ℝ)
⊢ (↑(#(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 → ℤ
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) : ℝ)
⊢ (↑(#(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 → ℤ
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) : ℝ)
⊢ (↑(#(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 → ℤ
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) : ℝ)
⊢ (↑(#(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δ