awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : Group G
A B : Finset G
hA : ∀ A' ⊆ A, #(A * B) * #A' ≤ #(A' * B) * #A
x : G
C : Finset G
h : x ∉ C
ih : #(C * A * B) * #A ≤ #(A * B) * #(C * A)
A' : Finset G := A ∩ ({x}⁻¹ * C * A)
hA' : A' = A ∩ ({x}⁻¹ * C * A)
C' : Finset G := insert x C
hC' : C' = insert x C
h₀ : {x} * A' = {x} * A ∩ (C * A)
h₁ : C' * A * B = C * A * B ∪ ({x} * A * B) \ ({x} * A' * B)
h₂ : {x} * A' * B ⊆ {x} * A * B
⊢ #(C * A * B ∪ ({x} * A * B) \ ({x} * A' * B)) ≤ #(C * A * B) + #(A * B) - #(A' * B)

Tactic:
(card_union_le _ _).trans_eq ?_

Premises used: LE.le.trans_eq, Finset.card_union_le
-- Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : Group G
A B : Finset G
hA : ∀ A' ⊆ A, #(A * B) * #A' ≤ #(A' * B) * #A
x : G
C : Finset G
h : x ∉ C
ih : #(C * A * B) * #A ≤ #(A * B) * #(C * A)
A' : Finset G := A ∩ ({x}⁻¹ * C * A)
hA' : A' = A ∩ ({x}⁻¹ * C * A)
C' : Finset G := insert x C
hC' : C' = insert x C
h₀ : {x} * A' = {x} * A ∩ (C * A)
h₁ : C' * A * B = C * A * B ∪ ({x} * A * B) \ ({x} * A' * B)
h₂ : {x} * A' * B ⊆ {x} * A * B
bc : #(C * A * B) + #(({x} * A * B) \ ({x} * A' * B)) = #(C * A * B) + #(A * B) - #(A' * B)
⊢ #(C * A * B ∪ ({x} * A * B) \ ({x} * A' * B)) ≤ #(C * A * B) + #(A * B) - #(A' * B)

Tactic:
refine (card_union_le _ _).trans_eq ?_

Premises used: LE.le.trans_eq, Finset.card_union_le
-- Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : Group G
A B : Finset G
hA : ∀ A' ⊆ A, #(A * B) * #A' ≤ #(A' * B) * #A
x : G
C : Finset G
h : x ∉ C
ih : #(C * A * B) * #A ≤ #(A * B) * #(C * A)
A' : Finset G := A ∩ ({x}⁻¹ * C * A)
hA' : A' = A ∩ ({x}⁻¹ * C * A)
C' : Finset G := insert x C
hC' : C' = insert x C
h₀ : {x} * A' = {x} * A ∩ (C * A)
h₁ : C' * A * B = C * A * B ∪ ({x} * A * B) \ ({x} * A' * B)
h₂ : {x} * A' * B ⊆ {x} * A * B
bc : #(C * A * B) + (#({x} * A * B) - #({x} * A' * B)) = #(C * A * B) + #(A * B) - #(A' * B)
bc₁ : #(C * A * B) + #({x} * A * B) - #({x} * A' * B) = #(C * A * B) + #(A * B) - #(A' * B)
bc₂ : #(C * A * B) + #({x} * (A * B)) - #({x} * A' * B) = #(C * A * B) + #(A * B) - #(A' * B)
bc₃ : #(C * A * B) + #({x} * (A * B)) - #({x} * (A' * B)) = #(C * A * B) + #(A * B) - #(A' * B)
bc₄ : #(C * A * B) + #(A * B) - #({x} * (A' * B)) = #(C * A * B) + #(A * B) - #(A' * B)
bc₅ bc₆ : #(C * A * B) + #(A * B) - #(A' * B) = #(C * A * B) + #(A * B) - #(A' * B)
⊢ #(C * A * B) + #(({x} * A * B) \ ({x} * A' * B)) = #(C * A * B) + #(A * B) - #(A' * B)

