α : Type u_1
β : Type ?u.15504
q : Semiquot α
p : IsPure q
a : α
⊢ a ∈ q ↔ a = get q p
α : Type u_1
β : Type ?u.15504
q : Semiquot α
p : IsPure q
a : α
⊢ a ∈ q ↔ a ∈ pure (get q p)
simp
no goals
α : Type u_1
β : Type ?u.15504
q : Semiquot α
p : IsPure q
a : α
⊢ a ∈ q ↔ a = get q p
exact ⟨fun h => p _ h _ (get_mem _), fun e => e.symm ▸ get_mem _⟩