[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s : Multiset α
h : a ∈ s
⊢ ↑card (ndinsert a s) = ↑card s
[PROOFSTEP]
simp [h]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s : Multiset α
h : ¬a ∈ s
⊢ ↑card (ndinsert a s) = ↑card s + 1
[PROOFSTEP]
simp [h]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s : Multiset α
⊢ dedup (a ::ₘ s) = ndinsert a (dedup s)
[PROOFSTEP]
by_cases h : a ∈ s
[GOAL]
case pos
α : Type u_1
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s : Multiset α
h : a ∈ s
⊢ dedup (a ::ₘ s) = ndinsert a (dedup s)
[PROOFSTEP]
simp [h]
[GOAL]
case neg
α : Type u_1
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s : Multiset α
h : ¬a ∈ s
⊢ dedup (a ::ₘ s) = ndinsert a (dedup s)
[PROOFSTEP]
simp [h]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s t : Multiset α
x✝ : s ≤ t ∧ a ∈ t
l : s ≤ t
m : a ∈ t
h : a ∈ s
⊢ ndinsert a s ≤ t
[PROOFSTEP]
simp [h, l]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s t : Multiset α
x✝ : s ≤ t ∧ a ∈ t
l : s ≤ t
m : a ∈ t
h : ¬a ∈ s
⊢ ndinsert a s ≤ t
[PROOFSTEP]
rw [ndinsert_of_not_mem h, ← cons_erase m, cons_le_cons_iff, ← le_cons_of_not_mem h, cons_erase m]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s t : Multiset α
x✝ : s ≤ t ∧ a ∈ t
l : s ≤ t
m : a ∈ t
h : ¬a ∈ s
⊢ s ≤ t
[PROOFSTEP]
exact l
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s : Multiset α
eq : ∀ (h : ∀ (p : { x // x ∈ s }), ↑p ∈ s), (fun p => { val := ↑p, property := (_ : ↑p ∈ s) }) = id
⊢ ∀ (t : Multiset α) (eq : ndinsert a s = t),
    attach t =
      ndinsert { val := a, property := (_ : a ∈ t) } (map (fun p => { val := ↑p, property := (_ : ↑p ∈ t) }) (attach s))
[PROOFSTEP]
intro t ht
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s : Multiset α
eq : ∀ (h : ∀ (p : { x // x ∈ s }), ↑p ∈ s), (fun p => { val := ↑p, property := (_ : ↑p ∈ s) }) = id
t : Multiset α
ht : ndinsert a s = t
⊢ attach t =
    ndinsert { val := a, property := (_ : a ∈ t) } (map (fun p => { val := ↑p, property := (_ : ↑p ∈ t) }) (attach s))
[PROOFSTEP]
by_cases h : a ∈ s
[GOAL]
case pos
α : Type u_1
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s : Multiset α
eq : ∀ (h : ∀ (p : { x // x ∈ s }), ↑p ∈ s), (fun p => { val := ↑p, property := (_ : ↑p ∈ s) }) = id
t : Multiset α
ht : ndinsert a s = t
h : a ∈ s
⊢ attach t =
    ndinsert { val := a, property := (_ : a ∈ t) } (map (fun p => { val := ↑p, property := (_ : ↑p ∈ t) }) (attach s))
[PROOFSTEP]
rw [ndinsert_of_mem h] at ht 
[GOAL]
case pos
α : Type u_1
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s : Multiset α
eq : ∀ (h : ∀ (p : { x // x ∈ s }), ↑p ∈ s), (fun p => { val := ↑p, property := (_ : ↑p ∈ s) }) = id
t : Multiset α
ht✝ : ndinsert a s = t
ht : s = t
h : a ∈ s
⊢ attach t =
    ndinsert { val := a, property := (_ : a ∈ t) } (map (fun p => { val := ↑p, property := (_ : ↑p ∈ t) }) (attach s))
[PROOFSTEP]
subst ht
[GOAL]
case pos
α : Type u_1
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s : Multiset α
eq : ∀ (h : ∀ (p : { x // x ∈ s }), ↑p ∈ s), (fun p => { val := ↑p, property := (_ : ↑p ∈ s) }) = id
h : a ∈ s
ht : ndinsert a s = s
⊢ attach s =
    ndinsert { val := a, property := (_ : a ∈ s) } (map (fun p => { val := ↑p, property := (_ : ↑p ∈ s) }) (attach s))
[PROOFSTEP]
rw [eq, map_id, ndinsert_of_mem (mem_attach _ _)]
[GOAL]
case neg
α : Type u_1
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s : Multiset α
eq : ∀ (h : ∀ (p : { x // x ∈ s }), ↑p ∈ s), (fun p => { val := ↑p, property := (_ : ↑p ∈ s) }) = id
t : Multiset α
ht : ndinsert a s = t
h : ¬a ∈ s
⊢ attach t =
    ndinsert { val := a, property := (_ : a ∈ t) } (map (fun p => { val := ↑p, property := (_ : ↑p ∈ t) }) (attach s))
[PROOFSTEP]
rw [ndinsert_of_not_mem h] at ht 
[GOAL]
case neg
α : Type u_1
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s : Multiset α
eq : ∀ (h : ∀ (p : { x // x ∈ s }), ↑p ∈ s), (fun p => { val := ↑p, property := (_ : ↑p ∈ s) }) = id
t : Multiset α
ht✝ : ndinsert a s = t
ht : a ::ₘ s = t
h : ¬a ∈ s
⊢ attach t =
    ndinsert { val := a, property := (_ : a ∈ t) } (map (fun p => { val := ↑p, property := (_ : ↑p ∈ t) }) (attach s))
[PROOFSTEP]
subst ht
[GOAL]
case neg
α : Type u_1
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s : Multiset α
eq : ∀ (h : ∀ (p : { x // x ∈ s }), ↑p ∈ s), (fun p => { val := ↑p, property := (_ : ↑p ∈ s) }) = id
h : ¬a ∈ s
ht : ndinsert a s = a ::ₘ s
⊢ attach (a ::ₘ s) =
    ndinsert { val := a, property := (_ : a ∈ a ::ₘ s) }
      (map (fun p => { val := ↑p, property := (_ : ↑p ∈ a ::ₘ s) }) (attach s))
[PROOFSTEP]
simp [attach_cons, h]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s t : Multiset α
⊢ Disjoint (ndinsert a s) t ↔ Disjoint (a ::ₘ s) t
[PROOFSTEP]
simp [Disjoint]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s t : Multiset α
⊢ Disjoint s (ndinsert a t) ↔ ¬a ∈ s ∧ Disjoint s t
[PROOFSTEP]
rw [disjoint_comm, disjoint_ndinsert_left]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s t : Multiset α
⊢ ¬a ∈ s ∧ Disjoint t s ↔ ¬a ∈ s ∧ Disjoint s t
[PROOFSTEP]
tauto
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s✝ s t u : Multiset α
⊢ ndunion 0 t ≤ u ↔ 0 ⊆ u ∧ t ≤ u
[PROOFSTEP]
simp [zero_ndunion]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s✝ s t u : Multiset α
x✝¹ : α
x✝ : Multiset α
h : ndunion x✝ t ≤ u ↔ x✝ ⊆ u ∧ t ≤ u
⊢ ndunion (x✝¹ ::ₘ x✝) t ≤ u ↔ x✝¹ ::ₘ x✝ ⊆ u ∧ t ≤ u
[PROOFSTEP]
simp only [cons_ndunion, mem_ndunion, ndinsert_le, and_comm, cons_subset, and_left_comm, h, and_assoc]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s t : Multiset α
h : a ∈ t
⊢ ndinter (a ::ₘ s) t = a ::ₘ ndinter s t
[PROOFSTEP]
simp [ndinter, h]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s✝ : Multiset α
a : α
s t : Multiset α
h : ¬a ∈ t
⊢ ndinter (a ::ₘ s) t = ndinter s t
[PROOFSTEP]
simp [ndinter, h]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s✝ s t : Multiset α
a : α
⊢ a ∈ ndinter s t ↔ a ∈ s ∧ a ∈ t
[PROOFSTEP]
simp [ndinter, mem_filter]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s✝ s t u : Multiset α
⊢ s ≤ ndinter t u ↔ s ≤ t ∧ s ⊆ u
[PROOFSTEP]
simp [ndinter, le_filter, subset_iff]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s✝ s t : Multiset α
⊢ ndinter s t = 0 ↔ Disjoint s t
[PROOFSTEP]
rw [← subset_zero]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s✝ s t : Multiset α
⊢ ndinter s t ⊆ 0 ↔ Disjoint s t
[PROOFSTEP]
simp [subset_iff, Disjoint]
