α : 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))
α : 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))
intro t ht
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))

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))
α : 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))
by_cases h : a ∈ s
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))
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))
rw [ndinsert_of_mem h] at ht
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))
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))
subst ht
no goals
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))
rw [eq, map_id, ndinsert_of_mem (mem_attach _ _)]
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))
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))
rw [ndinsert_of_not_mem h] at ht
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))
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))
subst ht
no goals
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))
simp [attach_cons, h]