awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Multiset.DershowitzManna (goal)
Goal:
α : Type u_1
inst : Preorder α
M : Multiset α
hM : ∀ (x : α), x ∈ M → Acc LT.lt x
⊢ Acc OneStep M
have empty : ∀ (hM : ∀ (x : α), Membership.mem (γ := Multiset α) 0 x → Acc LT.lt x), Acc.{u_1 + 1} (α := Multiset α) OneStep 0
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
Cleared hypotheses: hM
-- Lean 4 proof step from Mathlib.Data.Multiset.DershowitzManna (goal)
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
⊢ Acc OneStep M
have 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)
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
Cleared hypotheses: hM
-- Lean 4 proof step from Mathlib.Data.Multiset.DershowitzManna (goal)
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
⊢ TransGen OneStep M N
have 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
Tactic: induction Z using Multiset.induction_on generalizing X Y M N with
  | empty => simp at hZ
  | cons z Z ih => ?_
Cleared hypotheses: M, N, X, Y, Z, hZ, hM, hN, hYZ
-- Lean 4 proof step from Mathlib.Data.Multiset.DershowitzManna (goal)
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
have 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
Tactic: obtain rfl | hZ := eq_or_ne Z 0
Cleared hypotheses: Z, ih, hZ, hN, hYZ
-- Lean 4 proof step from Mathlib.Data.Multiset.DershowitzManna (goal)
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
⊢ TransGen OneStep M N
have cons₁ : ∀ (hZ : Z ≠ 0), TransGen OneStep M N
Tactic: obtain rfl | hZ := eq_or_ne Z 0
-- Lean 4 proof step from Mathlib.Data.Multiset.DershowitzManna (goal)
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
⊢ TransGen OneStep M N
have cons : M = X + Y' + (Y - Y')
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']⟩
-- Lean 4 proof step from Mathlib.Data.Multiset.DershowitzManna (goal)
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')
⊢ TransGen OneStep M N
have cons₁ : ∀ (y : α) (hy : y ∈ Y - Y'), ∃ (z : α), z ∈ Z ∧ y < z
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']⟩
-- Lean 4 proof step from Mathlib.Data.Multiset.DershowitzManna (goal)
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
⊢ M = X + Y' + (Y - Y')
have cons₁ : X + Y = X + Y
Tactic: rw [add_add_tsub_cancel (filter_le ..), hM]
-- Lean 4 proof step from Mathlib.Data.Multiset.DershowitzManna (hypothesis)
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 ∧ y < z
have hy₁ : y ∈ Y ∧ ¬y < z
Tactic: simp only [sub_filter_eq_filter_not, mem_filter, Y'] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Data.Multiset.DershowitzManna (goal)
Goal:
α : Type u_1
inst : Preorder α
M N : Multiset α
⊢ M.IsDershowitzMannaLT N → TransGen OneStep M N
have rintro : ∀ (X Y Z : Multiset α) (hZ : Z ≠ ∅) (hM : M = X + Y) (hN : N = X + Z)
  (hYZ : ∀ (y : α), y ∈ Y → ∃ (z : α), z ∈ Z ∧ y < z), TransGen OneStep M N
Tactic: classical
  rintro ⟨X, Y, Z, hZ, hM, hN, hYZ⟩
  induction Z using Multiset.induction_on generalizing X Y M N with
  | empty => simp at hZ
  | cons z Z ih => ?_
  obtain rfl | hZ := eq_or_ne Z 0
  · exact .single ⟨X, Y, z, hM, hN, by simpa using hYZ⟩
  let Y' : Multiset α := Y.filter (· < z)
  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']⟩
  · rw [add_add_tsub_cancel (filter_le ..), hM]
  · simp only [sub_filter_eq_filter_not, mem_filter, Y'] at hy
    simpa [hy.2] using hYZ y (by simp_all)
-- Lean 4 proof step from Mathlib.Data.Multiset.DershowitzManna (goal)
Goal:
α : Type u_1
inst : Preorder α
M N : Multiset α
rintro :
  ∀ (X Y Z : 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.IsDershowitzMannaLT N → TransGen OneStep M N
have 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
Tactic: classical
  rintro ⟨X, Y, Z, hZ, hM, hN, hYZ⟩
  induction Z using Multiset.induction_on generalizing X Y M N with
  | empty => simp at hZ
  | cons z Z ih => ?_
  obtain rfl | hZ := eq_or_ne Z 0
  · exact .single ⟨X, Y, z, hM, hN, by simpa using hYZ⟩
  let Y' : Multiset α := Y.filter (· < z)
  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']⟩
  · rw [add_add_tsub_cancel (filter_le ..), hM]
  · simp only [sub_filter_eq_filter_not, mem_filter, Y'] at hy
    simpa [hy.2] using hYZ y (by simp_all)
Cleared hypotheses: M, N
-- Lean 4 proof step from Mathlib.Data.Multiset.DershowitzManna (goal)
Goal:
α : Type u_1
inst : Preorder α
M N : Multiset α
rintro :
  ∀ (X Y Z : Multiset α) (hZ : Z ≠ ∅) (hM : M = X + Y) (hN : N = X + Z)
    (hYZ : ∀ (y : α), y ∈ Y → ∃ (z : α), z ∈ Z ∧ y < z), TransGen OneStep M N
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
⊢ M.IsDershowitzMannaLT N → TransGen OneStep M N
have cons₁ : ∀ (z : α) {M N : Multiset α} (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: classical
  rintro ⟨X, Y, Z, hZ, hM, hN, hYZ⟩
  induction Z using Multiset.induction_on generalizing X Y M N with
  | empty => simp at hZ
  | cons z Z ih => ?_
  obtain rfl | hZ := eq_or_ne Z 0
  · exact .single ⟨X, Y, z, hM, hN, by simpa using hYZ⟩
  let Y' : Multiset α := Y.filter (· < z)
  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']⟩
  · rw [add_add_tsub_cancel (filter_le ..), hM]
  · simp only [sub_filter_eq_filter_not, mem_filter, Y'] at hy
    simpa [hy.2] using hYZ y (by simp_all)
Cleared hypotheses: M, N
-- Lean 4 proof step from Mathlib.Data.Multiset.DershowitzManna (goal)
Goal:
α : Type u_1
inst : Preorder α
M N : Multiset α
rintro :
  ∀ (X Y Z : Multiset α) (hZ : Z ≠ ∅) (hM : M = X + Y) (hN : N = X + Z)
    (hYZ : ∀ (y : α), y ∈ Y → ∃ (z : α), z ∈ Z ∧ y < z), TransGen OneStep M N
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
cons₁ :
  ∀ (z : α) {M N : Multiset α} (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
⊢ M.IsDershowitzMannaLT N → TransGen OneStep M N
have 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) (hZ : Z ≠ 0), TransGen OneStep M N
Tactic: classical
  rintro ⟨X, Y, Z, hZ, hM, hN, hYZ⟩
  induction Z using Multiset.induction_on generalizing X Y M N with
  | empty => simp at hZ
  | cons z Z ih => ?_
  obtain rfl | hZ := eq_or_ne Z 0
  · exact .single ⟨X, Y, z, hM, hN, by simpa using hYZ⟩
  let Y' : Multiset α := Y.filter (· < z)
  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']⟩
  · rw [add_add_tsub_cancel (filter_le ..), hM]
  · simp only [sub_filter_eq_filter_not, mem_filter, Y'] at hy
    simpa [hy.2] using hYZ y (by simp_all)
Cleared hypotheses: M, N
-- Lean 4 proof step from Mathlib.Data.Multiset.DershowitzManna (goal)
Goal:
α : Type u_1
inst : Preorder α
M N : Multiset α
rintro :
  ∀ (X Y Z : Multiset α) (hZ : Z ≠ ∅) (hM : M = X + Y) (hN : N = X + Z)
    (hYZ : ∀ (y : α), y ∈ Y → ∃ (z : α), z ∈ Z ∧ y < z), TransGen OneStep M N
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
cons₁ :
  ∀ (z : α) {M N : Multiset α} (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
cons₂ 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) (hZ : Z ≠ 0), TransGen OneStep M N
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) (hZ : Z ≠ 0), TransGen OneStep M N
⊢ M.IsDershowitzMannaLT N → TransGen OneStep M N
have 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) (hZ : Z ≠ 0),
  let Y' := filter (fun (x : α) ↦ x < z) Y;
  M = X + Y' + (Y - Y')
Tactic: classical
  rintro ⟨X, Y, Z, hZ, hM, hN, hYZ⟩
  induction Z using Multiset.induction_on generalizing X Y M N with
  | empty => simp at hZ
  | cons z Z ih => ?_
  obtain rfl | hZ := eq_or_ne Z 0
  · exact .single ⟨X, Y, z, hM, hN, by simpa using hYZ⟩
  let Y' : Multiset α := Y.filter (· < z)
  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']⟩
  · rw [add_add_tsub_cancel (filter_le ..), hM]
  · simp only [sub_filter_eq_filter_not, mem_filter, Y'] at hy
    simpa [hy.2] using hYZ y (by simp_all)
Cleared hypotheses: M, N
-- Lean 4 proof step from Mathlib.Data.Multiset.DershowitzManna (goal)
Goal:
α : Type u_1
inst : Preorder α
⊢ Eq.{u_1 + 1} (α := Multiset α → Multiset α → Prop) (TransGen OneStep) IsDershowitzMannaLT
have h : ∀ (M N : Multiset α), TransGen OneStep M N ↔ M.IsDershowitzMannaLT N
Tactic: ext M N
-- Lean 4 proof step from Mathlib.Data.Multiset.DershowitzManna (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : WellFoundedLT α
⊢ WellFounded.{u_1 + 1} (α := Multiset α) IsDershowitzMannaLT
have rw : WellFounded.{u_1 + 1} (α := Multiset α) (TransGen OneStep)
Tactic: rw [← transGen_oneStep_eq_isDershowitzMannaLT]
-- Lean 4 proof step from Mathlib.Data.Multiset.Filter (goal)
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
a : α
s : Multiset α
⊢ filter p (a ::ₘ s) = (if p a then {a} else 0) + filter p s
have pos : ∀ (h : p a), filter p (a ::ₘ s) = {a} + filter p s
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.Multiset.Filter (goal)
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
a : α
s : Multiset α
pos : ∀ (h : p a), filter p (a ::ₘ s) = {a} + filter p s
⊢ filter p (a ::ₘ s) = (if p a then {a} else 0) + filter p s
have neg : ∀ (h : ¬p a), filter p (a ::ₘ s) = 0 + filter p s
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.Multiset.Filter (goal)
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
a : α
s : Multiset α
h : p a
⊢ filter p (a ::ₘ s) = {a} + filter p s
have pos : a ::ₘ filter p s = {a} + filter p s
Tactic: rw [filter_cons_of_pos _ h, singleton_add]
-- Lean 4 proof step from Mathlib.Data.Multiset.Filter (goal)
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
a : α
s : Multiset α
h : p a
pos : a ::ₘ filter p s = {a} + filter p s
⊢ filter p (a ::ₘ s) = {a} + filter p s
have pos₁ : a ::ₘ filter p s = a ::ₘ filter p s
Tactic: rw [filter_cons_of_pos _ h, singleton_add]
-- Lean 4 proof step from Mathlib.Data.Multiset.Filter (goal)
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
a : α
s : Multiset α
h : ¬p a
⊢ filter p (a ::ₘ s) = 0 + filter p s
have neg : filter p s = 0 + filter p s
Tactic: rw [filter_cons_of_neg _ h, Multiset.zero_add]
-- Lean 4 proof step from Mathlib.Data.Multiset.Filter (goal)
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
a : α
s : Multiset α
h : ¬p a
neg : filter p s = 0 + filter p s
⊢ filter p (a ::ₘ s) = 0 + filter p s
have neg₁ : filter p s = filter p s
Tactic: rw [filter_cons_of_neg _ h, Multiset.zero_add]
-- Lean 4 proof step from Mathlib.Data.Multiset.Filter (goal)
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
q : α → Prop
inst_1 : DecidablePred q
s_1 : Multiset α
a : α
s : Multiset α
IH : filter p s + filter q s = filter (fun (a : α) ↦ p a ∨ q a) s + filter (fun (a : α) ↦ p a ∧ q a) s
⊢ filter p (a ::ₘ s) + filter q (a ::ₘ s) =
    filter (fun (a : α) ↦ p a ∨ q a) (a ::ₘ s) + filter (fun (a : α) ↦ p a ∧ q a) (a ::ₘ s)
have pos : p a →
  filter p (a ::ₘ s) + filter q (a ::ₘ s) =
    filter (fun (a : α) ↦ p a ∨ q a) (a ::ₘ s) + filter (fun (a : α) ↦ p a ∧ q a) (a ::ₘ s)
Tactic: by_cases p a
-- Lean 4 proof step from Mathlib.Data.Multiset.Filter (goal)
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
q : α → Prop
inst_1 : DecidablePred q
s_1 : Multiset α
a : α
s : Multiset α
IH : filter p s + filter q s = filter (fun (a : α) ↦ p a ∨ q a) s + filter (fun (a : α) ↦ p a ∧ q a) s
pos :
  p a →
    filter p (a ::ₘ s) + filter q (a ::ₘ s) =
      filter (fun (a : α) ↦ p a ∨ q a) (a ::ₘ s) + filter (fun (a : α) ↦ p a ∧ q a) (a ::ₘ s)
⊢ filter p (a ::ₘ s) + filter q (a ::ₘ s) =
    filter (fun (a : α) ↦ p a ∨ q a) (a ::ₘ s) + filter (fun (a : α) ↦ p a ∧ q a) (a ::ₘ s)
have neg : ¬p a →
  filter p (a ::ₘ s) + filter q (a ::ₘ s) =
    filter (fun (a : α) ↦ p a ∨ q a) (a ::ₘ s) + filter (fun (a : α) ↦ p a ∧ q a) (a ::ₘ s)
Tactic: by_cases p a
-- Lean 4 proof step from Mathlib.Data.Multiset.Filter (goal)
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
q : α → Prop
inst_1 : DecidablePred q
s_1 : Multiset α
a : α
s : Multiset α
IH : filter p s + filter q s = filter (fun (a : α) ↦ p a ∨ q a) s + filter (fun (a : α) ↦ p a ∧ q a) s
h : p a
⊢ filter p (a ::ₘ s) + filter q (a ::ₘ s) =
    filter (fun (a : α) ↦ p a ∨ q a) (a ::ₘ s) + filter (fun (a : α) ↦ p a ∧ q a) (a ::ₘ s)
have pos : q a →
  filter p (a ::ₘ s) + filter q (a ::ₘ s) =
    filter (fun (a : α) ↦ p a ∨ q a) (a ::ₘ s) + filter (fun (a : α) ↦ p a ∧ q a) (a ::ₘ s)
Tactic: by_cases q a
-- Lean 4 proof step from Mathlib.Data.Multiset.Filter (goal)
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
q : α → Prop
inst_1 : DecidablePred q
s_1 : Multiset α
a : α
s : Multiset α
IH : filter p s + filter q s = filter (fun (a : α) ↦ p a ∨ q a) s + filter (fun (a : α) ↦ p a ∧ q a) s
h : p a
pos :
  q a →
    filter p (a ::ₘ s) + filter q (a ::ₘ s) =
      filter (fun (a : α) ↦ p a ∨ q a) (a ::ₘ s) + filter (fun (a : α) ↦ p a ∧ q a) (a ::ₘ s)
⊢ filter p (a ::ₘ s) + filter q (a ::ₘ s) =
    filter (fun (a : α) ↦ p a ∨ q a) (a ::ₘ s) + filter (fun (a : α) ↦ p a ∧ q a) (a ::ₘ s)
have neg : ¬q a →
  filter p (a ::ₘ s) + filter q (a ::ₘ s) =
    filter (fun (a : α) ↦ p a ∨ q a) (a ::ₘ s) + filter (fun (a : α) ↦ p a ∧ q a) (a ::ₘ s)
Tactic: by_cases q a
-- Lean 4 proof step from Mathlib.Data.Multiset.Filter (goal)
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
q : α → Prop
inst_1 : DecidablePred q
s_1 : Multiset α
a : α
s : Multiset α
IH : filter p s + filter q s = filter (fun (a : α) ↦ p a ∨ q a) s + filter (fun (a : α) ↦ p a ∧ q a) s
h : ¬p a
⊢ filter p (a ::ₘ s) + filter q (a ::ₘ s) =
    filter (fun (a : α) ↦ p a ∨ q a) (a ::ₘ s) + filter (fun (a : α) ↦ p a ∧ q a) (a ::ₘ s)
have pos : q a →
  filter p (a ::ₘ s) + filter q (a ::ₘ s) =
    filter (fun (a : α) ↦ p a ∨ q a) (a ::ₘ s) + filter (fun (a : α) ↦ p a ∧ q a) (a ::ₘ s)
Tactic: by_cases q a
-- Lean 4 proof step from Mathlib.Data.Multiset.Filter (goal)
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
q : α → Prop
inst_1 : DecidablePred q
s_1 : Multiset α
a : α
s : Multiset α
IH : filter p s + filter q s = filter (fun (a : α) ↦ p a ∨ q a) s + filter (fun (a : α) ↦ p a ∧ q a) s
h : ¬p a
pos :
  q a →
    filter p (a ::ₘ s) + filter q (a ::ₘ s) =
      filter (fun (a : α) ↦ p a ∨ q a) (a ::ₘ s) + filter (fun (a : α) ↦ p a ∧ q a) (a ::ₘ s)
⊢ filter p (a ::ₘ s) + filter q (a ::ₘ s) =
    filter (fun (a : α) ↦ p a ∨ q a) (a ::ₘ s) + filter (fun (a : α) ↦ p a ∧ q a) (a ::ₘ s)
have neg : ¬q a →
  filter p (a ::ₘ s) + filter q (a ::ₘ s) =
    filter (fun (a : α) ↦ p a ∨ q a) (a ::ₘ s) + filter (fun (a : α) ↦ p a ∧ q a) (a ::ₘ s)
Tactic: by_cases q a
-- Lean 4 proof step from Mathlib.Data.Multiset.Filter (goal)
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
s : Multiset α
⊢ filter p s + filter (fun (a : α) ↦ ¬p a) s = s
have rw : s + 0 = s
Tactic: rw [filter_add_filter, filter_eq_self.2, filter_eq_nil.2]
-- Lean 4 proof step from Mathlib.Data.Multiset.Filter (goal)
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
s : Multiset α
rw : s + 0 = s
⊢ filter p s + filter (fun (a : α) ↦ ¬p a) s = s
have rw₁ : ∀ (a : α), a ∈ s → ¬(p a ∧ ¬p a)
Tactic: rw [filter_add_filter, filter_eq_self.2, filter_eq_nil.2]
-- Lean 4 proof step from Mathlib.Data.Multiset.Filter (goal)
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
s : Multiset α
rw : s + 0 = s
rw₁ : ∀ (a : α), a ∈ s → ¬(p a ∧ ¬p a)
⊢ filter p s + filter (fun (a : α) ↦ ¬p a) s = s
have rw₂ : ∀ (a : α), a ∈ s → p a ∨ ¬p a
Tactic: rw [filter_add_filter, filter_eq_self.2, filter_eq_nil.2]
-- Lean 4 proof step from Mathlib.Data.Multiset.Filter (goal)
Goal:
α : Type u_1
β : Type v
p : α → Prop
inst : DecidablePred p
f : β → α
s : Multiset β
l : List β
⊢ filter p (map f (Quot.mk (⇑(isSetoid β) : List β → List β → Prop) l)) =
    map f (filter (p ∘ f) (Quot.mk (⇑(isSetoid β) : List β → List β → Prop) l))
have simp : List.map f (List.filter ((fun (b : α) ↦ decide (p b)) ∘ f) l) ~
  List.map f (List.filter ((fun (b : α) ↦ decide (p b)) ∘ f) l)
Tactic: simp [List.filter_map]