case pos
α : Type u_1
β : Type ?u.4838
s✝ t : Finset α
a✝ b : α
inst✝ : DecidableEq α
a : α
s : Finset α
h : a ∈ s
⊢ card (insert a s) ≤ card s + 1

case neg
α : Type u_1
β : Type ?u.4838
s✝ t : Finset α
a✝ b : α
inst✝ : DecidableEq α
a : α
s : Finset α
h : ¬a ∈ s
⊢ card (insert a s) ≤ card s + 1
α : Type u_1
β : Type ?u.4838
s✝ t : Finset α
a✝ b : α
inst✝ : DecidableEq α
a : α
s : Finset α
⊢ card (insert a s) ≤ card s + 1
by_cases h : a ∈ s
case pos
α : Type u_1
β : Type ?u.4838
s✝ t : Finset α
a✝ b : α
inst✝ : DecidableEq α
a : α
s : Finset α
h : a ∈ s
⊢ card s ≤ card s + 1
case pos
α : Type u_1
β : Type ?u.4838
s✝ t : Finset α
a✝ b : α
inst✝ : DecidableEq α
a : α
s : Finset α
h : a ∈ s
⊢ card (insert a s) ≤ card s + 1
rw [insert_eq_of_mem h]
no goals
case pos
α : Type u_1
β : Type ?u.4838
s✝ t : Finset α
a✝ b : α
inst✝ : DecidableEq α
a : α
s : Finset α
h : a ∈ s
⊢ card s ≤ card s + 1
exact Nat.le_succ _
no goals
case neg
α : Type u_1
β : Type ?u.4838
s✝ t : Finset α
a✝ b : α
inst✝ : DecidableEq α
a : α
s : Finset α
h : ¬a ∈ s
⊢ card (insert a s) ≤ card s + 1
rw [card_insert_of_not_mem h]