awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Multiset.Defs
Goal:
α : Type u_1
r : α → α → Prop
hr : Symmetric r
l : List α
⊢ Pairwise r (↑l : Multiset α) ↔ List.Pairwise r l

Tactic:
Iff.intro (fun ⟨_l', Eq, h⟩ => ((Quotient.exact Eq).pairwise_iff @hr).2 h) fun h => ⟨l, rfl, h⟩

Premises used: Iff.mpr, List.Pairwise, List.Perm.pairwise_iff, _private.0.Multiset.pairwise_coe_iff_pairwise.match_1, And.intro, Iff.intro, Quotient.exact, Exists.intro, rfl
-- Module: Mathlib.Data.Multiset.Defs
Goal:
α : Type u_1
l : List α
⊢ (↑l : Multiset α).Nodup ↔ l.Nodup

Tactic:
Iff.rfl

Premises used: Multiset.Nodup, Iff.rfl
-- Module: Mathlib.Data.Multiset.Defs
Goal:
α : Type u_1
s t : Multiset α
⊢ s.Nodup → t.Nodup → (s = t ↔ ∀ (a : α), a ∈ s ↔ a ∈ t)

Tactic:
Quotient.inductionOn₂ s t fun _ _ d₁ d₂ => Quotient.eq.trans <| perm_ext_iff_of_nodup d₁ d₂

Premises used: Quotient.inductionOn₂
-- Module: Mathlib.Data.Multiset.Defs
Goal:
α : Type u_1
s t : Multiset α
⊢ s.Nodup → (s ≤ t ↔ s ⊆ t)

Tactic:
Quotient.inductionOn₂ s t fun _ _ d => ⟨subset_of_le, d.subperm⟩

Premises used: Quotient.inductionOn₂
-- Module: Mathlib.Data.Multiset.Defs
Goal:
α : Type u_1
s t : Multiset α
h : s ≤ t
⊢ t.Nodup → s.Nodup

Tactic:
Multiset.leInductionOn h fun {_ _} => Nodup.sublist

Premises used: Multiset.leInductionOn
-- Module: Mathlib.Data.Multiset.DershowitzManna
Goal:
α : Type u_1
inst : Preorder α
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
⊢ Z₁ + X₁ = Y₂ + X₂

Tactic:
rw [add_comm X₁, add_comm X₂] at hXZXY

Premises used: add_comm
-- Module: Mathlib.Data.Multiset.DershowitzManna
Goal:
α : Type u_1
inst : Preorder α
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
hXZXY₁ : Z₁ + X₁ = Y₂ + X₂
⊢ ∀ (y : α), y ∈ Y₂ → ∃ (z : α), z ∈ Z₂ ∧ y < z

Tactic:
rw [add_comm X₁, add_comm X₂] at hXZXY

Premises used: add_comm
-- Module: Mathlib.Data.Multiset.DershowitzManna
Goal:
α : Type u_1
inst : Preorder α
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₂)

Tactic:
⟨X₁ ∩ X₂, Y₁ + (Y₂ - Z₁), Z₂ + (Z₁ - Y₂), ?_, ?_, ?_, ?_⟩

Premises used: HSub.hSub, Inter.inter, HAdd.hAdd, Multiset.IsDershowitzMannaLT, And.intro, Exists.intro
-- Module: Mathlib.Data.Multiset.DershowitzManna
Goal:
α : Type u_1
inst : Preorder α
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
refine_1 : Z₂ + (Z₁ - Y₂) ≠ ∅
refine_2 : X₁ + Y₁ = X₁ ∩ X₂ + (Y₁ + (Y₂ - Z₁))
refine_3 : X₂ + Z₂ = X₁ ∩ X₂ + (Z₂ + (Z₁ - Y₂))
refine_4 : ∀ (y : α), y ∈ Y₁ + (Y₂ - Z₁) → ∃ (z : α), z ∈ Z₂ + (Z₁ - Y₂) ∧ y < z
⊢ (X₁ + Y₁).IsDershowitzMannaLT (X₂ + Z₂)

Tactic:
refine ⟨X₁ ∩ X₂, Y₁ + (Y₂ - Z₁), Z₂ + (Z₁ - Y₂), ?_, ?_, ?_, ?_⟩
-- Module: Mathlib.Data.Multiset.DershowitzManna
Goal:
α : Type u_1
inst : Preorder α
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₂) ≠ ∅

Tactic:
simpa [-not_and, not_and_or] using .inl hZ₂

