rw [N1_def]
case MLT.MLT.a.x.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
this✝ : Z1 ∩ Z2 + (Y2 + (Y1 - X2)) = Z1 ∩ Z2 + (Y1 - X2) + Y2
this : Z1 ∩ Z2 + (Y1 - X2) = Z2 ∩ Z1 + (Y1 - X2)
⊢ N = Y1 + Z1
case MLT.MLT.a.x.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
this✝ : Z1 ∩ Z2 + (Y2 + (Y1 - X2)) = Z1 ∩ Z2 + (Y1 - X2) + Y2
this : Z1 ∩ Z2 + (Y1 - X2) = Z2 ∩ Z1 + (Y1 - X2)
⊢ Z1 + Y1 = Y1 + Z1