Theorem: red_insert (Pdl/MultisetOrder.lean)

State before:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N : Multiset α
H : MultisetRedLt N (a ::ₘ M)
⊢ ∃ M', N = a ::ₘ M' ∧ MultisetRedLt M' M ∨ N = M + M' ∧ ∀ x ∈ M', x < a
Tactic:
rcases H with ⟨X, Y, a0, H1, H0, H2⟩
State after:
case RedLt
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H0 : a ::ₘ M = X + {a0}
H2 : ∀ y ∈ Y, y < a0
⊢ ∃ M', N = a ::ₘ M' ∧ MultisetRedLt M' M ∨ N = M + M' ∧ ∀ x ∈ M', x < a

State before:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H0 : a ::ₘ M = X + {a0}
H2 : ∀ y ∈ Y, y < a0
hyp : a = a0
⊢ ∃ M', N = a ::ₘ M' ∧ MultisetRedLt M' M ∨ N = M + M' ∧ ∀ x ∈ M', x < a
Tactic:
exists Y
State after:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H0 : a ::ₘ M = X + {a0}
H2 : ∀ y ∈ Y, y < a0
hyp : a = a0
⊢ N = a ::ₘ Y ∧ MultisetRedLt Y M ∨ N = M + Y ∧ ∀ x ∈ Y, x < a

State before:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H0 : a ::ₘ M = X + {a0}
H2 : ∀ y ∈ Y, y < a0
hyp : a = a0
⊢ N = a ::ₘ Y ∧ MultisetRedLt Y M ∨ N = M + Y ∧ ∀ x ∈ Y, x < a
Tactic:
right
State after:
case h
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H0 : a ::ₘ M = X + {a0}
H2 : ∀ y ∈ Y, y < a0
hyp : a = a0
⊢ N = M + Y ∧ ∀ x ∈ Y, x < a

State before:
case h
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H0 : a ::ₘ M = X + {a0}
H2 : ∀ y ∈ Y, y < a0
hyp : a = a0
⊢ N = M + Y ∧ ∀ x ∈ Y, x < a
Tactic:
apply And.intro
State after:
case h.left
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H0 : a ::ₘ M = X + {a0}
H2 : ∀ y ∈ Y, y < a0
hyp : a = a0
⊢ N = M + Y

case h.right
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H0 : a ::ₘ M = X + {a0}
H2 : ∀ y ∈ Y, y < a0
hyp : a = a0
⊢ ∀ x ∈ Y, x < a

State before:
case h.left
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H0 : a ::ₘ M = X + {a0}
H2 : ∀ y ∈ Y, y < a0
hyp : a = a0
⊢ N = M + Y

case h.right
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H0 : a ::ₘ M = X + {a0}
H2 : ∀ y ∈ Y, y < a0
hyp : a = a0
⊢ ∀ x ∈ Y, x < a
Tactic:
. rw [H1]
  rw [add_left_inj]
  rw [mul_cons_trivial] at H0
  simp_all
State after:
case h.right
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H0 : a ::ₘ M = X + {a0}
H2 : ∀ y ∈ Y, y < a0
hyp : a = a0
⊢ ∀ x ∈ Y, x < a

State before:
case h.right
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H0 : a ::ₘ M = X + {a0}
H2 : ∀ y ∈ Y, y < a0
hyp : a = a0
⊢ ∀ x ∈ Y, x < a
Tactic:
. simp_all
State after:
no goals

State before:
case h.left
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H0 : a ::ₘ M = X + {a0}
H2 : ∀ y ∈ Y, y < a0
hyp : a = a0
⊢ N = M + Y
Tactic:
rw [H1]
State after:
case h.left
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H0 : a ::ₘ M = X + {a0}
H2 : ∀ y ∈ Y, y < a0
hyp : a = a0
⊢ X + Y = M + Y

