feat: lemmas to simplify equalities with Option-typed dependent if-then-else (#4037)

Closes #4013.

Add `dite_some_none_eq_none` and `dite_some_none_eq_some`, analogous to
the existing `ite_some_none_eq_none` and `ite_some_none_eq_some`.

src/Init/ByCases.lean

@@ -63,3 +63,16 @@ theorem ite_some_none_eq_none [Decidable P] :
 @[simp] theorem ite_some_none_eq_some [Decidable P] :
     (if P then some x else none) = some y ↔ P ∧ x = y := by
   split <;> simp_all
+
+-- This is not marked as `simp` as it is already handled by `dite_eq_right_iff`.
+theorem dite_some_none_eq_none [Decidable P] {x : P → α} :
+    (if h : P then some (x h) else none) = none ↔ ¬P := by
+  simp only [dite_eq_right_iff]
+  rfl
+
+@[simp] theorem dite_some_none_eq_some [Decidable P] {x : P → α} {y : α} :
+    (if h : P then some (x h) else none) = some y ↔ ∃ h : P, x h = y := by
+  by_cases h : P <;> simp only [h, dite_cond_eq_true, dite_cond_eq_false, Option.some.injEq,
+    false_iff, not_exists]
+  case pos => exact ⟨fun h_eq ↦ Exists.intro h h_eq, fun h_exists => h_exists.2⟩
+  case neg => exact fun h_false _ ↦ h_false