Premises used: not_and_or, not_and
-- Module: Mathlib.Data.Multiset.DershowitzManna
Goal:
α : Type u_1
inst : Preorder α
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
refine_2 : X₁ + Y₁ = X₁ ∩ X₂ + Y₁ + (Y₂ - Z₁)
refine_2₁ : X₁ + Y₁ = X₁ ∩ X₂ + (Y₂ - Z₁) + Y₁
refine_2₂ : X₁ + Y₁ = X₁ + Y₁
refine_2₃ : Z₁ + X₁ = Y₂ + X₂
refine_2₄ : X₁ + Y₁ = X₁ + Y₁
refine_2₅ refine_2₆ refine_2₇ : Z₁ + X₁ = Y₂ + X₂
⊢ X₁ + Y₁ = X₁ ∩ X₂ + (Y₁ + (Y₂ - Z₁))

Tactic:
rwa [← add_assoc, add_right_comm, inter_add_sub_of_add_eq_add]

Premises used: Multiset.inter_add_sub_of_add_eq_add, add_assoc, add_right_comm
-- Module: Mathlib.Data.Multiset.DershowitzManna
Goal:
α : Type u_1
inst : Preorder α
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
refine_3 : Y₂ + X₂ = Z₁ + X₁
⊢ X₂ + Z₂ = X₁ ∩ X₂ + (Z₂ + (Z₁ - Y₂))

Tactic:
rw [← add_assoc, add_right_comm, add_left_inj, inter_comm, inter_add_sub_of_add_eq_add]

Premises used: Multiset.inter_add_sub_of_add_eq_add, add_assoc, add_right_comm, add_left_inj, Multiset.inter_comm
-- Module: Mathlib.Data.Multiset.DershowitzManna
Goal:
α : Type u_1
inst : Preorder α
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
refine_3 refine_3₁ refine_3₂ refine_3₃ : Z₁ + X₁ = Y₂ + X₂
⊢ Y₂ + X₂ = Z₁ + X₁

Tactic:
rwa [eq_comm]

Premises used: eq_comm
-- Module: Mathlib.Data.Multiset.DershowitzManna
Goal:
α : Type u_1
inst : Preorder α
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
refine_4 :
  (∀ (x : α), x ∈ Y₁ → ∃ (z : α), (z ∈ Z₂ ∨ z ∈ Z₁ - Y₂) ∧ x < z) ∧
    ∀ (x : α), x ∈ Y₂ - Z₁ → ∃ (z : α), (z ∈ Z₂ ∨ z ∈ Z₁ - Y₂) ∧ x < z
⊢ ∀ (y : α), y ∈ Y₁ + (Y₂ - Z₁) → ∃ (z : α), z ∈ Z₂ + (Z₁ - Y₂) ∧ y < z

Tactic:
simp only [mem_add, or_imp, forall_and]

Premises used: or_imp, Multiset.mem_add, forall_and
-- Module: Mathlib.Data.Multiset.DershowitzManna
Goal:
α : Type u_1
inst : Preorder α
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 : α), x ∈ Y₁ → ∃ (z : α), (z ∈ Z₂ ∨ z ∈ Z₁ - Y₂) ∧ x < z) ∧
    ∀ (x : α), x ∈ Y₂ - Z₁ → ∃ (z : α), (z ∈ Z₂ ∨ z ∈ Z₁ - Y₂) ∧ x < z

Tactic:
⟨fun y hy ↦ ?_, fun y hy ↦ ?_⟩

Premises used: And.intro
-- Module: Mathlib.Data.Multiset.DershowitzManna
Goal:
α : Type u_1
inst : Preorder α
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
refine_4 : ∀ (y : α) (hy : y ∈ Y₁), ∃ (z : α), (z ∈ Z₂ ∨ z ∈ Z₁ - Y₂) ∧ y < z
refine_4₁ : ∀ (y : α) (hy : y ∈ Y₂ - Z₁), ∃ (z : α), (z ∈ Z₂ ∨ z ∈ Z₁ - Y₂) ∧ y < z
⊢ (∀ (x : α), x ∈ Y₁ → ∃ (z : α), (z ∈ Z₂ ∨ z ∈ Z₁ - Y₂) ∧ x < z) ∧
    ∀ (x : α), x ∈ Y₂ - Z₁ → ∃ (z : α), (z ∈ Z₂ ∨ z ∈ Z₁ - Y₂) ∧ x < z

Tactic:
refine ⟨fun y hy ↦ ?_, fun y hy ↦ ?_⟩
-- Module: Mathlib.Data.Multiset.DershowitzManna
Goal:
α : Type u_1
inst : Preorder α
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 : α
hy : y ∈ Y₁
refine_4 : ∀ (z : α) (hz : z ∈ Z₁) (hyz : y < z), ∃ (z : α), (z ∈ Z₂ ∨ z ∈ Z₁ - Y₂) ∧ y < z
⊢ ∃ (z : α), (z ∈ Z₂ ∨ z ∈ Z₁ - Y₂) ∧ y < z

