-- Mathlib/Combinatorics/Additive/SmallTripling.lean
@[to_additive]
private lemma small_pos_neg_pos_mul (hA : #(A ^ 3) ≤ K * #A) : #(A * A⁻¹ * A) ≤ K ^ 3 * #A

Proof state:
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
K : ℝ
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
hA₀ : A.Nonempty
this : 0 ≤ K
⊢ ↑(#(A * (A * A⁻¹))) * ↑(#(A * A)) = ↑(#(A * A * A⁻¹)) * ↑(#(A ^ 2))

Tactic:
simp [pow_succ, mul_assoc]

Result:
no goals

Proof state:
case h₂
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
K : ℝ
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
hA₀ : A.Nonempty
this : 0 ≤ K
⊢ ↑(#(A ^ 2)) ≤ K * ↑(#A)

Tactic:
calc
  (#(A ^ 2) : ℝ) ≤ #(A ^ 3) := mod_cast hA₀.card_pow_mono (by norm_num)
  _ ≤ K * #A := hA

Result:
no goals

Proof state:
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
K : ℝ
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
hA₀ : A.Nonempty
⊢ 0 < ↑(#A)

Tactic:
positivity

Result:
no goals

Proof state:
case h₁
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
K : ℝ
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
hA₀ : A.Nonempty
this : 0 ≤ K
⊢ ↑(#(A * A * A⁻¹)) ≤ K ^ 2 * ↑(#A)

Tactic:
exact small_pos_pos_neg_mul hA

Result:
no goals

Proof state:
case inr
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
K : ℝ
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
hA₀ : A.Nonempty
⊢ ↑(#(A * A⁻¹ * A)) ≤ K ^ 3 * ↑(#A)

Tactic:
have : 0 ≤ K := nonneg_of_mul_nonneg_left (hA.trans' <| by positivity) (by positivity)

Result:
case inr
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
K : ℝ
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
hA₀ : A.Nonempty
this : 0 ≤ K
⊢ ↑(#(A * A⁻¹ * A)) ≤ K ^ 3 * ↑(#A)

Proof state:
case inl
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
K : ℝ
hA : ↑(#(∅ ^ 3)) ≤ K * ↑(#∅)
⊢ ↑(#(∅ * ∅⁻¹ * ∅)) ≤ K ^ 3 * ↑(#∅)

Tactic:
simp

Result:
no goals

Proof state:
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
K : ℝ
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
hA₀ : A.Nonempty
this : 0 ≤ K
⊢ ↑(#A) * ↑(#(A * A⁻¹ * A)) ≤ ↑(#(A * (A * A⁻¹))) * ↑(#(A * A))

Tactic:
norm_cast

Result:
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
K : ℝ
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
hA₀ : A.Nonempty
this : 0 ≤ K
⊢ #A * #(A * A⁻¹ * A) ≤ #(A * (A * A⁻¹)) * #(A * A)

Proof state:
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
K : ℝ
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
hA₀ : A.Nonempty
this : 0 ≤ K
⊢ 0 < ↑(#A)

Tactic:
positivity

Result:
no goals

Proof state:
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
K : ℝ
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
hA₀ : A.Nonempty
this : 0 ≤ K
⊢ K ^ 2 * ↑(#A) * (K * ↑(#A)) = ↑(#A) * (K ^ 3 * ↑(#A))

Tactic:
ring

Result:
no goals

Proof state:
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
K : ℝ
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
hA₀ : A.Nonempty
this : 0 ≤ K
⊢ 2 ≤ 3

Tactic:
norm_num

Result:
no goals

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

Tactic:
obtain rfl | hA₀ := A.eq_empty_or_nonempty

Result:
case inl
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
K : ℝ
hA : ↑(#(∅ ^ 3)) ≤ K * ↑(#∅)
⊢ ↑(#(∅ * ∅⁻¹ * ∅)) ≤ K ^ 3 * ↑(#∅)

case inr
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
K : ℝ
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
hA₀ : A.Nonempty
⊢ ↑(#(A * A⁻¹ * A)) ≤ K ^ 3 * ↑(#A)

Proof state:
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
K : ℝ
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
hA₀ : A.Nonempty
this : 0 ≤ K
⊢ ↑(#(A * A * A⁻¹)) * ↑(#(A ^ 2)) ≤ K ^ 2 * ↑(#A) * (K * ↑(#A))

Tactic:
gcongr

Result:
case h₁
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
K : ℝ
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
hA₀ : A.Nonempty
this : 0 ≤ K
⊢ ↑(#(A * A * A⁻¹)) ≤ K ^ 2 * ↑(#A)

case h₂
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
K : ℝ
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
hA₀ : A.Nonempty
this : 0 ≤ K
⊢ ↑(#(A ^ 2)) ≤ K * ↑(#A)

Proof state:
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
K : ℝ
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
hA₀ : A.Nonempty
⊢ 0 ≤ ↑(#(A ^ 3))

Tactic:
positivity

Result:
no goals

Proof state:
case inr
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
K : ℝ
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
hA₀ : A.Nonempty
this : 0 ≤ K
⊢ ↑(#(A * A⁻¹ * A)) ≤ K ^ 3 * ↑(#A)

Tactic:
refine le_of_mul_le_mul_left ?_ (by positivity : (0 : ℝ) < #A)

Result:
case inr
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
K : ℝ
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
hA₀ : A.Nonempty
this : 0 ≤ K
⊢ ↑(#A) * ↑(#(A * A⁻¹ * A)) ≤ ↑(#A) * (K ^ 3 * ↑(#A))

Proof state:
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
K : ℝ
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
hA₀ : A.Nonempty
this : 0 ≤ K
⊢ #A * #(A * A⁻¹ * A) ≤ #(A * (A * A⁻¹)) * #(A * A)

Tactic:
simpa using ruzsa_triangle_inequality_invMul_mul_mul (A * A⁻¹) A A

Result:
no goals