no goals
α : Type u_1
β : Type ?u.21433
s t : Set α
a b x y : α
f : α → β
ha : ¬a ∈ s
hb : b ∈ s
⊢ ncard (insert a s \ {b}) = ncard s
rw [← ncard_exchange ha hb, ← singleton_union, ← singleton_union, union_diff_distrib,
  @diff_singleton_eq_self _ b {a} fun h ↦ ha (by rwa [← mem_singleton_iff.mp h])]
no goals
α : Type u_1
β : Type ?u.21433
s t : Set α
a b x y : α
f : α → β
ha : ¬a ∈ s
hb : b ∈ s
h : b ∈ {a}
⊢ a ∈ s
rwa [← mem_singleton_iff.mp h]