-- Mathlib/Combinatorics/Additive/PluenneckeRuzsa.lean
theorem pluennecke_petridis_inequality_mul (C : Finset G)
    (hA : ∀ A' ⊆ A, #(A * B) * #A' ≤ #(A' * B) * #A) :
    #(A * B * C) * #A ≤ #(A * B) * #(A * C)

Proof state:
case insert
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : CommGroup G
A B : Finset G
hA : ∀ A' ⊆ A, #(A * B) * #A' ≤ #(A' * B) * #A
x : G
C : Finset G
a✝ : x ∉ C
ih : #(A * B * C) * #A ≤ #(A * B) * #(A * C)
A' : Finset G := A ∩ (A * C / {x})
hA' : A' = A ∩ (A * C / {x})
⊢ #(A * B * insert x C) * #A ≤ #(A * B) * #(A * insert x C)

Tactic:
set C' := insert x C with hC'

Result:
case insert
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : CommGroup G
A B : Finset G
hA : ∀ A' ⊆ A, #(A * B) * #A' ≤ #(A' * B) * #A
x : G
C : Finset G
a✝ : x ∉ C
ih : #(A * B * C) * #A ≤ #(A * B) * #(A * C)
A' : Finset G := A ∩ (A * C / {x})
hA' : A' = A ∩ (A * C / {x})
C' : Finset G := insert x C
hC' : C' = insert x C
⊢ #(A * B * C') * #A ≤ #(A * B) * #(A * C')

Proof state:
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : CommGroup G
A B : Finset G
hA : ∀ A' ⊆ A, #(A * B) * #A' ≤ #(A' * B) * #A
x : G
C : Finset G
a✝ : x ∉ C
ih : #(A * B * C) * #A ≤ #(A * B) * #(A * C)
A' : Finset G := A ∩ (A * C / {x})
hA' : A' = A ∩ (A * C / {x})
C' : Finset G := insert x C
hC' : C' = insert x C
h₀ : A' * {x} = A * {x} ∩ (A * C)
⊢ A * B * C ∪ A * B * {x} = A * B * C ∪ (A * B * {x}) \ (A' * B * {x})

Tactic:
refine (sup_sdiff_eq_sup ?_).symm

Result:
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : CommGroup G
A B : Finset G
hA : ∀ A' ⊆ A, #(A * B) * #A' ≤ #(A' * B) * #A
x : G
C : Finset G
a✝ : x ∉ C
ih : #(A * B * C) * #A ≤ #(A * B) * #(A * C)
A' : Finset G := A ∩ (A * C / {x})
hA' : A' = A ∩ (A * C / {x})
C' : Finset G := insert x C
hC' : C' = insert x C
h₀ : A' * {x} = A * {x} ∩ (A * C)
⊢ A' * B * {x} ≤ A * B * C

Proof state:
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : CommGroup G
A B : Finset G
hA : ∀ A' ⊆ A, #(A * B) * #A' ≤ #(A' * B) * #A
x : G
C : Finset G
a✝ : x ∉ C
ih : #(A * B * C) * #A ≤ #(A * B) * #(A * C)
A' : Finset G := A ∩ (A * C / {x})
hA' : A' = A ∩ (A * C / {x})
C' : Finset G := insert x C
hC' : C' = insert x C
⊢ A' * {x} = A * {x} ∩ (A * C)

Tactic:
rw [hA', inter_mul_singleton, (isUnit_singleton x).div_mul_cancel]

Result:
no goals

Proof state:
case insert
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : CommGroup G
A B : Finset G
hA : ∀ A' ⊆ A, #(A * B) * #A' ≤ #(A' * B) * #A
x : G
C : Finset G
a✝ : x ∉ C
ih : #(A * B * C) * #A ≤ #(A * B) * #(A * C)
A' : Finset G := A ∩ (A * C / {x})
hA' : A' = A ∩ (A * C / {x})
C' : Finset G := insert x C
hC' : C' = insert x C
h₀ : A' * {x} = A * {x} ∩ (A * C)
h₁ : A * B * C' = A * B * C ∪ (A * B * {x}) \ (A' * B * {x})
h₂ : A' * B * {x} ⊆ A * B * {x}
⊢ #(A * B * C') * #A ≤ #(A * B) * #(A * C')

Tactic:
have h₃ : #(A * B * C') ≤ #(A * B * C) + #(A * B) - #(A' * B) := by
  rw [h₁]
  refine (card_union_le _ _).trans_eq ?_
  rw [card_sdiff h₂, ← add_tsub_assoc_of_le (card_le_card h₂), card_mul_singleton,
    card_mul_singleton]

Result:
case insert
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : CommGroup G
A B : Finset G
hA : ∀ A' ⊆ A, #(A * B) * #A' ≤ #(A' * B) * #A
x : G
C : Finset G
a✝ : x ∉ C
ih : #(A * B * C) * #A ≤ #(A * B) * #(A * C)
A' : Finset G := A ∩ (A * C / {x})
hA' : A' = A ∩ (A * C / {x})
C' : Finset G := insert x C
hC' : C' = insert x C
h₀ : A' * {x} = A * {x} ∩ (A * C)
h₁ : A * B * C' = A * B * C ∪ (A * B * {x}) \ (A' * B * {x})
h₂ : A' * B * {x} ⊆ A * B * {x}
h₃ : #(A * B * C') ≤ #(A * B * C) + #(A * B) - #(A' * B)
⊢ #(A * B * C') * #A ≤ #(A * B) * #(A * C')

Proof state:
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : CommGroup G
A B : Finset G
hA : ∀ A' ⊆ A, #(A * B) * #A' ≤ #(A' * B) * #A
x : G
C : Finset G
a✝ : x ∉ C
ih : #(A * B * C) * #A ≤ #(A * B) * #(A * C)
A' : Finset G := A ∩ (A * C / {x})
hA' : A' = A ∩ (A * C / {x})
C' : Finset G := insert x C
hC' : C' = insert x C
h₀ : A' * {x} = A * {x} ∩ (A * C)
⊢ A * B * C' = A * B * C ∪ (A * B * {x}) \ (A' * B * {x})

