case inl
α : Type u_1
β : Type ?u.11040
s✝ t : Set α
a✝ b x y : α
f : α → β
a : α
s : Set α
hs : Set.Finite s
⊢ ncard (insert a s) ≤ ncard s + 1

case inr
α : Type u_1
β : Type ?u.11040
s✝ t : Set α
a✝ b x y : α
f : α → β
a : α
s : Set α
hs : Set.Infinite s
⊢ ncard (insert a s) ≤ ncard s + 1
α : Type u_1
β : Type ?u.11040
s✝ t : Set α
a✝ b x y : α
f : α → β
a : α
s : Set α
⊢ ncard (insert a s) ≤ ncard s + 1
obtain hs | hs := s.finite_or_infinite
case inr
α : Type u_1
β : Type ?u.11040
s✝ t : Set α
a✝ b x y : α
f : α → β
a : α
s : Set α
hs : Set.Infinite s
⊢ 0 ≤ ncard s + 1
case inr
α : Type u_1
β : Type ?u.11040
s✝ t : Set α
a✝ b x y : α
f : α → β
a : α
s : Set α
hs : Set.Infinite s
⊢ ncard (insert a s) ≤ ncard s + 1
rw [(hs.mono (subset_insert a s)).ncard]
no goals
case inr
α : Type u_1
β : Type ?u.11040
s✝ t : Set α
a✝ b x y : α
f : α → β
a : α
s : Set α
hs : Set.Infinite s
⊢ 0 ≤ ncard s + 1
exact Nat.zero_le _
no goals
case inl
α : Type u_1
β : Type ?u.11040
s✝ t : Set α
a✝ b x y : α
f : α → β
a : α
s : Set α
hs : Set.Finite s
⊢ ncard (insert a s) ≤ ncard s + 1
exact (em (a ∈ s)).elim (fun h ↦ (ncard_insert_of_mem h).trans_le (Nat.le_succ _))
  (fun h ↦ by rw [ncard_insert_of_not_mem h hs])
no goals
α : Type u_1
β : Type ?u.11040
s✝ t : Set α
a✝ b x y : α
f : α → β
a : α
s : Set α
hs : Set.Finite s
h : ¬a ∈ s
⊢ ncard (insert a s) ≤ ncard s + 1
rw [ncard_insert_of_not_mem h hs]