Theorem: Set.pure_subset_of_mem (GMLInit/Data/Set/Subset.lean)

State before:
α : Type u_1
s t u : Set α
x : α
⊢ x ∈ s → (pure x).Subset s
Tactic:
intro | hs, _, rfl => exact hs
State after:
no goals

State before:
α : Type u_1
s t u : Set α
x : α
x✝² : x ∈ s
x✝¹ : α
x✝ : x✝¹ ∈ pure x
hs : x ∈ s
⊢ x ∈ s
Tactic:
exact hs
State after:
no goals