awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : CommGroup G
A B C : Finset G
⊢ #(A * C⁻¹) * #B ≤ #(A * B) * #(B * C⁻¹)

Tactic:
exact ruzsa_triangle_inequality_mul_mul_mul _ _ _

Premises used: Finset.ruzsa_triangle_inequality_mul_mul_mul
-- Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : CommGroup G
A B C : Finset G
rw : #(A * C⁻¹) * #B ≤ #(A / B) * #(B / C⁻¹)
⊢ #(A / C) * #B ≤ #(A / B) * #(B * C)

Tactic:
rw [← div_inv_eq_mul, div_eq_mul_inv]

Premises used: div_eq_mul_inv, div_inv_eq_mul
-- Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : CommGroup G
A B C : Finset G
⊢ #(A * C⁻¹) * #B ≤ #(A / B) * #(B / C⁻¹)

Tactic:
ruzsa_triangle_inequality_mul_div_div _ _ _

Premises used: Finset.ruzsa_triangle_inequality_mul_div_div
-- Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : CommGroup G
A B C : Finset G
⊢ #(A * C⁻¹) * #B ≤ #(A / B) * #(B / C⁻¹)

Tactic:
exact ruzsa_triangle_inequality_mul_div_div _ _ _

Premises used: Finset.ruzsa_triangle_inequality_mul_div_div
-- Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : CommGroup G
A B : Finset G
hAB : ∀ A' ⊆ A, #(A * B) * #A' ≤ #(A' * B) * #A
n : ℕ
inl :
  ∀ (hAB : ∀ A' ⊆ ∅, #(∅ * B) * #A' ≤ #(A' * B) * card.{u_1} (α := G) ∅),
    (↑(#(∅ * B ^ n)) : ℚ≥0) ≤
      HDiv.hDiv (α := ℚ≥0) (↑(#(∅ * B)) : ℚ≥0) (↑(card.{u_1} (α := G) ∅) : ℚ≥0) ^ n * (↑(card.{u_1} (α := G) ∅) : ℚ≥0)
inr :
  ∀ (hA : A.Nonempty),
    (↑(#(A * B ^ n)) : ℚ≥0) ≤ HDiv.hDiv (α := ℚ≥0) (↑(#(A * B)) : ℚ≥0) (↑(#A) : ℚ≥0) ^ n * (↑(#A) : ℚ≥0)
⊢ (↑(#(A * B ^ n)) : ℚ≥0) ≤ HDiv.hDiv (α := ℚ≥0) (↑(#(A * B)) : ℚ≥0) (↑(#A) : ℚ≥0) ^ n * (↑(#A) : ℚ≥0)

Tactic:
obtain rfl | hA := A.eq_empty_or_nonempty

Premises used: rfl, Finset.eq_empty_or_nonempty
-- Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : CommGroup G
B : Finset G
n : ℕ
hAB : ∀ A' ⊆ ∅, #(∅ * B) * #A' ≤ #(A' * B) * card.{u_1} (α := G) ∅
⊢ (↑(#(∅ * B ^ n)) : ℚ≥0) ≤
    HDiv.hDiv (α := ℚ≥0) (↑(#(∅ * B)) : ℚ≥0) (↑(card.{u_1} (α := G) ∅) : ℚ≥0) ^ n * (↑(card.{u_1} (α := G) ∅) : ℚ≥0)

Tactic:
simp
-- Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : CommGroup G
A B : Finset G
hAB : ∀ A' ⊆ A, #(A * B) * #A' ≤ #(A' * B) * #A
hA : A.Nonempty
⊢ (↑(#(A * HPow.hPow (β := ℕ) B 0)) : ℚ≥0) ≤
    HPow.hPow (β := ℕ) (HDiv.hDiv (α := ℚ≥0) (↑(#(A * B)) : ℚ≥0) (↑(#A) : ℚ≥0)) 0 * (↑(#A) : ℚ≥0)

Tactic:
simp
-- Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : CommGroup G
A B : Finset G
hAB : ∀ A' ⊆ A, #(A * B) * #A' ≤ #(A' * B) * #A
hA : A.Nonempty
n : ℕ
ih : (↑(#(A * B ^ n)) : ℚ≥0) ≤ HDiv.hDiv (α := ℚ≥0) (↑(#(A * B)) : ℚ≥0) (↑(#A) : ℚ≥0) ^ n * (↑(#A) : ℚ≥0)
⊢ LT.lt (α := ℚ≥0) 0 (↑(#A) : ℚ≥0)

Tactic:
positivity
-- Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : CommGroup G
A B : Finset G
hAB : ∀ A' ⊆ A, #(A * B) * #A' ≤ #(A' * B) * #A
hA : A.Nonempty
n : ℕ
ih : (↑(#(A * B ^ n)) : ℚ≥0) ≤ HDiv.hDiv (α := ℚ≥0) (↑(#(A * B)) : ℚ≥0) (↑(#A) : ℚ≥0) ^ n * (↑(#A) : ℚ≥0)
inr :
  HMul.hMul (α := ℚ≥0) (↑(#(A * B ^ (n + 1))) : ℚ≥0) (↑(#A) : ℚ≥0) ≤
    HDiv.hDiv (α := ℚ≥0) (↑(#(A * B)) : ℚ≥0) (↑(#A) : ℚ≥0) ^ (n + 1) * (↑(#A) : ℚ≥0) * (↑(#A) : ℚ≥0)
⊢ (↑(#(A * B ^ (n + 1))) : ℚ≥0) ≤ HDiv.hDiv (α := ℚ≥0) (↑(#(A * B)) : ℚ≥0) (↑(#A) : ℚ≥0) ^ (n + 1) * (↑(#A) : ℚ≥0)

Tactic:
refine le_of_mul_le_mul_right ?_ (by positivity : (0 : ℚ≥0) < #A)

Premises used: le_of_mul_le_mul_right
-- Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : CommGroup G
A B : Finset G
hAB : ∀ A' ⊆ A, #(A * B) * #A' ≤ #(A' * B) * #A
hA : A.Nonempty
n : ℕ
ih : (↑(#(A * B ^ n)) : ℚ≥0) ≤ HDiv.hDiv (α := ℚ≥0) (↑(#(A * B)) : ℚ≥0) (↑(#A) : ℚ≥0) ^ n * (↑(#A) : ℚ≥0)
rw :
  HMul.hMul (α := ℚ≥0) (↑(#(A * (B ^ n * B))) : ℚ≥0) (↑(#A) : ℚ≥0) =
    HMul.hMul (α := ℚ≥0) (↑(#(B ^ n * A * B)) : ℚ≥0) (↑(#A) : ℚ≥0)
rw₁ :
  HMul.hMul (α := ℚ≥0) (↑(#(B ^ n * (A * B))) : ℚ≥0) (↑(#A) : ℚ≥0) =
    HMul.hMul (α := ℚ≥0) (↑(#(B ^ n * A * B)) : ℚ≥0) (↑(#A) : ℚ≥0)
rw₂ rw₃ :
  HMul.hMul (α := ℚ≥0) (↑(#(B ^ n * (A * B))) : ℚ≥0) (↑(#A) : ℚ≥0) =
    HMul.hMul (α := ℚ≥0) (↑(#(B ^ n * (A * B))) : ℚ≥0) (↑(#A) : ℚ≥0)
⊢ HMul.hMul (α := ℚ≥0) (↑(#(A * B ^ (n + 1))) : ℚ≥0) (↑(#A) : ℚ≥0) =
    HMul.hMul (α := ℚ≥0) (↑(#(B ^ n * A * B)) : ℚ≥0) (↑(#A) : ℚ≥0)

Tactic:
rw [pow_succ, mul_left_comm, mul_assoc]

Premises used: pow_succ, mul_assoc, mul_left_comm
-- Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : CommGroup G
A B : Finset G
hAB : ∀ A' ⊆ A, #(A * B) * #A' ≤ #(A' * B) * #A
hA : A.Nonempty
n : ℕ
ih : (↑(#(A * B ^ n)) : ℚ≥0) ≤ HDiv.hDiv (α := ℚ≥0) (↑(#(A * B)) : ℚ≥0) (↑(#A) : ℚ≥0) ^ n * (↑(#A) : ℚ≥0)
⊢ HMul.hMul (α := ℚ≥0) (↑(#(B ^ n * A * B)) : ℚ≥0) (↑(#A) : ℚ≥0) ≤
    HMul.hMul (α := ℚ≥0) (↑(#(A * B)) : ℚ≥0) (↑(#(B ^ n * A)) : ℚ≥0)

Tactic:
mod_cast pluennecke_petridis_inequality_mul _ hAB

Premises used: Nat.cast_mul._simp_1, HMul.hMul, congrArg, cast, Nat.cast_le._simp_1, LE.le, HPow.hPow, congr, Finset.card, Eq.symm, Finset.pluennecke_petridis_inequality_mul, Eq.trans
-- Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : CommGroup G
A B : Finset G
hAB : ∀ A' ⊆ A, #(A * B) * #A' ≤ #(A' * B) * #A
hA : A.Nonempty
n : ℕ
ih : (↑(#(A * B ^ n)) : ℚ≥0) ≤ HDiv.hDiv (α := ℚ≥0) (↑(#(A * B)) : ℚ≥0) (↑(#A) : ℚ≥0) ^ n * (↑(#A) : ℚ≥0)
rw :
  HMul.hMul (α := ℚ≥0) (↑(#(A * B)) : ℚ≥0) (↑(#(A * B ^ n)) : ℚ≥0) ≤
    (↑(#(A * B)) : ℚ≥0) * (HDiv.hDiv (α := ℚ≥0) (↑(#(A * B)) : ℚ≥0) (↑(#A) : ℚ≥0) ^ n * (↑(#A) : ℚ≥0))
⊢ HMul.hMul (α := ℚ≥0) (↑(#(A * B)) : ℚ≥0) (↑(#(B ^ n * A)) : ℚ≥0) ≤
    (↑(#(A * B)) : ℚ≥0) * (HDiv.hDiv (α := ℚ≥0) (↑(#(A * B)) : ℚ≥0) (↑(#A) : ℚ≥0) ^ n * (↑(#A) : ℚ≥0))

Tactic:
rw [mul_comm _ A]

Premises used: mul_comm
-- Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : CommGroup G
A B : Finset G
hAB : ∀ A' ⊆ A, #(A * B) * #A' ≤ #(A' * B) * #A
hA : A.Nonempty
n : ℕ
ih : (↑(#(A * B ^ n)) : ℚ≥0) ≤ HDiv.hDiv (α := ℚ≥0) (↑(#(A * B)) : ℚ≥0) (↑(#A) : ℚ≥0) ^ n * (↑(#A) : ℚ≥0)
⊢ HMul.hMul (α := ℚ≥0) (↑(#(A * B)) : ℚ≥0) (↑(#(A * B ^ n)) : ℚ≥0) ≤
    (↑(#(A * B)) : ℚ≥0) * (HDiv.hDiv (α := ℚ≥0) (↑(#(A * B)) : ℚ≥0) (↑(#A) : ℚ≥0) ^ n * (↑(#A) : ℚ≥0))

Tactic:
gcongr
-- Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : CommGroup G
A B : Finset G
hAB : ∀ A' ⊆ A, #(A * B) * #A' ≤ #(A' * B) * #A
hA : A.Nonempty
n : ℕ
ih : (↑(#(A * B ^ n)) : ℚ≥0) ≤ HDiv.hDiv (α := ℚ≥0) (↑(#(A * B)) : ℚ≥0) (↑(#A) : ℚ≥0) ^ n * (↑(#A) : ℚ≥0)
⊢ (↑(#(A * B)) : ℚ≥0) * (HDiv.hDiv (α := ℚ≥0) (↑(#(A * B)) : ℚ≥0) (↑(#A) : ℚ≥0) ^ n * (↑(#A) : ℚ≥0)) =
    HDiv.hDiv (α := ℚ≥0) (↑(#(A * B)) : ℚ≥0) (↑(#A) : ℚ≥0) ^ (n + 1) * (↑(#A) : ℚ≥0) * (↑(#A) : ℚ≥0)

Tactic:
simp [field, pow_add]

Premises used: pow_add
-- Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : CommGroup G
A B : Finset G
hAB : ∀ A' ⊆ A, #(A * B) * #A' ≤ #(A' * B) * #A
hA : A.Nonempty
n : ℕ
ih : (↑(#(A * B ^ n)) : ℚ≥0) ≤ HDiv.hDiv (α := ℚ≥0) (↑(#(A * B)) : ℚ≥0) (↑(#A) : ℚ≥0) ^ n * (↑(#A) : ℚ≥0)
B₁ :
  HMul.hMul (α := ℚ≥0) (↑(#(A * B ^ (n + 1))) : ℚ≥0) (↑(#A) : ℚ≥0) =
    HMul.hMul (α := ℚ≥0) (↑(#(B ^ n * A * B)) : ℚ≥0) (↑(#A) : ℚ≥0)
B₂ :
  HMul.hMul (α := ℚ≥0) (↑(#(A * B)) : ℚ≥0) (↑(#(B ^ n * A)) : ℚ≥0) ≤
    (↑(#(A * B)) : ℚ≥0) * (HDiv.hDiv (α := ℚ≥0) (↑(#(A * B)) : ℚ≥0) (↑(#A) : ℚ≥0) ^ n * (↑(#A) : ℚ≥0))
B₃ :
  (↑(#(A * B)) : ℚ≥0) * (HDiv.hDiv (α := ℚ≥0) (↑(#(A * B)) : ℚ≥0) (↑(#A) : ℚ≥0) ^ n * (↑(#A) : ℚ≥0)) =
    HDiv.hDiv (α := ℚ≥0) (↑(#(A * B)) : ℚ≥0) (↑(#A) : ℚ≥0) ^ (n + 1) * (↑(#A) : ℚ≥0) * (↑(#A) : ℚ≥0)
⊢ HMul.hMul (α := ℚ≥0) (↑(#(A * B ^ (n + 1))) : ℚ≥0) (↑(#A) : ℚ≥0) ≤
    HDiv.hDiv (α := ℚ≥0) (↑(#(A * B)) : ℚ≥0) (↑(#A) : ℚ≥0) ^ (n + 1) * (↑(#A) : ℚ≥0) * (↑(#A) : ℚ≥0)

Tactic:
calc
      ((#(A * B ^ (n + 1))) * #A : ℚ≥0)
        = #(B ^ n * A * B) * #A := by rw [pow_succ, mul_left_comm, mul_assoc]
      _ ≤ #(A * B) * #(B ^ n * A) := mod_cast pluennecke_petridis_inequality_mul _ hAB
      _ ≤ #(A * B) * ((#(A * B) / #A) ^ n * #A) := by rw [mul_comm _ A]; gcongr
      _ = (#(A * B) / #A) ^ (n + 1) * #A * #A := by simp [field, pow_add]

Premises used: HMul.hMul, HDiv.hDiv, Nat.cast, HPow.hPow, HAdd.hAdd, Finset.card, OfNat.ofNat, Finset.pluennecke_petridis_inequality_mul
-- Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : CommGroup G
A B : Finset G
hAB : ∀ A' ⊆ A, #(A * B) * #A' ≤ #(A' * B) * #A
n : ℕ
hA : A.Nonempty
inr :
  (↑(#(A * HPow.hPow (β := ℕ) B 0)) : ℚ≥0) ≤
    HPow.hPow (β := ℕ) (HDiv.hDiv (α := ℚ≥0) (↑(#(A * B)) : ℚ≥0) (↑(#A) : ℚ≥0)) 0 * (↑(#A) : ℚ≥0)
inr₁ :
  ∀ (n : ℕ) (ih : (↑(#(A * B ^ n)) : ℚ≥0) ≤ HDiv.hDiv (α := ℚ≥0) (↑(#(A * B)) : ℚ≥0) (↑(#A) : ℚ≥0) ^ n * (↑(#A) : ℚ≥0)),
    (↑(#(A * B ^ (n + 1))) : ℚ≥0) ≤ HDiv.hDiv (α := ℚ≥0) (↑(#(A * B)) : ℚ≥0) (↑(#A) : ℚ≥0) ^ (n + 1) * (↑(#A) : ℚ≥0)
⊢ (↑(#(A * B ^ n)) : ℚ≥0) ≤ HDiv.hDiv (α := ℚ≥0) (↑(#(A * B)) : ℚ≥0) (↑(#A) : ℚ≥0) ^ n * (↑(#A) : ℚ≥0)

Tactic:
induction n with
  | zero => simp
  | succ n ih =>
    refine le_of_mul_le_mul_right ?_ (by positivity : (0 : ℚ≥0) < #A)
    calc
      ((#(A * B ^ (n + 1))) * #A : ℚ≥0)
        = #(B ^ n * A * B) * #A := by rw [pow_succ, mul_left_comm, mul_assoc]
      _ ≤ #(A * B) * #(B ^ n * A) := mod_cast pluennecke_petridis_inequality_mul _ hAB
      _ ≤ #(A * B) * ((#(A * B) / #A) ^ n * #A) := by rw [mul_comm _ A]; gcongr
      _ = (#(A * B) / #A) ^ (n + 1) * #A * #A := by simp [field, pow_add]

Premises used: HMul.hMul, le_of_mul_le_mul_right, HDiv.hDiv, Nat.cast, HPow.hPow, HAdd.hAdd, Finset.card, Nat.zero, OfNat.ofNat, Finset.pluennecke_petridis_inequality_mul, Nat.succ
-- Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : CommGroup G
A : Finset G
hA : A.Nonempty
B : Finset G
m n : ℕ
⊢ A ∈ A.powerset.erase ∅

Tactic:
have hA' : A ∈ A.powerset.erase ∅ := mem_erase_of_ne_of_mem hA.ne_empty (mem_powerset_self _)
-- Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : CommGroup G
A : Finset G
hA : A.Nonempty
B : Finset G
m n : ℕ
hA' : A ∈ A.powerset.erase ∅
obtain :
  ∀ (C : Finset G) (hC : C ∈ A.powerset.erase ∅)
    (hCmin :
      ∀ x' ∈ A.powerset.erase ∅,
        HDiv.hDiv (α := ℚ≥0) (↑(#(C * B)) : ℚ≥0) (↑(#C) : ℚ≥0) ≤
          HDiv.hDiv (α := ℚ≥0) (↑(#(x' * B)) : ℚ≥0) (↑(#x') : ℚ≥0)),
    (↑(#(B ^ m / B ^ n)) : ℚ≥0) ≤ HDiv.hDiv (α := ℚ≥0) (↑(#(A * B)) : ℚ≥0) (↑(#A) : ℚ≥0) ^ (m + n) * (↑(#A) : ℚ≥0)
⊢ (↑(#(B ^ m / B ^ n)) : ℚ≥0) ≤ HDiv.hDiv (α := ℚ≥0) (↑(#(A * B)) : ℚ≥0) (↑(#A) : ℚ≥0) ^ (m + n) * (↑(#A) : ℚ≥0)

Tactic:
obtain ⟨C, hC, hCmin⟩ :=
    exists_min_image (A.powerset.erase ∅) (fun C ↦ #(C * B) / #C : _ → ℚ≥0) ⟨A, hA'⟩

Premises used: HMul.hMul, HDiv.hDiv, Nat.cast, Exists.intro, Finset.exists_min_image, Finset.card, Finset.powerset, EmptyCollection.emptyCollection, Finset.erase
-- Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : CommGroup G
A : Finset G
hA : A.Nonempty
B : Finset G
m n : ℕ
hA' : A ∈ A.powerset.erase ∅
C : Finset G
hC : C ∈ A.powerset.erase ∅
hCmin :
  ∀ x' ∈ A.powerset.erase ∅,
    HDiv.hDiv (α := ℚ≥0) (↑(#(C * B)) : ℚ≥0) (↑(#C) : ℚ≥0) ≤ HDiv.hDiv (α := ℚ≥0) (↑(#(x' * B)) : ℚ≥0) (↑(#x') : ℚ≥0)
⊢ C.Nonempty ∧ C ⊆ A

Tactic:
rw [mem_erase, mem_powerset, ← nonempty_iff_ne_empty] at hC

Premises used: Finset.nonempty_iff_ne_empty, Finset.mem_powerset, Finset.mem_erase
-- Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : CommGroup G
A : Finset G
hA : A.Nonempty
B : Finset G
m n : ℕ
hA' : A ∈ A.powerset.erase ∅
C : Finset G
hC : C ∈ A.powerset.erase ∅
hCmin :
  ∀ x' ∈ A.powerset.erase ∅,
    HDiv.hDiv (α := ℚ≥0) (↑(#(C * B)) : ℚ≥0) (↑(#C) : ℚ≥0) ≤ HDiv.hDiv (α := ℚ≥0) (↑(#(x' * B)) : ℚ≥0) (↑(#x') : ℚ≥0)
hC₁ : C.Nonempty ∧ C ⊆ A
⊢ ∀ x' ∈ A.powerset.erase ∅,
    HDiv.hDiv (α := ℚ≥0) (↑(#(C * B)) : ℚ≥0) (↑(#C) : ℚ≥0) ≤ HDiv.hDiv (α := ℚ≥0) (↑(#(x' * B)) : ℚ≥0) (↑(#x') : ℚ≥0)

Tactic:
rw [mem_erase, mem_powerset, ← nonempty_iff_ne_empty] at hC

Premises used: Finset.nonempty_iff_ne_empty, Finset.mem_powerset, Finset.mem_erase
-- Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : CommGroup G
A : Finset G
hA : A.Nonempty
B : Finset G
m n : ℕ
hA' : A ∈ A.powerset.erase ∅
C : Finset G
hC : C.Nonempty ∧ C ⊆ A
hCmin :
  ∀ x' ∈ A.powerset.erase ∅,
    HDiv.hDiv (α := ℚ≥0) (↑(#(C * B)) : ℚ≥0) (↑(#C) : ℚ≥0) ≤ HDiv.hDiv (α := ℚ≥0) (↑(#(x' * B)) : ℚ≥0) (↑(#x') : ℚ≥0)
⊢ C.Nonempty

Tactic:
obtain ⟨hC, hCA⟩ := hC
-- Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : CommGroup G
A : Finset G
hA : A.Nonempty
B : Finset G
m n : ℕ
hA' : A ∈ A.powerset.erase ∅
C : Finset G
hC : C.Nonempty ∧ C ⊆ A
hCmin :
  ∀ x' ∈ A.powerset.erase ∅,
    HDiv.hDiv (α := ℚ≥0) (↑(#(C * B)) : ℚ≥0) (↑(#C) : ℚ≥0) ≤ HDiv.hDiv (α := ℚ≥0) (↑(#(x' * B)) : ℚ≥0) (↑(#x') : ℚ≥0)
hC₁ : C.Nonempty
⊢ C ⊆ A

Tactic:
obtain ⟨hC, hCA⟩ := hC
-- Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : CommGroup G
A : Finset G
hA : A.Nonempty
B : Finset G
m n : ℕ
hA' : A ∈ A.powerset.erase ∅
C : Finset G
hCmin :
  ∀ x' ∈ A.powerset.erase ∅,
    HDiv.hDiv (α := ℚ≥0) (↑(#(C * B)) : ℚ≥0) (↑(#C) : ℚ≥0) ≤ HDiv.hDiv (α := ℚ≥0) (↑(#(x' * B)) : ℚ≥0) (↑(#x') : ℚ≥0)
hC : C.Nonempty
hCA : C ⊆ A
⊢ LT.lt (α := ℚ≥0) 0 (↑(#C) : ℚ≥0)

Tactic:
positivity
-- Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : CommGroup G
A : Finset G
hA : A.Nonempty
B : Finset G
m n : ℕ
hA' : A ∈ A.powerset.erase ∅
C : Finset G
hCmin :
  ∀ x' ∈ A.powerset.erase ∅,
    HDiv.hDiv (α := ℚ≥0) (↑(#(C * B)) : ℚ≥0) (↑(#C) : ℚ≥0) ≤ HDiv.hDiv (α := ℚ≥0) (↑(#(x' * B)) : ℚ≥0) (↑(#x') : ℚ≥0)
hC : C.Nonempty
hCA : C ⊆ A
refine :
  HMul.hMul (α := ℚ≥0) (↑(#(B ^ m / B ^ n)) : ℚ≥0) (↑(#C) : ℚ≥0) ≤
    HDiv.hDiv (α := ℚ≥0) (↑(#(A * B)) : ℚ≥0) (↑(#A) : ℚ≥0) ^ (m + n) * (↑(#A) : ℚ≥0) * (↑(#C) : ℚ≥0)
⊢ (↑(#(B ^ m / B ^ n)) : ℚ≥0) ≤ HDiv.hDiv (α := ℚ≥0) (↑(#(A * B)) : ℚ≥0) (↑(#A) : ℚ≥0) ^ (m + n) * (↑(#A) : ℚ≥0)

Tactic:
refine le_of_mul_le_mul_right ?_ (by positivity : (0 : ℚ≥0) < #C)

Premises used: le_of_mul_le_mul_right
-- Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : CommGroup G
A : Finset G
hA : A.Nonempty
B : Finset G
m n : ℕ
hA' : A ∈ A.powerset.erase ∅
C : Finset G
hCmin :
  ∀ x' ∈ A.powerset.erase ∅,
    HDiv.hDiv (α := ℚ≥0) (↑(#(C * B)) : ℚ≥0) (↑(#C) : ℚ≥0) ≤ HDiv.hDiv (α := ℚ≥0) (↑(#(x' * B)) : ℚ≥0) (↑(#x') : ℚ≥0)
hC : C.Nonempty
hCA : C ⊆ A
⊢ HMul.hMul (α := ℚ≥0) (↑(#(B ^ m / B ^ n)) : ℚ≥0) (↑(#C) : ℚ≥0) ≤
    HMul.hMul (α := ℚ≥0) (↑(#(B ^ m * C)) : ℚ≥0) (↑(#(B ^ n * C)) : ℚ≥0)

Tactic:
mod_cast ruzsa_triangle_inequality_div_mul_mul ..

Premises used: Nat.cast_mul._simp_1, HMul.hMul, congrArg, cast, HDiv.hDiv, Finset.ruzsa_triangle_inequality_div_mul_mul, Nat.cast_le._simp_1, LE.le, HPow.hPow, congr, Finset.card, Eq.symm, Eq.trans
-- Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : CommGroup G
A : Finset G
hA : A.Nonempty
B : Finset G
m n : ℕ
hA' : A ∈ A.powerset.erase ∅
C : Finset G
hCmin :
  ∀ x' ∈ A.powerset.erase ∅,
    HDiv.hDiv (α := ℚ≥0) (↑(#(C * B)) : ℚ≥0) (↑(#C) : ℚ≥0) ≤ HDiv.hDiv (α := ℚ≥0) (↑(#(x' * B)) : ℚ≥0) (↑(#x') : ℚ≥0)
hC : C.Nonempty
hCA : C ⊆ A
⊢ HMul.hMul (α := ℚ≥0) (↑(#(B ^ m * C)) : ℚ≥0) (↑(#(B ^ n * C)) : ℚ≥0) =
    HMul.hMul (α := ℚ≥0) (↑(#(C * B ^ m)) : ℚ≥0) (↑(#(C * B ^ n)) : ℚ≥0)

Tactic:
simp_rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : CommGroup G
A : Finset G
hA : A.Nonempty
B : Finset G
m n : ℕ
hA' : A ∈ A.powerset.erase ∅
C : Finset G
hCmin :
  ∀ x' ∈ A.powerset.erase ∅,
    HDiv.hDiv (α := ℚ≥0) (↑(#(C * B)) : ℚ≥0) (↑(#C) : ℚ≥0) ≤ HDiv.hDiv (α := ℚ≥0) (↑(#(x' * B)) : ℚ≥0) (↑(#x') : ℚ≥0)
hC : C.Nonempty
hCA : C ⊆ A
h₁ : (↑(#(C * B ^ m)) : ℚ≥0) ≤ HDiv.hDiv (α := ℚ≥0) (↑(#(C * B)) : ℚ≥0) (↑(#C) : ℚ≥0) ^ m * (↑(#C) : ℚ≥0)
h₂ : (↑(#(C * B ^ n)) : ℚ≥0) ≤ HDiv.hDiv (α := ℚ≥0) (↑(#(C * B)) : ℚ≥0) (↑(#C) : ℚ≥0) ^ n * (↑(#C) : ℚ≥0)
⊢ HMul.hMul (α := ℚ≥0) (↑(#(C * B ^ m)) : ℚ≥0) (↑(#(C * B ^ n)) : ℚ≥0) ≤
    HDiv.hDiv (α := ℚ≥0) (↑(#(C * B)) : ℚ≥0) (↑(#C) : ℚ≥0) ^ m * (↑(#C) : ℚ≥0) *
      (HDiv.hDiv (α := ℚ≥0) (↑(#(C * B)) : ℚ≥0) (↑(#C) : ℚ≥0) ^ n * (↑(#C) : ℚ≥0))

Tactic:
gcongr
-- Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : CommGroup G
A : Finset G
hA : A.Nonempty
B : Finset G
m n : ℕ
hA' : A ∈ A.powerset.erase ∅
C : Finset G
hCmin :
  ∀ x' ∈ A.powerset.erase ∅,
    HDiv.hDiv (α := ℚ≥0) (↑(#(C * B)) : ℚ≥0) (↑(#C) : ℚ≥0) ≤ HDiv.hDiv (α := ℚ≥0) (↑(#(x' * B)) : ℚ≥0) (↑(#x') : ℚ≥0)
hC : C.Nonempty
hCA : C ⊆ A
⊢ (↑(#(C * B ^ m)) : ℚ≥0) ≤ HDiv.hDiv (α := ℚ≥0) (↑(#(C * B)) : ℚ≥0) (↑(#C) : ℚ≥0) ^ m * (↑(#C) : ℚ≥0)

Tactic:
card_mul_pow_le (mul_aux hC hCA hCmin) _

Premises used: _private.0.Finset.card_mul_pow_le, _private.0.Finset.mul_aux
-- Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : CommGroup G
A : Finset G
hA : A.Nonempty
B : Finset G
m n : ℕ
hA' : A ∈ A.powerset.erase ∅
C : Finset G
hCmin :
  ∀ x' ∈ A.powerset.erase ∅,
    HDiv.hDiv (α := ℚ≥0) (↑(#(C * B)) : ℚ≥0) (↑(#C) : ℚ≥0) ≤ HDiv.hDiv (α := ℚ≥0) (↑(#(x' * B)) : ℚ≥0) (↑(#x') : ℚ≥0)
hC : C.Nonempty
hCA : C ⊆ A
⊢ (↑(#(C * B ^ m)) : ℚ≥0) ≤ HDiv.hDiv (α := ℚ≥0) (↑(#(C * B)) : ℚ≥0) (↑(#C) : ℚ≥0) ^ m * (↑(#C) : ℚ≥0)

Tactic:
exact card_mul_pow_le (mul_aux hC hCA hCmin) _

Premises used: _private.0.Finset.card_mul_pow_le, _private.0.Finset.mul_aux
-- Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : CommGroup G
A : Finset G
hA : A.Nonempty
B : Finset G
m n : ℕ
hA' : A ∈ A.powerset.erase ∅
C : Finset G
hCmin :
  ∀ x' ∈ A.powerset.erase ∅,
    HDiv.hDiv (α := ℚ≥0) (↑(#(C * B)) : ℚ≥0) (↑(#C) : ℚ≥0) ≤ HDiv.hDiv (α := ℚ≥0) (↑(#(x' * B)) : ℚ≥0) (↑(#x') : ℚ≥0)
hC : C.Nonempty
hCA : C ⊆ A
⊢ (↑(#(C * B ^ n)) : ℚ≥0) ≤ HDiv.hDiv (α := ℚ≥0) (↑(#(C * B)) : ℚ≥0) (↑(#C) : ℚ≥0) ^ n * (↑(#C) : ℚ≥0)

Tactic:
card_mul_pow_le (mul_aux hC hCA hCmin) _

Premises used: _private.0.Finset.card_mul_pow_le, _private.0.Finset.mul_aux
-- Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : CommGroup G
A : Finset G
hA : A.Nonempty
B : Finset G
m n : ℕ
hA' : A ∈ A.powerset.erase ∅
C : Finset G
hCmin :
  ∀ x' ∈ A.powerset.erase ∅,
    HDiv.hDiv (α := ℚ≥0) (↑(#(C * B)) : ℚ≥0) (↑(#C) : ℚ≥0) ≤ HDiv.hDiv (α := ℚ≥0) (↑(#(x' * B)) : ℚ≥0) (↑(#x') : ℚ≥0)
hC : C.Nonempty
hCA : C ⊆ A
⊢ (↑(#(C * B ^ n)) : ℚ≥0) ≤ HDiv.hDiv (α := ℚ≥0) (↑(#(C * B)) : ℚ≥0) (↑(#C) : ℚ≥0) ^ n * (↑(#C) : ℚ≥0)

Tactic:
exact card_mul_pow_le (mul_aux hC hCA hCmin) _

Premises used: _private.0.Finset.card_mul_pow_le, _private.0.Finset.mul_aux
-- Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : CommGroup G
A : Finset G
hA : A.Nonempty
B : Finset G
m n : ℕ
hA' : A ∈ A.powerset.erase ∅
C : Finset G
hCmin :
  ∀ x' ∈ A.powerset.erase ∅,
    HDiv.hDiv (α := ℚ≥0) (↑(#(C * B)) : ℚ≥0) (↑(#C) : ℚ≥0) ≤ HDiv.hDiv (α := ℚ≥0) (↑(#(x' * B)) : ℚ≥0) (↑(#x') : ℚ≥0)
hC : C.Nonempty
hCA : C ⊆ A
⊢ HDiv.hDiv (α := ℚ≥0) (↑(#(C * B)) : ℚ≥0) (↑(#C) : ℚ≥0) ^ m * (↑(#C) : ℚ≥0) *
      (HDiv.hDiv (α := ℚ≥0) (↑(#(C * B)) : ℚ≥0) (↑(#C) : ℚ≥0) ^ n * (↑(#C) : ℚ≥0)) =
    HDiv.hDiv (α := ℚ≥0) (↑(#(C * B)) : ℚ≥0) (↑(#C) : ℚ≥0) ^ (m + n) * (↑(#C) : ℚ≥0) * (↑(#C) : ℚ≥0)

Tactic:
ring
-- Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : CommGroup G
A : Finset G
hA : A.Nonempty
B : Finset G
m n : ℕ
hA' : A ∈ A.powerset.erase ∅
C : Finset G
hCmin :
  ∀ x' ∈ A.powerset.erase ∅,
    HDiv.hDiv (α := ℚ≥0) (↑(#(C * B)) : ℚ≥0) (↑(#C) : ℚ≥0) ≤ HDiv.hDiv (α := ℚ≥0) (↑(#(x' * B)) : ℚ≥0) (↑(#x') : ℚ≥0)
hC : C.Nonempty
hCA : C ⊆ A
bc : HDiv.hDiv (α := ℚ≥0) (↑(#(C * B)) : ℚ≥0) (↑(#C) : ℚ≥0) ≤ HDiv.hDiv (α := ℚ≥0) (↑(#(A * B)) : ℚ≥0) (↑(#A) : ℚ≥0)
⊢ HDiv.hDiv (α := ℚ≥0) (↑(#(C * B)) : ℚ≥0) (↑(#C) : ℚ≥0) ^ (m + n) * (↑(#C) : ℚ≥0) * (↑(#C) : ℚ≥0) ≤
    HDiv.hDiv (α := ℚ≥0) (↑(#(A * B)) : ℚ≥0) (↑(#A) : ℚ≥0) ^ (m + n) * (↑(#A) : ℚ≥0) * (↑(#C) : ℚ≥0)

Tactic:
gcongr (?_ ^ _) * #?_ * _

Premises used: HPow.hPow
-- Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : CommGroup G
A : Finset G
hA : A.Nonempty
B : Finset G
m n : ℕ
hA' : A ∈ A.powerset.erase ∅
C : Finset G
hCmin :
  ∀ x' ∈ A.powerset.erase ∅,
    HDiv.hDiv (α := ℚ≥0) (↑(#(C * B)) : ℚ≥0) (↑(#C) : ℚ≥0) ≤ HDiv.hDiv (α := ℚ≥0) (↑(#(x' * B)) : ℚ≥0) (↑(#x') : ℚ≥0)
hC : C.Nonempty
hCA : C ⊆ A
⊢ HDiv.hDiv (α := ℚ≥0) (↑(#(C * B)) : ℚ≥0) (↑(#C) : ℚ≥0) ≤ HDiv.hDiv (α := ℚ≥0) (↑(#(A * B)) : ℚ≥0) (↑(#A) : ℚ≥0)

Tactic:
hCmin _ hA'
-- Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : CommGroup G
A : Finset G
hA : A.Nonempty
B : Finset G
m n : ℕ
hA' : A ∈ A.powerset.erase ∅
C : Finset G
hCmin :
  ∀ x' ∈ A.powerset.erase ∅,
    HDiv.hDiv (α := ℚ≥0) (↑(#(C * B)) : ℚ≥0) (↑(#C) : ℚ≥0) ≤ HDiv.hDiv (α := ℚ≥0) (↑(#(x' * B)) : ℚ≥0) (↑(#x') : ℚ≥0)
hC : C.Nonempty
hCA : C ⊆ A
⊢ HDiv.hDiv (α := ℚ≥0) (↑(#(C * B)) : ℚ≥0) (↑(#C) : ℚ≥0) ≤ HDiv.hDiv (α := ℚ≥0) (↑(#(A * B)) : ℚ≥0) (↑(#A) : ℚ≥0)

Tactic:
exact hCmin _ hA'
-- Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : CommGroup G
A : Finset G
hA : A.Nonempty
B : Finset G
m n : ℕ
hA' : A ∈ A.powerset.erase ∅
C : Finset G
hCmin :
  ∀ x' ∈ A.powerset.erase ∅,
    HDiv.hDiv (α := ℚ≥0) (↑(#(C * B)) : ℚ≥0) (↑(#C) : ℚ≥0) ≤ HDiv.hDiv (α := ℚ≥0) (↑(#(x' * B)) : ℚ≥0) (↑(#x') : ℚ≥0)
hC : C.Nonempty
hCA : C ⊆ A
m₁ :
  HMul.hMul (α := ℚ≥0) (↑(#(B ^ m * C)) : ℚ≥0) (↑(#(B ^ n * C)) : ℚ≥0) =
    HMul.hMul (α := ℚ≥0) (↑(#(C * B ^ m)) : ℚ≥0) (↑(#(C * B ^ n)) : ℚ≥0)
m₂ :
  HMul.hMul (α := ℚ≥0) (↑(#(C * B ^ m)) : ℚ≥0) (↑(#(C * B ^ n)) : ℚ≥0) ≤
    HDiv.hDiv (α := ℚ≥0) (↑(#(C * B)) : ℚ≥0) (↑(#C) : ℚ≥0) ^ m * (↑(#C) : ℚ≥0) *
      (HDiv.hDiv (α := ℚ≥0) (↑(#(C * B)) : ℚ≥0) (↑(#C) : ℚ≥0) ^ n * (↑(#C) : ℚ≥0))
m₃ :
  HDiv.hDiv (α := ℚ≥0) (↑(#(C * B)) : ℚ≥0) (↑(#C) : ℚ≥0) ^ m * (↑(#C) : ℚ≥0) *
      (HDiv.hDiv (α := ℚ≥0) (↑(#(C * B)) : ℚ≥0) (↑(#C) : ℚ≥0) ^ n * (↑(#C) : ℚ≥0)) =
    HDiv.hDiv (α := ℚ≥0) (↑(#(C * B)) : ℚ≥0) (↑(#C) : ℚ≥0) ^ (m + n) * (↑(#C) : ℚ≥0) * (↑(#C) : ℚ≥0)
m₄ :
  HDiv.hDiv (α := ℚ≥0) (↑(#(C * B)) : ℚ≥0) (↑(#C) : ℚ≥0) ^ (m + n) * (↑(#C) : ℚ≥0) * (↑(#C) : ℚ≥0) ≤
    HDiv.hDiv (α := ℚ≥0) (↑(#(A * B)) : ℚ≥0) (↑(#A) : ℚ≥0) ^ (m + n) * (↑(#A) : ℚ≥0) * (↑(#C) : ℚ≥0)
⊢ HMul.hMul (α := ℚ≥0) (↑(#(B ^ m / B ^ n)) : ℚ≥0) (↑(#C) : ℚ≥0) ≤
    HDiv.hDiv (α := ℚ≥0) (↑(#(A * B)) : ℚ≥0) (↑(#A) : ℚ≥0) ^ (m + n) * (↑(#A) : ℚ≥0) * (↑(#C) : ℚ≥0)

Tactic:
calc
    (#(B ^ m / B ^ n) * #C : ℚ≥0)
      ≤ #(B ^ m * C) * #(B ^ n * C) := mod_cast ruzsa_triangle_inequality_div_mul_mul ..
    _ = #(C * B ^ m) * #(C * B ^ n) := by simp_rw [mul_comm]
    _ ≤ ((#(C * B) / #C) ^ m * #C) * ((#(C * B) / #C : ℚ≥0) ^ n * #C) := by
      gcongr <;> exact card_mul_pow_le (mul_aux hC hCA hCmin) _
    _ = (#(C * B) / #C) ^ (m + n) * #C * #C := by ring
    _ ≤ (#(A * B) / #A) ^ (m + n) * #A * #C := by gcongr (?_ ^ _) * #?_ * _; exact hCmin _ hA'

Premises used: HMul.hMul, HDiv.hDiv, Finset.ruzsa_triangle_inequality_div_mul_mul, Nat.cast, HPow.hPow, HAdd.hAdd, Finset.card