State before:
case h.left
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H0 : a ::ₘ M = X + {a0}
H2 : ∀ y ∈ Y, y < a0
hyp : a = a0
⊢ X + Y = M + Y
Tactic:
rw [add_left_inj]
State after:
case h.left
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H0 : a ::ₘ M = X + {a0}
H2 : ∀ y ∈ Y, y < a0
hyp : a = a0
⊢ X = M

State before:
case h.left
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H0 : a ::ₘ M = X + {a0}
H2 : ∀ y ∈ Y, y < a0
hyp : a = a0
⊢ X = M
Tactic:
rw [mul_cons_trivial] at H0
State after:
case h.left
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H0 : a ::ₘ M = a0 ::ₘ X
H2 : ∀ y ∈ Y, y < a0
hyp : a = a0
⊢ X = M

State before:
case h.left
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H0 : a ::ₘ M = a0 ::ₘ X
H2 : ∀ y ∈ Y, y < a0
hyp : a = a0
⊢ X = M
Tactic:
simp_all
State after:
no goals

State before:
case h.right
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H0 : a ::ₘ M = X + {a0}
H2 : ∀ y ∈ Y, y < a0
hyp : a = a0
⊢ ∀ x ∈ Y, x < a
Tactic:
simp_all
State after:
no goals

State before:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H0 : a ::ₘ M = X + {a0}
H2 : ∀ y ∈ Y, y < a0
hyp : ¬a = a0
⊢ ∃ M', N = a ::ₘ M' ∧ MultisetRedLt M' M ∨ N = M + M' ∧ ∀ x ∈ M', x < a
Tactic:
exists (Y + (M - {a0}))
State after:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H0 : a ::ₘ M = X + {a0}
H2 : ∀ y ∈ Y, y < a0
hyp : ¬a = a0
⊢ N = a ::ₘ (Y + (M - {a0})) ∧ MultisetRedLt (Y + (M - {a0})) M ∨ N = M + (Y + (M - {a0})) ∧ ∀ x ∈ Y + (M - {a0}), x < a

State before:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H0 : a ::ₘ M = X + {a0}
H2 : ∀ y ∈ Y, y < a0
hyp : ¬a = a0
⊢ N = a ::ₘ (Y + (M - {a0})) ∧ MultisetRedLt (Y + (M - {a0})) M ∨ N = M + (Y + (M - {a0})) ∧ ∀ x ∈ Y + (M - {a0}), x < a
Tactic:
left
State after:
case h
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H0 : a ::ₘ M = X + {a0}
H2 : ∀ y ∈ Y, y < a0
hyp : ¬a = a0
⊢ N = a ::ₘ (Y + (M - {a0})) ∧ MultisetRedLt (Y + (M - {a0})) M

State before:
case h
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H0 : a ::ₘ M = X + {a0}
H2 : ∀ y ∈ Y, y < a0
hyp : ¬a = a0
⊢ N = a ::ₘ (Y + (M - {a0})) ∧ MultisetRedLt (Y + (M - {a0})) M
Tactic:
constructor
State after:
case h.left
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H0 : a ::ₘ M = X + {a0}
H2 : ∀ y ∈ Y, y < a0
hyp : ¬a = a0
⊢ N = a ::ₘ (Y + (M - {a0}))

case h.right
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H0 : a ::ₘ M = X + {a0}
H2 : ∀ y ∈ Y, y < a0
hyp : ¬a = a0
⊢ MultisetRedLt (Y + (M - {a0})) M

State before:
case h.left
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H0 : a ::ₘ M = X + {a0}
H2 : ∀ y ∈ Y, y < a0
hyp : ¬a = a0
⊢ N = a ::ₘ (Y + (M - {a0}))

