case empty
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
A B C : Finset α
hA : ∀ (A' : Finset α), A' ⊆ A → card (A * B) * card A' ≤ card (A' * B) * card A
⊢ card (A * B * ∅) * card A ≤ card (A * B) * card (A * ∅)

case insert
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
A B C✝ : Finset α
hA : ∀ (A' : Finset α), A' ⊆ A → card (A * B) * card A' ≤ card (A' * B) * card A
x : α
C : Finset α
a✝ : ¬x ∈ C
ih : card (A * B * C) * card A ≤ card (A * B) * card (A * C)
⊢ card (A * B * insert x C) * card A ≤ card (A * B) * card (A * insert x C)
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
A B C✝ C : Finset α
hA : ∀ (A' : Finset α), A' ⊆ A → card (A * B) * card A' ≤ card (A' * B) * card A
⊢ card (A * B * C) * card A ≤ card (A * B) * card (A * C)
induction' C using Finset.induction_on with x C _ ih
case insert
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
A B C✝ : Finset α
hA : ∀ (A' : Finset α), A' ⊆ A → card (A * B) * card A' ≤ card (A' * B) * card A
x : α
C : Finset α
a✝ : ¬x ∈ C
ih : card (A * B * C) * card A ≤ card (A * B) * card (A * C)
A' : Finset α := A ∩ (A * C / {x})
hA' : A' = A ∩ (A * C / {x})
⊢ card (A * B * insert x C) * card A ≤ card (A * B) * card (A * insert x C)
case insert
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
A B C✝ : Finset α
hA : ∀ (A' : Finset α), A' ⊆ A → card (A * B) * card A' ≤ card (A' * B) * card A
x : α
C : Finset α
a✝ : ¬x ∈ C
ih : card (A * B * C) * card A ≤ card (A * B) * card (A * C)
⊢ card (A * B * insert x C) * card A ≤ card (A * B) * card (A * insert x C)
set A' := A ∩ (A * C / {x}) with hA'
case insert
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
A B C✝ : Finset α
hA : ∀ (A' : Finset α), A' ⊆ A → card (A * B) * card A' ≤ card (A' * B) * card A
x : α
C : Finset α
a✝ : ¬x ∈ C
ih : card (A * B * C) * card A ≤ card (A * B) * card (A * C)
A' : Finset α := A ∩ (A * C / {x})
hA' : A' = A ∩ (A * C / {x})
C' : Finset α := insert x C
hC' : C' = insert x C
⊢ card (A * B * C') * card A ≤ card (A * B) * card (A * C')
case insert
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
A B C✝ : Finset α
hA : ∀ (A' : Finset α), A' ⊆ A → card (A * B) * card A' ≤ card (A' * B) * card A
x : α
C : Finset α
a✝ : ¬x ∈ C
ih : card (A * B * C) * card A ≤ card (A * B) * card (A * C)
A' : Finset α := A ∩ (A * C / {x})
hA' : A' = A ∩ (A * C / {x})
⊢ card (A * B * insert x C) * card A ≤ card (A * B) * card (A * insert x C)
set C' := insert x C with hC'
case insert
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
A B C✝ : Finset α
hA : ∀ (A' : Finset α), A' ⊆ A → card (A * B) * card A' ≤ card (A' * B) * card A
x : α
C : Finset α
a✝ : ¬x ∈ C
ih : card (A * B * C) * card A ≤ card (A * B) * card (A * C)
A' : Finset α := A ∩ (A * C / {x})
hA' : A' = A ∩ (A * C / {x})
C' : Finset α := insert x C
hC' : C' = insert x C
h₀ : A' * {x} = A * {x} ∩ (A * C)
⊢ card (A * B * C') * card A ≤ card (A * B) * card (A * C')
case insert
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
A B C✝ : Finset α
hA : ∀ (A' : Finset α), A' ⊆ A → card (A * B) * card A' ≤ card (A' * B) * card A
x : α
C : Finset α
a✝ : ¬x ∈ C
ih : card (A * B * C) * card A ≤ card (A * B) * card (A * C)
A' : Finset α := A ∩ (A * C / {x})
hA' : A' = A ∩ (A * C / {x})
C' : Finset α := insert x C
hC' : C' = insert x C
⊢ card (A * B * C') * card A ≤ card (A * B) * card (A * C')
have h₀ : A' * {x} = A * {x} ∩ (A * C) := by
  rw [hA', inter_mul_singleton, (isUnit_singleton x).div_mul_cancel]
case insert
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
A B C✝ : Finset α
hA : ∀ (A' : Finset α), A' ⊆ A → card (A * B) * card A' ≤ card (A' * B) * card A
x : α
C : Finset α
a✝ : ¬x ∈ C
ih : card (A * B * C) * card A ≤ card (A * B) * card (A * C)
A' : Finset α := A ∩ (A * C / {x})
hA' : A' = A ∩ (A * C / {x})
C' : Finset α := 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})
⊢ card (A * B * C') * card A ≤ card (A * B) * card (A * C')
case insert
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
A B C✝ : Finset α
hA : ∀ (A' : Finset α), A' ⊆ A → card (A * B) * card A' ≤ card (A' * B) * card A
x : α
C : Finset α
a✝ : ¬x ∈ C
ih : card (A * B * C) * card A ≤ card (A * B) * card (A * C)
A' : Finset α := A ∩ (A * C / {x})
hA' : A' = A ∩ (A * C / {x})
C' : Finset α := insert x C
hC' : C' = insert x C
h₀ : A' * {x} = A * {x} ∩ (A * C)
⊢ card (A * B * C') * card A ≤ card (A * B) * card (A * C')
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 _ _)
case insert
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
A B C✝ : Finset α
hA : ∀ (A' : Finset α), A' ⊆ A → card (A * B) * card A' ≤ card (A' * B) * card A
x : α
C : Finset α
a✝ : ¬x ∈ C
ih : card (A * B * C) * card A ≤ card (A * B) * card (A * C)
A' : Finset α := A ∩ (A * C / {x})
hA' : A' = A ∩ (A * C / {x})
C' : Finset α := 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}
⊢ card (A * B * C') * card A ≤ card (A * B) * card (A * C')
case insert
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
A B C✝ : Finset α
hA : ∀ (A' : Finset α), A' ⊆ A → card (A * B) * card A' ≤ card (A' * B) * card A
x : α
C : Finset α
a✝ : ¬x ∈ C
ih : card (A * B * C) * card A ≤ card (A * B) * card (A * C)
A' : Finset α := A ∩ (A * C / {x})
hA' : A' = A ∩ (A * C / {x})
C' : Finset α := 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})
⊢ card (A * B * C') * card A ≤ card (A * B) * card (A * C')
have h₂ : A' * B * {x} ⊆ A * B * {x} :=
  mul_subset_mul_right (mul_subset_mul_right <| inter_subset_left _ _)