Tactic:
obtain ⟨z, hz, hyz⟩ := hYZ₁ y hy
-- Module: Mathlib.Data.Multiset.DershowitzManna
Goal:
α : Type u_1
inst : Preorder α
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 : α
hy : y ∈ Y₁
z : α
hz : z ∈ Z₁
hyz : y < z
pos : ∀ (z_in : z ∈ Y₂), ∃ (z : α), (z ∈ Z₂ ∨ z ∈ Z₁ - Y₂) ∧ y < z
neg : ∀ (z_in : ¬z ∈ Y₂), ∃ (z : α), (z ∈ Z₂ ∨ z ∈ Z₁ - Y₂) ∧ y < z
⊢ ∃ (z : α), (z ∈ Z₂ ∨ z ∈ Z₁ - Y₂) ∧ y < z

Tactic:
by_cases z_in : z ∈ Y₂
-- Module: Mathlib.Data.Multiset.DershowitzManna
Goal:
α : Type u_1
inst : Preorder α
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 : α
hy : y ∈ Y₁
z : α
hz : z ∈ Z₁
hyz : y < z
z_in : z ∈ Y₂
pos : ∀ (w : α) (hw : w ∈ Z₂) (hzw : z < w), ∃ (z : α), (z ∈ Z₂ ∨ z ∈ Z₁ - Y₂) ∧ y < z
⊢ ∃ (z : α), (z ∈ Z₂ ∨ z ∈ Z₁ - Y₂) ∧ y < z

Tactic:
obtain ⟨w, hw, hzw⟩ := hYZ₂ z z_in
-- Module: Mathlib.Data.Multiset.DershowitzManna
Goal:
α : Type u_1
inst : Preorder α
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 : α
hy : y ∈ Y₁
z : α
hz : z ∈ Z₁
hyz : y < z
z_in : z ∈ Y₂
w : α
hw : w ∈ Z₂
hzw : z < w
⊢ ∃ (z : α), (z ∈ Z₂ ∨ z ∈ Z₁ - Y₂) ∧ y < z

Tactic:
⟨w, .inl hw, hyz.trans hzw⟩

Premises used: And.intro, Exists.intro, LT.lt.trans, Or.inl
-- Module: Mathlib.Data.Multiset.DershowitzManna
Goal:
α : Type u_1
inst : Preorder α
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 : α
hy : y ∈ Y₁
z : α
hz : z ∈ Z₁
hyz : y < z
z_in : z ∈ Y₂
w : α
hw : w ∈ Z₂
hzw : z < w
⊢ ∃ (z : α), (z ∈ Z₂ ∨ z ∈ Z₁ - Y₂) ∧ y < z

Tactic:
exact ⟨w, .inl hw, hyz.trans hzw⟩
-- Module: Mathlib.Data.Multiset.DershowitzManna
Goal:
α : Type u_1
inst : Preorder α
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 : α
hy : y ∈ Y₁
z : α
hz : z ∈ Z₁
hyz : y < z
z_in : ¬z ∈ Y₂
rwa : count z Y₂ < count z Z₁
rwa₁ : 0 < count z Z₁
rwa₂ rwa₃ rwa₄ rwa₅ : z ∈ Z₁
⊢ z ∈ Z₁ - Y₂

Tactic:
rwa [mem_sub, count_eq_zero_of_notMem z_in, count_pos]

Premises used: Multiset.count_pos, Multiset.count_eq_zero_of_notMem, Multiset.mem_sub
-- Module: Mathlib.Data.Multiset.DershowitzManna
Goal:
α : Type u_1
inst : Preorder α
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 : α
hy : y ∈ Y₁
z : α
hz : z ∈ Z₁
hyz : y < z
z_in : ¬z ∈ Y₂
⊢ ∃ (z : α), (z ∈ Z₂ ∨ z ∈ Z₁ - Y₂) ∧ y < z

Tactic:
exact ⟨z, .inr <| by rwa [mem_sub, count_eq_zero_of_notMem z_in, count_pos], hyz⟩
-- Module: Mathlib.Data.Multiset.DershowitzManna
Goal:
α : Type u_1
inst : Preorder α
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 : α
hy : y ∈ Y₂ - Z₁
refine_4 : ∀ (z : α) (hz : z ∈ Z₂) (hyz : y < z), ∃ (z : α), (z ∈ Z₂ ∨ z ∈ Z₁ - Y₂) ∧ y < z
⊢ ∃ (z : α), (z ∈ Z₂ ∨ z ∈ Z₁ - Y₂) ∧ y < z