case h.right
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H0 : a ::ₘ M = X + {a0}
H2 : ∀ y ∈ Y, y < a0
hyp : ¬a = a0
⊢ MultisetRedLt (Y + (M - {a0})) M
Tactic:
. rw [H1]
  have : X = (M - {a0} + {a}) := by
    simp [mul_cons_trivial] at *
    ext b
    rw [Multiset.count_cons]
    simp [Multiset.ext, Multiset.count_cons] at H0
    if h : b = a then
      rw [h]
      have := H0 b
      aesop
    else
      have := H0 b
      simp [mul_erase_trivial]
      aesop
  subst this
  rw [add_comm,mul_cons_trivial]
  aesop
State after:
case h.right
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H0 : a ::ₘ M = X + {a0}
H2 : ∀ y ∈ Y, y < a0
hyp : ¬a = a0
⊢ MultisetRedLt (Y + (M - {a0})) M

State before:
case h.left
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H0 : a ::ₘ M = X + {a0}
H2 : ∀ y ∈ Y, y < a0
hyp : ¬a = a0
⊢ N = a ::ₘ (Y + (M - {a0}))
Tactic:
rw [H1]
State after:
case h.left
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H0 : a ::ₘ M = X + {a0}
H2 : ∀ y ∈ Y, y < a0
hyp : ¬a = a0
⊢ X + Y = a ::ₘ (Y + (M - {a0}))

State before:
case h.left
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H0 : a ::ₘ M = X + {a0}
H2 : ∀ y ∈ Y, y < a0
hyp : ¬a = a0
⊢ X + Y = a ::ₘ (Y + (M - {a0}))
Tactic:
have : X = (M - {a0} + {a}) := by
  simp [mul_cons_trivial] at *
  ext b
  rw [Multiset.count_cons]
  simp [Multiset.ext, Multiset.count_cons] at H0
  if h : b = a then
    rw [h]
    have := H0 b
    aesop
  else
    have := H0 b
    simp [mul_erase_trivial]
    aesop
State after:
case h.left
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H0 : a ::ₘ M = X + {a0}
H2 : ∀ y ∈ Y, y < a0
hyp : ¬a = a0
this : X = M - {a0} + {a}
⊢ X + Y = a ::ₘ (Y + (M - {a0}))

State before:
case h.left
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H0 : a ::ₘ M = X + {a0}
H2 : ∀ y ∈ Y, y < a0
hyp : ¬a = a0
this : X = M - {a0} + {a}
⊢ X + Y = a ::ₘ (Y + (M - {a0}))
Tactic:
subst this
State after:
case h.left
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N Y : Multiset α
a0 : α
H2 : ∀ y ∈ Y, y < a0
hyp : ¬a = a0
H1 : N = M - {a0} + {a} + Y
H0 : a ::ₘ M = M - {a0} + {a} + {a0}
⊢ M - {a0} + {a} + Y = a ::ₘ (Y + (M - {a0}))

State before:
case h.left
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N Y : Multiset α
a0 : α
H2 : ∀ y ∈ Y, y < a0
hyp : ¬a = a0
H1 : N = M - {a0} + {a} + Y
H0 : a ::ₘ M = M - {a0} + {a} + {a0}
⊢ M - {a0} + {a} + Y = a ::ₘ (Y + (M - {a0}))
Tactic:
rw [add_comm,mul_cons_trivial]
State after:
case h.left
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N Y : Multiset α
a0 : α
H2 : ∀ y ∈ Y, y < a0
hyp : ¬a = a0
H1 : N = M - {a0} + {a} + Y
H0 : a ::ₘ M = M - {a0} + {a} + {a0}
⊢ Y + a ::ₘ (M - {a0}) = a ::ₘ (Y + (M - {a0}))

State before:
case h.left
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N Y : Multiset α
a0 : α
H2 : ∀ y ∈ Y, y < a0
hyp : ¬a = a0
H1 : N = M - {a0} + {a} + Y
H0 : a ::ₘ M = M - {a0} + {a} + {a0}
⊢ Y + a ::ₘ (M - {a0}) = a ::ₘ (Y + (M - {a0}))
Tactic:
aesop
State after:
no goals

