α : Type u_1
β : Type ?u.7918
s t : Set α
a b x y : α
f : α → β
⊢ Finset.card ({a} ∩ Finite.toFinset ?ht) ≤ 1

case ht
α : Type u_1
β : Type ?u.7918
s t : Set α
a b x y : α
f : α → β
⊢ Set.Finite ({a} ∩ s)

case ht
α : Type u_1
β : Type ?u.7918
s t : Set α
a b x y : α
f : α → β
⊢ Set.Finite ({a} ∩ s)
α : Type u_1
β : Type ?u.7918
s t : Set α
a b x y : α
f : α → β
⊢ ncard ({a} ∩ s) ≤ 1
rw [← inter_self {a}, inter_assoc, ncard_eq_toFinset_card _, Finite.toFinset_inter,
  Finite.toFinset_singleton]
no goals
case ht
α : Type u_1
β : Type ?u.7918
s t : Set α
a b x y : α
f : α → β
⊢ Set.Finite ({a} ∩ s)

case ht
α : Type u_1
β : Type ?u.7918
s t : Set α
a b x y : α
f : α → β
⊢ Set.Finite ({a} ∩ s)
all_goals toFinite_tac
no goals
α : Type u_1
β : Type ?u.7918
s t : Set α
a b x y : α
f : α → β
⊢ Finset.card ({a} ∩ Finite.toFinset ?ht) ≤ 1
apply Finset.card_singleton_inter
no goals
case ht
α : Type u_1
β : Type ?u.7918
s t : Set α
a b x y : α
f : α → β
⊢ Set.Finite ({a} ∩ s)
toFinite_tac