α : Type u_1
β : Type ?u.211528
γ : Type ?u.211531
inst✝ : DecidableEq α
s✝ t u v : Finset α
a✝ b a : α
s : Finset α
h : a ∈ s
x : α
⊢ x = a ∨ x ∈ s ↔ x ∈ s
α : Type u_1
β : Type ?u.211528
γ : Type ?u.211531
inst✝ : DecidableEq α
s✝ t u v : Finset α
a✝ b a : α
s : Finset α
h : a ∈ s
x : α
⊢ x ∈ insert a (erase s a) ↔ x ∈ s
simp only [mem_insert, mem_erase, or_and_left, dec_em, true_and_iff]
case ha
α : Type u_1
β : Type ?u.211528
γ : Type ?u.211531
inst✝ : DecidableEq α
s✝ t u v : Finset α
a✝ b a : α
s : Finset α
h : a ∈ s
x : α
⊢ x = a → x ∈ s
α : Type u_1
β : Type ?u.211528
γ : Type ?u.211531
inst✝ : DecidableEq α
s✝ t u v : Finset α
a✝ b a : α
s : Finset α
h : a ∈ s
x : α
⊢ x = a ∨ x ∈ s ↔ x ∈ s
apply or_iff_right_of_imp
case ha
α : Type u_1
β : Type ?u.211528
γ : Type ?u.211531
inst✝ : DecidableEq α
s✝ t u v : Finset α
a b : α
s : Finset α
x : α
h : x ∈ s
⊢ x ∈ s
case ha
α : Type u_1
β : Type ?u.211528
γ : Type ?u.211531
inst✝ : DecidableEq α
s✝ t u v : Finset α
a✝ b a : α
s : Finset α
h : a ∈ s
x : α
⊢ x = a → x ∈ s
rintro rfl
no goals
case ha
α : Type u_1
β : Type ?u.211528
γ : Type ?u.211531
inst✝ : DecidableEq α
s✝ t u v : Finset α
a b : α
s : Finset α
x : α
h : x ∈ s
⊢ x ∈ s
exact h