Coe map₂

@[simp] lemma coe_map₂ (B : E →L[ℝ] F →L[ℝ] G) (V : SimpleProcess E 𝓕)    (W : SimpleProcess F 𝓕) : ⇑(map₂ B V W) = fun i ω ↦ B (⇑V i ω) (⇑W i ω) := by  ext i ω  calc    _ = ({⊥} : Set ι).indicator (fun _ ↦ B (V.valueBot ω) (W.valueBot ω)) i +      V.value.sum fun p v ↦ W.value.sum fun q w ↦        (Finsupp.single (p.1 ⊔ q.1, p.2 ⊓ q.2)          (if q.1 ≤ p.2 ∧ p.1 ≤ q.2 then fun ω ↦ B (v ω) (w ω) else 0)).sum          fun p' v' ↦ (Set.Ioc p'.1 p'.2).indicator (fun _ ↦ v' ω) i := by      simp [apply_eq, Finsupp.sum_sum_index, Set.indicator_add]    _ = ({⊥} : Set ι).indicator (fun _ ↦ B (V.valueBot ω) (W.valueBot ω)) i +      V.value.sum fun p v ↦ W.value.sum fun q w ↦        (Set.Ioc (p.1 ⊔ q.1) (p.2 ⊓ q.2)).indicator (fun _ ↦ B (v ω) (w ω)) i := by      congr! with p v q w      split_ifs with h_le      · simp      · have : p.2 < q.1 ∨ q.2 < p.1 := by contrapose! h_le; exact h_le        have : p.2 ⊓ q.2 < p.1 ⊔ q.1 := by simp; tauto        simp [Set.Ioc_eq_empty_of_le this.le]    _ = B (V i ω) (W i ω) := by      have h1 (s t : Set ι) (f : ι → E) (g : ι → F) (i : ι) :          B (s.indicator f i) (t.indicator g i) = (s ∩ t).indicator (fun j ↦ B (f j) (g j)) i := by        rw [← Set.indicator_indicator]        unfold Set.indicator        split_ifs <;> simp      by_cases hi : i = ⊥      · simp [hi, apply_eq]      · simp [apply_eq, map_finsuppSum, h1, Set.Ioc_inter_Ioc, Pi.single_apply]        simp [hi]