State before:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H0 : a ::ₘ M = X + {a0}
H2 : ∀ y ∈ Y, y < a0
hyp : ¬a = a0
⊢ X = M - {a0} + {a}
Tactic:
simp [mul_cons_trivial] at *
State after:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H2 : ∀ y ∈ Y, y < a0
hyp : ¬a = a0
H0 : a ::ₘ M = a0 ::ₘ X
⊢ X = a ::ₘ (M - {a0})

State before:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H2 : ∀ y ∈ Y, y < a0
hyp : ¬a = a0
H0 : a ::ₘ M = a0 ::ₘ X
⊢ X = a ::ₘ (M - {a0})
Tactic:
ext b
State after:
case a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H2 : ∀ y ∈ Y, y < a0
hyp : ¬a = a0
H0 : a ::ₘ M = a0 ::ₘ X
b : α
⊢ Multiset.count b X = Multiset.count b (a ::ₘ (M - {a0}))

State before:
case a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H2 : ∀ y ∈ Y, y < a0
hyp : ¬a = a0
H0 : a ::ₘ M = a0 ::ₘ X
b : α
⊢ Multiset.count b X = Multiset.count b (a ::ₘ (M - {a0}))
Tactic:
rw [Multiset.count_cons]
State after:
case a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H2 : ∀ y ∈ Y, y < a0
hyp : ¬a = a0
H0 : a ::ₘ M = a0 ::ₘ X
b : α
⊢ Multiset.count b X = Multiset.count b (M - {a0}) + if b = a then 1 else 0

State before:
case a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H2 : ∀ y ∈ Y, y < a0
hyp : ¬a = a0
H0 : a ::ₘ M = a0 ::ₘ X
b : α
⊢ Multiset.count b X = Multiset.count b (M - {a0}) + if b = a then 1 else 0
Tactic:
simp [Multiset.ext, Multiset.count_cons] at H0
State after:
case a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H2 : ∀ y ∈ Y, y < a0
hyp : ¬a = a0
b : α
H0 : ∀ (a_1 : α), (Multiset.count a_1 M + if a_1 = a then 1 else 0) = Multiset.count a_1 X + if a_1 = a0 then 1 else 0
⊢ Multiset.count b X = Multiset.count b (M - {a0}) + if b = a then 1 else 0

State before:
case a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H2 : ∀ y ∈ Y, y < a0
hyp : ¬a = a0
b : α
H0 : ∀ (a_1 : α), (Multiset.count a_1 M + if a_1 = a then 1 else 0) = Multiset.count a_1 X + if a_1 = a0 then 1 else 0
⊢ Multiset.count b X = Multiset.count b (M - {a0}) + if b = a then 1 else 0
Tactic:
if h : b = a then
  rw [h]
  have := H0 b
  aesop
else
  have := H0 b
  simp [mul_erase_trivial]
  aesop
State after:
no goals

State before:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H2 : ∀ y ∈ Y, y < a0
hyp : ¬a = a0
b : α
H0 : ∀ (a_1 : α), (Multiset.count a_1 M + if a_1 = a then 1 else 0) = Multiset.count a_1 X + if a_1 = a0 then 1 else 0
h : b = a
⊢ Multiset.count b X = Multiset.count b (M - {a0}) + if b = a then 1 else 0
Tactic:
rw [h]
State after:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H2 : ∀ y ∈ Y, y < a0
hyp : ¬a = a0
b : α
H0 : ∀ (a_1 : α), (Multiset.count a_1 M + if a_1 = a then 1 else 0) = Multiset.count a_1 X + if a_1 = a0 then 1 else 0
h : b = a
⊢ Multiset.count a X = Multiset.count a (M - {a0}) + if a = a then 1 else 0

