-- Mathlib/Combinatorics/Additive/ApproximateSubgroup.lean
@[to_additive]
lemma of_small_tripling [DecidableEq G] {A : Finset G} (hA₁ : 1 ∈ A) (hAsymm : A⁻¹ = A)
    (hA : #(A ^ 3) ≤ K * #A) : IsApproximateSubgroup (K ^ 3) (A ^ 2 : Set G) where
  one_mem

Proof state:
G : Type u_1
inst✝¹ : Group G
K : ℝ
inst✝ : DecidableEq G
A : Finset G
hA₁ : 1 ∈ A
hAsymm : A⁻¹ = A
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
⊢ 1 * 1 ∈ ↑A * ↑A

Tactic:
exact Set.mul_mem_mul hA₁ hA₁

Result:
no goals

Proof state:
G : Type u_1
inst✝¹ : Group G
K : ℝ
inst✝ : DecidableEq G
A : Finset G
hA₁ : 1 ∈ A
hAsymm : A⁻¹ = A
hA : ↑(#(A ^ 4 * A)) ≤ K ^ 3 * ↑(#A)
hA₀ : A.Nonempty
F : Finset G
hF : ↑(#F) ≤ K ^ 3
hAF : A ^ 4 ⊆ F * (A / A)
⊢ (↑A ^ 2) ^ 2 ⊆ ↑F • ↑A ^ 2

Tactic:
norm_cast

Result:
G : Type u_1
inst✝¹ : Group G
K : ℝ
inst✝ : DecidableEq G
A : Finset G
hA₁ : 1 ∈ A
hAsymm : A⁻¹ = A
hA : ↑(#(A ^ 4 * A)) ≤ K ^ 3 * ↑(#A)
hA₀ : A.Nonempty
F : Finset G
hF : ↑(#F) ≤ K ^ 3
hAF : A ^ 4 ⊆ F * (A / A)
⊢ (A ^ 2) ^ 2 ⊆ F • A ^ 2

Proof state:
G : Type u_1
inst✝¹ : Group G
K : ℝ
inst✝ : DecidableEq G
A : Finset G
hA₁ : 1 ∈ A
hAsymm : A⁻¹ = A
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
⊢ 1 ∈ ↑A ^ 2

Tactic:
rw [sq, ← one_mul 1]

Result:
G : Type u_1
inst✝¹ : Group G
K : ℝ
inst✝ : DecidableEq G
A : Finset G
hA₁ : 1 ∈ A
hAsymm : A⁻¹ = A
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
⊢ 1 * 1 ∈ ↑A * ↑A

Proof state:
G : Type u_1
inst✝¹ : Group G
K : ℝ
inst✝ : DecidableEq G
A : Finset G
hA₁ : 1 ∈ A
hAsymm : A⁻¹ = A
hA : ↑(#(A ^ 4 * A)) ≤ K ^ 3 * ↑(#A)
hA₀ : A.Nonempty
F : Finset G
hF : ↑(#F) ≤ K ^ 3
hAF : A ^ 4 ⊆ F * (A / A)
⊢ (A ^ 2) ^ 2 ⊆ F • A ^ 2

Tactic:
simpa [div_eq_mul_inv, pow_succ, mul_assoc, hAsymm] using hAF

Result:
no goals

Proof state:
case intro.intro.intro
G : Type u_1
inst✝¹ : Group G
K : ℝ
inst✝ : DecidableEq G
A : Finset G
hA₁ : 1 ∈ A
hAsymm : A⁻¹ = A
hA : ↑(#(A ^ 4 * A)) ≤ K ^ 3 * ↑(#A)
hA₀ : A.Nonempty
F : Finset G
hF : ↑(#F) ≤ K ^ 3
hAF : A ^ 4 ⊆ F * (A / A)
⊢ CovBySMul G (K ^ 3) ((↑A ^ 2) ^ 2) (↑A ^ 2)

Tactic:
exact ⟨F, hF, by norm_cast; simpa [div_eq_mul_inv, pow_succ, mul_assoc, hAsymm] using hAF⟩

Result:
no goals

Proof state:
G : Type u_1
inst✝¹ : Group G
K : ℝ
inst✝ : DecidableEq G
A : Finset G
hA₁ : 1 ∈ A
hAsymm : A⁻¹ = A
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
⊢ 3 ≤ 5

Tactic:
omega

Result:
no goals

Proof state:
G : Type u_1
inst✝¹ : Group G
K : ℝ
inst✝ : DecidableEq G
A : Finset G
hA₁ : 1 ∈ A
hAsymm : A⁻¹ = A
hA : ↑(#(A ^ 4 * A)) ≤ K ^ 3 * ↑(#A)
hA₀ : A.Nonempty
⊢ CovBySMul G (K ^ 3) ((↑A ^ 2) ^ 2) (↑A ^ 2)

Tactic:
obtain ⟨F, -, hF, hAF⟩ := ruzsa_covering_mul hA₀ hA

Result:
case intro.intro.intro
G : Type u_1
inst✝¹ : Group G
K : ℝ
inst✝ : DecidableEq G
A : Finset G
hA₁ : 1 ∈ A
hAsymm : A⁻¹ = A
hA : ↑(#(A ^ 4 * A)) ≤ K ^ 3 * ↑(#A)
hA₀ : A.Nonempty
F : Finset G
hF : ↑(#F) ≤ K ^ 3
hAF : A ^ 4 ⊆ F * (A / A)
⊢ CovBySMul G (K ^ 3) ((↑A ^ 2) ^ 2) (↑A ^ 2)

Proof state:
G : Type u_1
inst✝¹ : Group G
K : ℝ
inst✝ : DecidableEq G
A : Finset G
hA₁ : 1 ∈ A
hAsymm : A⁻¹ = A
hA : ↑(#(A ^ 4 * A)) ≤ K ^ 3 * ↑(#A)
⊢ CovBySMul G (K ^ 3) ((↑A ^ 2) ^ 2) (↑A ^ 2)

Tactic:
have hA₀ : A.Nonempty := ⟨1, hA₁⟩

Result:
G : Type u_1
inst✝¹ : Group G
K : ℝ
inst✝ : DecidableEq G
A : Finset G
hA₁ : 1 ∈ A
hAsymm : A⁻¹ = A
hA : ↑(#(A ^ 4 * A)) ≤ K ^ 3 * ↑(#A)
hA₀ : A.Nonempty
⊢ CovBySMul G (K ^ 3) ((↑A ^ 2) ^ 2) (↑A ^ 2)

Proof state:
G : Type u_1
inst✝¹ : Group G
K : ℝ
inst✝ : DecidableEq G
A : Finset G
hA₁ : 1 ∈ A
hAsymm : A⁻¹ = A
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
⊢ (↑A ^ 2)⁻¹ = ↑A ^ 2

Tactic:
simp [← inv_pow, hAsymm, ← coe_inv]

Result:
no goals

Proof state:
G : Type u_1
inst✝¹ : Group G
K : ℝ
inst✝ : DecidableEq G
A : Finset G
hA₁ : 1 ∈ A
hAsymm : A⁻¹ = A
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
⊢ CovBySMul G (K ^ 3) ((↑A ^ 2) ^ 2) (↑A ^ 2)

Tactic:
replace hA := calc (#(A ^ 4 * A) : ℝ)
  _ = #(A ^ 5) := by rw [← pow_succ]
  _ ≤ K ^ 3 * #A := small_pow_of_small_tripling (by omega) hA hAsymm

Result:
G : Type u_1
inst✝¹ : Group G
K : ℝ
inst✝ : DecidableEq G
A : Finset G
hA₁ : 1 ∈ A
hAsymm : A⁻¹ = A
hA : ↑(#(A ^ 4 * A)) ≤ K ^ 3 * ↑(#A)
⊢ CovBySMul G (K ^ 3) ((↑A ^ 2) ^ 2) (↑A ^ 2)

Proof state:
G : Type u_1
inst✝¹ : Group G
K : ℝ
inst✝ : DecidableEq G
A : Finset G
hA₁ : 1 ∈ A
hAsymm : A⁻¹ = A
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
⊢ ↑(#(A ^ 4 * A)) = ↑(#(A ^ 5))

Tactic:
rw [← pow_succ]

Result:
no goals