feat(data/part): add 2 lemmas (#18153)

Author: urkud

src/data/part.lean

@@ -70,6 +70,14 @@ variables {α : Type*} {β : Type*} {γ : Type*}
 def to_option (o : part α) [decidable o.dom] : option α :=
 if h : dom o then some (o.get h) else none
 
+@[simp] lemma to_option_is_some (o : part α) [decidable o.dom] :
+  o.to_option.is_some ↔ o.dom :=
+by by_cases o.dom; simp [h, part.to_option]
+
+@[simp] lemma to_option_is_none (o : part α) [decidable o.dom] :
+  o.to_option.is_none ↔ ¬o.dom :=
+by by_cases o.dom; simp [h, part.to_option]
+
 /-- `part` extensionality -/
 theorem ext' : ∀ {o p : part α}
   (H1 : o.dom ↔ p.dom)