State before:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H2 : ∀ y ∈ Y, y < a0
hyp : ¬a = a0
b : α
H0 : ∀ (a_1 : α), (Multiset.count a_1 M + if a_1 = a then 1 else 0) = Multiset.count a_1 X + if a_1 = a0 then 1 else 0
h : b = a
⊢ Multiset.count a X = Multiset.count a (M - {a0}) + if a = a then 1 else 0
Tactic:
have := H0 b
State after:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H2 : ∀ y ∈ Y, y < a0
hyp : ¬a = a0
b : α
H0 : ∀ (a_1 : α), (Multiset.count a_1 M + if a_1 = a then 1 else 0) = Multiset.count a_1 X + if a_1 = a0 then 1 else 0
h : b = a
this : (Multiset.count b M + if b = a then 1 else 0) = Multiset.count b X + if b = a0 then 1 else 0
⊢ Multiset.count a X = Multiset.count a (M - {a0}) + if a = a then 1 else 0

State before:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H2 : ∀ y ∈ Y, y < a0
hyp : ¬a = a0
b : α
H0 : ∀ (a_1 : α), (Multiset.count a_1 M + if a_1 = a then 1 else 0) = Multiset.count a_1 X + if a_1 = a0 then 1 else 0
h : b = a
this : (Multiset.count b M + if b = a then 1 else 0) = Multiset.count b X + if b = a0 then 1 else 0
⊢ Multiset.count a X = Multiset.count a (M - {a0}) + if a = a then 1 else 0
Tactic:
aesop
State after:
no goals

State before:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H2 : ∀ y ∈ Y, y < a0
hyp : ¬a = a0
b : α
H0 : ∀ (a_1 : α), (Multiset.count a_1 M + if a_1 = a then 1 else 0) = Multiset.count a_1 X + if a_1 = a0 then 1 else 0
h : ¬b = a
⊢ Multiset.count b X = Multiset.count b (M - {a0}) + if b = a then 1 else 0
Tactic:
have := H0 b
State after:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H2 : ∀ y ∈ Y, y < a0
hyp : ¬a = a0
b : α
H0 : ∀ (a_1 : α), (Multiset.count a_1 M + if a_1 = a then 1 else 0) = Multiset.count a_1 X + if a_1 = a0 then 1 else 0
h : ¬b = a
this : (Multiset.count b M + if b = a then 1 else 0) = Multiset.count b X + if b = a0 then 1 else 0
⊢ Multiset.count b X = Multiset.count b (M - {a0}) + if b = a then 1 else 0

State before:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H2 : ∀ y ∈ Y, y < a0
hyp : ¬a = a0
b : α
H0 : ∀ (a_1 : α), (Multiset.count a_1 M + if a_1 = a then 1 else 0) = Multiset.count a_1 X + if a_1 = a0 then 1 else 0
h : ¬b = a
this : (Multiset.count b M + if b = a then 1 else 0) = Multiset.count b X + if b = a0 then 1 else 0
⊢ Multiset.count b X = Multiset.count b (M - {a0}) + if b = a then 1 else 0
Tactic:
simp [mul_erase_trivial]
State after:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H2 : ∀ y ∈ Y, y < a0
hyp : ¬a = a0
b : α
H0 : ∀ (a_1 : α), (Multiset.count a_1 M + if a_1 = a then 1 else 0) = Multiset.count a_1 X + if a_1 = a0 then 1 else 0
h : ¬b = a
this : (Multiset.count b M + if b = a then 1 else 0) = Multiset.count b X + if b = a0 then 1 else 0
⊢ Multiset.count b X = Multiset.count b (M.erase a0) + if b = a then 1 else 0

State before:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H2 : ∀ y ∈ Y, y < a0
hyp : ¬a = a0
b : α
H0 : ∀ (a_1 : α), (Multiset.count a_1 M + if a_1 = a then 1 else 0) = Multiset.count a_1 X + if a_1 = a0 then 1 else 0
h : ¬b = a
this : (Multiset.count b M + if b = a then 1 else 0) = Multiset.count b X + if b = a0 then 1 else 0
⊢ Multiset.count b X = Multiset.count b (M.erase a0) + if b = a then 1 else 0
Tactic:
aesop
State after:
no goals

