feat(logic/basic): apply_dite2, apply_ite2 (#4050)

Add variants of `apply_dite` and `apply_ite` for two-argument
functions (in the case where I wanted `apply_ite`, the function was
addition).  I don't think there is any need for corresponding versions
of `dite_apply` or `ite_apply`, as two-argument versions of those
would be exactly the same as applying the one-argument version twice,
whereas that's not the case with `apply_dite2` and `apply_ite2`.

src/logic/basic.lean

@@ -1112,6 +1112,15 @@ lemma apply_ite {α β : Type*} (f : α → β) (P : Prop) [decidable P] (x y :
   f (ite P x y) = ite P (f x) (f y) :=
 apply_dite f P (λ _, x) (λ _, y)
 
+lemma apply_dite2 {α β γ : Type*} (f : α → β → γ) (P : Prop) [decidable P] (a : P → α)
+  (b : ¬P → α) (c : P → β) (d : ¬P → β) :
+  f (dite P a b) (dite P c d) = dite P (λ h, f (a h) (c h)) (λ h, f (b h) (d h)) :=
+by { by_cases h : P; simp [h] }
+
+lemma apply_ite2 {α β γ : Type*} (f : α → β → γ) (P : Prop) [decidable P] (a b : α) (c d : β) :
+  f (ite P a b) (ite P c d) = ite P (f a c) (f b d) :=
+apply_dite2 f P (λ _, a) (λ _, b) (λ _, c) (λ _, d)
+
 lemma dite_apply {α : Type*} {β : α → Type*} (P : Prop) [decidable P]
   (f : P → Π a, β a) (g : ¬ P → Π a, β a) (x : α) :
   (dite P f g) x = dite P (λ h, f h x) (λ h, g h x) :=