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_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)) : ℝ)
⊢ 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) : ℝ))
have 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)) ↦ ℤ) ε))))) :
      ℝ)
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
-- 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_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)) ↦ ℤ) ε))))) :
        ℝ)
⊢ 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) : ℝ))
have 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) : ℝ))
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
-- 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_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) : ℝ))
⊢ 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) : ℝ))
have simp₄ : k * (↑(#A) : ℝ) * (k ^ (m - 1) * (↑(#A) : ℝ)) = (↑(#A) : ℝ) * (k ^ m * (↑(#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
-- 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
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
⊢ (↑(card.{u_1} (α := G) (prod (List.map (fun (i : Fin m) ↦ A ^ ε i) (finRange m)))) : ℝ) ≤ k ^ (m - 2) * (↑(#A) : ℝ)
have 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) : ℝ)
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
Cleared hypotheses: hm, ε, 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
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) : ℝ)
⊢ (↑(card.{u_1} (α := G) (prod (List.map (fun (i : Fin m) ↦ A ^ ε i) (finRange m)))) : ℝ) ≤ k ^ (m - 2) * (↑(#A) : ℝ)
have 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) : ℝ)
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
Cleared hypotheses: hm, ε, 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 : ℝ
hA : (↑(#(HPow.hPow (β := ℕ) A 3)) : ℝ) ≤ K * (↑(#A) : ℝ)
⊢ (↑(#(A⁻¹ * A * A)) : ℝ) ≤ HPow.hPow (β := ℕ) K 2 * (↑(#A) : ℝ)
have inl : ∀ (hA : (↑(#(HPow.hPow (α := Finset G) (β := ℕ) ∅ 3)) : ℝ) ≤ K * (↑(card.{u_1} (α := G) ∅) : ℝ)),
  (↑(#(HMul.hMul (α := Finset G) ∅⁻¹ ∅ * ∅)) : ℝ) ≤ HPow.hPow (β := ℕ) K 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 : ℝ
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) ∅) : ℝ)
⊢ (↑(#(A⁻¹ * A * A)) : ℝ) ≤ HPow.hPow (β := ℕ) K 2 * (↑(#A) : ℝ)
have inr : ∀ (hA₀ : A.Nonempty), (↑(#(A⁻¹ * A * A)) : ℝ) ≤ HPow.hPow (β := ℕ) K 2 * (↑(#A) : ℝ)
Tactic: obtain rfl | hA₀ := A.eq_empty_or_nonempty
-- 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 : ℝ
hA : (↑(#(HPow.hPow (β := ℕ) A 3)) : ℝ) ≤ K * (↑(#A) : ℝ)
hA₀ : A.Nonempty
⊢ (↑(#(A⁻¹ * A * A)) : ℝ) ≤ HPow.hPow (β := ℕ) K 2 * (↑(#A) : ℝ)
have this : 0 ≤ K
Tactic: have : 0 ≤ K := nonneg_of_mul_nonneg_left (hA.trans' <| by positivity) (by positivity)
-- 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
this : 0 ≤ K
⊢ (↑(#(A⁻¹ * A * A)) : ℝ) ≤ HPow.hPow (β := ℕ) K 2 * (↑(#A) : ℝ)
have inr : HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#(A⁻¹ * A * A)) : ℝ) ≤ (↑(#A) : ℝ) * (HPow.hPow (β := ℕ) K 2 * (↑(#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
this : 0 ≤ K
⊢ HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#(A⁻¹ * A * A)) : ℝ) = HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#(A⁻¹ * (A * A))) : ℝ)
have rw : HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#(A⁻¹ * (A * A))) : ℝ) = HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#(A⁻¹ * (A * A))) : ℝ)
Tactic: rw [mul_assoc]
-- 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
this : 0 ≤ K
⊢ 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
this : 0 ≤ K
⊢ HMul.hMul (α := ℝ) (↑(#(HPow.hPow (β := ℕ) A 2)) : ℝ) (↑(#(HPow.hPow (β := ℕ) A 3)) : ℝ) ≤
    K * (↑(#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
this : 0 ≤ K
⊢ HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#(A⁻¹ * A * A)) : ℝ) ≤ (↑(#A) : ℝ) * (HPow.hPow (β := ℕ) K 2 * (↑(#A) : ℝ))
have A₁ : HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#(A⁻¹ * A * A)) : ℝ) = HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#(A⁻¹ * (A * 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
-- 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
this : 0 ≤ K
A₁ : HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#(A⁻¹ * A * A)) : ℝ) = HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#(A⁻¹ * (A * A))) : ℝ)
⊢ HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#(A⁻¹ * A * A)) : ℝ) ≤ (↑(#A) : ℝ) * (HPow.hPow (β := ℕ) K 2 * (↑(#A) : ℝ))
have A₂ : HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#(A⁻¹ * (A * A))) : ℝ) ≤ HMul.hMul (α := ℝ) (↑(#(A * A)) : ℝ) (↑(#(A * (A * 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
-- 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
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))) : ℝ)
⊢ HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#(A⁻¹ * A * A)) : ℝ) ≤ (↑(#A) : ℝ) * (HPow.hPow (β := ℕ) K 2 * (↑(#A) : ℝ))
have A₃ : HMul.hMul (α := ℝ) (↑(#(A * A)) : ℝ) (↑(#(A * (A * A))) : ℝ) =
  HMul.hMul (α := ℝ) (↑(#(HPow.hPow (β := ℕ) A 2)) : ℝ) (↑(#(HPow.hPow (β := ℕ) A 3)) : ℝ)
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
-- 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
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)) : ℝ)
⊢ HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#(A⁻¹ * A * A)) : ℝ) ≤ (↑(#A) : ℝ) * (HPow.hPow (β := ℕ) K 2 * (↑(#A) : ℝ))
have A₄ : HMul.hMul (α := ℝ) (↑(#(HPow.hPow (β := ℕ) A 2)) : ℝ) (↑(#(HPow.hPow (β := ℕ) A 3)) : ℝ) ≤
  K * (↑(#A) : ℝ) * (K * (↑(#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
-- 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
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) : ℝ))
⊢ HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#(A⁻¹ * A * A)) : ℝ) ≤ (↑(#A) : ℝ) * (HPow.hPow (β := ℕ) K 2 * (↑(#A) : ℝ))
have A₅ : K * (↑(#A) : ℝ) * (K * (↑(#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
-- 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 2 * (↑(#A) : ℝ)
have rw : (↑(#(A⁻¹ * A⁻¹ * A)⁻¹) : ℝ) ≤ HPow.hPow (β := ℕ) K 2 * (↑(#A) : ℝ)
Tactic: rw [← card_inv]
-- 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 2 * (↑(#A) : ℝ)
have rw : (↑(#(A * A * A⁻¹)⁻¹) : ℝ) ≤ HPow.hPow (β := ℕ) K 2 * (↑(#A) : ℝ)
Tactic: rw [← card_inv]
-- 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 inl : ∀ (hA : (↑(#(HPow.hPow (α := Finset G) (β := ℕ) ∅ 3)) : ℝ) ≤ K * (↑(card.{u_1} (α := G) ∅) : ℝ)),
  (↑(#(HMul.hMul (α := Finset G) ∅ ∅⁻¹ * ∅)) : ℝ) ≤ HPow.hPow (β := ℕ) K 3 * (↑(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 : ℝ
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) ∅) : ℝ)
⊢ (↑(#(A * A⁻¹ * A)) : ℝ) ≤ HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ)
have inr : ∀ (hA₀ : A.Nonempty), (↑(#(A * A⁻¹ * A)) : ℝ) ≤ HPow.hPow (β := ℕ) K 3 * (↑(#A) : ℝ)
Tactic: obtain rfl | hA₀ := A.eq_empty_or_nonempty