awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
hN : ∀ (x : α), Membership.mem (γ := Multiset α) 0 x → x < a
⊢ Acc OneStep (M + 0)

Tactic:
simpa using .intro _ hM
-- 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)
b : α
N : Multiset α
ihN : ∀ (hN : ∀ (x : α), x ∈ N → x < a), Acc OneStep (M + N)
hN : ∀ (x : α), x ∈ b ::ₘ N → x < a
intro : ∀ (hN : b < a ∧ ∀ (a_2 : α), a_2 ∈ N → a_2 < a), Acc OneStep (b ::ₘ (M + N))
⊢ Acc OneStep (M + b ::ₘ N)

Tactic:
simp only [mem_cons, forall_eq_or_imp, add_cons] at hN ⊢

Premises used: Multiset.add_cons, forall_eq_or_imp, Multiset.mem_cons
-- 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)
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
⊢ b < a

Tactic:
obtain ⟨hba, hN⟩ := hN
-- 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)
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
⊢ ∀ (a_2 : α), a_2 ∈ N → a_2 < a

Tactic:
obtain ⟨hba, hN⟩ := hN
-- 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)
b : α
N : Multiset α
ihN : ∀ (hN : ∀ (x : α), x ∈ N → x < a), Acc OneStep (M + N)
hba : b < a
hN : ∀ (a_2 : α), a_2 ∈ N → a_2 < a
⊢ Acc OneStep (b ::ₘ (M + N))

Tactic:
ha _ hba <| ihN hN
-- 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)
b : α
N : Multiset α
ihN : ∀ (hN : ∀ (x : α), x ∈ N → x < a), Acc OneStep (M + N)
hba : b < a
hN : ∀ (a_2 : α), a_2 ∈ N → a_2 < a
⊢ Acc OneStep (b ::ₘ (M + N))

