-- Mathlib/Combinatorics/Additive/SmallTripling.lean
@[to_additive]
private lemma inductive_claim_mul (hm : 3 ≤ m)
    (h : ∀ ε : Fin 3 → ℤ, (∀ i, |ε i| = 1) → #((finRange 3).map fun i ↦ A ^ ε i).prod ≤ k * #A)
    (ε : Fin m → ℤ) (hε : ∀ i, |ε i| = 1) :
    #((finRange m).map fun i ↦ A ^ ε i).prod ≤ k ^ (m - 2) * #A

Proof state:
case succ
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
k : ℝ
m✝ : ℕ
h : ∀ (ε : Fin 3 → ℤ), (∀ (i : Fin 3), |ε i| = 1) → ↑(#(List.map (fun i => A ^ ε i) (finRange 3)).prod) ≤ k * ↑(#A)
m : ℕ
hm : 3 ≤ m
ih :
  ∀ (ε : Fin m → ℤ),
    (∀ (i : Fin m), |ε i| = 1) → ↑(#(List.map (fun i => A ^ ε i) (finRange m)).prod) ≤ k ^ (m - 2) * ↑(#A)
ε : Fin (m + 1) → ℤ
hε : ∀ (i : Fin (m + 1)), |ε i| = 1
⊢ ↑(#(List.map (fun i => A ^ ε i) (finRange (m + 1))).prod) ≤ k ^ (m + 1 - 2) * ↑(#A)

Tactic:
obtain _ | m := m

Result:
case succ.zero
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
k : ℝ
m : ℕ
h : ∀ (ε : Fin 3 → ℤ), (∀ (i : Fin 3), |ε i| = 1) → ↑(#(List.map (fun i => A ^ ε i) (finRange 3)).prod) ≤ k * ↑(#A)
hm : 3 ≤ 0
ih :
  ∀ (ε : Fin 0 → ℤ),
    (∀ (i : Fin 0), |ε i| = 1) → ↑(#(List.map (fun i => A ^ ε i) (finRange 0)).prod) ≤ k ^ (0 - 2) * ↑(#A)
ε : Fin (0 + 1) → ℤ
hε : ∀ (i : Fin (0 + 1)), |ε i| = 1
⊢ ↑(#(List.map (fun i => A ^ ε i) (finRange (0 + 1))).prod) ≤ k ^ (0 + 1 - 2) * ↑(#A)

case succ.succ
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
k : ℝ
m✝ : ℕ
h : ∀ (ε : Fin 3 → ℤ), (∀ (i : Fin 3), |ε i| = 1) → ↑(#(List.map (fun i => A ^ ε i) (finRange 3)).prod) ≤ k * ↑(#A)
m : ℕ
hm : 3 ≤ m + 1
ih :
  ∀ (ε : Fin (m + 1) → ℤ),
    (∀ (i : Fin (m + 1)), |ε i| = 1) →
      ↑(#(List.map (fun i => A ^ ε i) (finRange (m + 1))).prod) ≤ k ^ (m + 1 - 2) * ↑(#A)
ε : Fin (m + 1 + 1) → ℤ
hε : ∀ (i : Fin (m + 1 + 1)), |ε i| = 1
⊢ ↑(#(List.map (fun i => A ^ ε i) (finRange (m + 1 + 1))).prod) ≤ k ^ (m + 1 + 1 - 2) * ↑(#A)

Proof state:
case base
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
k : ℝ
m : ℕ
h : ∀ (ε : Fin 3 → ℤ), (∀ (i : Fin 3), |ε i| = 1) → ↑(#(List.map (fun i => A ^ ε i) (finRange 3)).prod) ≤ k * ↑(#A)
ε : Fin 3 → ℤ
hε : ∀ (i : Fin 3), |ε i| = 1
⊢ ↑(#(List.map (fun i => A ^ ε i) (finRange 3)).prod) ≤ k ^ (3 - 2) * ↑(#A)

Tactic:
simpa using h ε hε

Result:
no goals

Proof state:
case succ.zero
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
k : ℝ
m : ℕ
h : ∀ (ε : Fin 3 → ℤ), (∀ (i : Fin 3), |ε i| = 1) → ↑(#(List.map (fun i => A ^ ε i) (finRange 3)).prod) ≤ k * ↑(#A)
hm : 3 ≤ 0
ih :
  ∀ (ε : Fin 0 → ℤ),
    (∀ (i : Fin 0), |ε i| = 1) → ↑(#(List.map (fun i => A ^ ε i) (finRange 0)).prod) ≤ k ^ (0 - 2) * ↑(#A)
ε : Fin (0 + 1) → ℤ
hε : ∀ (i : Fin (0 + 1)), |ε i| = 1
⊢ ↑(#(List.map (fun i => A ^ ε i) (finRange (0 + 1))).prod) ≤ k ^ (0 + 1 - 2) * ↑(#A)

Tactic:
simp at hm

Result:
no goals

Proof state:
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
k : ℝ
m✝ : ℕ
h : ∀ (ε : Fin 3 → ℤ), (∀ (i : Fin 3), |ε i| = 1) → ↑(#(List.map (fun i => A ^ ε i) (finRange 3)).prod) ≤ k * ↑(#A)
m : ℕ
hm : 3 ≤ m + 1
ih :
  ∀ (ε : Fin (m + 1) → ℤ),
    (∀ (i : Fin (m + 1)), |ε i| = 1) →
      ↑(#(List.map (fun i => A ^ ε i) (finRange (m + 1))).prod) ≤ 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} δ => (List.map (fun i => A ^ δ i) (finRange n)).prod
V : Finset G := π ![-ε 1, -ε 0]
W : Finset G := π (tail (tail ε))
⊢ k * ↑(#A) * (k ^ (m - 1) * ↑(#A)) = ↑(#A) * (k ^ (m - 1) * k * ↑(#A))

Tactic:
ring

Result:
no goals