case insert
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
A B C✝ : Finset α
hA : ∀ (A' : Finset α), A' ⊆ A → card (A * B) * card A' ≤ card (A' * B) * card A
x : α
C : Finset α
a✝ : ¬x ∈ C
ih : card (A * B * C) * card A ≤ card (A * B) * card (A * C)
A' : Finset α := A ∩ (A * C / {x})
hA' : A' = A ∩ (A * C / {x})
C' : Finset α := 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₃ : card (A * B * C') ≤ card (A * B * C) + card (A * B) - card (A' * B)
⊢ card (A * B * C') * card A ≤ card (A * B) * card (A * C')
case insert
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
A B C✝ : Finset α
hA : ∀ (A' : Finset α), A' ⊆ A → card (A * B) * card A' ≤ card (A' * B) * card A
x : α
C : Finset α
a✝ : ¬x ∈ C
ih : card (A * B * C) * card A ≤ card (A * B) * card (A * C)
A' : Finset α := A ∩ (A * C / {x})
hA' : A' = A ∩ (A * C / {x})
C' : Finset α := 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}
⊢ card (A * B * C') * card A ≤ card (A * B) * card (A * C')
have h₃ : (A * B * C').card ≤ (A * B * C).card + (A * B).card - (A' * B).card := by
  rw [h₁]
  refine' (card_union_le _ _).trans_eq _
  rw [card_sdiff h₂, ← add_tsub_assoc_of_le (card_le_of_subset h₂), card_mul_singleton,
    card_mul_singleton]
case insert
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
A B C✝ : Finset α
hA : ∀ (A' : Finset α), A' ⊆ A → card (A * B) * card A' ≤ card (A' * B) * card A
x : α
C : Finset α
a✝ : ¬x ∈ C
ih : card (A * B * C) * card A ≤ card (A * B) * card (A * C)
A' : Finset α := A ∩ (A * C / {x})
hA' : A' = A ∩ (A * C / {x})
C' : Finset α := 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₃ : card (A * B * C') ≤ card (A * B * C) + card (A * B) - card (A' * B)
⊢ (card (A * B * C) + card (A * B) - card (A' * B)) * card A ≤ card (A * B) * card (A * C')
case insert
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
A B C✝ : Finset α
hA : ∀ (A' : Finset α), A' ⊆ A → card (A * B) * card A' ≤ card (A' * B) * card A
x : α
C : Finset α
a✝ : ¬x ∈ C
ih : card (A * B * C) * card A ≤ card (A * B) * card (A * C)
A' : Finset α := A ∩ (A * C / {x})
hA' : A' = A ∩ (A * C / {x})
C' : Finset α := 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₃ : card (A * B * C') ≤ card (A * B * C) + card (A * B) - card (A' * B)
⊢ card (A * B * C') * card A ≤ card (A * B) * card (A * C')
refine' (mul_le_mul_right' h₃ _).trans _
case insert
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
A B C✝ : Finset α
hA : ∀ (A' : Finset α), A' ⊆ A → card (A * B) * card A' ≤ card (A' * B) * card A
x : α
C : Finset α
a✝ : ¬x ∈ C
ih : card (A * B * C) * card A ≤ card (A * B) * card (A * C)
A' : Finset α := A ∩ (A * C / {x})
hA' : A' = A ∩ (A * C / {x})
C' : Finset α := 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₃ : card (A * B * C') ≤ card (A * B * C) + card (A * B) - card (A' * B)
⊢ card (A * B * C) * card A + card (A * B) * card A - card (A' * B) * card A ≤ card (A * B) * card (A * C')
case insert
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
A B C✝ : Finset α
hA : ∀ (A' : Finset α), A' ⊆ A → card (A * B) * card A' ≤ card (A' * B) * card A
x : α
C : Finset α
a✝ : ¬x ∈ C
ih : card (A * B * C) * card A ≤ card (A * B) * card (A * C)
A' : Finset α := A ∩ (A * C / {x})
hA' : A' = A ∩ (A * C / {x})
C' : Finset α := 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₃ : card (A * B * C') ≤ card (A * B * C) + card (A * B) - card (A' * B)
⊢ (card (A * B * C) + card (A * B) - card (A' * B)) * card A ≤ card (A * B) * card (A * C')
rw [tsub_mul, add_mul]
case insert
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
A B C✝ : Finset α
hA : ∀ (A' : Finset α), A' ⊆ A → card (A * B) * card A' ≤ card (A' * B) * card A
x : α
C : Finset α
a✝ : ¬x ∈ C
ih : card (A * B * C) * card A ≤ card (A * B) * card (A * C)
A' : Finset α := A ∩ (A * C / {x})
hA' : A' = A ∩ (A * C / {x})
C' : Finset α := 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₃ : card (A * B * C') ≤ card (A * B * C) + card (A * B) - card (A' * B)
⊢ card (A * B) * card (A * C) + card (A * B) * card A - card (A * B) * card (A ∩ (A * C / {x})) =
    card (A * B) * card (A * C')
case insert
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
A B C✝ : Finset α
hA : ∀ (A' : Finset α), A' ⊆ A → card (A * B) * card A' ≤ card (A' * B) * card A
x : α
C : Finset α
a✝ : ¬x ∈ C
ih : card (A * B * C) * card A ≤ card (A * B) * card (A * C)
A' : Finset α := A ∩ (A * C / {x})
hA' : A' = A ∩ (A * C / {x})
C' : Finset α := 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₃ : card (A * B * C') ≤ card (A * B * C) + card (A * B) - card (A' * B)
⊢ card (A * B * C) * card A + card (A * B) * card A - card (A' * B) * card A ≤ card (A * B) * card (A * C')
refine' (tsub_le_tsub (add_le_add_right ih _) <| hA _ <| inter_subset_left _ _).trans_eq _
no goals
case insert
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
A B C✝ : Finset α
hA : ∀ (A' : Finset α), A' ⊆ A → card (A * B) * card A' ≤ card (A' * B) * card A
x : α
C : Finset α
a✝ : ¬x ∈ C
ih : card (A * B * C) * card A ≤ card (A * B) * card (A * C)
A' : Finset α := A ∩ (A * C / {x})
hA' : A' = A ∩ (A * C / {x})
C' : Finset α := 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₃ : card (A * B * C') ≤ card (A * B * C) + card (A * B) - card (A' * B)
⊢ card (A * B) * card (A * C) + card (A * B) * card A - card (A * B) * card (A ∩ (A * C / {x})) =
    card (A * B) * card (A * C')
rw [← mul_add, ← mul_tsub, ← hA', hC', insert_eq, mul_union, ← card_mul_singleton A x, ←
  card_mul_singleton A' x, add_comm (card _), h₀,
  eq_tsub_of_add_eq (card_union_add_card_inter _ _)]
no goals
case empty
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
A B C : Finset α
hA : ∀ (A' : Finset α), A' ⊆ A → card (A * B) * card A' ≤ card (A' * B) * card A
⊢ card (A * B * ∅) * card A ≤ card (A * B) * card (A * ∅)
simp
no goals
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
A B C✝ : Finset α
hA : ∀ (A' : Finset α), A' ⊆ A → card (A * B) * card A' ≤ card (A' * B) * card A
x : α
C : Finset α
a✝ : ¬x ∈ C
ih : card (A * B * C) * card A ≤ card (A * B) * card (A * C)
A' : Finset α := A ∩ (A * C / {x})
hA' : A' = A ∩ (A * C / {x})
C' : Finset α := insert x C
hC' : C' = insert x C
⊢ A' * {x} = A * {x} ∩ (A * C)
rw [hA', inter_mul_singleton, (isUnit_singleton x).div_mul_cancel]
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
A B C✝ : Finset α
hA : ∀ (A' : Finset α), A' ⊆ A → card (A * B) * card A' ≤ card (A' * B) * card A
x : α
C : Finset α
a✝ : ¬x ∈ C
ih : card (A * B * C) * card A ≤ card (A * B) * card (A * C)
A' : Finset α := A ∩ (A * C / {x})
hA' : A' = A ∩ (A * C / {x})
C' : Finset α := 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})
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
A B C✝ : Finset α
hA : ∀ (A' : Finset α), A' ⊆ A → card (A * B) * card A' ≤ card (A' * B) * card A
x : α
C : Finset α
a✝ : ¬x ∈ C
ih : card (A * B * C) * card A ≤ card (A * B) * card (A * C)
A' : Finset α := A ∩ (A * C / {x})
hA' : A' = A ∩ (A * C / {x})
C' : Finset α := 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})
rw [hC', insert_eq, union_comm, mul_union]
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
A B C✝ : Finset α
hA : ∀ (A' : Finset α), A' ⊆ A → card (A * B) * card A' ≤ card (A' * B) * card A
x : α
C : Finset α
a✝ : ¬x ∈ C
ih : card (A * B * C) * card A ≤ card (A * B) * card (A * C)
A' : Finset α := A ∩ (A * C / {x})
hA' : A' = A ∩ (A * C / {x})
C' : Finset α := insert x C
hC' : C' = insert x C
h₀ : A' * {x} = A * {x} ∩ (A * C)
⊢ A' * B * {x} ≤ A * B * C
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
A B C✝ : Finset α
hA : ∀ (A' : Finset α), A' ⊆ A → card (A * B) * card A' ≤ card (A' * B) * card A
x : α
C : Finset α
a✝ : ¬x ∈ C
ih : card (A * B * C) * card A ≤ card (A * B) * card (A * C)
A' : Finset α := A ∩ (A * C / {x})
hA' : A' = A ∩ (A * C / {x})
C' : Finset α := 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})
refine' (sup_sdiff_eq_sup _).symm
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
A B C✝ : Finset α
hA : ∀ (A' : Finset α), A' ⊆ A → card (A * B) * card A' ≤ card (A' * B) * card A
x : α
C : Finset α
a✝ : ¬x ∈ C
ih : card (A * B * C) * card A ≤ card (A * B) * card (A * C)
A' : Finset α := A ∩ (A * C / {x})
hA' : A' = A ∩ (A * C / {x})
C' : Finset α := insert x C
hC' : C' = insert x C
h₀ : A' * {x} = A * {x} ∩ (A * C)
⊢ A * {x} ∩ (A * C) * B ≤ A * C * B
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
A B C✝ : Finset α
hA : ∀ (A' : Finset α), A' ⊆ A → card (A * B) * card A' ≤ card (A' * B) * card A
x : α
C : Finset α
a✝ : ¬x ∈ C
ih : card (A * B * C) * card A ≤ card (A * B) * card (A * C)
A' : Finset α := A ∩ (A * C / {x})
hA' : A' = A ∩ (A * C / {x})
C' : Finset α := insert x C
hC' : C' = insert x C
h₀ : A' * {x} = A * {x} ∩ (A * C)
⊢ A' * B * {x} ≤ A * B * C
rw [mul_right_comm, mul_right_comm A, h₀]
no goals
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
A B C✝ : Finset α
hA : ∀ (A' : Finset α), A' ⊆ A → card (A * B) * card A' ≤ card (A' * B) * card A
x : α
C : Finset α
a✝ : ¬x ∈ C
ih : card (A * B * C) * card A ≤ card (A * B) * card (A * C)
A' : Finset α := A ∩ (A * C / {x})
hA' : A' = A ∩ (A * C / {x})
C' : Finset α := insert x C
hC' : C' = insert x C
h₀ : A' * {x} = A * {x} ∩ (A * C)
⊢ A * {x} ∩ (A * C) * B ≤ A * C * B
exact mul_subset_mul_right (inter_subset_right _ _)
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
A B C✝ : Finset α
hA : ∀ (A' : Finset α), A' ⊆ A → card (A * B) * card A' ≤ card (A' * B) * card A
x : α
C : Finset α
a✝ : ¬x ∈ C
ih : card (A * B * C) * card A ≤ card (A * B) * card (A * C)
A' : Finset α := A ∩ (A * C / {x})
hA' : A' = A ∩ (A * C / {x})
C' : Finset α := 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}
⊢ card (A * B * C ∪ (A * B * {x}) \ (A' * B * {x})) ≤ card (A * B * C) + card (A * B) - card (A' * B)
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
A B C✝ : Finset α
hA : ∀ (A' : Finset α), A' ⊆ A → card (A * B) * card A' ≤ card (A' * B) * card A
x : α
C : Finset α
a✝ : ¬x ∈ C
ih : card (A * B * C) * card A ≤ card (A * B) * card (A * C)
A' : Finset α := A ∩ (A * C / {x})
hA' : A' = A ∩ (A * C / {x})
C' : Finset α := 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}
⊢ card (A * B * C') ≤ card (A * B * C) + card (A * B) - card (A' * B)
rw [h₁]
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
A B C✝ : Finset α
hA : ∀ (A' : Finset α), A' ⊆ A → card (A * B) * card A' ≤ card (A' * B) * card A
x : α
C : Finset α
a✝ : ¬x ∈ C
ih : card (A * B * C) * card A ≤ card (A * B) * card (A * C)
A' : Finset α := A ∩ (A * C / {x})
hA' : A' = A ∩ (A * C / {x})
C' : Finset α := 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}
⊢ card (A * B * C) + card ((A * B * {x}) \ (A' * B * {x})) = card (A * B * C) + card (A * B) - card (A' * B)
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
A B C✝ : Finset α
hA : ∀ (A' : Finset α), A' ⊆ A → card (A * B) * card A' ≤ card (A' * B) * card A
x : α
C : Finset α
a✝ : ¬x ∈ C
ih : card (A * B * C) * card A ≤ card (A * B) * card (A * C)
A' : Finset α := A ∩ (A * C / {x})
hA' : A' = A ∩ (A * C / {x})
C' : Finset α := 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}
⊢ card (A * B * C ∪ (A * B * {x}) \ (A' * B * {x})) ≤ card (A * B * C) + card (A * B) - card (A' * B)
refine' (card_union_le _ _).trans_eq _
no goals
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
A B C✝ : Finset α
hA : ∀ (A' : Finset α), A' ⊆ A → card (A * B) * card A' ≤ card (A' * B) * card A
x : α
C : Finset α
a✝ : ¬x ∈ C
ih : card (A * B * C) * card A ≤ card (A * B) * card (A * C)
A' : Finset α := A ∩ (A * C / {x})
hA' : A' = A ∩ (A * C / {x})
C' : Finset α := 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}
⊢ card (A * B * C) + card ((A * B * {x}) \ (A' * B * {x})) = card (A * B * C) + card (A * B) - card (A' * B)
rw [card_sdiff h₂, ← add_tsub_assoc_of_le (card_le_of_subset h₂), card_mul_singleton,
  card_mul_singleton]