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
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) : ℝ)
have succ : ∀ (hm : LE.le (α := ℕ) 3 0)
  (ih :
    ∀ (ε : Fin 0 → ℤ) (hε : ∀ (i : Fin 0), |ε i| = 1),
      (↑(card.{u_1} (α := G) (prod (List.map (fun (i : Fin 0) ↦ A ^ ε i) (finRange 0)))) : ℝ) ≤
        k ^ HSub.hSub (α := ℕ) 0 2 * (↑(#A) : ℝ))
  (ε : Fin (HAdd.hAdd (α := ℕ) 0 1) → ℤ) (hε : ∀ (i : Fin (HAdd.hAdd (α := ℕ) 0 1)), |ε i| = 1),
  (↑(card.{u_1} (α := G)
          (prod (List.map (fun (i : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ A ^ ε i) (finRange (HAdd.hAdd (α := ℕ) 0 1))))) :
      ℝ) ≤
    k ^ (HAdd.hAdd (α := ℕ) 0 1 - 2) * (↑(#A) : ℝ)
Tactic: obtain _ | m := m
Cleared hypotheses: m, hm, ih, ε, 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_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
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
succ :
  ∀ (hm : LE.le (α := ℕ) 3 0)
    (ih :
      ∀ (ε : Fin 0 → ℤ) (hε : ∀ (i : Fin 0), |ε i| = 1),
        (↑(card.{u_1} (α := G) (prod (List.map (fun (i : Fin 0) ↦ A ^ ε i) (finRange 0)))) : ℝ) ≤
          k ^ HSub.hSub (α := ℕ) 0 2 * (↑(#A) : ℝ))
    (ε : Fin (HAdd.hAdd (α := ℕ) 0 1) → ℤ) (hε : ∀ (i : Fin (HAdd.hAdd (α := ℕ) 0 1)), |ε i| = 1),
    (↑(card.{u_1} (α := G)
            (prod (List.map (fun (i : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ A ^ ε i) (finRange (HAdd.hAdd (α := ℕ) 0 1))))) :
        ℝ) ≤
      k ^ (HAdd.hAdd (α := ℕ) 0 1 - 2) * (↑(#A) : ℝ)
⊢ (↑(card.{u_1} (α := G) (prod (List.map (fun (i : Fin (m + 1)) ↦ A ^ ε i) (finRange (m + 1))))) : ℝ) ≤
    k ^ (m + 1 - 2) * (↑(#A) : ℝ)
have succ₁ : ∀ (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),
  (↑(card.{u_1} (α := G) (prod (List.map (fun (i : Fin (m + 1 + 1)) ↦ A ^ ε i) (finRange (m + 1 + 1))))) : ℝ) ≤
    k ^ (m + 1 + 1 - 2) * (↑(#A) : ℝ)
Tactic: obtain _ | m := m
Cleared hypotheses: m, hm, ih, ε, 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_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
⊢ m ≠ 0
have hm₁ : 2 ≤ m
Tactic: simp at hm
Cleared hypotheses: hm
-- 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_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
⊢ (↑(card.{u_1} (α := G) (prod (List.map (fun (i : Fin (m + 1 + 1)) ↦ A ^ ε i) (finRange (m + 1 + 1))))) : ℝ) ≤
    k ^ (m + 1 + 1 - 2) * (↑(#A) : ℝ)
have hm₀ : m ≠ 0
Tactic: have hm₀ : m ≠ 0 := by simp at hm; 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_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
⊢ (↑(card.{u_1} (α := G) (prod (List.map (fun (i : Fin (m + 1 + 1)) ↦ A ^ ε i) (finRange (m + 1 + 1))))) : ℝ) ≤
    k ^ (m + 1 + 1 - 2) * (↑(#A) : ℝ)
have hε₀ : ∀ (i : Fin (m + 1 + 1)), ε 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_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
⊢ (↑(card.{u_1} (α := G) (prod (List.map (fun (i : Fin (m + 1 + 1)) ↦ A ^ ε i) (finRange (m + 1 + 1))))) : ℝ) ≤
    k ^ (m + 1 + 1 - 2) * (↑(#A) : ℝ)
have succ : ∀
  (h :
    ∀ (ε : Fin 3 → ℤ),
      (∀ (i : Fin 3), |ε i| = 1) →
        (↑(card.{u_1} (α := G) (prod (List.map (fun (i : Fin 3) ↦ HPow.hPow (α := Finset G) ∅ (ε i)) (finRange 3)))) :
            ℝ) ≤
          k * (↑(card.{u_1} (α := G) ∅) : ℝ))
  (ih :
    ∀ (ε : Fin (m + 1) → ℤ) (hε : ∀ (i : Fin (m + 1)), |ε i| = 1),
      (↑(card.{u_1} (α := G)
              (prod (List.map (fun (i : Fin (m + 1)) ↦ HPow.hPow (α := Finset G) ∅ (ε i)) (finRange (m + 1))))) :
          ℝ) ≤
        k ^ (m + 1 - 2) * (↑(card.{u_1} (α := G) ∅) : ℝ)),
  (↑(card.{u_1} (α := G)
          (prod (List.map (fun (i : Fin (m + 1 + 1)) ↦ HPow.hPow (α := Finset G) ∅ (ε i)) (finRange (m + 1 + 1))))) :
      ℝ) ≤
    k ^ (m + 1 + 1 - 2) * (↑(card.{u_1} (α := G) ∅) : ℝ)
Tactic: obtain rfl | hA := A.eq_empty_or_nonempty
Cleared hypotheses: A, h, ih
-- 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
succ :
  ∀
    (h :
      ∀ (ε : Fin 3 → ℤ),
        (∀ (i : Fin 3), |ε i| = 1) →
          (↑(card.{u_1} (α := G) (prod (List.map (fun (i : Fin 3) ↦ HPow.hPow (α := Finset G) ∅ (ε i)) (finRange 3)))) :
              ℝ) ≤
            k * (↑(card.{u_1} (α := G) ∅) : ℝ))
    (ih :
      ∀ (ε : Fin (m + 1) → ℤ) (hε : ∀ (i : Fin (m + 1)), |ε i| = 1),
        (↑(card.{u_1} (α := G)
                (prod (List.map (fun (i : Fin (m + 1)) ↦ HPow.hPow (α := Finset G) ∅ (ε i)) (finRange (m + 1))))) :
            ℝ) ≤
          k ^ (m + 1 - 2) * (↑(card.{u_1} (α := G) ∅) : ℝ)),
    (↑(card.{u_1} (α := G)
            (prod (List.map (fun (i : Fin (m + 1 + 1)) ↦ HPow.hPow (α := Finset G) ∅ (ε i)) (finRange (m + 1 + 1))))) :
        ℝ) ≤
      k ^ (m + 1 + 1 - 2) * (↑(card.{u_1} (α := G) ∅) : ℝ)
⊢ (↑(card.{u_1} (α := G) (prod (List.map (fun (i : Fin (m + 1 + 1)) ↦ A ^ ε i) (finRange (m + 1 + 1))))) : ℝ) ≤
    k ^ (m + 1 + 1 - 2) * (↑(#A) : ℝ)
have succ₁ : ∀ (hA : A.Nonempty),
  (↑(card.{u_1} (α := G) (prod (List.map (fun (i : Fin (m + 1 + 1)) ↦ A ^ ε i) (finRange (m + 1 + 1))))) : ℝ) ≤
    k ^ (m + 1 + 1 - 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 : ℝ
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
⊢ (↑(card.{u_1} (α := G) (prod (List.map (fun (i : Fin (m + 1 + 1)) ↦ A ^ ε i) (finRange (m + 1 + 1))))) : ℝ) ≤
    k ^ (m + 1 + 1 - 2) * (↑(#A) : ℝ)
have hk : 0 ≤ k
Tactic: have hk : 0 ≤ k :=
      nonneg_of_mul_nonneg_left ((h 1 (by simp)).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 : ℝ
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)) ↦ ℤ) ε))
⊢ (↑(card.{u_1} (α := G) (prod (List.map (fun (i : Fin (m + 1 + 1)) ↦ A ^ ε i) (finRange (m + 1 + 1))))) : ℝ) ≤
    k ^ (m + 1 + 1 - 2) * (↑(#A) : ℝ)
have succ : 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: 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 : ℝ
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)) ↦ ℤ) ε))
⊢ 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) : ℝ))
have h₁ : (↑(#(π ![1, -ε 1, -ε 0])) : ℝ) ≤ 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 : ℝ
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)) ↦ ℤ) ε))
h₁ : (↑(#(π ![1, -ε 1, -ε 0])) : ℝ) ≤ k * (↑(#A) : ℝ)
⊢ 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) : ℝ))
have h₂ : (↑(#(π (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: 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 : ℝ
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)) ↦ ℤ) ε))
i : Fin 3
⊢ |![1, -ε 1, -ε 0] i| = 1
have 0 : |![1, -ε 1, -ε 0] ((fun (i : Fin 3) ↦ i) (⟨0, sorry⟩ : Fin 3))| = 1
Tactic: fin_cases i
Cleared hypotheses: 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_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)) ↦ ℤ) ε))
i : Fin 3
0 : |![1, -ε 1, -ε 0] ((fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3))| = 1
⊢ |![1, -ε 1, -ε 0] i| = 1
have 1 : |![1, -ε 1, -ε 0] ((fun (i : Fin 3) ↦ i) (⟨1, sorry⟩ : Fin 3))| = 1
Tactic: fin_cases i
Cleared hypotheses: 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_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)) ↦ ℤ) ε))
i : Fin 3
0 : |![1, -ε 1, -ε 0] ((fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3))| = 1
1 : |![1, -ε 1, -ε 0] ((fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3))| = 1
⊢ |![1, -ε 1, -ε 0] i| = 1
have 2 : |![1, -ε 1, -ε 0] ((fun (i : Fin 3) ↦ i) (⟨2, sorry⟩ : Fin 3))| = 1
Tactic: fin_cases i
Cleared hypotheses: 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_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 * (↑(#A) : ℝ))
have rw : k * (↑(#A) : ℝ) * (k ^ (m - 1) * (↑(#A) : ℝ)) = (↑(#A) : ℝ) * (k ^ (m - 1) * k * (↑(#A) : ℝ))
Tactic: rw [← pow_sub_one_mul hm₀]
-- 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)) ↦ ℤ) ε))
⊢ 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) : ℝ) (↑(#(π ε)) : ℝ) = HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#(V⁻¹ * W)) : ℝ)
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)) : ℝ)
⊢ 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⁻¹ * W)) : ℝ) ≤ HMul.hMul (α := ℝ) (↑(#(A * V)) : ℝ) (↑(#(A * W)) : ℝ)
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