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