case pos
α : Type u_1
β : Type ?u.109096
γ : Type ?u.109099
inst✝ : DecidableEq α
s✝ t : Multiset α
a✝ b a : α
s : Multiset α
h : a ∈ s
⊢ ↑card (erase s a) = if a ∈ s then pred (↑card s) else ↑card s

case neg
α : Type u_1
β : Type ?u.109096
γ : Type ?u.109099
inst✝ : DecidableEq α
s✝ t : Multiset α
a✝ b a : α
s : Multiset α
h : ¬a ∈ s
⊢ ↑card (erase s a) = if a ∈ s then pred (↑card s) else ↑card s
α : Type u_1
β : Type ?u.109096
γ : Type ?u.109099
inst✝ : DecidableEq α
s✝ t : Multiset α
a✝ b a : α
s : Multiset α
⊢ ↑card (erase s a) = if a ∈ s then pred (↑card s) else ↑card s
by_cases h : a ∈ s
no goals
case pos
α : Type u_1
β : Type ?u.109096
γ : Type ?u.109099
inst✝ : DecidableEq α
s✝ t : Multiset α
a✝ b a : α
s : Multiset α
h : a ∈ s
⊢ ↑card (erase s a) = if a ∈ s then pred (↑card s) else ↑card s
rwa [card_erase_of_mem h, if_pos]
no goals
case neg
α : Type u_1
β : Type ?u.109096
γ : Type ?u.109099
inst✝ : DecidableEq α
s✝ t : Multiset α
a✝ b a : α
s : Multiset α
h : ¬a ∈ s
⊢ ↑card (erase s a) = if a ∈ s then pred (↑card s) else ↑card s
rwa [erase_of_not_mem h, if_neg]