State before:
case h.right
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H0 : a ::ₘ M = X + {a0}
H2 : ∀ y ∈ Y, y < a0
hyp : ¬a = a0
⊢ MultisetRedLt (Y + (M - {a0})) M
Tactic:
constructor
State after:
case h.right.a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H0 : a ::ₘ M = X + {a0}
H2 : ∀ y ∈ Y, y < a0
hyp : ¬a = a0
⊢ Y + (M - {a0}) = ?h.right.X + ?h.right.Y

case h.right.a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H0 : a ::ₘ M = X + {a0}
H2 : ∀ y ∈ Y, y < a0
hyp : ¬a = a0
⊢ M = ?h.right.X + {?h.right.a}

case h.right.a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H0 : a ::ₘ M = X + {a0}
H2 : ∀ y ∈ Y, y < a0
hyp : ¬a = a0
⊢ ∀ y ∈ ?h.right.Y, y < ?h.right.a

case h.right.X
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H0 : a ::ₘ M = X + {a0}
H2 : ∀ y ∈ Y, y < a0
hyp : ¬a = a0
⊢ Multiset α

case h.right.Y
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H0 : a ::ₘ M = X + {a0}
H2 : ∀ y ∈ Y, y < a0
hyp : ¬a = a0
⊢ Multiset α

case h.right.a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H0 : a ::ₘ M = X + {a0}
H2 : ∀ y ∈ Y, y < a0
hyp : ¬a = a0
⊢ α

State before:
case h.right.a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H0 : a ::ₘ M = X + {a0}
H2 : ∀ y ∈ Y, y < a0
hyp : ¬a = a0
⊢ ∀ y ∈ Y, y < a0
Tactic:
exact H2
State after:
no goals

State before:
case h.right.a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H0 : a ::ₘ M = X + {a0}
H2 : ∀ y ∈ Y, y < a0
hyp : ¬a = a0
⊢ Y + (M - {a0}) = ?h.right.X + ?h.right.Y
Tactic:
change Y + (M - {a0}) = (M - {a0}) + Y
State after:
case h.right.a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H0 : a ::ₘ M = X + {a0}
H2 : ∀ y ∈ Y, y < a0
hyp : ¬a = a0
⊢ Y + (M - {a0}) = M - {a0} + Y

State before:
case h.right.a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H0 : a ::ₘ M = X + {a0}
H2 : ∀ y ∈ Y, y < a0
hyp : ¬a = a0
⊢ Y + (M - {a0}) = M - {a0} + Y
Tactic:
rw [add_comm]
State after:
no goals

State before:
case h.right.a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H0 : a ::ₘ M = X + {a0}
H2 : ∀ y ∈ Y, y < a0
hyp : ¬a = a0
⊢ M = M - {a0} + {?h.right.a}
Tactic:
change M = M - {a0} + {a0}
State after:
case h.right.a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H0 : a ::ₘ M = X + {a0}
H2 : ∀ y ∈ Y, y < a0
hyp : ¬a = a0
⊢ M = M - {a0} + {a0}

State before:
case h.right.a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H0 : a ::ₘ M = X + {a0}
H2 : ∀ y ∈ Y, y < a0
hyp : ¬a = a0
⊢ M = M - {a0} + {a0}
Tactic:
have this0: M = X + {a0} - {a} := by apply cons_erase ; exact H0
State after:
case h.right.a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H0 : a ::ₘ M = X + {a0}
H2 : ∀ y ∈ Y, y < a0
hyp : ¬a = a0
this0 : M = X + {a0} - {a}
⊢ M = M - {a0} + {a0}

