Subtypes

These are ported from the Lean 3 standard library file init/data/subtype/basic.lean.

theorem Subtype.exists_of_subtype {α : Type u} {p : α → Prop} : { x // p x } → ∃ x, p x

theorem Subtype.tag_irrelevant {α : Type u} {p : α → Prop} {a : α} (h1 : p a) (h2 : p a) : { val := a, property := h1 } = { val := a, property := h2 }

theorem Subtype.ne_of_val_ne {α : Type u} {p : α → Prop} {a1 : { x // p x }} {a2 : { x // p x }} : a1.val ≠ a2.val → a1 ≠ a2

def Subtype.inhabited {α : Type u} {p : α → Prop} {a : α} (h : p a) : Inhabited { x // p x }

If there is some element satisfying the predicate, then the subtype is inhabited.