Tactic:
rw [hC', insert_eq, union_comm, mul_union]

Result:
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : CommGroup G
A B : Finset G
hA : ∀ A' ⊆ A, #(A * B) * #A' ≤ #(A' * B) * #A
x : G
C : Finset G
a✝ : x ∉ C
ih : #(A * B * C) * #A ≤ #(A * B) * #(A * C)
A' : Finset G := A ∩ (A * C / {x})
hA' : A' = A ∩ (A * C / {x})
C' : Finset G := insert x C
hC' : C' = insert x C
h₀ : A' * {x} = A * {x} ∩ (A * C)
⊢ A * B * C ∪ A * B * {x} = A * B * C ∪ (A * B * {x}) \ (A' * B * {x})

Proof state:
case insert
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : CommGroup G
A B : Finset G
hA : ∀ A' ⊆ A, #(A * B) * #A' ≤ #(A' * B) * #A
x : G
C : Finset G
a✝ : x ∉ C
ih : #(A * B * C) * #A ≤ #(A * B) * #(A * C)
A' : Finset G := A ∩ (A * C / {x})
hA' : A' = A ∩ (A * C / {x})
C' : Finset G := insert x C
hC' : C' = insert x C
h₀ : A' * {x} = A * {x} ∩ (A * C)
h₁ : A * B * C' = A * B * C ∪ (A * B * {x}) \ (A' * B * {x})
h₂ : A' * B * {x} ⊆ A * B * {x}
h₃ : #(A * B * C') ≤ #(A * B * C) + #(A * B) - #(A' * B)
⊢ #(A * B * C) * #A + #(A * B) * #A - #(A' * B) * #A ≤ #(A * B) * #(A * C')

Tactic:
refine (tsub_le_tsub (add_le_add_right ih _) <| hA _ inter_subset_left).trans_eq ?_

Result:
case insert
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : CommGroup G
A B : Finset G
hA : ∀ A' ⊆ A, #(A * B) * #A' ≤ #(A' * B) * #A
x : G
C : Finset G
a✝ : x ∉ C
ih : #(A * B * C) * #A ≤ #(A * B) * #(A * C)
A' : Finset G := A ∩ (A * C / {x})
hA' : A' = A ∩ (A * C / {x})
C' : Finset G := insert x C
hC' : C' = insert x C
h₀ : A' * {x} = A * {x} ∩ (A * C)
h₁ : A * B * C' = A * B * C ∪ (A * B * {x}) \ (A' * B * {x})
h₂ : A' * B * {x} ⊆ A * B * {x}
h₃ : #(A * B * C') ≤ #(A * B * C) + #(A * B) - #(A' * B)
⊢ #(A * B) * #(A * C) + #(A * B) * #A - #(A * B) * #(A ∩ (A * C / {x})) = #(A * B) * #(A * C')

