awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Multiset.DershowitzManna (goal)
Goal:
α : Type u_1
inst : Preorder α
M N P : Multiset α
rintro :
  ∀ (X₁ Y₁ Z₁ : Multiset α) (hYZ₁ : ∀ (y : α), y ∈ Y₁ → ∃ (z : α), z ∈ Z₁ ∧ y < z) (X₂ Y₂ Z₂ : Multiset α)
    (hZ₂ : Z₂ ≠ ∅) (hXZXY : X₁ + Z₁ = X₂ + Y₂) (hYZ₂ : ∀ (y : α), y ∈ Y₂ → ∃ (z : α), z ∈ Z₂ ∧ y < z),
    (X₁ + Y₁).IsDershowitzMannaLT (X₂ + Z₂)
rintro₁ :
  ∀ (X₁ Y₁ Z₁ : Multiset α) (hYZ₁ : ∀ (y : α), y ∈ Y₁ → ∃ (z : α), z ∈ Z₁ ∧ y < z) (X₂ Y₂ Z₂ : Multiset α)
    (hZ₂ : Z₂ ≠ ∅) (hXZXY : Z₁ + X₁ = Y₂ + X₂) (hYZ₂ : ∀ (y : α), y ∈ Y₂ → ∃ (z : α), z ∈ Z₂ ∧ y < z),
    (X₁ + Y₁).IsDershowitzMannaLT (X₂ + Z₂)
refine_1 :
  ∀ (X₁ Y₁ Z₁ : Multiset α) (hYZ₁ : ∀ (y : α), y ∈ Y₁ → ∃ (z : α), z ∈ Z₁ ∧ y < z) (X₂ Y₂ Z₂ : Multiset α)
    (hZ₂ : Z₂ ≠ ∅) (hXZXY : Z₁ + X₁ = Y₂ + X₂) (hYZ₂ : ∀ (y : α), y ∈ Y₂ → ∃ (z : α), z ∈ Z₂ ∧ y < z),
    Z₂ + (Z₁ - Y₂) ≠ ∅
refine_2 :
  ∀ (X₁ Y₁ Z₁ : Multiset α) (hYZ₁ : ∀ (y : α), y ∈ Y₁ → ∃ (z : α), z ∈ Z₁ ∧ y < z) (X₂ Y₂ Z₂ : Multiset α)
    (hZ₂ : Z₂ ≠ ∅) (hXZXY : Z₁ + X₁ = Y₂ + X₂) (hYZ₂ : ∀ (y : α), y ∈ Y₂ → ∃ (z : α), z ∈ Z₂ ∧ y < z),
    X₁ + Y₁ = X₁ ∩ X₂ + (Y₁ + (Y₂ - Z₁))
⊢ M.IsDershowitzMannaLT N → N.IsDershowitzMannaLT P → M.IsDershowitzMannaLT P
have refine_3 : ∀ (X₁ Y₁ Z₁ : Multiset α) (hYZ₁ : ∀ (y : α), y ∈ Y₁ → ∃ (z : α), z ∈ Z₁ ∧ y < z) (X₂ Y₂ Z₂ : Multiset α) (hZ₂ : Z₂ ≠ ∅)
  (hXZXY : Z₁ + X₁ = Y₂ + X₂) (hYZ₂ : ∀ (y : α), y ∈ Y₂ → ∃ (z : α), z ∈ Z₂ ∧ y < z),
  X₂ + Z₂ = X₁ ∩ X₂ + (Z₂ + (Z₁ - Y₂))
Tactic: classical
  rintro ⟨X₁, Y₁, Z₁, -, rfl, rfl, hYZ₁⟩ ⟨X₂, Y₂, Z₂, hZ₂, hXZXY, rfl, hYZ₂⟩
  rw [add_comm X₁, add_comm X₂] at hXZXY
  refine ⟨X₁ ∩ X₂, Y₁ + (Y₂ - Z₁), Z₂ + (Z₁ - Y₂), ?_, ?_, ?_, ?_⟩
  · simpa [-not_and, not_and_or] using .inl hZ₂
  · rwa [← add_assoc, add_right_comm, inter_add_sub_of_add_eq_add]
  · rw [← add_assoc, add_right_comm, add_left_inj, inter_comm, inter_add_sub_of_add_eq_add]
    rwa [eq_comm]
  simp only [mem_add, or_imp, forall_and]
  refine ⟨fun y hy ↦ ?_, fun y hy ↦ ?_⟩
  · obtain ⟨z, hz, hyz⟩ := hYZ₁ y hy
    by_cases z_in : z ∈ Y₂
    · obtain ⟨w, hw, hzw⟩ := hYZ₂ z z_in
      exact ⟨w, .inl hw, hyz.trans hzw⟩
    · exact ⟨z, .inr <| by rwa [mem_sub, count_eq_zero_of_notMem z_in, count_pos], hyz⟩
  · obtain ⟨z, hz, hyz⟩ := hYZ₂ y <| mem_of_le (Multiset.sub_le_self ..) hy
    exact ⟨z, .inl hz, hyz⟩
