-- Mathlib/Data/Multiset/DershowitzManna.lean
private lemma isDershowitzMannaLT_singleton_insert (h : OneStep N (a ::ₘ M)) :
    ∃ M', N = a ::ₘ M' ∧ OneStep M' M ∨ N = M + M' ∧ ∀ x ∈ M', x < a

Proof state:
case intro.intro.intro.intro.intro.inl
α : Type u_1
inst✝ : Preorder α
M : Multiset α
a : α
X Y : Multiset α
h0 : a ::ₘ M = X + {a}
h2 : ∀ y ∈ Y, y < a
⊢ X + Y = M + Y

Tactic:
simpa [add_comm _ {a}, singleton_add, eq_comm] using h0

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.inr.refine_1
α : Type u_1
inst✝ : Preorder α
M : Multiset α
a : α
X Y : Multiset α
b : α
h0 : M + {a} = X + {b}
h2 : ∀ y ∈ Y, y < b
hab : a ≠ b
⊢ X + Y = a ::ₘ (Y + (M - {b}))

Tactic:
rw [tsub_eq_tsub_of_add_eq_add h0, add_comm Y, ← singleton_add, ← add_assoc,
  add_tsub_cancel_of_le]

Result:
case intro.intro.intro.intro.intro.inr.refine_1
α : Type u_1
inst✝ : Preorder α
M : Multiset α
a : α
X Y : Multiset α
b : α
h0 : M + {a} = X + {b}
h2 : ∀ y ∈ Y, y < b
hab : a ≠ b
⊢ {a} ≤ X

Proof state:
case intro.intro.intro.intro.intro.inr
α : Type u_1
inst✝ : Preorder α
M : Multiset α
a : α
X Y : Multiset α
b : α
h0 : a ::ₘ M = X + {b}
h2 : ∀ y ∈ Y, y < b
hab : a ≠ b
⊢ ∃ M', X + Y = a ::ₘ M' ∧ Multiset.OneStep M' M ∨ X + Y = M + M' ∧ ∀ x ∈ M', x < a

Tactic:
refine ⟨Y + (M - {b}), .inl ⟨?_, M - {b}, Y, b, add_comm .., ?_, h2⟩⟩

Result:
case intro.intro.intro.intro.intro.inr.refine_1
α : Type u_1
inst✝ : Preorder α
M : Multiset α
a : α
X Y : Multiset α
b : α
h0 : a ::ₘ M = X + {b}
h2 : ∀ y ∈ Y, y < b
hab : a ≠ b
⊢ X + Y = a ::ₘ (Y + (M - {b}))

case intro.intro.intro.intro.intro.inr.refine_2
α : Type u_1
inst✝ : Preorder α
M : Multiset α
a : α
X Y : Multiset α
b : α
h0 : a ::ₘ M = X + {b}
h2 : ∀ y ∈ Y, y < b
hab : a ≠ b
⊢ M = M - {b} + {b}

Proof state:
case intro.intro.intro.intro.intro.inr.refine_2
α : Type u_1
inst✝ : Preorder α
M : Multiset α
a : α
X Y : Multiset α
b : α
h0 : a ::ₘ M = X + {b}
h2 : ∀ y ∈ Y, y < b
hab : a ≠ b
this : b ∈ a ::ₘ M
⊢ {b} ≤ M

Tactic:
simpa [hab.symm] using this

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.inr.refine_2
α : Type u_1
inst✝ : Preorder α
M : Multiset α
a : α
X Y : Multiset α
b : α
h0 : a ::ₘ M = X + {b}
h2 : ∀ y ∈ Y, y < b
hab : a ≠ b
⊢ {b} ≤ M

Tactic:
have : b ∈ a ::ₘ M := by simp [h0]

Result:
case intro.intro.intro.intro.intro.inr.refine_2
α : Type u_1
inst✝ : Preorder α
M : Multiset α
a : α
X Y : Multiset α
b : α
h0 : a ::ₘ M = X + {b}
h2 : ∀ y ∈ Y, y < b
hab : a ≠ b
this : b ∈ a ::ₘ M
⊢ {b} ≤ M

Proof state:
α : Type u_1
inst✝ : Preorder α
M N : Multiset α
a : α
h : Multiset.OneStep N (a ::ₘ M)
⊢ ∃ M', N = a ::ₘ M' ∧ Multiset.OneStep M' M ∨ N = M + M' ∧ ∀ x ∈ M', x < a

Tactic:
obtain ⟨X, Y, b, rfl, h0, h2⟩ := h

Result:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝ : Preorder α
M : Multiset α
a : α
X Y : Multiset α
b : α
h0 : a ::ₘ M = X + {b}
h2 : ∀ y ∈ Y, y < b
⊢ ∃ M', X + Y = a ::ₘ M' ∧ Multiset.OneStep M' M ∨ X + Y = M + M' ∧ ∀ x ∈ M', x < a

Proof state:
α : Type u_1
inst✝ : Preorder α
M : Multiset α
a : α
X Y : Multiset α
b : α
h0 : a ::ₘ M = X + {b}
h2 : ∀ y ∈ Y, y < b
hab : a ≠ b
⊢ b ∈ a ::ₘ M