Proof state:
case insert
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : CommGroup G
A B : Finset G
hA : ∀ A' ⊆ A, #(A * B) * #A' ≤ #(A' * B) * #A
x : G
C : Finset G
a✝ : x ∉ C
ih : #(A * B * C) * #A ≤ #(A * B) * #(A * C)
A' : Finset G := A ∩ (A * C / {x})
hA' : A' = A ∩ (A * C / {x})
C' : Finset G := insert x C
hC' : C' = insert x C
h₀ : A' * {x} = A * {x} ∩ (A * C)
h₁ : A * B * C' = A * B * C ∪ (A * B * {x}) \ (A' * B * {x})
h₂ : A' * B * {x} ⊆ A * B * {x}
h₃ : #(A * B * C') ≤ #(A * B * C) + #(A * B) - #(A' * B)
⊢ (#(A * B * C) + #(A * B) - #(A' * B)) * #A ≤ #(A * B) * #(A * C')

Tactic:
rw [tsub_mul, add_mul]

Result:
case insert
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : CommGroup G
A B : Finset G
hA : ∀ A' ⊆ A, #(A * B) * #A' ≤ #(A' * B) * #A
x : G
C : Finset G
a✝ : x ∉ C
ih : #(A * B * C) * #A ≤ #(A * B) * #(A * C)
A' : Finset G := A ∩ (A * C / {x})
hA' : A' = A ∩ (A * C / {x})
C' : Finset G := insert x C
hC' : C' = insert x C
h₀ : A' * {x} = A * {x} ∩ (A * C)
h₁ : A * B * C' = A * B * C ∪ (A * B * {x}) \ (A' * B * {x})
h₂ : A' * B * {x} ⊆ A * B * {x}
h₃ : #(A * B * C') ≤ #(A * B * C) + #(A * B) - #(A' * B)
⊢ #(A * B * C) * #A + #(A * B) * #A - #(A' * B) * #A ≤ #(A * B) * #(A * C')

Proof state:
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : CommGroup G
A B : Finset G
hA : ∀ A' ⊆ A, #(A * B) * #A' ≤ #(A' * B) * #A
x : G
C : Finset G
a✝ : x ∉ C
ih : #(A * B * C) * #A ≤ #(A * B) * #(A * C)
A' : Finset G := A ∩ (A * C / {x})
hA' : A' = A ∩ (A * C / {x})
C' : Finset G := insert x C
hC' : C' = insert x C
h₀ : A' * {x} = A * {x} ∩ (A * C)
⊢ A' * B * {x} ≤ A * B * C

Tactic:
rw [mul_right_comm, mul_right_comm A, h₀]

Result:
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : CommGroup G
A B : Finset G
hA : ∀ A' ⊆ A, #(A * B) * #A' ≤ #(A' * B) * #A
x : G
C : Finset G
a✝ : x ∉ C
ih : #(A * B * C) * #A ≤ #(A * B) * #(A * C)
A' : Finset G := A ∩ (A * C / {x})
hA' : A' = A ∩ (A * C / {x})
C' : Finset G := insert x C
hC' : C' = insert x C
h₀ : A' * {x} = A * {x} ∩ (A * C)
⊢ A * {x} ∩ (A * C) * B ≤ A * C * B