case inl
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a✝ b : α
inst✝ : DecidableEq α
a : α
l : List α
d : Nodup l
h : a ∈ l
⊢ count a l = 1

case inr
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a✝ b : α
inst✝ : DecidableEq α
a : α
l : List α
d : Nodup l
h : ¬a ∈ l
⊢ count a l = 0
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a✝ b : α
inst✝ : DecidableEq α
a : α
l : List α
d : Nodup l
⊢ count a l = if a ∈ l then 1 else 0
split_ifs with h
no goals
case inl
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a✝ b : α
inst✝ : DecidableEq α
a : α
l : List α
d : Nodup l
h : a ∈ l
⊢ count a l = 1
exact count_eq_one_of_mem d h
no goals
case inr
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a✝ b : α
inst✝ : DecidableEq α
a : α
l : List α
d : Nodup l
h : ¬a ∈ l
⊢ count a l = 0
exact count_eq_zero_of_not_mem h