case inl
α : Type u_1
β : Type ?u.16509
s✝ t : Set α
a✝ b x y : α
f : α → β
s : Set α
a : α
hs : Set.Finite s
⊢ ncard (s \ {a}) ≤ ncard s

case inr
α : Type u_1
β : Type ?u.16509
s✝ t : Set α
a✝ b x y : α
f : α → β
s : Set α
a : α
hs : Set.Infinite s
⊢ ncard (s \ {a}) ≤ ncard s
α : Type u_1
β : Type ?u.16509
s✝ t : Set α
a✝ b x y : α
f : α → β
s : Set α
a : α
⊢ ncard (s \ {a}) ≤ ncard s
obtain hs | hs := s.finite_or_infinite
case h.e'_3
α : Type u_1
β : Type ?u.16509
s✝ t : Set α
a✝ b x y : α
f : α → β
s : Set α
a : α
hs : Set.Infinite s
⊢ ncard (s \ {a}) = 0
case inr
α : Type u_1
β : Type ?u.16509
s✝ t : Set α
a✝ b x y : α
f : α → β
s : Set α
a : α
hs : Set.Infinite s
⊢ ncard (s \ {a}) ≤ ncard s
convert @zero_le ℕ _ _
no goals
case h.e'_3
α : Type u_1
β : Type ?u.16509
s✝ t : Set α
a✝ b x y : α
f : α → β
s : Set α
a : α
hs : Set.Infinite s
⊢ ncard (s \ {a}) = 0
exact (hs.diff (by simp : Set.Finite {a})).ncard
no goals
case inl
α : Type u_1
β : Type ?u.16509
s✝ t : Set α
a✝ b x y : α
f : α → β
s : Set α
a : α
hs : Set.Finite s
⊢ ncard (s \ {a}) ≤ ncard s
apply ncard_le_of_subset (diff_subset _ _) hs
no goals
α : Type u_1
β : Type ?u.16509
s✝ t : Set α
a✝ b x y : α
f : α → β
s : Set α
a : α
hs : Set.Infinite s
⊢ Set.Finite {a}
simp