-- 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
a✝¹ : G
s✝ : Finset G
a✝ : a✝¹ ∉ s✝
ih : #(A * B * s✝) * #A ≤ #(A * B) * #(A * s✝)
⊢ #(A * B * insert a✝¹ s✝) * #A ≤ #(A * B) * #(A * insert a✝¹ s✝)

Tactic:
rename_i x C _

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 * B * insert x C) * #A ≤ #(A * B) * #(A * insert x C)

Proof state:
case empty
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : CommGroup G
A B : Finset G
hA : ∀ A' ⊆ A, #(A * B) * #A' ≤ #(A' * B) * #A
⊢ #(A * B * ∅) * #A ≤ #(A * B) * #(A * ∅)

Tactic:
simp

Result:
no goals

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)
h₁ : A * B * C' = A * B * C ∪ (A * B * {x}) \ (A' * B * {x})
h₂ : A' * B * {x} ⊆ A * B * {x}
⊢ #(A * B * C) + #((A * B * {x}) \ (A' * B * {x})) = #(A * B * C) + #(A * B) - #(A' * B)

Tactic:
rw [card_sdiff h₂, ← add_tsub_assoc_of_le (card_le_card h₂), card_mul_singleton,
  card_mul_singleton]

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}
h₃ : #(A * B * C') ≤ #(A * B * C) + #(A * B) - #(A' * B)
⊢ #(A * B * C') * #A ≤ #(A * B) * #(A * C')

Tactic:
refine (mul_le_mul_right' h₃ _).trans ?_

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 * B) - #(A' * B)) * #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})
C' : Finset G := insert x C
hC' : C' = insert x C
h₀ : A' * {x} = A * {x} ∩ (A * C)
⊢ #(A * B * C') * #A ≤ #(A * B) * #(A * C')

Tactic:
have h₁ : A * B * C' = A * B * C ∪ (A * B * {x}) \ (A' * B * {x}) := by
  rw [hC', insert_eq, union_comm, mul_union]
  refine (sup_sdiff_eq_sup ?_).symm
  rw [mul_right_comm, mul_right_comm A, h₀]
  exact mul_subset_mul_right inter_subset_right

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})
⊢ #(A * B * C') * #A ≤ #(A * B) * #(A * C')