change fx ≤ x at count_lt
case intro.a.MZX.a
α : Type u_1
dec : DecidableEq α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x y => x < y
Y M N X Z : Multiset α
y : α
newY : Multiset α := Y.erase y
f : α → Multiset α := fun y' => Multiset.filter (fun x => x < y') X
N' : Multiset α := Z + newY + f y
a : α
IH :
  ∀ t < Y,
    ¬t = 0 →
      ∀ (M N X Z : Multiset α), M = Z + X → N = Z + t → (∀ x ∈ X, ∃ y ∈ t, x < y) → TC MultisetRedLt (Z + X) (Z + t)
Y_not_empty : ¬Y = 0
M_def : M = Z + X
N_def : N = Z + Y
X_lt_Y : ∀ x ∈ X, ∃ y ∈ Y, x < y
hyp : ¬Multiset.card Y = 1
claim : y ∈ Y
newY_nonEmpty : ¬newY = 0
newY_sub_Y : newY < Y
this : f y ≤ X
count_lt : Multiset.count a (f y) ≤ Multiset.count a X
x : ℕ := Multiset.count a X
z : ℕ := Multiset.count a Z
fx : ℕ := Multiset.count a (Multiset.filter (fun x => x < y) X)
⊢ z + x = z + fx + (x - fx)
case intro.a.MZX.a
α : Type u_1
dec : DecidableEq α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x y => x < y
Y M N X Z : Multiset α
y : α
newY : Multiset α := Y.erase y
f : α → Multiset α := fun y' => Multiset.filter (fun x => x < y') X
N' : Multiset α := Z + newY + f y
a : α
IH :
  ∀ t < Y,
    ¬t = 0 →
      ∀ (M N X Z : Multiset α), M = Z + X → N = Z + t → (∀ x ∈ X, ∃ y ∈ t, x < y) → TC MultisetRedLt (Z + X) (Z + t)
Y_not_empty : ¬Y = 0
M_def : M = Z + X
N_def : N = Z + Y
X_lt_Y : ∀ x ∈ X, ∃ y ∈ Y, x < y
hyp : ¬Multiset.card Y = 1
claim : y ∈ Y
newY_nonEmpty : ¬newY = 0
newY_sub_Y : newY < Y
this : f y ≤ X
x : ℕ := Multiset.count a X
z : ℕ := Multiset.count a Z
fx : ℕ := Multiset.count a (Multiset.filter (fun x => x < y) X)
count_lt : fx ≤ x
⊢ z + x = z + fx + (x - fx)