case inl
α : Type u_1
β : Type ?u.3481
γ : Type ?u.3484
r : α → α → Prop
s✝ t : Multiset α
a✝ : α
inst✝ : DecidableEq α
a : α
s : Multiset α
d : Nodup s
h : a ∈ s
⊢ count a s = 1

case inr
α : Type u_1
β : Type ?u.3481
γ : Type ?u.3484
r : α → α → Prop
s✝ t : Multiset α
a✝ : α
inst✝ : DecidableEq α
a : α
s : Multiset α
d : Nodup s
h : ¬a ∈ s
⊢ count a s = 0
α : Type u_1
β : Type ?u.3481
γ : Type ?u.3484
r : α → α → Prop
s✝ t : Multiset α
a✝ : α
inst✝ : DecidableEq α
a : α
s : Multiset α
d : Nodup s
⊢ count a s = if a ∈ s then 1 else 0
split_ifs with h
no goals
case inl
α : Type u_1
β : Type ?u.3481
γ : Type ?u.3484
r : α → α → Prop
s✝ t : Multiset α
a✝ : α
inst✝ : DecidableEq α
a : α
s : Multiset α
d : Nodup s
h : a ∈ s
⊢ count a s = 1
exact count_eq_one_of_mem d h
no goals
case inr
α : Type u_1
β : Type ?u.3481
γ : Type ?u.3484
r : α → α → Prop
s✝ t : Multiset α
a✝ : α
inst✝ : DecidableEq α
a : α
s : Multiset α
d : Nodup s
h : ¬a ∈ s
⊢ count a s = 0
exact count_eq_zero_of_not_mem h