State before:
case h.right.a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H0 : a ::ₘ M = X + {a0}
H2 : ∀ y ∈ Y, y < a0
hyp : ¬a = a0
this0 : M = X + {a0} - {a}
⊢ M = M - {a0} + {a0}
Tactic:
have a0M: a0 ∈ M := by
  apply mul_mem_not_erase
  . change M = Multiset.erase (a0 ::ₘ X) a
    rw [mul_erase_trivial] at this0
    rw [mul_cons_trivial] at this0
    exact this0
  . exact hyp
State after:
case h.right.a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H0 : a ::ₘ M = X + {a0}
H2 : ∀ y ∈ Y, y < a0
hyp : ¬a = a0
this0 : M = X + {a0} - {a}
a0M : a0 ∈ M
⊢ M = M - {a0} + {a0}

State before:
case h.right.a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H0 : a ::ₘ M = X + {a0}
H2 : ∀ y ∈ Y, y < a0
hyp : ¬a = a0
this0 : M = X + {a0} - {a}
a0M : a0 ∈ M
⊢ M = M - {a0} + {a0}
Tactic:
apply mem_erase_cons
State after:
case h.right.a.x
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H0 : a ::ₘ M = X + {a0}
H2 : ∀ y ∈ Y, y < a0
hyp : ¬a = a0
this0 : M = X + {a0} - {a}
a0M : a0 ∈ M
⊢ a0 ∈ M

State before:
case h.right.a.x
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H0 : a ::ₘ M = X + {a0}
H2 : ∀ y ∈ Y, y < a0
hyp : ¬a = a0
this0 : M = X + {a0} - {a}
a0M : a0 ∈ M
⊢ a0 ∈ M
Tactic:
. exact a0M
State after:
no goals

State before:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H0 : a ::ₘ M = X + {a0}
H2 : ∀ y ∈ Y, y < a0
hyp : ¬a = a0
⊢ M = X + {a0} - {a}
Tactic:
apply cons_erase
State after:
case H
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H0 : a ::ₘ M = X + {a0}
H2 : ∀ y ∈ Y, y < a0
hyp : ¬a = a0
⊢ a ::ₘ M = X + {a0}

State before:
case H
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H0 : a ::ₘ M = X + {a0}
H2 : ∀ y ∈ Y, y < a0
hyp : ¬a = a0
⊢ a ::ₘ M = X + {a0}
Tactic:
exact H0
State after:
no goals

State before:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H0 : a ::ₘ M = X + {a0}
H2 : ∀ y ∈ Y, y < a0
hyp : ¬a = a0
this0 : M = X + {a0} - {a}
⊢ a0 ∈ M
Tactic:
apply mul_mem_not_erase
State after:
case H
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H0 : a ::ₘ M = X + {a0}
H2 : ∀ y ∈ Y, y < a0
hyp : ¬a = a0
this0 : M = X + {a0} - {a}
⊢ M = (a0 ::ₘ ?X).erase ?a

case hyp
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H0 : a ::ₘ M = X + {a0}
H2 : ∀ y ∈ Y, y < a0
hyp : ¬a = a0
this0 : M = X + {a0} - {a}
⊢ ¬?a = a0

case a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H0 : a ::ₘ M = X + {a0}
H2 : ∀ y ∈ Y, y < a0
hyp : ¬a = a0
this0 : M = X + {a0} - {a}
⊢ α

case X
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H0 : a ::ₘ M = X + {a0}
H2 : ∀ y ∈ Y, y < a0
hyp : ¬a = a0
this0 : M = X + {a0} - {a}
⊢ Multiset α

State before:
case H
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H0 : a ::ₘ M = X + {a0}
H2 : ∀ y ∈ Y, y < a0
hyp : ¬a = a0
this0 : M = X + {a0} - {a}
⊢ M = (a0 ::ₘ ?X).erase ?a