Tactic:
exact ha _ hba <| ihN hN
-- 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 α
hN : ∀ (x : α), x ∈ N → x < a
intro : ∀ (hN : ∀ (x : α), Membership.mem (γ := Multiset α) 0 x → x < a), Acc OneStep (M + 0)
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)
⊢ Acc OneStep (M + 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

Premises used: Multiset.cons, Multiset.add_cons, forall_eq_or_imp, Multiset.mem_cons
-- Module: Mathlib.Data.Multiset.DershowitzManna
Goal:
α : Type u_1
inst : Preorder α
M : Multiset α
hM : ∀ (x : α), Membership.mem (γ := Multiset α) 0 x → Acc LT.lt x
empty : ∀ (y : Multiset α), y.OneStep 0 → Acc OneStep y
⊢ Acc.{u_1 + 1} (α := Multiset α) OneStep 0

Tactic:
constructor
-- Module: Mathlib.Data.Multiset.DershowitzManna
Goal:
α : Type u_1
inst : Preorder α
M : Multiset α
hM : ∀ (x : α), Membership.mem (γ := Multiset α) 0 x → Acc LT.lt x
⊢ ∀ (y : Multiset α), y.OneStep 0 → Acc OneStep y

Tactic:
simp [OneStep, eq_comm (b := _ + _)]

Premises used: eq_comm, _private.0.Multiset.OneStep
-- Module: Mathlib.Data.Multiset.DershowitzManna
Goal:
α : Type u_1
inst : Preorder α
M_1 : Multiset α
a : α
M : Multiset α
ih : ∀ (hM : ∀ (x : α), x ∈ M → Acc LT.lt x), Acc OneStep M
hM : ∀ (x : α), x ∈ a ::ₘ M → Acc LT.lt x
⊢ Acc OneStep (a ::ₘ M)

Tactic:
acc_oneStep_cons_of_acc_lt (hM _ <| mem_cons_self ..) <| ih fun x hx ↦
      hM _ <| mem_cons_of_mem hx

Premises used: _private.0.Multiset.acc_oneStep_cons_of_acc_lt, Multiset.mem_cons_of_mem, Multiset.mem_cons_self
-- Module: Mathlib.Data.Multiset.DershowitzManna
Goal:
α : Type u_1
inst : Preorder α
M_1 : Multiset α
a : α
M : Multiset α
ih : ∀ (hM : ∀ (x : α), x ∈ M → Acc LT.lt x), Acc OneStep M
hM : ∀ (x : α), x ∈ a ::ₘ M → Acc LT.lt x
⊢ Acc OneStep (a ::ₘ M)

Tactic:
exact acc_oneStep_cons_of_acc_lt (hM _ <| mem_cons_self ..) <| ih fun x hx ↦
      hM _ <| mem_cons_of_mem hx

Premises used: _private.0.Multiset.acc_oneStep_cons_of_acc_lt, Multiset.mem_cons_of_mem, Multiset.mem_cons_self
-- Module: Mathlib.Data.Multiset.DershowitzManna
Goal:
α : Type u_1
inst : Preorder α
M : Multiset α
hM : ∀ (x : α), x ∈ M → Acc LT.lt x
empty :
  ∀ (hM : ∀ (x : α), Membership.mem (γ := Multiset α) 0 x → Acc LT.lt x), Acc.{u_1 + 1} (α := Multiset α) OneStep 0
cons :
  ∀ (a : α) (M : Multiset α) (ih : ∀ (hM : ∀ (x : α), x ∈ M → Acc LT.lt x), Acc OneStep M)
    (hM : ∀ (x : α), x ∈ a ::ₘ M → Acc LT.lt x), Acc OneStep (a ::ₘ M)
⊢ Acc OneStep M

Tactic:
induction M using Multiset.induction_on with
  | empty =>
    constructor
    simp [OneStep, eq_comm (b := _ + _)]
  | cons a M ih =>
    exact acc_oneStep_cons_of_acc_lt (hM _ <| mem_cons_self ..) <| ih fun x hx ↦
      hM _ <| mem_cons_of_mem hx

Premises used: _private.0.Multiset.acc_oneStep_cons_of_acc_lt, Multiset.cons, eq_comm, _private.0.Multiset.OneStep
-- Module: Mathlib.Data.Multiset.DershowitzManna
Goal:
α : Type u_1
inst : Preorder α
inst_1 : WellFoundedLT α
⊢ WellFounded.{u_1 + 1} (α := Multiset α) OneStep

Tactic:
⟨fun _M ↦ acc_oneStep_of_acc_lt fun a _ ↦ WellFoundedLT.apply a⟩

Premises used: _private.0.Multiset.acc_oneStep_of_acc_lt, WellFounded.intro, WellFoundedLT.apply
-- Module: Mathlib.Data.Multiset.DershowitzManna
Goal:
α : Type u_1
inst : Preorder α
M N X Y : Multiset α
hZ : Ne.{u_1 + 1} (α := Multiset α) 0 ∅
hM : M = X + Y
hN : N = X + 0
hYZ : ∀ (y : α), y ∈ Y → ∃ (z : α), Membership.mem (γ := Multiset α) 0 z ∧ y < z
⊢ TransGen OneStep M N

Tactic:
simp at hZ
-- Module: Mathlib.Data.Multiset.DershowitzManna
Goal:
α : Type u_1
inst : Preorder α
z : α
Z : Multiset α
ih :
  ∀ {M N : Multiset α} (X Y : Multiset α) (hZ : Z ≠ ∅) (hM : M = X + Y) (hN : N = X + Z)
    (hYZ : ∀ (y : α), y ∈ Y → ∃ (z : α), z ∈ Z ∧ y < z), TransGen OneStep M N
M N X Y : Multiset α
hZ : z ::ₘ Z ≠ ∅
hM : M = X + Y
hN : N = X + z ::ₘ Z
hYZ : ∀ (y : α), y ∈ Y → ∃ (z_1 : α), z_1 ∈ z ::ₘ Z ∧ y < z_1
⊢ TransGen OneStep M N

Tactic:
?_
-- Module: Mathlib.Data.Multiset.DershowitzManna
Goal:
α : Type u_1
inst : Preorder α
M N X Y Z : Multiset α
hZ : Z ≠ ∅
hM : M = X + Y
hN : N = X + Z
hYZ : ∀ (y : α), y ∈ Y → ∃ (z : α), z ∈ Z ∧ y < z
cons :
  ∀ (z : α) (Z : Multiset α)
    (ih :
      ∀ {M N : Multiset α} (X Y : Multiset α) (hZ : Z ≠ ∅) (hM : M = X + Y) (hN : N = X + Z)
        (hYZ : ∀ (y : α), y ∈ Y → ∃ (z : α), z ∈ Z ∧ y < z), TransGen OneStep M N)
    {M N : Multiset α} (X Y : Multiset α) (hZ : z ::ₘ Z ≠ ∅) (hM : M = X + Y) (hN : N = X + z ::ₘ Z)
    (hYZ : ∀ (y : α), y ∈ Y → ∃ (z_1 : α), z_1 ∈ z ::ₘ Z ∧ y < z_1), TransGen OneStep M N
⊢ TransGen OneStep M N

Tactic:
induction Z using Multiset.induction_on generalizing X Y M N with
  | empty => simp at hZ
  | cons z Z ih => ?_

Premises used: Multiset.cons
-- Module: Mathlib.Data.Multiset.DershowitzManna
Goal:
α : Type u_1
inst : Preorder α
z : α
Z : Multiset α
ih :
  ∀ {M N : Multiset α} (X Y : Multiset α) (hZ : Z ≠ ∅) (hM : M = X + Y) (hN : N = X + Z)
    (hYZ : ∀ (y : α), y ∈ Y → ∃ (z : α), z ∈ Z ∧ y < z), TransGen OneStep M N
M N X Y : Multiset α
hZ : z ::ₘ Z ≠ ∅
hM : M = X + Y
hN : N = X + z ::ₘ Z
hYZ : ∀ (y : α), y ∈ Y → ∃ (z_1 : α), z_1 ∈ z ::ₘ Z ∧ y < z_1
cons :
  ∀
    (ih :
      ∀ {M N : Multiset α} (X Y : Multiset α) (hZ : Ne.{u_1 + 1} (α := Multiset α) 0 ∅) (hM : M = X + Y)
        (hN : N = X + 0) (hYZ : ∀ (y : α), y ∈ Y → ∃ (z : α), Membership.mem (γ := Multiset α) 0 z ∧ y < z),
        TransGen OneStep M N)
    (hZ : z ::ₘ 0 ≠ ∅) (hN : N = X + z ::ₘ 0) (hYZ : ∀ (y : α), y ∈ Y → ∃ (z_1 : α), z_1 ∈ z ::ₘ 0 ∧ y < z_1),
    TransGen OneStep M N
cons₁ : ∀ (hZ : Z ≠ 0), TransGen OneStep M N
⊢ TransGen OneStep M N

Tactic:
obtain rfl | hZ := eq_or_ne Z 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Data.Multiset.DershowitzManna
Goal:
α : Type u_1
inst : Preorder α
z : α
M N X Y : Multiset α
hM : M = X + Y
ih :
  ∀ {M N : Multiset α} (X Y : Multiset α) (hZ : Ne.{u_1 + 1} (α := Multiset α) 0 ∅) (hM : M = X + Y) (hN : N = X + 0)
    (hYZ : ∀ (y : α), y ∈ Y → ∃ (z : α), Membership.mem (γ := Multiset α) 0 z ∧ y < z), TransGen OneStep M N
hZ : z ::ₘ 0 ≠ ∅
hN : N = X + z ::ₘ 0
hYZ : ∀ (y : α), y ∈ Y → ∃ (z_1 : α), z_1 ∈ z ::ₘ 0 ∧ y < z_1
⊢ ∀ (y : α), y ∈ Y → y < z

Tactic:
simpa using hYZ
-- Module: Mathlib.Data.Multiset.DershowitzManna
Goal:
α : Type u_1
inst : Preorder α
z : α
M N X Y : Multiset α
hM : M = X + Y
ih :
  ∀ {M N : Multiset α} (X Y : Multiset α) (hZ : Ne.{u_1 + 1} (α := Multiset α) 0 ∅) (hM : M = X + Y) (hN : N = X + 0)
    (hYZ : ∀ (y : α), y ∈ Y → ∃ (z : α), Membership.mem (γ := Multiset α) 0 z ∧ y < z), TransGen OneStep M N
hZ : z ::ₘ 0 ≠ ∅
hN : N = X + z ::ₘ 0
hYZ : ∀ (y : α), y ∈ Y → ∃ (z_1 : α), z_1 ∈ z ::ₘ 0 ∧ y < z_1
⊢ TransGen OneStep M N

Tactic:
exact .single ⟨X, Y, z, hM, hN, by simpa using hYZ⟩
-- Module: Mathlib.Data.Multiset.DershowitzManna
Goal:
α : Type u_1
inst : Preorder α
z : α
Z : Multiset α
ih :
  ∀ {M N : Multiset α} (X Y : Multiset α) (hZ : Z ≠ ∅) (hM : M = X + Y) (hN : N = X + Z)
    (hYZ : ∀ (y : α), y ∈ Y → ∃ (z : α), z ∈ Z ∧ y < z), TransGen OneStep M N
M N X Y : Multiset α
hZ_1 : z ::ₘ Z ≠ ∅
hM : M = X + Y
hN : N = X + z ::ₘ Z
hYZ : ∀ (y : α), y ∈ Y → ∃ (z_1 : α), z_1 ∈ z ::ₘ Z ∧ y < z_1
hZ : Z ≠ 0
Y' : Multiset α := filter (fun (x : α) ↦ x < z) Y
⊢ N = X + Z + {z}

Tactic:
simp [hN, add_comm (_ + _)]

Premises used: add_comm, HAdd.hAdd
-- Module: Mathlib.Data.Multiset.DershowitzManna
Goal:
α : Type u_1
inst : Preorder α
z : α
Z : Multiset α
ih :
  ∀ {M N : Multiset α} (X Y : Multiset α) (hZ : Z ≠ ∅) (hM : M = X + Y) (hN : N = X + Z)
    (hYZ : ∀ (y : α), y ∈ Y → ∃ (z : α), z ∈ Z ∧ y < z), TransGen OneStep M N
M N X Y : Multiset α
hZ_1 : z ::ₘ Z ≠ ∅
hM : M = X + Y
hN : N = X + z ::ₘ Z
hYZ : ∀ (y : α), y ∈ Y → ∃ (z_1 : α), z_1 ∈ z ::ₘ Z ∧ y < z_1
hZ : Z ≠ 0
Y' : Multiset α := filter (fun (x : α) ↦ x < z) Y
⊢ ∀ (y : α), y ∈ Y' → y < z

Tactic:
simp [Y']
-- Module: Mathlib.Data.Multiset.DershowitzManna
Goal:
α : Type u_1
inst : Preorder α
z : α
Z : Multiset α
ih :
  ∀ {M N : Multiset α} (X Y : Multiset α) (hZ : Z ≠ ∅) (hM : M = X + Y) (hN : N = X + Z)
    (hYZ : ∀ (y : α), y ∈ Y → ∃ (z : α), z ∈ Z ∧ y < z), TransGen OneStep M N
M N X Y : Multiset α
hZ_1 : z ::ₘ Z ≠ ∅
hM : M = X + Y
hN : N = X + z ::ₘ Z
hYZ : ∀ (y : α), y ∈ Y → ∃ (z_1 : α), z_1 ∈ z ::ₘ Z ∧ y < z_1
hZ : Z ≠ 0
Y' : Multiset α := filter (fun (x : α) ↦ x < z) Y
cons : M = X + Y' + (Y - Y')
cons₁ : ∀ (y : α) (hy : y ∈ Y - Y'), ∃ (z : α), z ∈ Z ∧ y < z
⊢ TransGen OneStep M N

Tactic:
refine .tail (b := X + Y' + Z) (ih (X + Y') (Y - Y') hZ ?_ rfl fun y hy ↦ ?_) <|
    ⟨X + Z, Y', z, add_right_comm .., by simp [hN, add_comm (_ + _)], by simp [Y']⟩
-- Module: Mathlib.Data.Multiset.DershowitzManna
Goal:
α : Type u_1
inst : Preorder α
z : α
Z : Multiset α
ih :
  ∀ {M N : Multiset α} (X Y : Multiset α) (hZ : Z ≠ ∅) (hM : M = X + Y) (hN : N = X + Z)
    (hYZ : ∀ (y : α), y ∈ Y → ∃ (z : α), z ∈ Z ∧ y < z), TransGen OneStep M N
M N X Y : Multiset α
hZ_1 : z ::ₘ Z ≠ ∅
hM : M = X + Y
hN : N = X + z ::ₘ Z
hYZ : ∀ (y : α), y ∈ Y → ∃ (z_1 : α), z_1 ∈ z ::ₘ Z ∧ y < z_1
hZ : Z ≠ 0
Y' : Multiset α := filter (fun (x : α) ↦ x < z) Y
cons : M = X + Y
cons₁ cons₂ : X + Y = X + Y
⊢ M = X + Y' + (Y - Y')

Tactic:
rw [add_add_tsub_cancel (filter_le ..), hM]

Premises used: add_add_tsub_cancel, Multiset.filter_le
-- Module: Mathlib.Data.Multiset.DershowitzManna
Goal:
α : Type u_1
inst : Preorder α
z : α
Z : Multiset α
ih :
  ∀ {M N : Multiset α} (X Y : Multiset α) (hZ : Z ≠ ∅) (hM : M = X + Y) (hN : N = X + Z)
    (hYZ : ∀ (y : α), y ∈ Y → ∃ (z : α), z ∈ Z ∧ y < z), TransGen OneStep M N
M N X Y : Multiset α
hZ_1 : z ::ₘ Z ≠ ∅
hM : M = X + Y
hN : N = X + z ::ₘ Z
hYZ : ∀ (y : α), y ∈ Y → ∃ (z_1 : α), z_1 ∈ z ::ₘ Z ∧ y < z_1
hZ : Z ≠ 0
Y' : Multiset α := filter (fun (x : α) ↦ x < z) Y
y : α
hy : y ∈ Y - Y'
⊢ y ∈ Y ∧ ¬y < z

Tactic:
simp only [sub_filter_eq_filter_not, mem_filter, Y'] at hy

Premises used: Multiset.mem_filter, Multiset.sub_filter_eq_filter_not
-- Module: Mathlib.Data.Multiset.DershowitzManna
Goal:
α : Type u_1
inst : Preorder α
z : α
Z : Multiset α
ih :
  ∀ {M N : Multiset α} (X Y : Multiset α) (hZ : Z ≠ ∅) (hM : M = X + Y) (hN : N = X + Z)
    (hYZ : ∀ (y : α), y ∈ Y → ∃ (z : α), z ∈ Z ∧ y < z), TransGen OneStep M N
M N X Y : Multiset α
hZ_1 : z ::ₘ Z ≠ ∅
hM : M = X + Y
hN : N = X + z ::ₘ Z
hYZ : ∀ (y : α), y ∈ Y → ∃ (z_1 : α), z_1 ∈ z ::ₘ Z ∧ y < z_1
hZ : Z ≠ 0
Y' : Multiset α := filter (fun (x : α) ↦ x < z) Y
y : α
hy : y ∈ Y ∧ ¬y < z
⊢ y ∈ Y

Tactic:
simp_all
-- Module: Mathlib.Data.Multiset.DershowitzManna
Goal:
α : Type u_1
inst : Preorder α
z : α
Z : Multiset α
ih :
  ∀ {M N : Multiset α} (X Y : Multiset α) (hZ : Z ≠ ∅) (hM : M = X + Y) (hN : N = X + Z)
    (hYZ : ∀ (y : α), y ∈ Y → ∃ (z : α), z ∈ Z ∧ y < z), TransGen OneStep M N
M N X Y : Multiset α
hZ_1 : z ::ₘ Z ≠ ∅
hM : M = X + Y
hN : N = X + z ::ₘ Z
hYZ : ∀ (y : α), y ∈ Y → ∃ (z_1 : α), z_1 ∈ z ::ₘ Z ∧ y < z_1
hZ : Z ≠ 0
Y' : Multiset α := filter (fun (x : α) ↦ x < z) Y
y : α
hy : y ∈ Y ∧ ¬y < z
⊢ ∃ (z : α), z ∈ Z ∧ y < z

Tactic:
simpa [hy.2] using hYZ y (by simp_all)

Premises used: And.right
-- Module: Mathlib.Data.Multiset.DershowitzManna
Goal:
α : Type u_1
inst : Preorder α
M N : Multiset α
hMN : TransGen OneStep M N
X Y : Multiset α
a : α
hYa : ∀ (y : α), y ∈ Y → y < a
⊢ Ne (α := Multiset α) {a} ∅ ∧
    X + Y = X + Y ∧ X + {a} = X + {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 α
hMN : TransGen OneStep M N
X Y : Multiset α
a : α
hYa : ∀ (y : α), y ∈ Y → y < a
⊢ (X + Y).IsDershowitzMannaLT (X + {a})

Tactic:
exact ⟨X, Y, {a}, by simpa⟩
-- Module: Mathlib.Data.Multiset.DershowitzManna
Goal:
α : Type u_1
inst : Preorder α
h : ∀ (M N : Multiset α), TransGen OneStep M N ↔ M.IsDershowitzMannaLT N
⊢ Eq.{u_1 + 1} (α := Multiset α → Multiset α → Prop) (TransGen OneStep) IsDershowitzMannaLT

Tactic:
ext M N
-- Module: Mathlib.Data.Multiset.DershowitzManna
Goal:
α : Type u_1
inst : Preorder α
M N : Multiset α
⊢ TransGen OneStep M N ↔ M.IsDershowitzMannaLT N

Tactic:
⟨isDershowitzMannaLT_of_transGen_oneStep, transGen_oneStep_of_isDershowitzMannaLT⟩

Premises used: _private.0.Multiset.transGen_oneStep_of_isDershowitzMannaLT, _private.0.Multiset.isDershowitzMannaLT_of_transGen_oneStep, Iff.intro
-- Module: Mathlib.Data.Multiset.DershowitzManna
Goal:
α : Type u_1
inst : Preorder α
M N : Multiset α
⊢ TransGen OneStep M N ↔ M.IsDershowitzMannaLT N

Tactic:
exact ⟨isDershowitzMannaLT_of_transGen_oneStep, transGen_oneStep_of_isDershowitzMannaLT⟩
-- Module: Mathlib.Data.Multiset.DershowitzManna
Goal:
α : Type u_1
inst : Preorder α
inst_1 : WellFoundedLT α
rw : WellFounded.{u_1 + 1} (α := Multiset α) (TransGen OneStep)
⊢ WellFounded.{u_1 + 1} (α := Multiset α) IsDershowitzMannaLT

Tactic:
rw [← transGen_oneStep_eq_isDershowitzMannaLT]

Premises used: _private.0.Multiset.transGen_oneStep_eq_isDershowitzMannaLT
-- Module: Mathlib.Data.Multiset.DershowitzManna
Goal:
α : Type u_1
inst : Preorder α
inst_1 : WellFoundedLT α
⊢ WellFounded.{u_1 + 1} (α := Multiset α) (TransGen OneStep)

Tactic:
isDershowitzMannaLT_singleton_wf.transGen

Premises used: _private.0.Multiset.isDershowitzMannaLT_singleton_wf, WellFounded.transGen
-- Module: Mathlib.Data.Multiset.DershowitzManna
Goal:
α : Type u_1
inst : Preorder α
inst_1 : WellFoundedLT α
⊢ WellFounded.{u_1 + 1} (α := Multiset α) (TransGen OneStep)

Tactic:
exact isDershowitzMannaLT_singleton_wf.transGen

Premises used: _private.0.Multiset.isDershowitzMannaLT_singleton_wf, WellFounded.transGen
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
l : List α
⊢ filter p (↑l : Multiset α) = (↑(List.filter (fun (b : α) ↦ decide (p b)) l) : Multiset α)

Tactic:
rfl

Premises used: rfl, Multiset.filter
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
⊢ filter p 0 = 0

Tactic:
rfl

Premises used: Multiset.zero, Multiset.ofList, List.filter, rfl, Multiset.filter
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
p q : α → Prop
inst : DecidablePred p
inst_1 : DecidablePred q
s : Multiset α
_l : List α
h : ∀ (x : α), Membership.mem (γ := Multiset α) (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) _l) x → (p x ↔ q x)
⊢ ∀ (x : α), x ∈ _l → decide (p x) = decide (q x)

Tactic:
simpa using h
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
s t : Multiset α
⊢ filter p (s + t) = filter p s + filter p t

Tactic:
Quotient.inductionOn₂ s t fun _l₁ _l₂ => congr_arg ofList <| filter_append _ _

Premises used: Quotient.inductionOn₂
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
s : Multiset α
⊢ filter p s ≤ s

Tactic:
Quot.inductionOn s fun _l => filter_sublist.subperm

Premises used: Quot.inductionOn
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
s : Multiset α
⊢ filter p s ⊆ s

Tactic:
subset_of_le <| filter_le _ _

Premises used: Multiset.subset_of_le, Multiset.filter_le
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
s t : Multiset α
h : s ≤ t
⊢ filter p s ≤ filter p t

Tactic:
leInductionOn h fun h => (h.filter (p ·)).subperm

Premises used: Multiset.leInductionOn
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
⊢ Monotone (filter p)

Tactic:
fun _s _t => filter_le_filter p

Premises used: Multiset.filter_le_filter, Monotone
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
s : Multiset α
p q : α → Prop
inst : DecidablePred p
inst_1 : DecidablePred q
h : ∀ (b : α), p b → q b
l : List α
⊢ ∀ (a : α), decide (p a) = true → decide (q a) = true

Tactic:
simpa using h
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
a : α
s : Multiset α
x : List α
h : p a
⊢ decide (p a) = true

Tactic:
simpa using h
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
a : α
s : Multiset α
x : List α
h : ¬p a
⊢ ¬decide (p a) = true

Tactic:
simpa using h
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
a : α
s : Multiset α
_l : List α
⊢ a ∈ filter p (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) _l) ↔
    Membership.mem (γ := Multiset α) (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) _l) a ∧ p a

