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
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)) ↦ ℤ) ε))
⊢ (↑(#(π (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) : ℝ)

Tactic:
exact ih (Fin.cons 1 <| tail <| tail ε) <| Fin.cons (by simp) (by simp [hε, Fin.tail])

Premises used: Fin.cons, OfNat.ofNat, 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)) ↦ ℤ) ε))
rw : k * (↑(#A) : ℝ) * (k ^ (m - 1) * (↑(#A) : ℝ)) = (↑(#A) : ℝ) * (k ^ (m - 1) * k * (↑(#A) : ℝ))
⊢ k * (↑(#A) : ℝ) * (k ^ (m - 1) * (↑(#A) : ℝ)) = (↑(#A) : ℝ) * (k ^ m * (↑(#A) : ℝ))

Tactic:
rw [← pow_sub_one_mul hm₀]

Premises used: pow_sub_one_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)) ↦ ℤ) ε))
⊢ k * (↑(#A) : ℝ) * (k ^ (m - 1) * (↑(#A) : ℝ)) = (↑(#A) : ℝ) * (k ^ (m - 1) * k * (↑(#A) : ℝ))

Tactic:
ring
-- 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)) ↦ ℤ) ε))
simp : HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#(π ε)) : ℝ) = HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#(V⁻¹ * W)) : ℝ)
simp₁ : HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#(V⁻¹ * W)) : ℝ) ≤ HMul.hMul (α := ℝ) (↑(#(A * V)) : ℝ) (↑(#(A * W)) : ℝ)
simp₂ :
  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)) ↦ ℤ) ε))))) :
        ℝ)
simp₃ :
  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) : ℝ))
simp₄ : k * (↑(#A) : ℝ) * (k ^ (m - 1) * (↑(#A) : ℝ)) = (↑(#A) : ℝ) * (k ^ m * (↑(#A) : ℝ))
⊢ 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) : ℝ))

