α : Type u_1
β : Type ?u.185481
γ : Type ?u.185484
inst✝ : DecidableEq α
s s₁✝ s₂✝ t t₁ t₂ u v : Finset α
a✝ b : α
s₁ s₂ : Finset α
a : α
h : ¬a ∈ s₂
x : α
this : ¬(x = a ∧ x ∈ s₂)
⊢ x ∈ insert a s₁ ∩ s₂ ↔ x ∈ s₁ ∩ s₂
α : Type u_1
β : Type ?u.185481
γ : Type ?u.185484
inst✝ : DecidableEq α
s s₁✝ s₂✝ t t₁ t₂ u v : Finset α
a✝ b : α
s₁ s₂ : Finset α
a : α
h : ¬a ∈ s₂
x : α
⊢ x ∈ insert a s₁ ∩ s₂ ↔ x ∈ s₁ ∩ s₂
have : ¬(x = a ∧ x ∈ s₂) := by rintro ⟨rfl, H⟩; exact h H
no goals
α : Type u_1
β : Type ?u.185481
γ : Type ?u.185484
inst✝ : DecidableEq α
s s₁✝ s₂✝ t t₁ t₂ u v : Finset α
a✝ b : α
s₁ s₂ : Finset α
a : α
h : ¬a ∈ s₂
x : α
this : ¬(x = a ∧ x ∈ s₂)
⊢ x ∈ insert a s₁ ∩ s₂ ↔ x ∈ s₁ ∩ s₂
simp only [mem_inter, mem_insert, or_and_right, this, false_or_iff]
case intro
α : Type u_1
β : Type ?u.185481
γ : Type ?u.185484
inst✝ : DecidableEq α
s s₁✝ s₂✝ t t₁ t₂ u v : Finset α
a b : α
s₁ s₂ : Finset α
x : α
H : x ∈ s₂
h : ¬x ∈ s₂
⊢ False
α : Type u_1
β : Type ?u.185481
γ : Type ?u.185484
inst✝ : DecidableEq α
s s₁✝ s₂✝ t t₁ t₂ u v : Finset α
a✝ b : α
s₁ s₂ : Finset α
a : α
h : ¬a ∈ s₂
x : α
⊢ ¬(x = a ∧ x ∈ s₂)
rintro ⟨rfl, H⟩
no goals
case intro
α : Type u_1
β : Type ?u.185481
γ : Type ?u.185484
inst✝ : DecidableEq α
s s₁✝ s₂✝ t t₁ t₂ u v : Finset α
a b : α
s₁ s₂ : Finset α
x : α
H : x ∈ s₂
h : ¬x ∈ s₂
⊢ False
exact h H