-- Mathlib/Data/Multiset/FinsetOps.lean
theorem attach_ndinsert (a : α) (s : Multiset α) :
    (s.ndinsert a).attach =
      ndinsert ⟨a, mem_ndinsert_self a s⟩ (s.attach.map fun p => ⟨p.1, mem_ndinsert_of_mem p.2⟩) :=
  have eq :
    ∀ h : ∀ p : { x // x ∈ s }, p.1 ∈ s,
      (fun p : { x // x ∈ s } => ⟨p.val, h p⟩ : { x // x ∈ s } → { x // x ∈ s }) = id :=
    fun _ => funext fun _ => Subtype.eq rfl
  have : ∀ (t) (eq : s.ndinsert a = t), t.attach = ndinsert ⟨a, eq ▸ mem_ndinsert_self a s⟩
      (s.attach.map fun p => ⟨p.1, eq ▸ mem_ndinsert_of_mem p.2⟩)

Proof state:
case neg
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
eq : ∀ (h : ∀ (p : { x // x ∈ s }), ↑p ∈ s), (fun p => ⟨↑p, ⋯⟩) = id
h : a ∉ s
ht : ndinsert a s = a ::ₘ s
⊢ (a ::ₘ s).attach = ndinsert ⟨a, ⋯⟩ (map (fun p => ⟨↑p, ⋯⟩) s.attach)

Tactic:
simp [attach_cons, h]

Result:
no goals

Proof state:
case neg
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
eq : ∀ (h : ∀ (p : { x // x ∈ s }), ↑p ∈ s), (fun p => ⟨↑p, ⋯⟩) = id
t : Multiset α
ht✝ : ndinsert a s = t
ht : a ::ₘ s = t
h : a ∉ s
⊢ t.attach = ndinsert ⟨a, ⋯⟩ (map (fun p => ⟨↑p, ⋯⟩) s.attach)

Tactic:
subst ht

Result:
case neg
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
eq : ∀ (h : ∀ (p : { x // x ∈ s }), ↑p ∈ s), (fun p => ⟨↑p, ⋯⟩) = id
h : a ∉ s
ht : ndinsert a s = a ::ₘ s
⊢ (a ::ₘ s).attach = ndinsert ⟨a, ⋯⟩ (map (fun p => ⟨↑p, ⋯⟩) s.attach)

Proof state:
case neg
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
eq : ∀ (h : ∀ (p : { x // x ∈ s }), ↑p ∈ s), (fun p => ⟨↑p, ⋯⟩) = id
t : Multiset α
ht : ndinsert a s = t
h : a ∉ s
⊢ t.attach = ndinsert ⟨a, ⋯⟩ (map (fun p => ⟨↑p, ⋯⟩) s.attach)

Tactic:
rw [ndinsert_of_not_mem h] at ht

Result:
case neg
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
eq : ∀ (h : ∀ (p : { x // x ∈ s }), ↑p ∈ s), (fun p => ⟨↑p, ⋯⟩) = id
t : Multiset α
ht✝ : ndinsert a s = t
ht : a ::ₘ s = t
h : a ∉ s
⊢ t.attach = ndinsert ⟨a, ⋯⟩ (map (fun p => ⟨↑p, ⋯⟩) s.attach)

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
eq : ∀ (h : ∀ (p : { x // x ∈ s }), ↑p ∈ s), (fun p => ⟨↑p, ⋯⟩) = id
⊢ ∀ (t : Multiset α) (eq : ndinsert a s = t), t.attach = ndinsert ⟨a, ⋯⟩ (map (fun p => ⟨↑p, ⋯⟩) s.attach)

Tactic:
intro t ht

Result:
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
eq : ∀ (h : ∀ (p : { x // x ∈ s }), ↑p ∈ s), (fun p => ⟨↑p, ⋯⟩) = id
t : Multiset α
ht : ndinsert a s = t
⊢ t.attach = ndinsert ⟨a, ⋯⟩ (map (fun p => ⟨↑p, ⋯⟩) s.attach)

Proof state:
case pos
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
eq : ∀ (h : ∀ (p : { x // x ∈ s }), ↑p ∈ s), (fun p => ⟨↑p, ⋯⟩) = id
t : Multiset α
ht✝ : ndinsert a s = t
ht : s = t
h : a ∈ s
⊢ t.attach = ndinsert ⟨a, ⋯⟩ (map (fun p => ⟨↑p, ⋯⟩) s.attach)

Tactic:
subst ht

Result:
case pos
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
eq : ∀ (h : ∀ (p : { x // x ∈ s }), ↑p ∈ s), (fun p => ⟨↑p, ⋯⟩) = id
h : a ∈ s
ht : ndinsert a s = s
⊢ s.attach = ndinsert ⟨a, ⋯⟩ (map (fun p => ⟨↑p, ⋯⟩) s.attach)

Proof state:
case pos
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
eq : ∀ (h : ∀ (p : { x // x ∈ s }), ↑p ∈ s), (fun p => ⟨↑p, ⋯⟩) = id
t : Multiset α
ht : ndinsert a s = t
h : a ∈ s
⊢ t.attach = ndinsert ⟨a, ⋯⟩ (map (fun p => ⟨↑p, ⋯⟩) s.attach)

Tactic:
rw [ndinsert_of_mem h] at ht

Result:
case pos
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
eq : ∀ (h : ∀ (p : { x // x ∈ s }), ↑p ∈ s), (fun p => ⟨↑p, ⋯⟩) = id
t : Multiset α
ht✝ : ndinsert a s = t
ht : s = t
h : a ∈ s
⊢ t.attach = ndinsert ⟨a, ⋯⟩ (map (fun p => ⟨↑p, ⋯⟩) s.attach)

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
eq : ∀ (h : ∀ (p : { x // x ∈ s }), ↑p ∈ s), (fun p => ⟨↑p, ⋯⟩) = id
t : Multiset α
ht : ndinsert a s = t
⊢ t.attach = ndinsert ⟨a, ⋯⟩ (map (fun p => ⟨↑p, ⋯⟩) s.attach)

Tactic:
by_cases h : a ∈ s

Result:
case pos
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
eq : ∀ (h : ∀ (p : { x // x ∈ s }), ↑p ∈ s), (fun p => ⟨↑p, ⋯⟩) = id
t : Multiset α
ht : ndinsert a s = t
h : a ∈ s
⊢ t.attach = ndinsert ⟨a, ⋯⟩ (map (fun p => ⟨↑p, ⋯⟩) s.attach)

case neg
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
eq : ∀ (h : ∀ (p : { x // x ∈ s }), ↑p ∈ s), (fun p => ⟨↑p, ⋯⟩) = id
t : Multiset α
ht : ndinsert a s = t
h : a ∉ s
⊢ t.attach = ndinsert ⟨a, ⋯⟩ (map (fun p => ⟨↑p, ⋯⟩) s.attach)

Proof state:
case pos
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
eq : ∀ (h : ∀ (p : { x // x ∈ s }), ↑p ∈ s), (fun p => ⟨↑p, ⋯⟩) = id
h : a ∈ s
ht : ndinsert a s = s
⊢ s.attach = ndinsert ⟨a, ⋯⟩ (map (fun p => ⟨↑p, ⋯⟩) s.attach)

Tactic:
rw [eq, map_id, ndinsert_of_mem (mem_attach _ _)]

Result:
no goals