Map Union union map Union

public theorem mapUnion_union_mapUnion' {α β} [LT α] [StrictLT α] [DecidableLT α] {f g : β → Set α} {xs : List β} :  (∀ x ∈ xs, (f x).WellFormed ∧ (g x).WellFormed) →  List.mapUnion f xs ∪ List.mapUnion g xs = List.mapUnion (λ x => f x ∪ g x) xs:= by  cases xs  case nil => simp [mapUnion, EmptyCollection.emptyCollection, Set.union_empty_left Set.empty_wf]  case cons hd tl =>    intro wf    simp only [mem_cons, forall_eq_or_imp] at wf    replace ⟨⟨fwf, gwf⟩, tlwf⟩ := wf ; clear wf    rw [mapUnion_cons, mapUnion_cons, mapUnion_cons]    · have ih := mapUnion_union_mapUnion' tlwf      rw [Set.union_assoc]      conv => lhs ; rhs ; rw [← Set.union_assoc] ; lhs ; rw [Set.union_comm]      conv => lhs ; rhs ; rw [Set.union_assoc, ih]      simp [Set.union_assoc]    · intro b hb ; cases hb      · exact Set.union_wf _ _      · exact Set.union_wf _ _    · intro b hb ; cases hb      case head => exact gwf      case tail htl => exact (tlwf b htl).right    · intro b hb ; cases hb      case head => exact fwf      case tail htl => exact (tlwf b htl).left