α : Type u_1
β : Type ?u.39090
s t : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
h : s ⊆ t
⊢ card (t \ s) = card (t \ s ∪ s) - card s
α : Type u_1
β : Type ?u.39090
s t : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
h : s ⊆ t
⊢ card (t \ s) = card t - card s
suffices card (t \ s) = card (t \ s ∪ s) - s.card by rwa [sdiff_union_of_subset h] at this
no goals
α : Type u_1
β : Type ?u.39090
s t : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
h : s ⊆ t
⊢ card (t \ s) = card (t \ s ∪ s) - card s
rw [card_disjoint_union sdiff_disjoint, add_tsub_cancel_right]
no goals
α : Type u_1
β : Type ?u.39090
s t : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
h : s ⊆ t
this : card (t \ s) = card (t \ s ∪ s) - card s
⊢ card (t \ s) = card t - card s
rwa [sdiff_union_of_subset h] at this