Tactic:
obtain ⟨z, hz, hyz⟩ := hYZ₂ y <| mem_of_le (Multiset.sub_le_self ..) hy

Premises used: Multiset.sub_le_self, Multiset.mem_of_le
-- Module: Mathlib.Data.Multiset.DershowitzManna
Goal:
α : Type u_1
inst : Preorder α
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 : α
hy : y ∈ Y₂ - Z₁
z : α
hz : z ∈ Z₂
hyz : y < z
⊢ ∃ (z : α), (z ∈ Z₂ ∨ z ∈ Z₁ - Y₂) ∧ y < z

Tactic:
⟨z, .inl hz, hyz⟩

Premises used: And.intro, Exists.intro, Or.inl
-- Module: Mathlib.Data.Multiset.DershowitzManna
Goal:
α : Type u_1
inst : Preorder α
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 : α
hy : y ∈ Y₂ - Z₁
z : α
hz : z ∈ Z₂
hyz : y < z
⊢ ∃ (z : α), (z ∈ Z₂ ∨ z ∈ Z₁ - Y₂) ∧ y < z

Tactic:
exact ⟨z, .inl hz, hyz⟩
-- Module: Mathlib.Data.Multiset.DershowitzManna
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
⊢ Ne (α := Multiset α) {a} ∅

Tactic:
simp
-- Module: Mathlib.Data.Multiset.DershowitzManna
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
right : ∀ (y : α), y ∈ Y → ∃ (z : α), Membership.mem (γ := Multiset α) {a} z ∧ y < z
⊢ M.IsDershowitzMannaLT N

Tactic:
use X, Y, {a}, by simp, M_def, N_def
-- Module: Mathlib.Data.Multiset.DershowitzManna
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
⊢ ∀ (y : α), y ∈ Y → ∃ (z : α), Membership.mem (γ := Multiset α) {a} z ∧ y < z

Tactic:
simpa
-- Module: Mathlib.Data.Multiset.DershowitzManna
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

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

Premises used: rfl
-- Module: Mathlib.Data.Multiset.DershowitzManna
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
inr : ∀ (hab : a ≠ b), ∃ (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

Tactic:
obtain rfl | hab := eq_or_ne a b

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Data.Multiset.DershowitzManna
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

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

Premises used: And.intro, Exists.intro, Or.inr
-- Module: Mathlib.Data.Multiset.DershowitzManna
Goal:
α : Type u_1
inst : Preorder α
M : Multiset α
a : α
X Y : Multiset α
h0 : a ::ₘ M = X + {a}
h2 : ∀ (y : α), y ∈ Y → y < a
inl : X + Y = M + Y
⊢ ∃ (M' : Multiset α), X + Y = a ::ₘ M' ∧ M'.OneStep M ∨ X + Y = M + M' ∧ ∀ (x : α), x ∈ M' → x < a

Tactic:
refine ⟨Y, .inr ⟨?_, h2⟩⟩
-- Module: Mathlib.Data.Multiset.DershowitzManna
Goal:
α : Type u_1
inst : Preorder α
M : Multiset α
a : α
X Y : Multiset α
h0 : a ::ₘ M = X + {a}
h2 : ∀ (y : α), y ∈ Y → y < a
⊢ X + Y = M + Y

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

Premises used: Multiset.singleton_add, eq_comm, add_comm
-- Module: Mathlib.Data.Multiset.DershowitzManna
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

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

Premises used: HSub.hSub, HAdd.hAdd, And.intro, Exists.intro, Or.inl
-- Module: Mathlib.Data.Multiset.DershowitzManna
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}))
inr₁ : M = M - {b} + {b}
⊢ ∃ (M' : Multiset α), X + Y = a ::ₘ M' ∧ M'.OneStep M ∨ X + Y = M + M' ∧ ∀ (x : α), x ∈ M' → x < a

Tactic:
refine ⟨Y + (M - {b}), .inl ⟨?_, M - {b}, Y, b, add_comm .., ?_, h2⟩⟩
-- Module: Mathlib.Data.Multiset.DershowitzManna
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 + {a} = X + {b}

Tactic:
rw [← singleton_add, add_comm] at h0

Premises used: Multiset.singleton_add, add_comm
-- Module: Mathlib.Data.Multiset.DershowitzManna
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
h0₁ : M + {a} = X + {b}
⊢ ∀ (y : α), y ∈ Y → y < b

Tactic:
rw [← singleton_add, add_comm] at h0

Premises used: Multiset.singleton_add, add_comm
-- Module: Mathlib.Data.Multiset.DershowitzManna
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
h0₁ : M + {a} = X + {b}
h2₁ : ∀ (y : α), y ∈ Y → y < b
⊢ a ≠ b

Tactic:
rw [← singleton_add, add_comm] at h0

Premises used: Multiset.singleton_add, add_comm
-- Module: Mathlib.Data.Multiset.DershowitzManna
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
inr : {a} ≤ X
⊢ 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]