case hyp
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H0 : a ::ₘ M = X + {a0}
H2 : ∀ y ∈ Y, y < a0
hyp : ¬a = a0
this0 : M = X + {a0} - {a}
⊢ ¬?a = a0

case a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H0 : a ::ₘ M = X + {a0}
H2 : ∀ y ∈ Y, y < a0
hyp : ¬a = a0
this0 : M = X + {a0} - {a}
⊢ α

case X
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H0 : a ::ₘ M = X + {a0}
H2 : ∀ y ∈ Y, y < a0
hyp : ¬a = a0
this0 : M = X + {a0} - {a}
⊢ Multiset α
Tactic:
. change M = Multiset.erase (a0 ::ₘ X) a
  rw [mul_erase_trivial] at this0
  rw [mul_cons_trivial] at this0
  exact this0
State after:
case hyp
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H0 : a ::ₘ M = X + {a0}
H2 : ∀ y ∈ Y, y < a0
hyp : ¬a = a0
this0 : M = X + {a0} - {a}
⊢ ¬a = a0

State before:
case hyp
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H0 : a ::ₘ M = X + {a0}
H2 : ∀ y ∈ Y, y < a0
hyp : ¬a = a0
this0 : M = X + {a0} - {a}
⊢ ¬a = a0
Tactic:
. exact hyp
State after:
no goals

State before:
case H
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H0 : a ::ₘ M = X + {a0}
H2 : ∀ y ∈ Y, y < a0
hyp : ¬a = a0
this0 : M = X + {a0} - {a}
⊢ M = (a0 ::ₘ ?X).erase ?a
Tactic:
change M = Multiset.erase (a0 ::ₘ X) a
State after:
case H
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H0 : a ::ₘ M = X + {a0}
H2 : ∀ y ∈ Y, y < a0
hyp : ¬a = a0
this0 : M = X + {a0} - {a}
⊢ M = (a0 ::ₘ X).erase a

State before:
case H
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H0 : a ::ₘ M = X + {a0}
H2 : ∀ y ∈ Y, y < a0
hyp : ¬a = a0
this0 : M = X + {a0} - {a}
⊢ M = (a0 ::ₘ X).erase a
Tactic:
rw [mul_erase_trivial] at this0
State after:
case H
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H0 : a ::ₘ M = X + {a0}
H2 : ∀ y ∈ Y, y < a0
hyp : ¬a = a0
this0 : M = (X + {a0}).erase a
⊢ M = (a0 ::ₘ X).erase a

State before:
case H
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H0 : a ::ₘ M = X + {a0}
H2 : ∀ y ∈ Y, y < a0
hyp : ¬a = a0
this0 : M = (X + {a0}).erase a
⊢ M = (a0 ::ₘ X).erase a
Tactic:
rw [mul_cons_trivial] at this0
State after:
case H
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H0 : a ::ₘ M = X + {a0}
H2 : ∀ y ∈ Y, y < a0
hyp : ¬a = a0
this0 : M = (a0 ::ₘ X).erase a
⊢ M = (a0 ::ₘ X).erase a

State before:
case H
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H0 : a ::ₘ M = X + {a0}
H2 : ∀ y ∈ Y, y < a0
hyp : ¬a = a0
this0 : M = (a0 ::ₘ X).erase a
⊢ M = (a0 ::ₘ X).erase a
Tactic:
exact this0
State after:
no goals

State before:
case hyp
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H0 : a ::ₘ M = X + {a0}
H2 : ∀ y ∈ Y, y < a0
hyp : ¬a = a0
this0 : M = X + {a0} - {a}
⊢ ¬a = a0
Tactic:
exact hyp
State after:
no goals

State before:
case h.right.a.x
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H0 : a ::ₘ M = X + {a0}
H2 : ∀ y ∈ Y, y < a0
hyp : ¬a = a0
this0 : M = X + {a0} - {a}
a0M : a0 ∈ M
⊢ a0 ∈ M
Tactic:
exact a0M
State after:
no goals