set_like type of element

Stream: new members

[Winston Yin]

I have an instance of set_like (some_class A) A. If p : some_class A, how can I get a : ↥p from x : A with x ∈ p and vice versa?

[Winston Yin]

I feel like I could do such a thing intuitively, but let me know if I'm thinking about this wrong

[Winston Yin]

As an example:

variables
  {k : Type*} {M : Type*}
  [semiring k] [add_comm_monoid M] [module k M]
  {p : submodule k M}

lemma lem1 (x : M) (h : x ∈ p) : p := sorry
def def2 (a : p) : M := sorry
lemma lem2 (a : p) : def2 a ∈ p := sorry

[Winston Yin]

I managed to answer my own question...

lemma lem1 (x : M) (h : x ∈ p) : p := ⟨x, h⟩
def def2 (a : p) : M := by {cases a, exact a_val}
lemma lem2 (a : p) : def2 a ∈ p := by {cases a, exact a_property}

[Eric Wieser]

More idiomatic would be:

def def2 (a : p) : M := a  -- coercion happens here
lemma lem2 (a : p) : def2 a ∈ p := a.prop

(docs#subtype.prop)