Tactic:
simp [h0]

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝ : Preorder α
M : Multiset α
a : α
X Y : Multiset α
b : α
h0 : a ::ₘ M = X + {b}
h2 : ∀ y ∈ Y, y < b
⊢ ∃ M', X + Y = a ::ₘ M' ∧ Multiset.OneStep M' M ∨ X + Y = M + M' ∧ ∀ x ∈ M', x < a

Tactic:
obtain rfl | hab := eq_or_ne a b

Result:
case intro.intro.intro.intro.intro.inl
α : Type u_1
inst✝ : Preorder α
M : Multiset α
a : α
X Y : Multiset α
h0 : a ::ₘ M = X + {a}
h2 : ∀ y ∈ Y, y < a
⊢ ∃ M', X + Y = a ::ₘ M' ∧ Multiset.OneStep M' M ∨ X + Y = M + M' ∧ ∀ x ∈ M', x < a

case intro.intro.intro.intro.intro.inr
α : Type u_1
inst✝ : Preorder α
M : Multiset α
a : α
X Y : Multiset α
b : α
h0 : a ::ₘ M = X + {b}
h2 : ∀ y ∈ Y, y < b
hab : a ≠ b
⊢ ∃ M', X + Y = a ::ₘ M' ∧ Multiset.OneStep M' M ∨ X + Y = M + M' ∧ ∀ x ∈ M', x < a

Proof state:
case intro.intro.intro.intro.intro.inl
α : Type u_1
inst✝ : Preorder α
M : Multiset α
a : α
X Y : Multiset α
h0 : a ::ₘ M = X + {a}
h2 : ∀ y ∈ Y, y < a
⊢ ∃ M', X + Y = a ::ₘ M' ∧ Multiset.OneStep M' M ∨ X + Y = M + M' ∧ ∀ x ∈ M', x < a

Tactic:
refine ⟨Y, .inr ⟨?_, h2⟩⟩

Result:
case intro.intro.intro.intro.intro.inl
α : Type u_1
inst✝ : Preorder α
M : Multiset α
a : α
X Y : Multiset α
h0 : a ::ₘ M = X + {a}
h2 : ∀ y ∈ Y, y < a
⊢ X + Y = M + Y

Proof state:
case intro.intro.intro.intro.intro.inr.refine_2
α : Type u_1
inst✝ : Preorder α
M : Multiset α
a : α
X Y : Multiset α
b : α
h0 : a ::ₘ M = X + {b}
h2 : ∀ y ∈ Y, y < b
hab : a ≠ b
⊢ M = M - {b} + {b}

Tactic:
rw [tsub_add_cancel_of_le]

Result:
case intro.intro.intro.intro.intro.inr.refine_2
α : Type u_1
inst✝ : Preorder α
M : Multiset α
a : α
X Y : Multiset α
b : α
h0 : a ::ₘ M = X + {b}
h2 : ∀ y ∈ Y, y < b
hab : a ≠ b
⊢ {b} ≤ M

Proof state:
case intro.intro.intro.intro.intro.inr.refine_1
α : Type u_1
inst✝ : Preorder α
M : Multiset α
a : α
X Y : Multiset α
b : α
h0 : M + {a} = X + {b}
h2 : ∀ y ∈ Y, y < b
hab : a ≠ b
⊢ {a} ≤ X

Tactic:
have : a ∈ X + {b} := by simp [← h0]

Result:
case intro.intro.intro.intro.intro.inr.refine_1
α : Type u_1
inst✝ : Preorder α
M : Multiset α
a : α
X Y : Multiset α
b : α
h0 : M + {a} = X + {b}
h2 : ∀ y ∈ Y, y < b
hab : a ≠ b
this : a ∈ X + {b}
⊢ {a} ≤ X

Proof state:
α : Type u_1
inst✝ : Preorder α
M : Multiset α
a : α
X Y : Multiset α
b : α
h0 : M + {a} = X + {b}
h2 : ∀ y ∈ Y, y < b
hab : a ≠ b
⊢ a ∈ X + {b}

Tactic:
simp [← h0]

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.inr.refine_1
α : Type u_1
inst✝ : Preorder α
M : Multiset α
a : α
X Y : Multiset α
b : α
h0 : M + {a} = X + {b}
h2 : ∀ y ∈ Y, y < b
hab : a ≠ b
this : a ∈ X + {b}
⊢ {a} ≤ X

Tactic:
simpa [hab] using this

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.inr.refine_1
α : Type u_1
inst✝ : Preorder α
M : Multiset α
a : α
X Y : Multiset α
b : α
h0 : a ::ₘ M = X + {b}
h2 : ∀ y ∈ Y, y < b
hab : a ≠ b
⊢ X + Y = a ::ₘ (Y + (M - {b}))

Tactic:
rw [← singleton_add, add_comm] at h0

Result:
case intro.intro.intro.intro.intro.inr.refine_1
α : Type u_1
inst✝ : Preorder α
M : Multiset α
a : α
X Y : Multiset α
b : α
h0 : M + {a} = X + {b}
h2 : ∀ y ∈ Y, y < b
hab : a ≠ b
⊢ X + Y = a ::ₘ (Y + (M - {b}))