case inl
α : Type u_1
β : Type ?u.124878
s✝ t✝ : Set α
a b x y : α
f : α → β
s t : Set α
ht : autoParam (Set.Finite t) _auto✝
h : Set.Finite s
⊢ ncard s ≤ ncard (s \ t) + ncard t

case inr
α : Type u_1
β : Type ?u.124878
s✝ t✝ : Set α
a b x y : α
f : α → β
s t : Set α
ht : autoParam (Set.Finite t) _auto✝
h : Set.Infinite s
⊢ ncard s ≤ ncard (s \ t) + ncard t
α : Type u_1
β : Type ?u.124878
s✝ t✝ : Set α
a b x y : α
f : α → β
s t : Set α
ht : autoParam (Set.Finite t) _auto✝
⊢ ncard s ≤ ncard (s \ t) + ncard t
cases' s.finite_or_infinite with h h
case h.e'_3
α : Type u_1
β : Type ?u.124878
s✝ t✝ : Set α
a b x y : α
f : α → β
s t : Set α
ht : autoParam (Set.Finite t) _auto✝
h : Set.Infinite s
⊢ ncard s = 0
case inr
α : Type u_1
β : Type ?u.124878
s✝ t✝ : Set α
a b x y : α
f : α → β
s t : Set α
ht : autoParam (Set.Finite t) _auto✝
h : Set.Infinite s
⊢ ncard s ≤ ncard (s \ t) + ncard t
convert Nat.zero_le _
no goals
case h.e'_3
α : Type u_1
β : Type ?u.124878
s✝ t✝ : Set α
a b x y : α
f : α → β
s t : Set α
ht : autoParam (Set.Finite t) _auto✝
h : Set.Infinite s
⊢ ncard s = 0
rw [h.ncard]
case inl
α : Type u_1
β : Type ?u.124878
s✝ t✝ : Set α
a b x y : α
f : α → β
s t : Set α
ht : autoParam (Set.Finite t) _auto✝
h : Set.Finite s
⊢ ncard (t ∩ s) ≤ ncard t
case inl
α : Type u_1
β : Type ?u.124878
s✝ t✝ : Set α
a b x y : α
f : α → β
s t : Set α
ht : autoParam (Set.Finite t) _auto✝
h : Set.Finite s
⊢ ncard s ≤ ncard (s \ t) + ncard t
rw [← diff_inter_self_eq_diff, ← ncard_diff_add_ncard_eq_ncard (inter_subset_right t s) h,
  add_le_add_iff_left]
no goals
case inl
α : Type u_1
β : Type ?u.124878
s✝ t✝ : Set α
a b x y : α
f : α → β
s t : Set α
ht : autoParam (Set.Finite t) _auto✝
h : Set.Finite s
⊢ ncard (t ∩ s) ≤ ncard t
apply ncard_inter_le_ncard_left _ _ ht