Cleared hypotheses: M, N, P
-- Lean 4 proof step from Mathlib.Data.Multiset.DershowitzManna (goal)
Goal:
α : Type u_1
inst : Preorder α
M N P : Multiset α
rintro :
  ∀ (X₁ Y₁ Z₁ : Multiset α) (hYZ₁ : ∀ (y : α), y ∈ Y₁ → ∃ (z : α), z ∈ Z₁ ∧ y < z) (X₂ Y₂ Z₂ : Multiset α)
    (hZ₂ : Z₂ ≠ ∅) (hXZXY : X₁ + Z₁ = X₂ + Y₂) (hYZ₂ : ∀ (y : α), y ∈ Y₂ → ∃ (z : α), z ∈ Z₂ ∧ y < z),
    (X₁ + Y₁).IsDershowitzMannaLT (X₂ + Z₂)
rintro₁ :
  ∀ (X₁ Y₁ Z₁ : Multiset α) (hYZ₁ : ∀ (y : α), y ∈ Y₁ → ∃ (z : α), z ∈ Z₁ ∧ y < z) (X₂ Y₂ Z₂ : Multiset α)
    (hZ₂ : Z₂ ≠ ∅) (hXZXY : Z₁ + X₁ = Y₂ + X₂) (hYZ₂ : ∀ (y : α), y ∈ Y₂ → ∃ (z : α), z ∈ Z₂ ∧ y < z),
    (X₁ + Y₁).IsDershowitzMannaLT (X₂ + Z₂)
refine_1 :
  ∀ (X₁ Y₁ Z₁ : Multiset α) (hYZ₁ : ∀ (y : α), y ∈ Y₁ → ∃ (z : α), z ∈ Z₁ ∧ y < z) (X₂ Y₂ Z₂ : Multiset α)
    (hZ₂ : Z₂ ≠ ∅) (hXZXY : Z₁ + X₁ = Y₂ + X₂) (hYZ₂ : ∀ (y : α), y ∈ Y₂ → ∃ (z : α), z ∈ Z₂ ∧ y < z),
    Z₂ + (Z₁ - Y₂) ≠ ∅
refine_2 :
  ∀ (X₁ Y₁ Z₁ : Multiset α) (hYZ₁ : ∀ (y : α), y ∈ Y₁ → ∃ (z : α), z ∈ Z₁ ∧ y < z) (X₂ Y₂ Z₂ : Multiset α)
    (hZ₂ : Z₂ ≠ ∅) (hXZXY : Z₁ + X₁ = Y₂ + X₂) (hYZ₂ : ∀ (y : α), y ∈ Y₂ → ∃ (z : α), z ∈ Z₂ ∧ y < z),
    X₁ + Y₁ = X₁ ∩ X₂ + (Y₁ + (Y₂ - Z₁))
refine_3 :
  ∀ (X₁ Y₁ Z₁ : Multiset α) (hYZ₁ : ∀ (y : α), y ∈ Y₁ → ∃ (z : α), z ∈ Z₁ ∧ y < z) (X₂ Y₂ Z₂ : Multiset α)
    (hZ₂ : Z₂ ≠ ∅) (hXZXY : Z₁ + X₁ = Y₂ + X₂) (hYZ₂ : ∀ (y : α), y ∈ Y₂ → ∃ (z : α), z ∈ Z₂ ∧ y < z),
    X₂ + Z₂ = X₁ ∩ X₂ + (Z₂ + (Z₁ - Y₂))
⊢ M.IsDershowitzMannaLT N → N.IsDershowitzMannaLT P → M.IsDershowitzMannaLT P
have refine_4 : ∀ (X₁ Y₁ Z₁ : Multiset α) (hYZ₁ : ∀ (y : α), y ∈ Y₁ → ∃ (z : α), z ∈ Z₁ ∧ y < z) (X₂ Y₂ Z₂ : Multiset α) (hZ₂ : Z₂ ≠ ∅)
  (hXZXY : Z₁ + X₁ = Y₂ + X₂) (hYZ₂ : ∀ (y : α), y ∈ Y₂ → ∃ (z : α), z ∈ Z₂ ∧ y < z) (y : α),
  y ∈ Y₁ + (Y₂ - Z₁) → ∃ (z : α), z ∈ Z₂ + (Z₁ - Y₂) ∧ y < z
Tactic: classical
  rintro ⟨X₁, Y₁, Z₁, -, rfl, rfl, hYZ₁⟩ ⟨X₂, Y₂, Z₂, hZ₂, hXZXY, rfl, hYZ₂⟩
  rw [add_comm X₁, add_comm X₂] at hXZXY
  refine ⟨X₁ ∩ X₂, Y₁ + (Y₂ - Z₁), Z₂ + (Z₁ - Y₂), ?_, ?_, ?_, ?_⟩
  · simpa [-not_and, not_and_or] using .inl hZ₂
  · rwa [← add_assoc, add_right_comm, inter_add_sub_of_add_eq_add]
  · rw [← add_assoc, add_right_comm, add_left_inj, inter_comm, inter_add_sub_of_add_eq_add]
    rwa [eq_comm]
  simp only [mem_add, or_imp, forall_and]
  refine ⟨fun y hy ↦ ?_, fun y hy ↦ ?_⟩
  · obtain ⟨z, hz, hyz⟩ := hYZ₁ y hy
    by_cases z_in : z ∈ Y₂
    · obtain ⟨w, hw, hzw⟩ := hYZ₂ z z_in
      exact ⟨w, .inl hw, hyz.trans hzw⟩
    · exact ⟨z, .inr <| by rwa [mem_sub, count_eq_zero_of_notMem z_in, count_pos], hyz⟩
  · obtain ⟨z, hz, hyz⟩ := hYZ₂ y <| mem_of_le (Multiset.sub_le_self ..) hy
    exact ⟨z, .inl hz, hyz⟩