Tactic:
rw [card_sdiff_of_subset h₂, ← add_tsub_assoc_of_le (card_le_card h₂), mul_assoc {_},
          mul_assoc {_}, card_singleton_mul, card_singleton_mul]

Premises used: add_tsub_assoc_of_le, Finset.card_le_card, Finset.card_sdiff_of_subset, mul_assoc, Singleton.singleton, Finset.card_singleton_mul
-- Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : Group G
A B : Finset G
hA : ∀ A' ⊆ A, #(A * B) * #A' ≤ #(A' * B) * #A
x : G
C : Finset G
h : x ∉ C
ih : #(C * A * B) * #A ≤ #(A * B) * #(C * A)
A' : Finset G := A ∩ ({x}⁻¹ * C * A)
hA' : A' = A ∩ ({x}⁻¹ * C * A)
C' : Finset G := insert x C
hC' : C' = insert x C
h₀ : {x} * A' = {x} * A ∩ (C * A)
h₁ : C' * A * B = C * A * B ∪ ({x} * A * B) \ ({x} * A' * B)
h₂ : {x} * A' * B ⊆ {x} * A * B
rw : (#(C * A * B) + #(A * B)) * #A - #(A' * B) * #A = #(C * A * B) * #A + #(A * B) * #A - #(A' * B) * #A
rw₁ rw₂ : #(C * A * B) * #A + #(A * B) * #A - #(A' * B) * #A = #(C * A * B) * #A + #(A * B) * #A - #(A' * B) * #A
⊢ (#(C * A * B) + #(A * B) - #(A' * B)) * #A = #(C * A * B) * #A + #(A * B) * #A - #(A' * B) * #A

Tactic:
rw [tsub_mul, add_mul]

Premises used: add_mul, tsub_mul
-- Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : Group G
A B : Finset G
hA : ∀ A' ⊆ A, #(A * B) * #A' ≤ #(A' * B) * #A
x : G
C : Finset G
h : x ∉ C
ih : #(C * A * B) * #A ≤ #(A * B) * #(C * A)
A' : Finset G := A ∩ ({x}⁻¹ * C * A)
hA' : A' = A ∩ ({x}⁻¹ * C * A)
C' : Finset G := insert x C
hC' : C' = insert x C
h₀ : {x} * A' = {x} * A ∩ (C * A)
h₁ : C' * A * B = C * A * B ∪ ({x} * A * B) \ ({x} * A' * B)
h₂ : {x} * A' * B ⊆ {x} * A * B
hcd : #(A * B) * #(A ∩ ({x}⁻¹ * C * A)) ≤ #(A' * B) * #A
⊢ #(C * A * B) * #A + #(A * B) * #A - #(A' * B) * #A ≤
    #(A * B) * #(C * A) + #(A * B) * #A - #(A * B) * #(A ∩ ({x}⁻¹ * C * A))

Tactic:
gcongr ?_ + _ - ?_
-- Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : Group G
A B : Finset G
hA : ∀ A' ⊆ A, #(A * B) * #A' ≤ #(A' * B) * #A
x : G
C : Finset G
h : x ∉ C
ih : #(C * A * B) * #A ≤ #(A * B) * #(C * A)
A' : Finset G := A ∩ ({x}⁻¹ * C * A)
hA' : A' = A ∩ ({x}⁻¹ * C * A)
C' : Finset G := insert x C
hC' : C' = insert x C
h₀ : {x} * A' = {x} * A ∩ (C * A)
h₁ : C' * A * B = C * A * B ∪ ({x} * A * B) \ ({x} * A' * B)
h₂ : {x} * A' * B ⊆ {x} * A * B
⊢ #(A * B) * #(A ∩ ({x}⁻¹ * C * A)) ≤ #(A' * B) * #A

Tactic:
hA _ inter_subset_left

