feat: lemmas about if-then-else (#438)

Std/Data/String/Lemmas.lean

@@ -712,7 +712,7 @@ theorem foldrAux_of_valid (f : Char → α → α) (l m r a) :
   rw [← m.reverse_reverse]
   induction m.reverse generalizing r a with (unfold foldrAux; simp)
   | cons c m IH =>
-    rw [dif_pos (by exact Nat.lt_add_of_pos_right add_csize_pos)]
+    rw [if_pos (by exact Nat.lt_add_of_pos_right add_csize_pos)]
     simp [← Nat.add_assoc, by simpa using prev_of_valid (l++m.reverse) c r]
     simp [by simpa using get_of_valid (l++m.reverse) (c::r)]
     simpa using IH (c::r) (f c a)

Std/Logic.lean

@@ -784,6 +784,18 @@ theorem apply_ite (f : α → β) (P : Prop) [Decidable P] (x y : α) :
 @[simp] theorem ite_eq_right_iff {P : Prop} [Decidable P] : ite P a b = b ↔ P → a = b :=
   dite_eq_right_iff
 
+/-- A `dite` whose results do not actually depend on the condition may be reduced to an `ite`. -/
+@[simp] theorem dite_eq_ite [Decidable P] : (dite P (fun _ => a) fun _ => b) = ite P a b := rfl
+
+-- We don't mark this as `simp` as it is already handled by `ite_eq_right_iff`.
+theorem ite_some_none_eq_none [Decidable P] :
+    (if P then some x else none) = none ↔ ¬ P := by
+  simp only [ite_eq_right_iff]
+
+@[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
+
 /-! ## miscellaneous -/
 
 attribute [simp] inline