α : Type u_1
β : Type ?u.112192
γ : Type ?u.112195
inst✝ : DecidableEq α
s✝ t✝ u v : Finset α
a✝ b : α
s t : Finset α
a : α
h : s = insert a t
⊢ a ∈ s
α : Type u_1
β : Type ?u.112192
γ : Type ?u.112195
inst✝ : DecidableEq α
s✝ t✝ u v : Finset α
a✝ b : α
s t : Finset α
a : α
h : ¬a ∈ s
⊢ s ≠ insert a t
contrapose! h
no goals
α : Type u_1
β : Type ?u.112192
γ : Type ?u.112195
inst✝ : DecidableEq α
s✝ t✝ u v : Finset α
a✝ b : α
s t : Finset α
a : α
h : s = insert a t
⊢ a ∈ s
simp [h]