case pos
α : Type u_1
β : Type ?u.5325
s t : Finset α
a b : α
inst✝ : DecidableEq α
h : a ∈ s
⊢ card (insert a s) = if a ∈ s then card s else card s + 1

case neg
α : Type u_1
β : Type ?u.5325
s t : Finset α
a b : α
inst✝ : DecidableEq α
h : ¬a ∈ s
⊢ card (insert a s) = if a ∈ s then card s else card s + 1
α : Type u_1
β : Type ?u.5325
s t : Finset α
a b : α
inst✝ : DecidableEq α
⊢ card (insert a s) = if a ∈ s then card s else card s + 1
by_cases h : a ∈ s
no goals
case pos
α : Type u_1
β : Type ?u.5325
s t : Finset α
a b : α
inst✝ : DecidableEq α
h : a ∈ s
⊢ card (insert a s) = if a ∈ s then card s else card s + 1
rw [card_insert_of_mem h, if_pos h]
no goals
case neg
α : Type u_1
β : Type ?u.5325
s t : Finset α
a b : α
inst✝ : DecidableEq α
h : ¬a ∈ s
⊢ card (insert a s) = if a ∈ s then card s else card s + 1
rw [card_insert_of_not_mem h, if_neg h]