Tactic:
simp
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
a : α
s : Multiset α
h : a ∈ filter p s
⊢ p a

Tactic:
(mem_filter.1 h).2

Premises used: And.right, Iff.mp, Multiset.mem_filter
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
a : α
s : Multiset α
h : a ∈ filter p s
⊢ a ∈ s

Tactic:
(mem_filter.1 h).1

Premises used: And.left, Iff.mp, Multiset.mem_filter
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
a : α
l : Multiset α
m : a ∈ l
h : p a
⊢ a ∈ filter p l

Tactic:
mem_filter.2 ⟨m, h⟩

Premises used: Iff.mpr, And.intro, Multiset.mem_filter
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
s : Multiset α
_l : List α
⊢ List.filter (fun (b : α) ↦ decide (p b)) _l = _l ↔
    ∀ (a : α), Membership.mem (γ := Multiset α) (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) _l) a → p a

Tactic:
simp
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
s : Multiset α
_l : List α
⊢ List.filter (fun (b : α) ↦ decide (p b)) _l = [] ↔
    ∀ (a : α), Membership.mem (γ := Multiset α) (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) _l) a → ¬p a

Tactic:
simp
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
s : Multiset α
⊢ filter (fun (x : α) ↦ True) s = s

Tactic:
simp
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
s : Multiset α
⊢ filter (fun (x : α) ↦ False) s = 0

