α✝ β α : Type u
s : Set α
a : α
h : ¬a ∈ s
⊢ Disjoint s {a}
α✝ β α : Type u
s : Set α
a : α
h : ¬a ∈ s
⊢ (#↑(insert a s)) = (#↑s) + 1
rw [← union_singleton, mk_union_of_disjoint, mk_singleton]
no goals
α✝ β α : Type u
s : Set α
a : α
h : ¬a ∈ s
⊢ Disjoint s {a}
simpa