awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.PluenneckeRuzsa (hypothesis)
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : CommGroup G
A B C : Finset G
hB : B.Nonempty
⊢ #(A * C) * #B ≤ #(A * B) * #(B * C)
have hB' : B ∈ B.powerset.erase ∅
Tactic: have hB' : B ∈ B.powerset.erase ∅ := mem_erase_of_ne_of_mem hB.ne_empty (mem_powerset_self _)
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.PluenneckeRuzsa (goal)
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : CommGroup G
A B C : Finset G
hB : B.Nonempty
hB' : B ∈ B.powerset.erase ∅
⊢ #(A * C) * #B ≤ #(A * B) * #(B * C)
have inr : ∀ (U : Finset G) (hU : U ∈ B.powerset.erase ∅)
  (hUA :
    ∀ x' ∈ B.powerset.erase ∅,
      HDiv.hDiv (α := ℚ≥0) (↑(#(U * A)) : ℚ≥0) (↑(#U) : ℚ≥0) ≤
        HDiv.hDiv (α := ℚ≥0) (↑(#(x' * A)) : ℚ≥0) (↑(#x') : ℚ≥0)),
  #(A * C) * #B ≤ #(A * B) * #(B * C)
Tactic: obtain ⟨U, hU, hUA⟩ :=
    exists_min_image (B.powerset.erase ∅) (fun U ↦ #(U * A) / #U : _ → ℚ≥0) ⟨B, hB'⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.PluenneckeRuzsa (hypothesis)
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : CommGroup G
A B C : Finset G
hB : B.Nonempty
hB' : B ∈ B.powerset.erase ∅
U : Finset G
hU : U ∈ B.powerset.erase ∅
hUA :
  ∀ x' ∈ B.powerset.erase ∅,
    HDiv.hDiv (α := ℚ≥0) (↑(#(U * A)) : ℚ≥0) (↑(#U) : ℚ≥0) ≤ HDiv.hDiv (α := ℚ≥0) (↑(#(x' * A)) : ℚ≥0) (↑(#x') : ℚ≥0)
⊢ #(A * C) * #B ≤ #(A * B) * #(B * C)
have hU₁ : U.Nonempty ∧ U ⊆ B
Tactic: rw [mem_erase, mem_powerset, ← nonempty_iff_ne_empty] at hU
Cleared hypotheses: hU, hUA
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.PluenneckeRuzsa (goal)
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : CommGroup G
A B C : Finset G
hB : B.Nonempty
hB' : B ∈ B.powerset.erase ∅
U : Finset G
hU : U.Nonempty ∧ U ⊆ B
hUA :
  ∀ x' ∈ B.powerset.erase ∅,
    HDiv.hDiv (α := ℚ≥0) (↑(#(U * A)) : ℚ≥0) (↑(#U) : ℚ≥0) ≤ HDiv.hDiv (α := ℚ≥0) (↑(#(x' * A)) : ℚ≥0) (↑(#x') : ℚ≥0)
⊢ #(A * C) * #B ≤ #(A * B) * #(B * C)
have inr : LE.le (α := ℚ≥0) (↑(#(A * C) * #B) : ℚ≥0) (↑(#(A * B) * #(B * C)) : ℚ≥0)
Tactic: refine cast_le.1 (?_ : (_ : ℚ≥0) ≤ _)
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.PluenneckeRuzsa (goal)
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : CommGroup G
A B C : Finset G
hB : B.Nonempty
hB' : B ∈ B.powerset.erase ∅
U : Finset G
hU : U.Nonempty ∧ U ⊆ B
hUA :
  ∀ x' ∈ B.powerset.erase ∅,
    HDiv.hDiv (α := ℚ≥0) (↑(#(U * A)) : ℚ≥0) (↑(#U) : ℚ≥0) ≤ HDiv.hDiv (α := ℚ≥0) (↑(#(x' * A)) : ℚ≥0) (↑(#x') : ℚ≥0)
⊢ LE.le (α := ℚ≥0) (↑(#(A * C) * #B) : ℚ≥0) (↑(#(A * B) * #(B * C)) : ℚ≥0)
have inr : HMul.hMul (α := ℚ≥0) (↑(#(A * C)) : ℚ≥0) (↑(#B) : ℚ≥0) ≤ HMul.hMul (α := ℚ≥0) (↑(#(A * B)) : ℚ≥0) (↑(#(B * C)) : ℚ≥0)
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.PluenneckeRuzsa (goal)
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : CommGroup G
A B C : Finset G
hB : B.Nonempty
hB' : B ∈ B.powerset.erase ∅
U : Finset G
hU : U.Nonempty ∧ U ⊆ B
hUA :
  ∀ x' ∈ B.powerset.erase ∅,
    HDiv.hDiv (α := ℚ≥0) (↑(#(U * A)) : ℚ≥0) (↑(#U) : ℚ≥0) ≤ HDiv.hDiv (α := ℚ≥0) (↑(#(x' * A)) : ℚ≥0) (↑(#x') : ℚ≥0)
⊢ HMul.hMul (α := ℚ≥0) (↑(#(A * C)) : ℚ≥0) (↑(#B) : ℚ≥0) ≤ HMul.hMul (α := ℚ≥0) (↑(#(A * B)) : ℚ≥0) (↑(#(B * C)) : ℚ≥0)
have inr : (↑(#(A * C)) : ℚ≥0) ≤ HDiv.hDiv (α := ℚ≥0) (↑(#(B * A)) : ℚ≥0) (↑(#B) : ℚ≥0) * (↑(#(B * C)) : ℚ≥0)
Tactic: rw [← le_div_iff₀ (cast_pos.2 hB.card_pos), mul_div_right_comm, mul_comm _ B]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.PluenneckeRuzsa (goal)
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : CommGroup G
A B C : Finset G
hB : B.Nonempty
hB' : B ∈ B.powerset.erase ∅
U : Finset G
hU : U.Nonempty ∧ U ⊆ B
hUA :
  ∀ x' ∈ B.powerset.erase ∅,
    HDiv.hDiv (α := ℚ≥0) (↑(#(U * A)) : ℚ≥0) (↑(#U) : ℚ≥0) ≤ HDiv.hDiv (α := ℚ≥0) (↑(#(x' * A)) : ℚ≥0) (↑(#x') : ℚ≥0)
⊢ (↑(#(U * (A * C))) : ℚ≥0) ≤ HDiv.hDiv (α := ℚ≥0) (↑(#(U * A)) : ℚ≥0) (↑(#U) : ℚ≥0) * (↑(#(U * C)) : ℚ≥0)
have inr : HMul.hMul (α := ℚ≥0) (↑(#(C * U * A)) : ℚ≥0) (↑(#U) : ℚ≥0) ≤
  HMul.hMul (α := ℚ≥0) (↑(#(U * A)) : ℚ≥0) (↑(#(C * U)) : ℚ≥0)
Tactic: rw [← mul_div_right_comm, ← mul_assoc, le_div_iff₀ (cast_pos.2 hU.1.card_pos), mul_comm _ C,
    ← mul_assoc, mul_comm _ C]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.PluenneckeRuzsa (goal)
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : CommGroup G
A B C : Finset G
⊢ #(A * C) * #B ≤ #(A / B) * #(B / C)
have rw : #(A * C) * #B⁻¹ ≤ #(A * B⁻¹) * #(B⁻¹ * C)
Tactic: rw [div_eq_mul_inv, ← card_inv B, ← card_inv (B / C), inv_div', div_inv_eq_mul]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.PluenneckeRuzsa (goal)
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : CommGroup G
A B C : Finset G
⊢ #(A / C) * #B ≤ #(A * B) * #(B / C)
have rw : #(A * C⁻¹) * #B ≤ #(A * B) * #(B * C⁻¹)
Tactic: rw [div_eq_mul_inv, div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.PluenneckeRuzsa (goal)
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : CommGroup G
A B C : Finset G
⊢ #(A / C) * #B ≤ #(A / B) * #(B * C)
have rw : #(A * C⁻¹) * #B ≤ #(A / B) * #(B / C⁻¹)
Tactic: rw [← div_inv_eq_mul, div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.PluenneckeRuzsa (goal)
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 : ℕ
⊢ (↑(#(A * B ^ n)) : ℚ≥0) ≤ HDiv.hDiv (α := ℚ≥0) (↑(#(A * B)) : ℚ≥0) (↑(#A) : ℚ≥0) ^ n * (↑(#A) : ℚ≥0)
have 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)
Tactic: obtain rfl | hA := A.eq_empty_or_nonempty
Cleared hypotheses: A, hAB
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.PluenneckeRuzsa (goal)
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)
⊢ (↑(#(A * B ^ n)) : ℚ≥0) ≤ HDiv.hDiv (α := ℚ≥0) (↑(#(A * B)) : ℚ≥0) (↑(#A) : ℚ≥0) ^ n * (↑(#A) : ℚ≥0)
have inr : ∀ (hA : A.Nonempty),
  (↑(#(A * B ^ n)) : ℚ≥0) ≤ HDiv.hDiv (α := ℚ≥0) (↑(#(A * B)) : ℚ≥0) (↑(#A) : ℚ≥0) ^ n * (↑(#A) : ℚ≥0)
Tactic: obtain rfl | hA := A.eq_empty_or_nonempty
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.PluenneckeRuzsa (goal)
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 ^ (n + 1))) : ℚ≥0) ≤ HDiv.hDiv (α := ℚ≥0) (↑(#(A * B)) : ℚ≥0) (↑(#A) : ℚ≥0) ^ (n + 1) * (↑(#A) : ℚ≥0)
have 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)
Tactic: refine le_of_mul_le_mul_right ?_ (by positivity : (0 : ℚ≥0) < #A)
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.PluenneckeRuzsa (goal)
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 ^ (n + 1))) : ℚ≥0) (↑(#A) : ℚ≥0) =
    HMul.hMul (α := ℚ≥0) (↑(#(B ^ n * A * B)) : ℚ≥0) (↑(#A) : ℚ≥0)
have rw : HMul.hMul (α := ℚ≥0) (↑(#(A * (B ^ n * B))) : ℚ≥0) (↑(#A) : ℚ≥0) =
  HMul.hMul (α := ℚ≥0) (↑(#(B ^ n * A * B)) : ℚ≥0) (↑(#A) : ℚ≥0)
Tactic: rw [pow_succ, mul_left_comm, mul_assoc]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.PluenneckeRuzsa (goal)
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)
⊢ HMul.hMul (α := ℚ≥0) (↑(#(A * B ^ (n + 1))) : ℚ≥0) (↑(#A) : ℚ≥0) =
    HMul.hMul (α := ℚ≥0) (↑(#(B ^ n * A * B)) : ℚ≥0) (↑(#A) : ℚ≥0)
have rw₁ : HMul.hMul (α := ℚ≥0) (↑(#(B ^ n * (A * B))) : ℚ≥0) (↑(#A) : ℚ≥0) =
  HMul.hMul (α := ℚ≥0) (↑(#(B ^ n * A * B)) : ℚ≥0) (↑(#A) : ℚ≥0)
Tactic: rw [pow_succ, mul_left_comm, mul_assoc]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.PluenneckeRuzsa (goal)
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)
⊢ HMul.hMul (α := ℚ≥0) (↑(#(A * B ^ (n + 1))) : ℚ≥0) (↑(#A) : ℚ≥0) =
    HMul.hMul (α := ℚ≥0) (↑(#(B ^ n * A * B)) : ℚ≥0) (↑(#A) : ℚ≥0)
have rw₂ : HMul.hMul (α := ℚ≥0) (↑(#(B ^ n * (A * B))) : ℚ≥0) (↑(#A) : ℚ≥0) =
  HMul.hMul (α := ℚ≥0) (↑(#(B ^ n * (A * B))) : ℚ≥0) (↑(#A) : ℚ≥0)
Tactic: rw [pow_succ, mul_left_comm, mul_assoc]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.PluenneckeRuzsa (goal)
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) (↑(#(B ^ n * A)) : ℚ≥0) ≤
    (↑(#(A * B)) : ℚ≥0) * (HDiv.hDiv (α := ℚ≥0) (↑(#(A * B)) : ℚ≥0) (↑(#A) : ℚ≥0) ^ n * (↑(#A) : ℚ≥0))
have 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))
Tactic: rw [mul_comm _ A]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.PluenneckeRuzsa (goal)
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 ^ (n + 1))) : ℚ≥0) (↑(#A) : ℚ≥0) ≤
    HDiv.hDiv (α := ℚ≥0) (↑(#(A * B)) : ℚ≥0) (↑(#A) : ℚ≥0) ^ (n + 1) * (↑(#A) : ℚ≥0) * (↑(#A) : ℚ≥0)
have B₁ : HMul.hMul (α := ℚ≥0) (↑(#(A * B ^ (n + 1))) : ℚ≥0) (↑(#A) : ℚ≥0) =
  HMul.hMul (α := ℚ≥0) (↑(#(B ^ n * A * B)) : ℚ≥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]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.PluenneckeRuzsa (goal)
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)
⊢ HMul.hMul (α := ℚ≥0) (↑(#(A * B ^ (n + 1))) : ℚ≥0) (↑(#A) : ℚ≥0) ≤
    HDiv.hDiv (α := ℚ≥0) (↑(#(A * B)) : ℚ≥0) (↑(#A) : ℚ≥0) ^ (n + 1) * (↑(#A) : ℚ≥0) * (↑(#A) : ℚ≥0)
have 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))
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]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.PluenneckeRuzsa (goal)
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))
⊢ HMul.hMul (α := ℚ≥0) (↑(#(A * B ^ (n + 1))) : ℚ≥0) (↑(#A) : ℚ≥0) ≤
    HDiv.hDiv (α := ℚ≥0) (↑(#(A * B)) : ℚ≥0) (↑(#A) : ℚ≥0) ^ (n + 1) * (↑(#A) : ℚ≥0) * (↑(#A) : ℚ≥0)
have 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)
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]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.PluenneckeRuzsa (goal)
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
⊢ (↑(#(A * B ^ n)) : ℚ≥0) ≤ HDiv.hDiv (α := ℚ≥0) (↑(#(A * B)) : ℚ≥0) (↑(#A) : ℚ≥0) ^ n * (↑(#A) : ℚ≥0)
have inr : (↑(#(A * HPow.hPow (β := ℕ) B 0)) : ℚ≥0) ≤
  HPow.hPow (β := ℕ) (HDiv.hDiv (α := ℚ≥0) (↑(#(A * B)) : ℚ≥0) (↑(#A) : ℚ≥0)) 0 * (↑(#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]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.PluenneckeRuzsa (goal)
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)
⊢ (↑(#(A * B ^ n)) : ℚ≥0) ≤ HDiv.hDiv (α := ℚ≥0) (↑(#(A * B)) : ℚ≥0) (↑(#A) : ℚ≥0) ^ n * (↑(#A) : ℚ≥0)
have 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)
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]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.PluenneckeRuzsa (hypothesis)
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : CommGroup G
A : Finset G
hA : A.Nonempty
B : Finset G
m n : ℕ
⊢ (↑(#(B ^ m / B ^ n)) : ℚ≥0) ≤ HDiv.hDiv (α := ℚ≥0) (↑(#(A * B)) : ℚ≥0) (↑(#A) : ℚ≥0) ^ (m + n) * (↑(#A) : ℚ≥0)
have hA' : A ∈ A.powerset.erase ∅
Tactic: have hA' : A ∈ A.powerset.erase ∅ := mem_erase_of_ne_of_mem hA.ne_empty (mem_powerset_self _)
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.PluenneckeRuzsa (goal)
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 ∅
⊢ (↑(#(B ^ m / B ^ n)) : ℚ≥0) ≤ HDiv.hDiv (α := ℚ≥0) (↑(#(A * B)) : ℚ≥0) (↑(#A) : ℚ≥0) ^ (m + n) * (↑(#A) : ℚ≥0)
have 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)
Tactic: obtain ⟨C, hC, hCmin⟩ :=
    exists_min_image (A.powerset.erase ∅) (fun C ↦ #(C * B) / #C : _ → ℚ≥0) ⟨A, hA'⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.PluenneckeRuzsa (hypothesis)
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)
⊢ (↑(#(B ^ m / B ^ n)) : ℚ≥0) ≤ HDiv.hDiv (α := ℚ≥0) (↑(#(A * B)) : ℚ≥0) (↑(#A) : ℚ≥0) ^ (m + n) * (↑(#A) : ℚ≥0)
have hC₁ : C.Nonempty ∧ C ⊆ A
Tactic: rw [mem_erase, mem_powerset, ← nonempty_iff_ne_empty] at hC
Cleared hypotheses: hC, hCmin
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.PluenneckeRuzsa (hypothesis)
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)
⊢ (↑(#(B ^ m / B ^ n)) : ℚ≥0) ≤ HDiv.hDiv (α := ℚ≥0) (↑(#(A * B)) : ℚ≥0) (↑(#A) : ℚ≥0) ^ (m + n) * (↑(#A) : ℚ≥0)
have hC₁ : C.Nonempty
Tactic: obtain ⟨hC, hCA⟩ := hC
Cleared hypotheses: hC
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.PluenneckeRuzsa (hypothesis)
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
⊢ (↑(#(B ^ m / B ^ n)) : ℚ≥0) ≤ HDiv.hDiv (α := ℚ≥0) (↑(#(A * B)) : ℚ≥0) (↑(#A) : ℚ≥0) ^ (m + n) * (↑(#A) : ℚ≥0)
have hCA : C ⊆ A
Tactic: obtain ⟨hC, hCA⟩ := hC
Cleared hypotheses: hC
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.PluenneckeRuzsa (goal)
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
⊢ (↑(#(B ^ m / B ^ n)) : ℚ≥0) ≤ HDiv.hDiv (α := ℚ≥0) (↑(#(A * B)) : ℚ≥0) (↑(#A) : ℚ≥0) ^ (m + n) * (↑(#A) : ℚ≥0)
have 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)
Tactic: refine le_of_mul_le_mul_right ?_ (by positivity : (0 : ℚ≥0) < #C)
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.PluenneckeRuzsa (goal)
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) (↑(#(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))
have h₁ : (↑(#(C * B ^ m)) : ℚ≥0) ≤ HDiv.hDiv (α := ℚ≥0) (↑(#(C * B)) : ℚ≥0) (↑(#C) : ℚ≥0) ^ m * (↑(#C) : ℚ≥0)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.PluenneckeRuzsa (goal)
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)
⊢ 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))
have h₂ : (↑(#(C * B ^ n)) : ℚ≥0) ≤ HDiv.hDiv (α := ℚ≥0) (↑(#(C * B)) : ℚ≥0) (↑(#C) : ℚ≥0) ^ n * (↑(#C) : ℚ≥0)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.PluenneckeRuzsa (goal)
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 + n) * (↑(#C) : ℚ≥0) * (↑(#C) : ℚ≥0) ≤
    HDiv.hDiv (α := ℚ≥0) (↑(#(A * B)) : ℚ≥0) (↑(#A) : ℚ≥0) ^ (m + n) * (↑(#A) : ℚ≥0) * (↑(#C) : ℚ≥0)
have bc : HDiv.hDiv (α := ℚ≥0) (↑(#(C * B)) : ℚ≥0) (↑(#C) : ℚ≥0) ≤ HDiv.hDiv (α := ℚ≥0) (↑(#(A * B)) : ℚ≥0) (↑(#A) : ℚ≥0)
Tactic: gcongr (?_ ^ _) * #?_ * _
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.PluenneckeRuzsa (goal)
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) ≤
    HDiv.hDiv (α := ℚ≥0) (↑(#(A * B)) : ℚ≥0) (↑(#A) : ℚ≥0) ^ (m + n) * (↑(#A) : ℚ≥0) * (↑(#C) : ℚ≥0)
have m₁ : HMul.hMul (α := ℚ≥0) (↑(#(B ^ m * C)) : ℚ≥0) (↑(#(B ^ n * C)) : ℚ≥0) =
  HMul.hMul (α := ℚ≥0) (↑(#(C * B ^ m)) : ℚ≥0) (↑(#(C * B ^ n)) : ℚ≥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'