Tactic:
calc
      (#A * #(π ε) : ℝ)
        = #A * #(V⁻¹ * W) := by
        simp [π, V, W, List.finRange_succ, Fin.tail, Function.comp_def, mul_assoc]
      _ ≤ #(A * V) * #(A * W) := by norm_cast; exact ruzsa_triangle_inequality_invMul_mul_mul ..
      _ = #(π ![1, -ε 1, -ε 0]) * #(π <| Fin.cons 1 <| tail <| tail ε) := by
        simp [π, V, W, List.finRange_succ, Fin.tail, Function.comp_def]
      _ ≤ (k * #A) * (k ^ (m - 1) * #A) := by
        gcongr
        · exact h ![1, -ε 1, -ε 0] fun i ↦ by fin_cases i <;> simp [hε]
        · exact ih (Fin.cons 1 <| tail <| tail ε) <| Fin.cons (by simp) (by simp [hε, Fin.tail])
      _ = #A * (k ^ m * #A) := by rw [← pow_sub_one_mul hm₀]; ring

Premises used: HMul.hMul, HSub.hSub, Fin.cons, Nat.cast, Inv.inv, HPow.hPow, Matrix.vecEmpty, Finset.card, OfNat.ofNat, Fin.tail, 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 : ℕ
hm : 3 ≤ m
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) : ℝ)
ε : Fin m → ℤ
hε : ∀ (i : Fin m), |ε i| = 1
base :
  ∀ (ε : Fin 3 → ℤ) (hε : ∀ (i : Fin 3), |ε i| = 1),
    (↑(card.{u_1} (α := G) (prod (List.map (fun (i : Fin 3) ↦ A ^ ε i) (finRange 3)))) : ℝ) ≤
      k ^ HSub.hSub (α := ℕ) 3 2 * (↑(#A) : ℝ)
succ :
  ∀ (m : ℕ) (hm : 3 ≤ m)
    (ih :
      ∀ (ε : Fin m → ℤ) (hε : ∀ (i : Fin m), |ε i| = 1),
        (↑(card.{u_1} (α := G) (prod (List.map (fun (i : Fin m) ↦ A ^ ε i) (finRange m)))) : ℝ) ≤
          k ^ (m - 2) * (↑(#A) : ℝ))
    (ε : 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) : ℝ)
⊢ (↑(card.{u_1} (α := G) (prod (List.map (fun (i : Fin m) ↦ A ^ ε i) (finRange m)))) : ℝ) ≤ k ^ (m - 2) * (↑(#A) : ℝ)

Tactic:
induction m, hm using Nat.le_induction with
  | base => simpa using h ε hε
  | succ m hm ih =>
    obtain _ | m := m
    · simp at hm
    have hm₀ : m ≠ 0 := by simp at hm; positivity
    have hε₀ i : ε i ≠ 0 := fun h ↦ by simpa [h] using hε i
    obtain rfl | hA := A.eq_empty_or_nonempty
    · simp [hε₀]
    have hk : 0 ≤ k :=
      nonneg_of_mul_nonneg_left ((h 1 (by simp)).trans' (by positivity)) (by positivity)
    let π {n} (δ : Fin n → ℤ) : Finset G := ((finRange _).map fun i ↦ A ^ δ i).prod
    let V : Finset G := π ![-ε 1, -ε 0]
    let W : Finset G := π <| tail <| tail ε
    refine le_of_mul_le_mul_left ?_ (by positivity : (0 : ℝ) < #A)
    calc
      (#A * #(π ε) : ℝ)
        = #A * #(V⁻¹ * W) := by
        simp [π, V, W, List.finRange_succ, Fin.tail, Function.comp_def, mul_assoc]
      _ ≤ #(A * V) * #(A * W) := by norm_cast; exact ruzsa_triangle_inequality_invMul_mul_mul ..
      _ = #(π ![1, -ε 1, -ε 0]) * #(π <| Fin.cons 1 <| tail <| tail ε) := by
        simp [π, V, W, List.finRange_succ, Fin.tail, Function.comp_def]
      _ ≤ (k * #A) * (k ^ (m - 1) * #A) := by
        gcongr
        · exact h ![1, -ε 1, -ε 0] fun i ↦ by fin_cases i <;> simp [hε]
        · exact ih (Fin.cons 1 <| tail <| tail ε) <| Fin.cons (by simp) (by simp [hε, Fin.tail])
      _ = #A * (k ^ m * #A) := by rw [← pow_sub_one_mul hm₀]; ring

Premises used: HMul.hMul, Fin.succ, HSub.hSub, Nat.cast, le_of_mul_le_mul_left, HPow.hPow, Finset.card, OfNat.ofNat, rfl, Finset.eq_empty_or_nonempty
-- 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) : ℝ)
inl :
  ∀ (hA : (↑(#(HPow.hPow (α := Finset G) (β := ℕ) ∅ 3)) : ℝ) ≤ K * (↑(card.{u_1} (α := G) ∅) : ℝ)),
    (↑(#(HMul.hMul (α := Finset G) ∅⁻¹ ∅ * ∅)) : ℝ) ≤ HPow.hPow (β := ℕ) K 2 * (↑(card.{u_1} (α := G) ∅) : ℝ)
inr : ∀ (hA₀ : A.Nonempty), (↑(#(A⁻¹ * A * A)) : ℝ) ≤ HPow.hPow (β := ℕ) K 2 * (↑(#A) : ℝ)
⊢ (↑(#(A⁻¹ * A * A)) : ℝ) ≤ HPow.hPow (β := ℕ) K 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 : ℝ
hA : (↑(#(HPow.hPow (α := Finset G) (β := ℕ) ∅ 3)) : ℝ) ≤ K * (↑(card.{u_1} (α := G) ∅) : ℝ)
⊢ (↑(#(HMul.hMul (α := Finset G) ∅⁻¹ ∅ * ∅)) : ℝ) ≤ HPow.hPow (β := ℕ) K 2 * (↑(card.{u_1} (α := G) ∅) : ℝ)

Tactic:
simp
-- 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
⊢ LE.le (α := ℝ) 0 (↑(#(HPow.hPow (β := ℕ) A 3)) : ℝ)

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

Tactic:
have : 0 ≤ K := nonneg_of_mul_nonneg_left (hA.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 : ℝ
hA : (↑(#(HPow.hPow (β := ℕ) A 3)) : ℝ) ≤ K * (↑(#A) : ℝ)
hA₀ : A.Nonempty
this : 0 ≤ K
⊢ 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 : ℝ
hA : (↑(#(HPow.hPow (β := ℕ) A 3)) : ℝ) ≤ K * (↑(#A) : ℝ)
hA₀ : A.Nonempty
this : 0 ≤ K
inr : HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#(A⁻¹ * A * A)) : ℝ) ≤ (↑(#A) : ℝ) * (HPow.hPow (β := ℕ) K 2 * (↑(#A) : ℝ))
⊢ (↑(#(A⁻¹ * A * A)) : ℝ) ≤ HPow.hPow (β := ℕ) K 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 : ℝ
hA : (↑(#(HPow.hPow (β := ℕ) A 3)) : ℝ) ≤ K * (↑(#A) : ℝ)
hA₀ : A.Nonempty
this : 0 ≤ K
rw rw₁ :
  HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#(A⁻¹ * (A * A))) : ℝ) = HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#(A⁻¹ * (A * A))) : ℝ)
⊢ HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#(A⁻¹ * A * A)) : ℝ) = HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#(A⁻¹ * (A * A))) : ℝ)

Tactic:
rw [mul_assoc]

Premises used: mul_assoc
-- 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
this : 0 ≤ K
norm_cast : #A * #(A⁻¹ * (A * A)) ≤ #(A * A) * #(A * (A * A))
⊢ HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#(A⁻¹ * (A * A))) : ℝ) ≤
    HMul.hMul (α := ℝ) (↑(#(A * A)) : ℝ) (↑(#(A * (A * A))) : ℝ)

Tactic:
norm_cast
-- 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
this : 0 ≤ K
⊢ #A * #(A⁻¹ * (A * A)) ≤ #(A * A) * #(A * (A * A))

Tactic:
ruzsa_triangle_inequality_invMul_mul_mul A A (A * A)

Premises used: Finset.ruzsa_triangle_inequality_invMul_mul_mul, HMul.hMul
-- 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
this : 0 ≤ K
⊢ #A * #(A⁻¹ * (A * A)) ≤ #(A * A) * #(A * (A * A))

Tactic:
exact ruzsa_triangle_inequality_invMul_mul_mul A A (A * A)

Premises used: Finset.ruzsa_triangle_inequality_invMul_mul_mul, HMul.hMul
-- 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
this : 0 ≤ K
⊢ HMul.hMul (α := ℝ) (↑(#(A * A)) : ℝ) (↑(#(A * (A * A))) : ℝ) =
    HMul.hMul (α := ℝ) (↑(#(HPow.hPow (β := ℕ) A 2)) : ℝ) (↑(#(HPow.hPow (β := ℕ) A 3)) : ℝ)

Tactic:
simp [pow_succ']

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

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

Tactic:
hA
-- 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
this : 0 ≤ K
⊢ (↑(#(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
this : 0 ≤ K
⊢ K * (↑(#A) : ℝ) * (K * (↑(#A) : ℝ)) = (↑(#A) : ℝ) * (HPow.hPow (β := ℕ) K 2 * (↑(#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
this : 0 ≤ K
A₁ : HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#(A⁻¹ * A * A)) : ℝ) = HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#(A⁻¹ * (A * A))) : ℝ)
A₂ :
  HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#(A⁻¹ * (A * A))) : ℝ) ≤
    HMul.hMul (α := ℝ) (↑(#(A * A)) : ℝ) (↑(#(A * (A * A))) : ℝ)
A₃ :
  HMul.hMul (α := ℝ) (↑(#(A * A)) : ℝ) (↑(#(A * (A * A))) : ℝ) =
    HMul.hMul (α := ℝ) (↑(#(HPow.hPow (β := ℕ) A 2)) : ℝ) (↑(#(HPow.hPow (β := ℕ) A 3)) : ℝ)
A₄ :
  HMul.hMul (α := ℝ) (↑(#(HPow.hPow (β := ℕ) A 2)) : ℝ) (↑(#(HPow.hPow (β := ℕ) A 3)) : ℝ) ≤
    K * (↑(#A) : ℝ) * (K * (↑(#A) : ℝ))
A₅ : K * (↑(#A) : ℝ) * (K * (↑(#A) : ℝ)) = (↑(#A) : ℝ) * (HPow.hPow (β := ℕ) K 2 * (↑(#A) : ℝ))
⊢ HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#(A⁻¹ * A * A)) : ℝ) ≤ (↑(#A) : ℝ) * (HPow.hPow (β := ℕ) K 2 * (↑(#A) : ℝ))

Tactic:
calc
    (#A * #(A⁻¹ * A * A) : ℝ) = #A * #(A⁻¹ * (A * A)) := by rw [mul_assoc]
    _ ≤ #(A * A) * #(A * (A * A)) := by
      norm_cast; exact ruzsa_triangle_inequality_invMul_mul_mul A A (A * A)
    _ = #(A ^ 2) * #(A ^ 3) := by simp [pow_succ']
    _ ≤ (K * #A) * (K * #A) := by
      gcongr
      calc
        (#(A ^ 2) : ℝ) ≤ #(A ^ 3) := mod_cast hA₀.card_pow_mono (by simp)
        _ ≤ K * #A := hA
    _ = #A * (K ^ 2 * #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 2 * (↑(#A) : ℝ)
⊢ (↑(#(A⁻¹ * A⁻¹ * A)) : ℝ) ≤ HPow.hPow (β := ℕ) K 2 * (↑(#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) : ℝ)
⊢ (↑(#(HPow.hPow (β := ℕ) A 3)) : ℝ) ≤ K * (↑(#A) : ℝ)

Tactic:
simpa
-- 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 2 * (↑(#A) : ℝ)

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

Premises used: mul_assoc, _private.0.Finset.small_neg_pos_pos_mul
-- 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) : ℝ)
⊢ (↑(#(HPow.hPow (β := ℕ) A⁻¹ 3)) : ℝ) ≤ K * (↑(#A⁻¹) : ℝ)

Tactic:
simpa
-- 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 2 * (↑(#A) : ℝ)

Tactic:
simpa using small_neg_pos_pos_mul (A := A⁻¹) (by simpa)

Premises used: _private.0.Finset.small_neg_pos_pos_mul
-- 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 2 * (↑(#A) : ℝ)
⊢ (↑(#(A * A * A⁻¹)) : ℝ) ≤ HPow.hPow (β := ℕ) K 2 * (↑(#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 2 * (↑(#A) : ℝ)

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

Premises used: mul_assoc, _private.0.Finset.small_pos_neg_neg_mul
-- 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) : ℝ)
inl :
  ∀ (hA : (↑(#(HPow.hPow (α := Finset G) (β := ℕ) ∅ 3)) : ℝ) ≤ K * (↑(card.{u_1} (α := G) ∅) : ℝ)),
    (↑(#(HMul.hMul (α := Finset G) ∅ ∅⁻¹ * ∅)) : ℝ) ≤ HPow.hPow (β := ℕ) K 3 * (↑(card.{u_1} (α := G) ∅) : ℝ)
inr : ∀ (hA₀ : A.Nonempty), (↑(#(A * A⁻¹ * A)) : ℝ) ≤ HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ)
⊢ (↑(#(A * A⁻¹ * A)) : ℝ) ≤ HPow.hPow (β := ℕ) K 3 * (↑(#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 : ℝ
hA : (↑(#(HPow.hPow (α := Finset G) (β := ℕ) ∅ 3)) : ℝ) ≤ K * (↑(card.{u_1} (α := G) ∅) : ℝ)
⊢ (↑(#(HMul.hMul (α := Finset G) ∅ ∅⁻¹ * ∅)) : ℝ) ≤ HPow.hPow (β := ℕ) K 3 * (↑(card.{u_1} (α := G) ∅) : ℝ)

Tactic:
simp
-- 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
inr : HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#(A * A⁻¹ * A)) : ℝ) ≤ (↑(#A) : ℝ) * (HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ))
⊢ (↑(#(A * A⁻¹ * A)) : ℝ) ≤ HPow.hPow (β := ℕ) K 3 * (↑(#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 : ℝ
hA : (↑(#(HPow.hPow (β := ℕ) A 3)) : ℝ) ≤ K * (↑(#A) : ℝ)
hA₀ : A.Nonempty
norm_cast : #A * #(A * A⁻¹ * A) ≤ #(A * (A * A⁻¹)) * #(A * A)
⊢ HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#(A * A⁻¹ * A)) : ℝ) ≤
    HMul.hMul (α := ℝ) (↑(#(A * (A * A⁻¹))) : ℝ) (↑(#(A * A)) : ℝ)

Tactic:
norm_cast
-- 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
⊢ #A * #(A * A⁻¹ * A) ≤ #(A * (A * A⁻¹)) * #(A * A)

Tactic:
simpa using ruzsa_triangle_inequality_invMul_mul_mul (A * A⁻¹) A A

Premises used: Finset.ruzsa_triangle_inequality_invMul_mul_mul, HMul.hMul, Inv.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) : ℝ)
hA₀ : A.Nonempty
⊢ HMul.hMul (α := ℝ) (↑(#(A * (A * A⁻¹))) : ℝ) (↑(#(A * A)) : ℝ) =
    HMul.hMul (α := ℝ) (↑(#(A * A * A⁻¹)) : ℝ) (↑(#(HPow.hPow (β := ℕ) A 2)) : ℝ)

Tactic:
simp [pow_succ, mul_assoc]

Premises used: pow_succ, mul_assoc
-- 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
h₁ : (↑(#(A * A * A⁻¹)) : ℝ) ≤ HPow.hPow (β := ℕ) K 2 * (↑(#A) : ℝ)
h₂ : (↑(#(HPow.hPow (β := ℕ) A 2)) : ℝ) ≤ K * (↑(#A) : ℝ)
⊢ HMul.hMul (α := ℝ) (↑(#(A * A * A⁻¹)) : ℝ) (↑(#(HPow.hPow (β := ℕ) A 2)) : ℝ) ≤
    HPow.hPow (β := ℕ) K 2 * (↑(#A) : ℝ) * (K * (↑(#A) : ℝ))

Tactic:
gcongr
-- 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
⊢ (↑(#(A * A * A⁻¹)) : ℝ) ≤ HPow.hPow (β := ℕ) K 2 * (↑(#A) : ℝ)

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

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

Tactic:
hA