α : Type u_1
β : Type ?u.250835
γ : Type ?u.250838
inst✝ : DecidableEq α
s t u v : Finset α
a b : α
ha : ¬a ∈ t
hst : _root_.Disjoint (erase s a) t
⊢ ¬a ∈ erase s a ∧ _root_.Disjoint (erase s a) t
α : Type u_1
β : Type ?u.250835
γ : Type ?u.250838
inst✝ : DecidableEq α
s t u v : Finset α
a b : α
ha : ¬a ∈ t
hst : _root_.Disjoint (erase s a) t
⊢ _root_.Disjoint s t
rw [← erase_insert ha, ← disjoint_erase_comm, disjoint_insert_right]
no goals
α : Type u_1
β : Type ?u.250835
γ : Type ?u.250838
inst✝ : DecidableEq α
s t u v : Finset α
a b : α
ha : ¬a ∈ t
hst : _root_.Disjoint (erase s a) t
⊢ ¬a ∈ erase s a ∧ _root_.Disjoint (erase s a) t
exact ⟨not_mem_erase _ _, hst⟩