feat(logic/basic): add four lemmas about (d)ite (#16879)
```lean
lemma dite_eq_iff' : dite P A B = c ↔ (∀ h, A h = c) ∧ (∀ h, B h = c) :=
lemma ite_eq_iff' : ite P a b = c ↔ (P → a = c) ∧ (¬ P → b = c) := dite_eq_iff'
lemma dite_dite_comm {B : Q → α} {C : ¬P → ¬Q → α} (h : P → ¬Q) :
(if p : P then A p else if q : Q then B q else C p q) =
(if q : Q then B q else if p : P then A p else C p q) :=
lemma ite_ite_comm (h : P → ¬Q) :
(if P then a else if Q then b else c) =
(if Q then b else if P then a else c) :=
```
for #15681