Cleared hypotheses: M, N, P
-- Lean 4 proof step from Mathlib.Data.Multiset.DershowitzManna (goal)
Goal:
α : Type u_1
inst : Preorder α
M N X Y : Multiset α
a : α
M_def : M = X + Y
N_def : N = X + {a}
ys_lt_a : ∀ (y : α), y ∈ Y → y < a
⊢ M.IsDershowitzMannaLT N
have right : ∀ (y : α), y ∈ Y → ∃ (z : α), Membership.mem (γ := Multiset α) {a} z ∧ y < z
Tactic: use X, Y, {a}, by simp, M_def, N_def
-- Lean 4 proof step from Mathlib.Data.Multiset.DershowitzManna (goal)
Goal:
α : Type u_1
inst : Preorder α
M N : Multiset α
a : α
h : N.OneStep (a ::ₘ M)
⊢ ∃ (M' : Multiset α), N = a ::ₘ M' ∧ M'.OneStep M ∨ N = M + M' ∧ ∀ (x : α), x ∈ M' → x < a
have obtain : ∀ (X Y : Multiset α) (b : α) (h0 : a ::ₘ M = X + {b}) (h2 : ∀ (y : α), y ∈ Y → y < b),
  ∃ (M' : Multiset α), X + Y = a ::ₘ M' ∧ M'.OneStep M ∨ X + Y = M + M' ∧ ∀ (x : α), x ∈ M' → x < a
Tactic: obtain ⟨X, Y, b, rfl, h0, h2⟩ := h
Cleared hypotheses: N, h
-- Lean 4 proof step from Mathlib.Data.Multiset.DershowitzManna (goal)
Goal:
α : Type u_1
inst : Preorder α
M : Multiset α
a : α
X Y : Multiset α
b : α
h0 : a ::ₘ M = X + {b}
h2 : ∀ (y : α), y ∈ Y → y < b
⊢ ∃ (M' : Multiset α), X + Y = a ::ₘ M' ∧ M'.OneStep M ∨ X + Y = M + M' ∧ ∀ (x : α), x ∈ M' → x < a
have inl : ∀ (h0 : a ::ₘ M = X + {a}) (h2 : ∀ (y : α), y ∈ Y → y < a),
  ∃ (M' : Multiset α), X + Y = a ::ₘ M' ∧ M'.OneStep M ∨ X + Y = M + M' ∧ ∀ (x : α), x ∈ M' → x < a
Tactic: obtain rfl | hab := eq_or_ne a b
Cleared hypotheses: b, h0, h2
-- Lean 4 proof step from Mathlib.Data.Multiset.DershowitzManna (goal)
Goal:
α : Type u_1
inst : Preorder α
M : Multiset α
a : α
X Y : Multiset α
b : α
h0 : a ::ₘ M = X + {b}
h2 : ∀ (y : α), y ∈ Y → y < b
inl :
  ∀ (h0 : a ::ₘ M = X + {a}) (h2 : ∀ (y : α), y ∈ Y → y < a),
    ∃ (M' : Multiset α), X + Y = a ::ₘ M' ∧ M'.OneStep M ∨ X + Y = M + M' ∧ ∀ (x : α), x ∈ M' → x < a
⊢ ∃ (M' : Multiset α), X + Y = a ::ₘ M' ∧ M'.OneStep M ∨ X + Y = M + M' ∧ ∀ (x : α), x ∈ M' → x < a
have inr : ∀ (hab : a ≠ b), ∃ (M' : Multiset α), X + Y = a ::ₘ M' ∧ M'.OneStep M ∨ X + Y = M + M' ∧ ∀ (x : α), x ∈ M' → x < a
Tactic: obtain rfl | hab := eq_or_ne a b
-- Lean 4 proof step from Mathlib.Data.Multiset.DershowitzManna (goal)
Goal:
α : Type u_1
inst : Preorder α
M : Multiset α
a : α
X Y : Multiset α
h0 : a ::ₘ M = X + {a}
h2 : ∀ (y : α), y ∈ Y → y < a
⊢ ∃ (M' : Multiset α), X + Y = a ::ₘ M' ∧ M'.OneStep M ∨ X + Y = M + M' ∧ ∀ (x : α), x ∈ M' → x < a
have inl : X + Y = M + Y
Tactic: refine ⟨Y, .inr ⟨?_, h2⟩⟩
-- Lean 4 proof step from Mathlib.Data.Multiset.DershowitzManna (goal)
Goal:
α : Type u_1
inst : Preorder α
M : Multiset α
a : α
X Y : Multiset α
b : α
h0 : a ::ₘ M = X + {b}
h2 : ∀ (y : α), y ∈ Y → y < b
hab : a ≠ b
⊢ ∃ (M' : Multiset α), X + Y = a ::ₘ M' ∧ M'.OneStep M ∨ X + Y = M + M' ∧ ∀ (x : α), x ∈ M' → x < a
have inr : X + Y = a ::ₘ (Y + (M - {b}))
Tactic: refine ⟨Y + (M - {b}), .inl ⟨?_, M - {b}, Y, b, add_comm .., ?_, h2⟩⟩
-- Lean 4 proof step from Mathlib.Data.Multiset.DershowitzManna (goal)
Goal:
α : Type u_1
inst : Preorder α
M : Multiset α
a : α
X Y : Multiset α
b : α
h0 : a ::ₘ M = X + {b}
h2 : ∀ (y : α), y ∈ Y → y < b
hab : a ≠ b
inr : X + Y = a ::ₘ (Y + (M - {b}))
⊢ ∃ (M' : Multiset α), X + Y = a ::ₘ M' ∧ M'.OneStep M ∨ X + Y = M + M' ∧ ∀ (x : α), x ∈ M' → x < a
have inr₁ : M = M - {b} + {b}
Tactic: refine ⟨Y + (M - {b}), .inl ⟨?_, M - {b}, Y, b, add_comm .., ?_, h2⟩⟩
-- Lean 4 proof step from Mathlib.Data.Multiset.DershowitzManna (hypothesis)
Goal:
α : Type u_1
inst : Preorder α
M : Multiset α
a : α
X Y : Multiset α
b : α
h0 : a ::ₘ M = X + {b}
h2 : ∀ (y : α), y ∈ Y → y < b
hab : a ≠ b
⊢ X + Y = a ::ₘ (Y + (M - {b}))
have h0₁ : M + {a} = X + {b}
Tactic: rw [← singleton_add, add_comm] at h0
Cleared hypotheses: h0, h2, hab
-- Lean 4 proof step from Mathlib.Data.Multiset.DershowitzManna (goal)
Goal:
α : Type u_1
inst : Preorder α
M : Multiset α
a : α
X Y : Multiset α
b : α
h0 : M + {a} = X + {b}
h2 : ∀ (y : α), y ∈ Y → y < b
hab : a ≠ b
⊢ X + Y = a ::ₘ (Y + (M - {b}))
have inr : {a} ≤ X
Tactic: rw [tsub_eq_tsub_of_add_eq_add h0, add_comm Y, ← singleton_add, ← add_assoc,
      add_tsub_cancel_of_le]
-- Lean 4 proof step from Mathlib.Data.Multiset.DershowitzManna (hypothesis)
Goal:
α : Type u_1
inst : Preorder α
M : Multiset α
a : α
X Y : Multiset α
b : α
h0 : M + {a} = X + {b}
h2 : ∀ (y : α), y ∈ Y → y < b
hab : a ≠ b
⊢ {a} ≤ X
have this : a ∈ X + {b}
Tactic: have : a ∈ X + {b} := by simp [← h0]
-- Lean 4 proof step from Mathlib.Data.Multiset.DershowitzManna (goal)
Goal:
α : Type u_1
inst : Preorder α
M : Multiset α
a : α
X Y : Multiset α
b : α
h0 : a ::ₘ M = X + {b}
h2 : ∀ (y : α), y ∈ Y → y < b
hab : a ≠ b
⊢ M = M - {b} + {b}
have inr : {b} ≤ M
Tactic: rw [tsub_add_cancel_of_le]
-- Lean 4 proof step from Mathlib.Data.Multiset.DershowitzManna (hypothesis)
Goal:
α : Type u_1
inst : Preorder α
M : Multiset α
a : α
X Y : Multiset α
b : α
h0 : a ::ₘ M = X + {b}
h2 : ∀ (y : α), y ∈ Y → y < b
hab : a ≠ b
⊢ {b} ≤ M
have this : b ∈ a ::ₘ M
Tactic: have : b ∈ a ::ₘ M := by simp [h0]
-- Lean 4 proof step from Mathlib.Data.Multiset.DershowitzManna (goal)
Goal:
α : Type u_1
inst : Preorder α
M N : Multiset α
a : α
h : N.OneStep (a ::ₘ M)
⊢ ∃ (M' : Multiset α), N = a ::ₘ M' ∧ M'.OneStep M ∨ N = M + M' ∧ ∀ (x : α), x ∈ M' → x < a
have obtain : ∀ (X Y : Multiset α) (b : α) (h0 : a ::ₘ M = X + {b}) (h2 : ∀ (y : α), y ∈ Y → y < b),
  ∃ (M' : Multiset α), X + Y = a ::ₘ M' ∧ M'.OneStep M ∨ X + Y = M + M' ∧ ∀ (x : α), x ∈ M' → x < a
Tactic: classical
  obtain ⟨X, Y, b, rfl, h0, h2⟩ := h
  obtain rfl | hab := eq_or_ne a b
  · refine ⟨Y, .inr ⟨?_, h2⟩⟩
    simpa [add_comm _ {a}, singleton_add, eq_comm] using h0
  refine ⟨Y + (M - {b}), .inl ⟨?_, M - {b}, Y, b, add_comm .., ?_, h2⟩⟩
  · rw [← singleton_add, add_comm] at h0
    rw [tsub_eq_tsub_of_add_eq_add h0, add_comm Y, ← singleton_add, ← add_assoc,
      add_tsub_cancel_of_le]
    have : a ∈ X + {b} := by simp [← h0]
    simpa [hab] using this
  · rw [tsub_add_cancel_of_le]
    have : b ∈ a ::ₘ M := by simp [h0]
    simpa [hab.symm] using this
Cleared hypotheses: N, h
-- Lean 4 proof step from Mathlib.Data.Multiset.DershowitzManna (goal)
Goal:
α : Type u_1
inst : Preorder α
M N : Multiset α
a : α
h : N.OneStep (a ::ₘ M)
obtain :
  ∀ (X Y : Multiset α) (b : α) (h0 : a ::ₘ M = X + {b}) (h2 : ∀ (y : α), y ∈ Y → y < b),
    ∃ (M' : Multiset α), X + Y = a ::ₘ M' ∧ M'.OneStep M ∨ X + Y = M + M' ∧ ∀ (x : α), x ∈ M' → x < a
⊢ ∃ (M' : Multiset α), N = a ::ₘ M' ∧ M'.OneStep M ∨ N = M + M' ∧ ∀ (x : α), x ∈ M' → x < a
have inl : ∀ (X Y : Multiset α) (h0 : a ::ₘ M = X + {a}) (h2 : ∀ (y : α), y ∈ Y → y < a),
  ∃ (M' : Multiset α), X + Y = a ::ₘ M' ∧ M'.OneStep M ∨ X + Y = M + M' ∧ ∀ (x : α), x ∈ M' → x < a
Tactic: classical
  obtain ⟨X, Y, b, rfl, h0, h2⟩ := h
  obtain rfl | hab := eq_or_ne a b
  · refine ⟨Y, .inr ⟨?_, h2⟩⟩
    simpa [add_comm _ {a}, singleton_add, eq_comm] using h0
  refine ⟨Y + (M - {b}), .inl ⟨?_, M - {b}, Y, b, add_comm .., ?_, h2⟩⟩
  · rw [← singleton_add, add_comm] at h0
    rw [tsub_eq_tsub_of_add_eq_add h0, add_comm Y, ← singleton_add, ← add_assoc,
      add_tsub_cancel_of_le]
    have : a ∈ X + {b} := by simp [← h0]
    simpa [hab] using this
  · rw [tsub_add_cancel_of_le]
    have : b ∈ a ::ₘ M := by simp [h0]
    simpa [hab.symm] using this
Cleared hypotheses: N, h
-- Lean 4 proof step from Mathlib.Data.Multiset.DershowitzManna (goal)
Goal:
α : Type u_1
inst : Preorder α
M N : Multiset α
a : α
h : N.OneStep (a ::ₘ M)
obtain :
  ∀ (X Y : Multiset α) (b : α) (h0 : a ::ₘ M = X + {b}) (h2 : ∀ (y : α), y ∈ Y → y < b),
    ∃ (M' : Multiset α), X + Y = a ::ₘ M' ∧ M'.OneStep M ∨ X + Y = M + M' ∧ ∀ (x : α), x ∈ M' → x < a
inl :
  ∀ (X Y : Multiset α) (h0 : a ::ₘ M = X + {a}) (h2 : ∀ (y : α), y ∈ Y → y < a),
    ∃ (M' : Multiset α), X + Y = a ::ₘ M' ∧ M'.OneStep M ∨ X + Y = M + M' ∧ ∀ (x : α), x ∈ M' → x < a
⊢ ∃ (M' : Multiset α), N = a ::ₘ M' ∧ M'.OneStep M ∨ N = M + M' ∧ ∀ (x : α), x ∈ M' → x < a
have inr : ∀ (X Y : Multiset α) (b : α) (h0 : a ::ₘ M = X + {b}) (h2 : ∀ (y : α), y ∈ Y → y < b) (hab : a ≠ b),
  ∃ (M' : Multiset α), X + Y = a ::ₘ M' ∧ M'.OneStep M ∨ X + Y = M + M' ∧ ∀ (x : α), x ∈ M' → x < a
Tactic: classical
  obtain ⟨X, Y, b, rfl, h0, h2⟩ := h
  obtain rfl | hab := eq_or_ne a b
  · refine ⟨Y, .inr ⟨?_, h2⟩⟩
    simpa [add_comm _ {a}, singleton_add, eq_comm] using h0
  refine ⟨Y + (M - {b}), .inl ⟨?_, M - {b}, Y, b, add_comm .., ?_, h2⟩⟩
  · rw [← singleton_add, add_comm] at h0
    rw [tsub_eq_tsub_of_add_eq_add h0, add_comm Y, ← singleton_add, ← add_assoc,
      add_tsub_cancel_of_le]
    have : a ∈ X + {b} := by simp [← h0]
    simpa [hab] using this
  · rw [tsub_add_cancel_of_le]
    have : b ∈ a ::ₘ M := by simp [h0]
    simpa [hab.symm] using this
Cleared hypotheses: N, h
-- Lean 4 proof step from Mathlib.Data.Multiset.DershowitzManna (goal)
Goal:
α : Type u_1
inst : Preorder α
M N : Multiset α
a : α
h : N.OneStep (a ::ₘ M)
obtain :
  ∀ (X Y : Multiset α) (b : α) (h0 : a ::ₘ M = X + {b}) (h2 : ∀ (y : α), y ∈ Y → y < b),
    ∃ (M' : Multiset α), X + Y = a ::ₘ M' ∧ M'.OneStep M ∨ X + Y = M + M' ∧ ∀ (x : α), x ∈ M' → x < a
inl :
  ∀ (X Y : Multiset α) (h0 : a ::ₘ M = X + {a}) (h2 : ∀ (y : α), y ∈ Y → y < a),
    ∃ (M' : Multiset α), X + Y = a ::ₘ M' ∧ M'.OneStep M ∨ X + Y = M + M' ∧ ∀ (x : α), x ∈ M' → x < a
inr inr₁ :
  ∀ (X Y : Multiset α) (b : α) (h0 : a ::ₘ M = X + {b}) (h2 : ∀ (y : α), y ∈ Y → y < b) (hab : a ≠ b),
    ∃ (M' : Multiset α), X + Y = a ::ₘ M' ∧ M'.OneStep M ∨ X + Y = M + M' ∧ ∀ (x : α), x ∈ M' → x < a
⊢ ∃ (M' : Multiset α), N = a ::ₘ M' ∧ M'.OneStep M ∨ N = M + M' ∧ ∀ (x : α), x ∈ M' → x < a
have inr₂ : ∀ (X Y : Multiset α) (b : α) (h0 : a ::ₘ M = X + {b}) (h2 : ∀ (y : α), y ∈ Y → y < b) (hab : a ≠ b),
  X + Y = a ::ₘ (Y + (M - {b}))
Tactic: classical
  obtain ⟨X, Y, b, rfl, h0, h2⟩ := h
  obtain rfl | hab := eq_or_ne a b
  · refine ⟨Y, .inr ⟨?_, h2⟩⟩
    simpa [add_comm _ {a}, singleton_add, eq_comm] using h0
  refine ⟨Y + (M - {b}), .inl ⟨?_, M - {b}, Y, b, add_comm .., ?_, h2⟩⟩
  · rw [← singleton_add, add_comm] at h0
    rw [tsub_eq_tsub_of_add_eq_add h0, add_comm Y, ← singleton_add, ← add_assoc,
      add_tsub_cancel_of_le]
    have : a ∈ X + {b} := by simp [← h0]
    simpa [hab] using this
  · rw [tsub_add_cancel_of_le]
    have : b ∈ a ::ₘ M := by simp [h0]
    simpa [hab.symm] using this
Cleared hypotheses: N, h
-- Lean 4 proof step from Mathlib.Data.Multiset.DershowitzManna (goal)
Goal:
α : Type u_1
inst : Preorder α
M N : Multiset α
a : α
h : N.OneStep (a ::ₘ M)
obtain :
  ∀ (X Y : Multiset α) (b : α) (h0 : a ::ₘ M = X + {b}) (h2 : ∀ (y : α), y ∈ Y → y < b),
    ∃ (M' : Multiset α), X + Y = a ::ₘ M' ∧ M'.OneStep M ∨ X + Y = M + M' ∧ ∀ (x : α), x ∈ M' → x < a
inl :
  ∀ (X Y : Multiset α) (h0 : a ::ₘ M = X + {a}) (h2 : ∀ (y : α), y ∈ Y → y < a),
    ∃ (M' : Multiset α), X + Y = a ::ₘ M' ∧ M'.OneStep M ∨ X + Y = M + M' ∧ ∀ (x : α), x ∈ M' → x < a
inr inr₁ :
  ∀ (X Y : Multiset α) (b : α) (h0 : a ::ₘ M = X + {b}) (h2 : ∀ (y : α), y ∈ Y → y < b) (hab : a ≠ b),
    ∃ (M' : Multiset α), X + Y = a ::ₘ M' ∧ M'.OneStep M ∨ X + Y = M + M' ∧ ∀ (x : α), x ∈ M' → x < a
inr₂ :
  ∀ (X Y : Multiset α) (b : α) (h0 : a ::ₘ M = X + {b}) (h2 : ∀ (y : α), y ∈ Y → y < b) (hab : a ≠ b),
    X + Y = a ::ₘ (Y + (M - {b}))
⊢ ∃ (M' : Multiset α), N = a ::ₘ M' ∧ M'.OneStep M ∨ N = M + M' ∧ ∀ (x : α), x ∈ M' → x < a
have inr₃ : ∀ (X Y : Multiset α) (b : α) (h0 : a ::ₘ M = X + {b}) (h2 : ∀ (y : α), y ∈ Y → y < b) (hab : a ≠ b), M = M - {b} + {b}
Tactic: classical
  obtain ⟨X, Y, b, rfl, h0, h2⟩ := h
  obtain rfl | hab := eq_or_ne a b
  · refine ⟨Y, .inr ⟨?_, h2⟩⟩
    simpa [add_comm _ {a}, singleton_add, eq_comm] using h0
  refine ⟨Y + (M - {b}), .inl ⟨?_, M - {b}, Y, b, add_comm .., ?_, h2⟩⟩
  · rw [← singleton_add, add_comm] at h0
    rw [tsub_eq_tsub_of_add_eq_add h0, add_comm Y, ← singleton_add, ← add_assoc,
      add_tsub_cancel_of_le]
    have : a ∈ X + {b} := by simp [← h0]
    simpa [hab] using this
  · rw [tsub_add_cancel_of_le]
    have : b ∈ a ::ₘ M := by simp [h0]
    simpa [hab.symm] using this
Cleared hypotheses: N, h
-- Lean 4 proof step from Mathlib.Data.Multiset.DershowitzManna (goal)
Goal:
α : Type u_1
inst : Preorder α
a : α
ha : Acc LT.lt a
⊢ ∀ {M : Multiset α}, Acc OneStep M → Acc OneStep (a ::ₘ M)
have intro : ∀ (a : α),
  (∀ (y : α), y < a → Acc LT.lt y) →
    ∀ (ha : ∀ (y : α), y < a → ∀ {M : Multiset α}, Acc OneStep M → Acc OneStep (y ::ₘ M)) {M : Multiset α},
      Acc OneStep M → Acc OneStep (a ::ₘ M)
Tactic: induction ha with | _ a _ ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Data.Multiset.DershowitzManna (goal)
Goal:
α : Type u_1
inst : Preorder α
a_1 a : α
h : ∀ (y : α), y < a → Acc LT.lt y
ha : ∀ (y : α), y < a → ∀ {M : Multiset α}, Acc OneStep M → Acc OneStep (y ::ₘ M)
M : Multiset α
hM : Acc OneStep M
⊢ Acc OneStep (a ::ₘ M)
have intro : ∀ (M : Multiset α) (hM : ∀ (y : Multiset α), y.OneStep M → Acc OneStep y)
  (ihM : ∀ (y : Multiset α), y.OneStep M → Acc OneStep (a ::ₘ y)), Acc OneStep (a ::ₘ M)
Tactic: induction hM with | _ M hM ihM
Cleared hypotheses: hM
-- Lean 4 proof step from Mathlib.Data.Multiset.DershowitzManna (goal)
Goal:
α : Type u_1
inst : Preorder α
a_1 a : α
h : ∀ (y : α), y < a → Acc LT.lt y
ha : ∀ (y : α), y < a → ∀ {M : Multiset α}, Acc OneStep M → Acc OneStep (y ::ₘ M)
M_1 M : Multiset α
hM : ∀ (y : Multiset α), y.OneStep M → Acc OneStep y
ihM : ∀ (y : Multiset α), y.OneStep M → Acc OneStep (a ::ₘ y)
⊢ Acc OneStep (a ::ₘ M)
have intro : ∀ (N : Multiset α) (hNM : N.OneStep (a ::ₘ M)), Acc OneStep N
Tactic: refine .intro _ fun N hNM ↦ ?_
-- Lean 4 proof step from Mathlib.Data.Multiset.DershowitzManna (goal)
Goal:
α : Type u_1
inst : Preorder α
a_1 a : α
h : ∀ (y : α), y < a → Acc LT.lt y
ha : ∀ (y : α), y < a → ∀ {M : Multiset α}, Acc OneStep M → Acc OneStep (y ::ₘ M)
M_1 M : Multiset α
hM : ∀ (y : Multiset α), y.OneStep M → Acc OneStep y
ihM : ∀ (y : Multiset α), y.OneStep M → Acc OneStep (a ::ₘ y)
N : Multiset α
hNM : N.OneStep (a ::ₘ M)
⊢ Acc OneStep N
have intro : ∀ (N : Multiset α) (hNM' : N.OneStep M) (hNM : (a ::ₘ N).OneStep (a ::ₘ M)), Acc OneStep (a ::ₘ N)
Tactic: obtain ⟨N, ⟨rfl, hNM'⟩ | ⟨rfl, hN⟩⟩ := isDershowitzMannaLT_singleton_insert hNM
Cleared hypotheses: N, hNM
-- Lean 4 proof step from Mathlib.Data.Multiset.DershowitzManna (goal)
Goal:
α : Type u_1
inst : Preorder α
a_1 a : α
h : ∀ (y : α), y < a → Acc LT.lt y
ha : ∀ (y : α), y < a → ∀ {M : Multiset α}, Acc OneStep M → Acc OneStep (y ::ₘ M)
M_1 M : Multiset α
hM : ∀ (y : Multiset α), y.OneStep M → Acc OneStep y
ihM : ∀ (y : Multiset α), y.OneStep M → Acc OneStep (a ::ₘ y)
N : Multiset α
hNM : N.OneStep (a ::ₘ M)
intro : ∀ (N : Multiset α) (hNM' : N.OneStep M) (hNM : (a ::ₘ N).OneStep (a ::ₘ M)), Acc OneStep (a ::ₘ N)
⊢ Acc OneStep N
have intro₁ : ∀ (N : Multiset α) (hN : ∀ (x : α), x ∈ N → x < a) (hNM : (M + N).OneStep (a ::ₘ M)), Acc OneStep (M + N)
Tactic: obtain ⟨N, ⟨rfl, hNM'⟩ | ⟨rfl, hN⟩⟩ := isDershowitzMannaLT_singleton_insert hNM
Cleared hypotheses: N, hNM
-- Lean 4 proof step from Mathlib.Data.Multiset.DershowitzManna (goal)
Goal:
α : Type u_1
inst : Preorder α
a_1 a : α
h : ∀ (y : α), y < a → Acc LT.lt y
ha : ∀ (y : α), y < a → ∀ {M : Multiset α}, Acc OneStep M → Acc OneStep (y ::ₘ M)
M_1 M : Multiset α
hM : ∀ (y : Multiset α), y.OneStep M → Acc OneStep y
ihM : ∀ (y : Multiset α), y.OneStep M → Acc OneStep (a ::ₘ y)
b : α
N : Multiset α
ihN : ∀ (hN : ∀ (x : α), x ∈ N → x < a), Acc OneStep (M + N)
hN : ∀ (x : α), x ∈ b ::ₘ N → x < a
⊢ Acc OneStep (M + b ::ₘ N)
have intro : ∀ (hN : b < a ∧ ∀ (a_2 : α), a_2 ∈ N → a_2 < a), Acc OneStep (b ::ₘ (M + N))
Tactic: simp only [mem_cons, forall_eq_or_imp, add_cons] at hN ⊢
Cleared hypotheses: hN
-- Lean 4 proof step from Mathlib.Data.Multiset.DershowitzManna (hypothesis)
Goal:
α : Type u_1
inst : Preorder α
a_1 a : α
h : ∀ (y : α), y < a → Acc LT.lt y
ha : ∀ (y : α), y < a → ∀ {M : Multiset α}, Acc OneStep M → Acc OneStep (y ::ₘ M)
M_1 M : Multiset α
hM : ∀ (y : Multiset α), y.OneStep M → Acc OneStep y
ihM : ∀ (y : Multiset α), y.OneStep M → Acc OneStep (a ::ₘ y)
b : α
N : Multiset α
ihN : ∀ (hN : ∀ (x : α), x ∈ N → x < a), Acc OneStep (M + N)
hN : b < a ∧ ∀ (a_2 : α), a_2 ∈ N → a_2 < a
⊢ Acc OneStep (b ::ₘ (M + N))
have hba : b < a
Tactic: obtain ⟨hba, hN⟩ := hN
Cleared hypotheses: hN
-- Lean 4 proof step from Mathlib.Data.Multiset.DershowitzManna (hypothesis)
Goal:
α : Type u_1
inst : Preorder α
a_1 a : α
h : ∀ (y : α), y < a → Acc LT.lt y
ha : ∀ (y : α), y < a → ∀ {M : Multiset α}, Acc OneStep M → Acc OneStep (y ::ₘ M)
M_1 M : Multiset α
hM : ∀ (y : Multiset α), y.OneStep M → Acc OneStep y
ihM : ∀ (y : Multiset α), y.OneStep M → Acc OneStep (a ::ₘ y)
b : α
N : Multiset α
ihN : ∀ (hN : ∀ (x : α), x ∈ N → x < a), Acc OneStep (M + N)
hN : b < a ∧ ∀ (a_2 : α), a_2 ∈ N → a_2 < a
hba : b < a
⊢ Acc OneStep (b ::ₘ (M + N))
have hN₁ : ∀ (a_2 : α), a_2 ∈ N → a_2 < a
Tactic: obtain ⟨hba, hN⟩ := hN
Cleared hypotheses: hN
-- Lean 4 proof step from Mathlib.Data.Multiset.DershowitzManna (goal)
Goal:
α : Type u_1
inst : Preorder α
a_1 a : α
h : ∀ (y : α), y < a → Acc LT.lt y
ha : ∀ (y : α), y < a → ∀ {M : Multiset α}, Acc OneStep M → Acc OneStep (y ::ₘ M)
M_1 M : Multiset α
hM : ∀ (y : Multiset α), y.OneStep M → Acc OneStep y
ihM : ∀ (y : Multiset α), y.OneStep M → Acc OneStep (a ::ₘ y)
N : Multiset α
hN : ∀ (x : α), x ∈ N → x < a
⊢ Acc OneStep (M + N)
have intro : ∀ (hN : ∀ (x : α), Membership.mem (γ := Multiset α) 0 x → x < a), Acc OneStep (M + 0)
Tactic: induction N using Multiset.induction with
  | empty =>
    simpa using .intro _ hM
  | @cons b N ihN =>
    simp only [mem_cons, forall_eq_or_imp, add_cons] at hN ⊢
    obtain ⟨hba, hN⟩ := hN
    exact ha _ hba <| ihN hN
Cleared hypotheses: N, hN
-- Lean 4 proof step from Mathlib.Data.Multiset.DershowitzManna (goal)
Goal:
α : Type u_1
inst : Preorder α
a_1 a : α
h : ∀ (y : α), y < a → Acc LT.lt y
ha : ∀ (y : α), y < a → ∀ {M : Multiset α}, Acc OneStep M → Acc OneStep (y ::ₘ M)
M_1 M : Multiset α
hM : ∀ (y : Multiset α), y.OneStep M → Acc OneStep y
ihM : ∀ (y : Multiset α), y.OneStep M → Acc OneStep (a ::ₘ y)
N : Multiset α
hN : ∀ (x : α), x ∈ N → x < a
intro : ∀ (hN : ∀ (x : α), Membership.mem (γ := Multiset α) 0 x → x < a), Acc OneStep (M + 0)
⊢ Acc OneStep (M + N)
have intro₁ : ∀ (b : α) (N : Multiset α) (ihN : ∀ (hN : ∀ (x : α), x ∈ N → x < a), Acc OneStep (M + N))
  (hN : ∀ (x : α), x ∈ b ::ₘ N → x < a), Acc OneStep (M + b ::ₘ N)
Tactic: induction N using Multiset.induction with
  | empty =>
    simpa using .intro _ hM
  | @cons b N ihN =>
    simp only [mem_cons, forall_eq_or_imp, add_cons] at hN ⊢
    obtain ⟨hba, hN⟩ := hN
    exact ha _ hba <| ihN hN
Cleared hypotheses: N, hN
-- Lean 4 proof step from Mathlib.Data.Multiset.DershowitzManna (goal)
Goal:
α : Type u_1
inst : Preorder α
M : Multiset α
hM : ∀ (x : α), Membership.mem (γ := Multiset α) 0 x → Acc LT.lt x
⊢ Acc.{u_1 + 1} (α := Multiset α) OneStep 0
have empty : ∀ (y : Multiset α), y.OneStep 0 → Acc OneStep y
Tactic: constructor