Premises used: Multiset.singleton_add, add_assoc, tsub_eq_tsub_of_add_eq_add, add_comm, add_tsub_cancel_of_le
-- Module: Mathlib.Data.Multiset.DershowitzManna
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 + {b}

Tactic:
simp [← h0]
-- Module: Mathlib.Data.Multiset.DershowitzManna
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 + {b}

Tactic:
have : a ∈ X + {b} := by simp [← h0]
-- Module: Mathlib.Data.Multiset.DershowitzManna
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
this : a ∈ X + {b}
⊢ {a} ≤ X

Tactic:
simpa [hab] using this
-- Module: Mathlib.Data.Multiset.DershowitzManna
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 : {b} ≤ M
⊢ M = M - {b} + {b}

Tactic:
rw [tsub_add_cancel_of_le]

Premises used: tsub_add_cancel_of_le
-- Module: Mathlib.Data.Multiset.DershowitzManna
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 ∈ a ::ₘ M

Tactic:
simp [h0]
-- Module: Mathlib.Data.Multiset.DershowitzManna
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 ∈ a ::ₘ M

Tactic:
have : b ∈ a ::ₘ M := by simp [h0]
-- Module: Mathlib.Data.Multiset.DershowitzManna
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
this : b ∈ a ::ₘ M
⊢ {b} ≤ M

Tactic:
simpa [hab.symm] using this

Premises used: Ne.symm
-- Module: Mathlib.Data.Multiset.DershowitzManna
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}))
inr₃ inr₄ :
  ∀ (X Y : Multiset α) (b : α) (h0 : a ::ₘ M = X + {b}) (h2 : ∀ (y : α), y ∈ Y → y < b) (hab : a ≠ b), M = M - {b} + {b}
⊢ ∃ (M' : Multiset α), N = a ::ₘ M' ∧ M'.OneStep M ∨ N = 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

Premises used: Multiset.singleton_add, add_assoc, tsub_add_cancel_of_le, eq_comm, add_comm, add_tsub_cancel_of_le, rfl
-- Module: Mathlib.Data.Multiset.DershowitzManna
Goal:
α : Type u_1
inst : Preorder α
a : α
ha : Acc LT.lt a
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)
⊢ ∀ {M : Multiset α}, Acc OneStep M → Acc OneStep (a ::ₘ M)

Tactic:
induction ha with | _ a _ ha
-- Module: Mathlib.Data.Multiset.DershowitzManna
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
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)
⊢ Acc OneStep (a ::ₘ M)

Tactic:
induction hM with | _ M hM ihM
-- Module: Mathlib.Data.Multiset.DershowitzManna
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)

Tactic:
.intro _ fun N hNM ↦ ?_

Premises used: Acc.intro
-- Module: Mathlib.Data.Multiset.DershowitzManna
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)
intro : ∀ (N : Multiset α) (hNM : N.OneStep (a ::ₘ M)), Acc OneStep N
⊢ Acc OneStep (a ::ₘ M)

Tactic:
refine .intro _ fun N hNM ↦ ?_
-- Module: Mathlib.Data.Multiset.DershowitzManna
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)
intro₁ : ∀ (N : Multiset α) (hN : ∀ (x : α), x ∈ N → x < a) (hNM : (M + N).OneStep (a ::ₘ M)), Acc OneStep (M + N)
⊢ Acc OneStep N

Tactic:
obtain ⟨N, ⟨rfl, hNM'⟩ | ⟨rfl, hN⟩⟩ := isDershowitzMannaLT_singleton_insert hNM

Premises used: _private.0.Multiset.isDershowitzMannaLT_singleton_insert, rfl
-- Module: Mathlib.Data.Multiset.DershowitzManna
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 M
hNM : (a ::ₘ N).OneStep (a ::ₘ M)
⊢ Acc OneStep (a ::ₘ N)

Tactic:
ihM _ hNM'
-- Module: Mathlib.Data.Multiset.DershowitzManna
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 M
hNM : (a ::ₘ N).OneStep (a ::ₘ M)
⊢ Acc OneStep (a ::ₘ N)

Tactic:
exact ihM _ hNM'