Theorem: mul_mem_not_erase (Pdl/MultisetOrder.lean)

State before:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a a0 : α
M X : Multiset α
H : M = (a0 ::ₘ X).erase a
hyp : ¬a = a0
⊢ a0 ∈ M
Tactic:
rw [H]
State after:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a a0 : α
M X : Multiset α
H : M = (a0 ::ₘ X).erase a
hyp : ¬a = a0
⊢ a0 ∈ (a0 ::ₘ X).erase a

State before:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a a0 : α
M X : Multiset α
H : M = (a0 ::ₘ X).erase a
hyp : ¬a = a0
⊢ a0 ∈ (a0 ::ₘ X).erase a
Tactic:
have : a0 ∈ Multiset.erase (a0 ::ₘ X) a ↔ a0 ∈ (a0 ::ₘ X) := by
  apply Multiset.mem_erase_of_ne
  aesop
State after:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a a0 : α
M X : Multiset α
H : M = (a0 ::ₘ X).erase a
hyp : ¬a = a0
this : a0 ∈ (a0 ::ₘ X).erase a ↔ a0 ∈ a0 ::ₘ X
⊢ a0 ∈ (a0 ::ₘ X).erase a

State before:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a a0 : α
M X : Multiset α
H : M = (a0 ::ₘ X).erase a
hyp : ¬a = a0
this : a0 ∈ (a0 ::ₘ X).erase a ↔ a0 ∈ a0 ::ₘ X
⊢ a0 ∈ (a0 ::ₘ X).erase a
Tactic:
rw [this]
State after:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a a0 : α
M X : Multiset α
H : M = (a0 ::ₘ X).erase a
hyp : ¬a = a0
this : a0 ∈ (a0 ::ₘ X).erase a ↔ a0 ∈ a0 ::ₘ X
⊢ a0 ∈ a0 ::ₘ X

State before:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a a0 : α
M X : Multiset α
H : M = (a0 ::ₘ X).erase a
hyp : ¬a = a0
this : a0 ∈ (a0 ::ₘ X).erase a ↔ a0 ∈ a0 ::ₘ X
⊢ a0 ∈ a0 ::ₘ X
Tactic:
aesop
State after:
no goals

State before:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a a0 : α
M X : Multiset α
H : M = (a0 ::ₘ X).erase a
hyp : ¬a = a0
⊢ a0 ∈ (a0 ::ₘ X).erase a ↔ a0 ∈ a0 ::ₘ X
Tactic:
apply Multiset.mem_erase_of_ne
State after:
case ab
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a a0 : α
M X : Multiset α
H : M = (a0 ::ₘ X).erase a
hyp : ¬a = a0
⊢ a0 ≠ a

State before:
case ab
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a a0 : α
M X : Multiset α
H : M = (a0 ::ₘ X).erase a
hyp : ¬a = a0
⊢ a0 ≠ a
Tactic:
aesop
State after:
no goals