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
case intro.intro
α : 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
y : α
y_in_union : y ∈ Y2 + (Y1 - X2)
y_in : y ∈ Y2
x : α
x_in_X2 : x ∈ X2
y_lt_x : y < x
⊢ ∃ y_1 ∈ X1 + (X2 - Y1), y < y_1
no goals