Premises used: Finset.inter_subset_left
-- Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : Group G
A B : Finset G
hA : ∀ A' ⊆ A, #(A * B) * #A' ≤ #(A' * B) * #A
x : G
C : Finset G
h : x ∉ C
ih : #(C * A * B) * #A ≤ #(A * B) * #(C * A)
A' : Finset G := A ∩ ({x}⁻¹ * C * A)
hA' : A' = A ∩ ({x}⁻¹ * C * A)
C' : Finset G := insert x C
hC' : C' = insert x C
h₀ : {x} * A' = {x} * A ∩ (C * A)
h₁ : C' * A * B = C * A * B ∪ ({x} * A * B) \ ({x} * A' * B)
h₂ : {x} * A' * B ⊆ {x} * A * B
⊢ #(A * B) * #(A ∩ ({x}⁻¹ * C * A)) ≤ #(A' * B) * #A

Tactic:
exact hA _ inter_subset_left

Premises used: Finset.inter_subset_left
-- Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : Group G
A B : Finset G
hA : ∀ A' ⊆ A, #(A * B) * #A' ≤ #(A' * B) * #A
x : G
C : Finset G
h : x ∉ C
ih : #(C * A * B) * #A ≤ #(A * B) * #(C * A)
A' : Finset G := A ∩ ({x}⁻¹ * C * A)
hA' : A' = A ∩ ({x}⁻¹ * C * A)
C' : Finset G := insert x C
hC' : C' = insert x C
h₀ : {x} * A' = {x} * A ∩ (C * A)
h₁ : C' * A * B = C * A * B ∪ ({x} * A * B) \ ({x} * A' * B)
h₂ : {x} * A' * B ⊆ {x} * A * B
rw : #(A * B) * (#(C * A) + #A) - #(A * B) * #(A ∩ ({x}⁻¹ * C * A)) = #(A * B) * #(C' * A)
rw₁ : #(A * B) * (#(C * A) + #A - #(A ∩ ({x}⁻¹ * C * A))) = #(A * B) * #(C' * A)
rw₂ : #(A * B) * (#(C * A) + #A - #A') = #(A * B) * #(C' * A)
rw₃ : #(A * B) * (#(C * A) + #A - #A') = #(A * B) * #(insert x C * A)
rw₄ : #(A * B) * (#(C * A) + #A - #A') = #(A * B) * #(({x} ∪ C) * A)
rw₅ : #(A * B) * (#(C * A) + #A - #A') = #(A * B) * #({x} * A ∪ C * A)
rw₆ : #(A * B) * (#(C * A) + #({x} * A) - #A') = #(A * B) * #({x} * A ∪ C * A)
rw₇ : #(A * B) * (#(C * A) + #({x} * A) - #({x} * A')) = #(A * B) * #({x} * A ∪ C * A)
rw₈ : #(A * B) * (#({x} * A) + #(C * A) - #({x} * A')) = #(A * B) * #({x} * A ∪ C * A)
rw₉ : #(A * B) * (#({x} * A) + #(C * A) - #({x} * A ∩ (C * A))) = #(A * B) * #({x} * A ∪ C * A)
rw₁₀ rw₁₁ :
  #(A * B) * (#({x} * A) + #(C * A) - #({x} * A ∩ (C * A))) = #(A * B) * (#({x} * A) + #(C * A) - #({x} * A ∩ (C * A)))
⊢ #(A * B) * #(C * A) + #(A * B) * #A - #(A * B) * #(A ∩ ({x}⁻¹ * C * A)) = #(A * B) * #(C' * A)

Tactic:
rw [← mul_add, ← mul_tsub, ← hA', hC', insert_eq, union_mul, ← card_singleton_mul x A,
          ← card_singleton_mul x A', add_comm #_, h₀,
          eq_tsub_of_add_eq (card_union_add_card_inter _ _)]

