α : Type u_1
β : Type ?u.221592
γ : Type ?u.221595
inst✝ : DecidableEq α
s t u v : Finset α
a b : α
s₁ s₂ : Finset α
⊢ ∀ (x : α), ¬(x ∈ s₁ ∧ x ∈ s₂ ∧ ¬x ∈ s₁)
α : Type u_1
β : Type ?u.221592
γ : Type ?u.221595
inst✝ : DecidableEq α
s t u v : Finset α
a b : α
s₁ s₂ : Finset α
⊢ ∀ (x : α), ¬x ∈ s₁ ∩ (s₂ \ s₁)
simp only [mem_inter, mem_sdiff]
case intro.intro
α : Type u_1
β : Type ?u.221592
γ : Type ?u.221595
inst✝ : DecidableEq α
s t u v : Finset α
a b : α
s₁ s₂ : Finset α
x : α
h : x ∈ s₁
left✝ : x ∈ s₂
hn : ¬x ∈ s₁
⊢ False
α : Type u_1
β : Type ?u.221592
γ : Type ?u.221595
inst✝ : DecidableEq α
s t u v : Finset α
a b : α
s₁ s₂ : Finset α
⊢ ∀ (x : α), ¬(x ∈ s₁ ∧ x ∈ s₂ ∧ ¬x ∈ s₁)
rintro x ⟨h, _, hn⟩
no goals
case intro.intro
α : Type u_1
β : Type ?u.221592
γ : Type ?u.221595
inst✝ : DecidableEq α
s t u v : Finset α
a b : α
s₁ s₂ : Finset α
x : α
h : x ∈ s₁
left✝ : x ∈ s₂
hn : ¬x ∈ s₁
⊢ False
exact hn h