α : Type u_1
β : Type ?u.126847
s✝ t✝ : Set α
a b x y : α
f : α → β
s t : Set α
hs : autoParam (Set.Finite s) _auto✝
⊢ ncard t ≤ ncard (t \ s) + ncard s
α : Type u_1
β : Type ?u.126847
s✝ t✝ : Set α
a b x y : α
f : α → β
s t : Set α
hs : autoParam (Set.Finite s) _auto✝
⊢ ncard t ≤ ncard s + ncard (t \ s)
rw [add_comm]
no goals
α : Type u_1
β : Type ?u.126847
s✝ t✝ : Set α
a b x y : α
f : α → β
s t : Set α
hs : autoParam (Set.Finite s) _auto✝
⊢ ncard t ≤ ncard (t \ s) + ncard s
apply ncard_le_ncard_diff_add_ncard _ _ hs