Tactic:
simp
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
s t : Multiset α
⊢ s ≤ filter p t ↔ s ≤ t ∧ ∀ (a : α), a ∈ s → p a

Tactic:
⟨fun h => ⟨le_trans h (filter_le _ _), fun _a m => of_mem_filter (mem_of_le h m)⟩, fun ⟨h, al⟩ =>
    filter_eq_self.2 al ▸ filter_le_filter p h⟩

Premises used: Iff.mpr, Multiset.filter_eq_self, _private.0.Multiset.le_filter.match_1, Multiset.filter_le_filter, Eq.rec, LE.le, Multiset.of_mem_filter, Multiset.filter_le, Multiset.mem_of_le, And.intro, Iff.intro, Multiset.filter, le_trans
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
a : α
s : Multiset α
pos : ∀ (h : p a), filter p (a ::ₘ s) = {a} + filter p s
neg : ∀ (h : ¬p a), filter p (a ::ₘ s) = 0 + filter p s
⊢ filter p (a ::ₘ s) = (if p a then {a} else 0) + filter p s

Tactic:
split_ifs with h
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
a : α
s : Multiset α
h : p a
pos : a ::ₘ filter p s = {a} + filter p s
pos₁ pos₂ : a ::ₘ filter p s = a ::ₘ filter p s
⊢ filter p (a ::ₘ s) = {a} + filter p s

