ι : Type u_1
α : Type u_2
β : Type ?u.112786
M : Type ?u.112789
N : Type ?u.112792
G : Type ?u.112795
k : Type ?u.112798
R : Type ?u.112801
inst✝ : DecidableEq α
s✝ : Finset α
B : Finset (Finset α)
n : ℕ
s : Finset ι
f : ι → Finset α
hs : Set.PairwiseDisjoint (↑s) f
⊢ card (filter (fun a => ¬f a = ∅) s) + card (filter (fun i => f i = ∅) s) ≤
    card (Finset.biUnion s f) + card (filter (fun i => f i = ∅) s)
ι : Type u_1
α : Type u_2
β : Type ?u.112786
M : Type ?u.112789
N : Type ?u.112792
G : Type ?u.112795
k : Type ?u.112798
R : Type ?u.112801
inst✝ : DecidableEq α
s✝ : Finset α
B : Finset (Finset α)
n : ℕ
s : Finset ι
f : ι → Finset α
hs : Set.PairwiseDisjoint (↑s) f
⊢ card s ≤ card (Finset.biUnion s f) + card (filter (fun i => f i = ∅) s)
rw [← Finset.filter_card_add_filter_neg_card_eq_card fun i ↦ f i = ∅, add_comm]
no goals
ι : Type u_1
α : Type u_2
β : Type ?u.112786
M : Type ?u.112789
N : Type ?u.112792
G : Type ?u.112795
k : Type ?u.112798
R : Type ?u.112801
inst✝ : DecidableEq α
s✝ : Finset α
B : Finset (Finset α)
n : ℕ
s : Finset ι
f : ι → Finset α
hs : Set.PairwiseDisjoint (↑s) f
⊢ card (filter (fun a => ¬f a = ∅) s) + card (filter (fun i => f i = ∅) s) ≤
    card (Finset.biUnion s f) + card (filter (fun i => f i = ∅) s)
exact
  add_le_add_right
    ((card_le_card_biUnion (hs.subset <| filter_subset _ _) fun i hi ↦
          nonempty_of_ne_empty <| (mem_filter.1 hi).2).trans <|
      card_le_of_subset <| biUnion_subset_biUnion_of_subset_left _ <| filter_subset _ _)
    _