. intros y y_in_union
  if y_in : y ∈ Y2 then
    rcases (Ord2 y y_in) with ⟨x, x_in_X2, y_lt_x⟩
    if x_in : x ∈ Y1 then
      rcases (Ord1 x x_in) with ⟨x', x'_in_X1, x_lt_x'⟩
      use x'
      constructor
      . rw [Multiset.mem_add]
        constructor
        exact x'_in_X1
      . exact lt_trans y_lt_x x_lt_x'
      else
        use x
        constructor
        . rw [add_comm]
          rw [Multiset.mem_add]
          constructor
          apply in_notin_diff
          exact x_in_X2
          exact x_in
        . exact y_lt_x
    else
      have y_in : y ∈ (Y1 - X2) := by aesop
      let h := (Ord1 y)
      have y_in_Y1 : y ∈ Y1 := by
        have : Y1 - X2 ≤ Y1 := by aesop
        apply Multiset.mem_of_le
        exact this
        exact y_in
      let _ := h y_in_Y1
      aesop
case MLT.MLT.a
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P Y1 X1 Z1 : Multiset α
X1_ne : X1 ≠ ∅
N1_def : N = Z1 + Y1
M1_def : M = Z1 + X1
Ord1 : ∀ x ∈ Y1, ∃ y ∈ X1, x < y
Y2 X2 Z2 : Multiset α
a✝ : X2 ≠ ∅
P2_def : P = Z2 + Y2
N2_def : N = Z2 + X2
Ord2 : ∀ x ∈ Y2, ∃ y ∈ X2, x < y
⊢ ∀ x ∈ Y2 + (Y1 - X2), ∃ y ∈ X1 + (X2 - Y1), x < y
no goals