Premises used: Finset.union_mul, Finset.insert_eq, Finset.card_union_add_card_inter, add_comm, eq_tsub_of_add_eq, Finset.card, mul_add, Finset.card_singleton_mul, mul_tsub
-- Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : Group G
A B : Finset G
hA : ∀ A' ⊆ A, #(A * B) * #A' ≤ #(A' * B) * #A
x : G
C : Finset G
h : x ∉ C
ih : #(C * A * B) * #A ≤ #(A * B) * #(C * A)
A' : Finset G := A ∩ ({x}⁻¹ * C * A)
hA' : A' = A ∩ ({x}⁻¹ * C * A)
C' : Finset G := insert x C
hC' : C' = insert x C
h₀ : {x} * A' = {x} * A ∩ (C * A)
h₁ : C' * A * B = C * A * B ∪ ({x} * A * B) \ ({x} * A' * B)
h₂ : {x} * A' * B ⊆ {x} * A * B
A₁ : #(C' * A * B) * #A ≤ (#(C * A * B) + #(A * B) - #(A' * B)) * #A
A₂ : (#(C * A * B) + #(A * B) - #(A' * B)) * #A = #(C * A * B) * #A + #(A * B) * #A - #(A' * B) * #A
A₃ :
  #(C * A * B) * #A + #(A * B) * #A - #(A' * B) * #A ≤
    #(A * B) * #(C * A) + #(A * B) * #A - #(A * B) * #(A ∩ ({x}⁻¹ * C * A))
A₄ : #(A * B) * #(C * A) + #(A * B) * #A - #(A * B) * #(A ∩ ({x}⁻¹ * C * A)) = #(A * B) * #(C' * A)
⊢ #(C' * A * B) * #A ≤ #(A * B) * #(C' * A)

Tactic:
calc
      #(C' * A * B) * #A
      _ ≤ (#(C * A * B) + #(A * B) - #(A' * B)) * #A := by
        gcongr
        rw [h₁]
        refine (card_union_le _ _).trans_eq ?_
        rw [card_sdiff_of_subset h₂, ← add_tsub_assoc_of_le (card_le_card h₂), mul_assoc {_},
          mul_assoc {_}, card_singleton_mul, card_singleton_mul]
      _ = #(C * A * B) * #A + #(A * B) * #A - #(A' * B) * #A := by rw [tsub_mul, add_mul]
      _ ≤ #(A * B) * #(C * A) + #(A * B) * #A - #(A * B) * #(A ∩ ({x}⁻¹ * C * A)) := by
        gcongr ?_ + _ - ?_; exact hA _ inter_subset_left
      _ = #(A * B) * #(C' * A) := by
        rw [← mul_add, ← mul_tsub, ← hA', hC', insert_eq, union_mul, ← card_singleton_mul x A,
          ← card_singleton_mul x A', add_comm #_, h₀,
          eq_tsub_of_add_eq (card_union_add_card_inter _ _)]

Premises used: HMul.hMul, HSub.hSub, Inter.inter, Inv.inv, HAdd.hAdd, Finset.card
-- Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : Group G
A B C : Finset G
hA : ∀ A' ⊆ A, #(A * B) * #A' ≤ #(A' * B) * #A
empty : #(∅ * A * B) * #A ≤ #(A * B) * #(∅ * A)
insert :
  ∀ (x : G) (C : Finset G),
    x ∉ C →
      ∀ (ih : #(C * A * B) * #A ≤ #(A * B) * #(C * A)),
        #(Insert.insert x C * A * B) * #A ≤ #(A * B) * #(Insert.insert x C * A)
⊢ #(C * A * B) * #A ≤ #(A * B) * #(C * A)

Tactic:
induction C using Finset.induction_on with
  | empty => simp
  | insert x C _ ih =>
    set A' := A ∩ ({x}⁻¹ * C * A) with hA'
    set C' := insert x C with hC'
    have h₀ : {x} * A' = {x} * A ∩ (C * A) := by
      rw [hA', mul_assoc, singleton_mul_inter, (isUnit_singleton x).mul_inv_cancel_left]
    have h₁ : C' * A * B = C * A * B ∪ ({x} * A * B) \ ({x} * A' * B) := by
      rw [hC', insert_eq, union_comm, union_mul, union_mul]
      refine (sup_sdiff_eq_sup ?_).symm
      rw [h₀]
      gcongr
      exact inter_subset_right
    have h₂ : {x} * A' * B ⊆ {x} * A * B := by gcongr; exact inter_subset_left
    calc
      #(C' * A * B) * #A
      _ ≤ (#(C * A * B) + #(A * B) - #(A' * B)) * #A := by
        gcongr
        rw [h₁]
        refine (card_union_le _ _).trans_eq ?_
        rw [card_sdiff_of_subset h₂, ← add_tsub_assoc_of_le (card_le_card h₂), mul_assoc {_},
          mul_assoc {_}, card_singleton_mul, card_singleton_mul]
      _ = #(C * A * B) * #A + #(A * B) * #A - #(A' * B) * #A := by rw [tsub_mul, add_mul]
      _ ≤ #(A * B) * #(C * A) + #(A * B) * #A - #(A * B) * #(A ∩ ({x}⁻¹ * C * A)) := by
        gcongr ?_ + _ - ?_; exact hA _ inter_subset_left
      _ = #(A * B) * #(C' * A) := by
        rw [← mul_add, ← mul_tsub, ← hA', hC', insert_eq, union_mul, ← card_singleton_mul x A,
          ← card_singleton_mul x A', add_comm #_, h₀,
          eq_tsub_of_add_eq (card_union_add_card_inter _ _)]

Premises used: HMul.hMul, Insert.insert, Inter.inter, Inv.inv
-- Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : CommGroup G
A B C : Finset G
hA : A.Nonempty
hAB : A ⊆ B
h :
  ∀ A' ∈ B.powerset.erase ∅,
    HDiv.hDiv (α := ℚ≥0) (↑(#(A * C)) : ℚ≥0) (↑(#A) : ℚ≥0) ≤ HDiv.hDiv (α := ℚ≥0) (↑(#(A' * C)) : ℚ≥0) (↑(#A') : ℚ≥0)
A' : Finset G
hAA' : A' ⊆ A
inl : ∀ (hAA' : ∅ ⊆ A), #(A * C) * card.{u_1} (α := G) ∅ ≤ #(∅ * C) * #A
inr : ∀ (hA' : A'.Nonempty), #(A * C) * #A' ≤ #(A' * C) * #A
⊢ #(A * C) * #A' ≤ #(A' * C) * #A

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
A B C : Finset G
hA : A.Nonempty
hAB : A ⊆ B
h :
  ∀ A' ∈ B.powerset.erase ∅,
    HDiv.hDiv (α := ℚ≥0) (↑(#(A * C)) : ℚ≥0) (↑(#A) : ℚ≥0) ≤ HDiv.hDiv (α := ℚ≥0) (↑(#(A' * C)) : ℚ≥0) (↑(#A') : ℚ≥0)
hAA' : ∅ ⊆ A
⊢ #(A * C) * card.{u_1} (α := G) ∅ ≤ #(∅ * C) * #A

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

Tactic:
have hA₀ : (0 : ℚ≥0) < #A := cast_pos.2 hA.card_pos
-- Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : CommGroup G
A B C : Finset G
hA : A.Nonempty
hAB : A ⊆ B
h :
  ∀ A' ∈ B.powerset.erase ∅,
    HDiv.hDiv (α := ℚ≥0) (↑(#(A * C)) : ℚ≥0) (↑(#A) : ℚ≥0) ≤ HDiv.hDiv (α := ℚ≥0) (↑(#(A' * C)) : ℚ≥0) (↑(#A') : ℚ≥0)
A' : Finset G
hAA' : A' ⊆ A
hA' : A'.Nonempty
hA₀ : LT.lt (α := ℚ≥0) 0 (↑(#A) : ℚ≥0)
⊢ LT.lt (α := ℚ≥0) 0 (↑(#A') : ℚ≥0)

Tactic:
have hA₀' : (0 : ℚ≥0) < #A' := cast_pos.2 hA'.card_pos
-- Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : CommGroup G
A B C : Finset G
hA : A.Nonempty
hAB : A ⊆ B
h :
  ∀ A' ∈ B.powerset.erase ∅,
    HDiv.hDiv (α := ℚ≥0) (↑(#(A * C)) : ℚ≥0) (↑(#A) : ℚ≥0) ≤ HDiv.hDiv (α := ℚ≥0) (↑(#(A' * C)) : ℚ≥0) (↑(#A') : ℚ≥0)
A' : Finset G
hAA' : A' ⊆ A
hA' : A'.Nonempty
hA₀ : LT.lt (α := ℚ≥0) 0 (↑(#A) : ℚ≥0)
hA₀' : LT.lt (α := ℚ≥0) 0 (↑(#A') : ℚ≥0)
⊢ #(A * C) * #A' ≤ #(A' * C) * #A

Tactic:
mod_cast
    (div_le_div_iff₀ hA₀ hA₀').1
      (h _ <| mem_erase_of_ne_of_mem hA'.ne_empty <| mem_powerset.2 <| hAA'.trans hAB)

Premises used: Nat.cast_mul._simp_1, Iff.mpr, HMul.hMul, congrArg, cast, HasSubset.Subset.trans, Finset.mem_erase_of_ne_of_mem, Nat.cast_le._simp_1, LE.le, Finset.mem_powerset, Finset.Nonempty.ne_empty, div_le_div_iff₀, congr, Iff.mp, Finset.card, Eq.trans
-- Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : CommGroup G
A B C : Finset G
hA : A.Nonempty
hAB : A ⊆ B
h :
  ∀ A' ∈ B.powerset.erase ∅,
    HDiv.hDiv (α := ℚ≥0) (↑(#(A * C)) : ℚ≥0) (↑(#A) : ℚ≥0) ≤ HDiv.hDiv (α := ℚ≥0) (↑(#(A' * C)) : ℚ≥0) (↑(#A') : ℚ≥0)
A' : Finset G
hAA' : A' ⊆ A
hA' : A'.Nonempty
hA₀ : LT.lt (α := ℚ≥0) 0 (↑(#A) : ℚ≥0)
hA₀' : LT.lt (α := ℚ≥0) 0 (↑(#A') : ℚ≥0)
⊢ #(A * C) * #A' ≤ #(A' * C) * #A

Tactic:
exact mod_cast
    (div_le_div_iff₀ hA₀ hA₀').1
      (h _ <| mem_erase_of_ne_of_mem hA'.ne_empty <| mem_powerset.2 <| hAA'.trans hAB)

Premises used: Iff.mpr, HasSubset.Subset.trans, Finset.mem_erase_of_ne_of_mem, Finset.mem_powerset, Finset.Nonempty.ne_empty, div_le_div_iff₀, Iff.mp
-- Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : CommGroup G
A B C : Finset G
inl : #(A * C) * card.{u_1} (α := G) ∅ ≤ #(A * ∅) * #(∅ * C)
inr : ∀ (hB : B.Nonempty), #(A * C) * #B ≤ #(A * B) * #(B * C)
⊢ #(A * C) * #B ≤ #(A * B) * #(B * C)

Tactic:
obtain rfl | hB := B.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
A C : Finset G
⊢ #(A * C) * card.{u_1} (α := G) ∅ ≤ #(A * ∅) * #(∅ * C)

Tactic:
simp
-- Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa
Goal:
G : Type u_1
inst : DecidableEq G
inst_1 : CommGroup G
A B C : Finset G
hB : B.Nonempty
⊢ B ∈ B.powerset.erase ∅

Tactic:
have hB' : B ∈ B.powerset.erase ∅ := mem_erase_of_ne_of_mem hB.ne_empty (mem_powerset_self _)
-- Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa
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 ∅
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)
⊢ #(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'⟩

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 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)
⊢ U.Nonempty ∧ U ⊆ B

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

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 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)
hU₁ : U.Nonempty ∧ U ⊆ B
⊢ ∀ x' ∈ B.powerset.erase ∅,
    HDiv.hDiv (α := ℚ≥0) (↑(#(U * A)) : ℚ≥0) (↑(#U) : ℚ≥0) ≤ HDiv.hDiv (α := ℚ≥0) (↑(#(x' * A)) : ℚ≥0) (↑(#x') : ℚ≥0)

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

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 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)

Tactic:
cast_le.1 (?_ : (_ : ℚ≥0) ≤ _)

Premises used: Iff.mp, Nat.cast_le
-- Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa
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)
inr : LE.le (α := ℚ≥0) (↑(#(A * C) * #B) : ℚ≥0) (↑(#(A * B) * #(B * C)) : ℚ≥0)
⊢ #(A * C) * #B ≤ #(A * B) * #(B * C)

Tactic:
refine cast_le.1 (?_ : (_ : ℚ≥0) ≤ _)

Premises used: Iff.mp, Nat.cast_le
-- Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa
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)
inr :
  HMul.hMul (α := ℚ≥0) (↑(#(A * C)) : ℚ≥0) (↑(#B) : ℚ≥0) ≤ HMul.hMul (α := ℚ≥0) (↑(#(A * B)) : ℚ≥0) (↑(#(B * C)) : ℚ≥0)
⊢ LE.le (α := ℚ≥0) (↑(#(A * C) * #B) : ℚ≥0) (↑(#(A * B) * #(B * C)) : ℚ≥0)

Tactic:
push_cast
-- Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa
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)
inr : (↑(#(A * C)) : ℚ≥0) ≤ HDiv.hDiv (α := ℚ≥0) (↑(#(B * A)) : ℚ≥0) (↑(#B) : ℚ≥0) * (↑(#(B * C)) : ℚ≥0)
⊢ HMul.hMul (α := ℚ≥0) (↑(#(A * C)) : ℚ≥0) (↑(#B) : ℚ≥0) ≤ HMul.hMul (α := ℚ≥0) (↑(#(A * B)) : ℚ≥0) (↑(#(B * C)) : ℚ≥0)

Tactic:
rw [← le_div_iff₀ (cast_pos.2 hB.card_pos), mul_div_right_comm, mul_comm _ B]

Premises used: mul_div_right_comm, mul_comm, le_div_iff₀
-- Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa
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)
inr :
  HMul.hMul (α := ℚ≥0) (↑(#(C * U * A)) : ℚ≥0) (↑(#U) : ℚ≥0) ≤
    HMul.hMul (α := ℚ≥0) (↑(#(U * A)) : ℚ≥0) (↑(#(C * U)) : ℚ≥0)
⊢ (↑(#(U * (A * C))) : ℚ≥0) ≤ HDiv.hDiv (α := ℚ≥0) (↑(#(U * A)) : ℚ≥0) (↑(#U) : ℚ≥0) * (↑(#(U * C)) : ℚ≥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]

Premises used: mul_assoc, mul_div_right_comm, mul_comm, le_div_iff₀
-- Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa
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) (↑(#(C * U * A)) : ℚ≥0) (↑(#U) : ℚ≥0) ≤
    HMul.hMul (α := ℚ≥0) (↑(#(U * A)) : ℚ≥0) (↑(#(C * U)) : ℚ≥0)

Tactic:
mod_cast pluennecke_petridis_inequality_mul C (mul_aux hU.1 hU.2 hUA)

Premises used: Nat.cast_mul._simp_1, HMul.hMul, congrArg, cast, Nat.cast_le._simp_1, LE.le, And.right, And.left, congr, Finset.card, Eq.symm, Finset.pluennecke_petridis_inequality_mul, Eq.trans, _private.0.Finset.mul_aux
-- Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa
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) (↑(#(C * U * A)) : ℚ≥0) (↑(#U) : ℚ≥0) ≤
    HMul.hMul (α := ℚ≥0) (↑(#(U * A)) : ℚ≥0) (↑(#(C * U)) : ℚ≥0)

Tactic:
exact mod_cast pluennecke_petridis_inequality_mul C (mul_aux hU.1 hU.2 hUA)

Premises used: And.right, And.left, Finset.pluennecke_petridis_inequality_mul, _private.0.Finset.mul_aux
-- 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_eq_mul_inv, ← card_inv B, ← card_inv (B / C), inv_div', div_inv_eq_mul]

Premises used: Finset.card_inv, HDiv.hDiv, div_eq_mul_inv, inv_div', 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_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
⊢ #(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_eq_mul_inv, div_eq_mul_inv]

Premises used: div_eq_mul_inv
-- 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_mul_mul _ _ _

Premises used: Finset.ruzsa_triangle_inequality_mul_mul_mul