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

leanprover-community · Jan 14, 2023 · 80c4301 · 80c4301
1 parent 3310acf
commit 80c4301
Showing 1 changed file with 8 additions and 0 deletions.
diff --git a/src/data/part.lean b/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)