Tactic:
rw [filter_cons_of_pos _ h, singleton_add]

Premises used: Multiset.singleton_add, Multiset.filter_cons_of_pos
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
a : α
s : Multiset α
h : ¬p a
neg : filter p s = 0 + filter p s
neg₁ neg₂ : filter p s = filter p s
⊢ filter p (a ::ₘ s) = 0 + filter p s

Tactic:
rw [filter_cons_of_neg _ h, Multiset.zero_add]

Premises used: Multiset.zero_add, Multiset.filter_cons_of_neg
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
a : α
p : α → Prop
inst : DecidablePred p
⊢ filter p {a} = if p a then {a} else ∅

Tactic:
simp only [singleton, filter_cons, filter_zero, Multiset.add_zero, empty_eq_zero]

Premises used: Multiset.add_zero, Multiset.filter_cons, Multiset.empty_eq_zero, Multiset.filter_zero, Singleton.singleton
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
q : α → Prop
inst_1 : DecidablePred q
s : Multiset α
l : List α
⊢ filter p (filter q (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) l)) =
    filter (fun (a : α) ↦ p a ∧ q a) (Quot.mk (⇑(isSetoid α) : List α → List α → Prop) l)

Tactic:
simp
-- Module: Mathlib.Data.Multiset.Filter
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
q : α → Prop
inst_1 : DecidablePred q
s : Multiset α
⊢ filter p (filter q s) = filter q (filter p s)

Tactic:
simp [and_comm]

Premises used: and_comm