case isFalse
α : Type u_1
β : Type ?u.3414
s t : Finset α
a b : α
inst✝ : DecidableEq α
h : ¬a ∈ s
⊢ card ({a} ∩ s) ≤ 1

case isTrue
α : Type u_1
β : Type ?u.3414
s t : Finset α
a b : α
inst✝ : DecidableEq α
h : a ∈ s
⊢ card ({a} ∩ s) ≤ 1
α : Type u_1
β : Type ?u.3414
s t : Finset α
a b : α
inst✝ : DecidableEq α
⊢ card ({a} ∩ s) ≤ 1
cases' Finset.decidableMem a s with h h
no goals
case isFalse
α : Type u_1
β : Type ?u.3414
s t : Finset α
a b : α
inst✝ : DecidableEq α
h : ¬a ∈ s
⊢ card ({a} ∩ s) ≤ 1
simp [Finset.singleton_inter_of_not_mem h]
no goals
case isTrue
α : Type u_1
β : Type ?u.3414
s t : Finset α
a b : α
inst✝ : DecidableEq α
h : a ∈ s
⊢ card ({a} ∩ s) ≤ 1
simp [Finset.singleton_inter_of_mem h]