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

Tactic:
exact mul_subset_mul_right inter_subset_right

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

Tactic:
set A' := A ∩ (A * C / {x}) with hA'

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})
⊢ #(A * B * insert x C) * #A ≤ #(A * B) * #(A * insert x 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)
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:
refine (card_union_le _ _).trans_eq ?_

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

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

Tactic:
induction C using Finset.induction_on with
| empty => simp
| insert _ ih =>
  rename_i x C _
  set A' := A ∩ (A * C / {x}) with hA'
  set C' := insert x C with hC'
  have h₀ : A' * {x} = A * {x} ∩ (A * C) := by
    rw [hA', inter_mul_singleton, (isUnit_singleton x).div_mul_cancel]
  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
  have h₂ : A' * B * {x} ⊆ A * B * {x} :=
    mul_subset_mul_right (mul_subset_mul_right inter_subset_left)
  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]
  refine (mul_le_mul_right' h₃ _).trans ?_
  rw [tsub_mul, add_mul]
  refine (tsub_le_tsub (add_le_add_right ih _) <| hA _ inter_subset_left).trans_eq ?_
  rw [← mul_add, ← mul_tsub, ← hA', hC', insert_eq, mul_union, ← card_mul_singleton A x, ←
    card_mul_singleton A' x, add_comm #_, h₀,
    eq_tsub_of_add_eq (card_union_add_card_inter _ _)]

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

Tactic:
have h₂ : A' * B * {x} ⊆ A * B * {x} :=
  mul_subset_mul_right (mul_subset_mul_right inter_subset_left)

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

Tactic:
have h₀ : A' * {x} = A * {x} ∩ (A * C) := by
  rw [hA', inter_mul_singleton, (isUnit_singleton x).div_mul_cancel]

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)
⊢ #(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})
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')

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

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

Tactic:
rw [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)
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)