-- Mathlib/Combinatorics/Additive/ApproximateSubgroup.lean
@[to_additive]
lemma card_pow_le [DecidableEq G] {A : Finset G} (hA : IsApproximateSubgroup K (A : Set G)) :
    ∀ {n}, #(A ^ n) ≤ K ^ (n - 1) * #A
  | 0 => by simpa using hA.nonempty
  | 1 => by simp
  | n + 2 => by
    obtain ⟨F, hF, hSF⟩ := hA.sq_covBySMul
    calc
      (#(A ^ (n + 2)) : ℝ) ≤ #(F ^ (n + 1) * A)

Proof state:
case intro.intro
G : Type u_1
inst✝¹ : Group G
K : ℝ
inst✝ : DecidableEq G
A : Finset G
hA : IsApproximateSubgroup K ↑A
n : ℕ
F : Finset G
hF : ↑(#F) ≤ K
hSF : ↑A ^ 2 ⊆ ↑F • ↑A
⊢ ↑(#(A ^ (n + 2))) ≤ K ^ (n + 2 - 1) * ↑(#A)

Tactic:
calc
  (#(A ^ (n + 2)) : ℝ) ≤ #(F ^ (n + 1) * A) := by
    gcongr; exact mod_cast Set.pow_subset_pow_mul_of_sq_subset_mul hSF (by omega)
  _ ≤ #(F ^ (n + 1)) * #A := mod_cast Finset.card_mul_le
  _ ≤ #F ^ (n + 1) * #A := by gcongr; exact mod_cast Finset.card_pow_le
  _ ≤ K ^ (n + 1) * #A := by gcongr

Result:
no goals

Proof state:
G : Type u_1
inst✝¹ : Group G
K : ℝ
inst✝ : DecidableEq G
A : Finset G
hA : IsApproximateSubgroup K ↑A
n : ℕ
F : Finset G
hF : ↑(#F) ≤ K
hSF : ↑A ^ 2 ⊆ ↑F • ↑A
⊢ ↑(#(F ^ (n + 1))) * ↑(#A) ≤ ↑(#F) ^ (n + 1) * ↑(#A)

Tactic:
gcongr

Result:
case h
G : Type u_1
inst✝¹ : Group G
K : ℝ
inst✝ : DecidableEq G
A : Finset G
hA : IsApproximateSubgroup K ↑A
n : ℕ
F : Finset G
hF : ↑(#F) ≤ K
hSF : ↑A ^ 2 ⊆ ↑F • ↑A
⊢ ↑(#(F ^ (n + 1))) ≤ ↑(#F) ^ (n + 1)

Proof state:
G : Type u_1
inst✝¹ : Group G
K : ℝ
inst✝ : DecidableEq G
A : Finset G
hA : IsApproximateSubgroup K ↑A
n : ℕ
⊢ ↑(#(A ^ (n + 2))) ≤ K ^ (n + 2 - 1) * ↑(#A)

Tactic:
obtain ⟨F, hF, hSF⟩ := hA.sq_covBySMul

Result:
case intro.intro
G : Type u_1
inst✝¹ : Group G
K : ℝ
inst✝ : DecidableEq G
A : Finset G
hA : IsApproximateSubgroup K ↑A
n : ℕ
F : Finset G
hF : ↑(#F) ≤ K
hSF : ↑A ^ 2 ⊆ ↑F • ↑A
⊢ ↑(#(A ^ (n + 2))) ≤ K ^ (n + 2 - 1) * ↑(#A)

Proof state:
G : Type u_1
inst✝¹ : Group G
K : ℝ
inst✝ : DecidableEq G
A : Finset G
hA : IsApproximateSubgroup K ↑A
n : ℕ
F : Finset G
hF : ↑(#F) ≤ K
hSF : ↑A ^ 2 ⊆ ↑F • ↑A
⊢ n + 2 ≠ 0

Tactic:
omega

Result:
no goals

Proof state:
case h.a
G : Type u_1
inst✝¹ : Group G
K : ℝ
inst✝ : DecidableEq G
A : Finset G
hA : IsApproximateSubgroup K ↑A
n : ℕ
F : Finset G
hF : ↑(#F) ≤ K
hSF : ↑A ^ 2 ⊆ ↑F • ↑A
⊢ A ^ (n + 2) ⊆ F ^ (n + 1) * A

Tactic:
exact mod_cast Set.pow_subset_pow_mul_of_sq_subset_mul hSF (by omega)

Result:
no goals

Proof state:
G : Type u_1
inst✝¹ : Group G
K : ℝ
inst✝ : DecidableEq G
A : Finset G
hA : IsApproximateSubgroup K ↑A
⊢ ↑(#(A ^ 1)) ≤ K ^ (1 - 1) * ↑(#A)

Tactic:
simp

Result:
no goals

Proof state:
case h
G : Type u_1
inst✝¹ : Group G
K : ℝ
inst✝ : DecidableEq G
A : Finset G
hA : IsApproximateSubgroup K ↑A
n : ℕ
F : Finset G
hF : ↑(#F) ≤ K
hSF : ↑A ^ 2 ⊆ ↑F • ↑A
⊢ ↑(#(F ^ (n + 1))) ≤ ↑(#F) ^ (n + 1)

Tactic:
exact mod_cast Finset.card_pow_le

Result:
no goals

Proof state:
G : Type u_1
inst✝¹ : Group G
K : ℝ
inst✝ : DecidableEq G
A : Finset G
hA : IsApproximateSubgroup K ↑A
⊢ ↑(#(A ^ 0)) ≤ K ^ (0 - 1) * ↑(#A)

Tactic:
simpa using hA.nonempty

Result:
no goals

Proof state:
G : Type u_1
inst✝¹ : Group G
K : ℝ
inst✝ : DecidableEq G
A : Finset G
hA : IsApproximateSubgroup K ↑A
n : ℕ
F : Finset G
hF : ↑(#F) ≤ K
hSF : ↑A ^ 2 ⊆ ↑F • ↑A
⊢ ↑(#F) ^ (n + 1) * ↑(#A) ≤ K ^ (n + 1) * ↑(#A)

Tactic:
gcongr

Result:
no goals

Proof state:
G : Type u_1
inst✝¹ : Group G
K : ℝ
inst✝ : DecidableEq G
A : Finset G
hA : IsApproximateSubgroup K ↑A
n : ℕ
F : Finset G
hF : ↑(#F) ≤ K
hSF : ↑A ^ 2 ⊆ ↑F • ↑A
⊢ ↑(#(A ^ (n + 2))) ≤ ↑(#(F ^ (n + 1) * A))

Tactic:
gcongr

Result:
case h.a
G : Type u_1
inst✝¹ : Group G
K : ℝ
inst✝ : DecidableEq G
A : Finset G
hA : IsApproximateSubgroup K ↑A
n : ℕ
F : Finset G
hF : ↑(#F) ≤ K
hSF : ↑A ^ 2 ⊆ ↑F • ↑A
⊢ A ^ (n + 2) ⊆ F ^ (n + 1) * A