-- Mathlib/Combinatorics/Additive/SmallTripling.lean
@[to_additive]
private lemma small_neg_pos_pos_mul (hA : #(A ^ 3) ≤ K * #A) : #(A⁻¹ * A * A) ≤ K ^ 2 * #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
⊢ 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)
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 * A)) ≤ ↑(#A) * (K ^ 2 * ↑(#A))

Tactic:
calc
  (#A * #(A⁻¹ * A * A) : ℝ) = #A * #(A⁻¹ * (A * A)) := by rw [mul_assoc]
  _ ≤ #(A * A) * #(A * (A * A)) := by
    norm_cast; exact ruzsa_triangle_inequality_invMul_mul_mul A A (A * A)
  _ = #(A ^ 2) * #(A ^ 3) := by simp [pow_succ']
  _ ≤ (K * #A) * (K * #A) := by
    gcongr
    calc
      (#(A ^ 2) : ℝ) ≤ #(A ^ 3) := mod_cast hA₀.card_pow_mono (by norm_num)
      _ ≤ K * #A := hA
  _ = #A * (K ^ 2 * #A) := by 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
⊢ ↑(#(A * A)) * ↑(#(A * (A * A))) = ↑(#(A ^ 2)) * ↑(#(A ^ 3))

Tactic:
simp [pow_succ']

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
⊢ ↑(#A) * ↑(#(A⁻¹ * A * A)) = ↑(#A) * ↑(#(A⁻¹ * (A * A)))

Tactic:
rw [mul_assoc]

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 ^ 2 * ↑(#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 ^ 2 * ↑(#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)

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
⊢ 0 < ↑(#A)

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
⊢ ↑(#(A⁻¹ * A * A)) ≤ K ^ 2 * ↑(#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 ^ 2 * ↑(#A)

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

Tactic:
simp

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
this : 0 ≤ K
⊢ #A * #(A⁻¹ * (A * A)) ≤ #(A * A) * #(A * (A * A))

Tactic:
exact ruzsa_triangle_inequality_invMul_mul_mul A A (A * A)

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 ^ 2 * ↑(#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 ^ 2 * ↑(#∅)

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 ^ 2 * ↑(#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
⊢ K * ↑(#A) * (K * ↑(#A)) = ↑(#A) * (K ^ 2 * ↑(#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
⊢ ↑(#(A ^ 2)) * ↑(#(A ^ 3)) ≤ K * ↑(#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 ^ 2)) ≤ K * ↑(#A)