Theorem: mem_leq_diff (Pdl/MultisetOrder.lean)

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Preorder α
⊢ ∀ (M N : Multiset α), N ≤ M → M = M - N + N
Tactic:
intros M N h
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Preorder α
M N : Multiset α
h : N ≤ M
⊢ M = M - N + N

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Preorder α
M N : Multiset α
h : N ≤ M
⊢ M = M - N + N
Tactic:
rw [← Multiset.union_def]
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Preorder α
M N : Multiset α
h : N ≤ M
⊢ M = M ∪ N

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Preorder α
M N : Multiset α
h : N ≤ M
⊢ M = M ∪ N
Tactic:
rw [Multiset.eq_union_left]
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Preorder α
M N : Multiset α
h : N ≤ M
⊢ N ≤ M

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Preorder α
M N : Multiset α
h : N ≤ M
⊢ N ≤ M
Tactic:
exact h
State after:
no goals