-- Mathlib/Data/Multiset/MapFold.lean
theorem map_eq_cons [DecidableEq α] (f : α → β) (s : Multiset α) (t : Multiset β) (b : β) :
    (∃ a ∈ s, f a = b ∧ (s.erase a).map f = t) ↔ s.map f = b ::ₘ t

Proof state:
case mp
α : Type u_1
β : Type v
inst✝ : DecidableEq α
f : α → β
s : Multiset α
t : Multiset β
b : β
⊢ (∃ a ∈ s, f a = b ∧ map f (s.erase a) = t) → map f s = b ::ₘ t

Tactic:
rintro ⟨a, ha, rfl, rfl⟩

Result:
case mp.intro.intro.intro
α : Type u_1
β : Type v
inst✝ : DecidableEq α
f : α → β
s : Multiset α
a : α
ha : a ∈ s
⊢ map f s = f a ::ₘ map f (s.erase a)

Proof state:
case mpr.intro.intro.intro
α : Type u_1
β : Type v
inst✝ : DecidableEq α
f : α → β
t : Multiset β
a : α
u : Multiset α
h1 : a ∈ a ::ₘ u
h : map f u = t
this : f a ∈ map f (a ::ₘ u)
⊢ map f ((a ::ₘ u).erase a) = t

Tactic:
rw [Multiset.erase_cons_head, h]

Result:
no goals

Proof state:
α : Type u_1
β : Type v
inst✝ : DecidableEq α
f : α → β
s : Multiset α
t : Multiset β
b : β
⊢ (∃ a ∈ s, f a = b ∧ map f (s.erase a) = t) ↔ map f s = b ::ₘ t

Tactic:
constructor

Result:
case mp
α : Type u_1
β : Type v
inst✝ : DecidableEq α
f : α → β
s : Multiset α
t : Multiset β
b : β
⊢ (∃ a ∈ s, f a = b ∧ map f (s.erase a) = t) → map f s = b ::ₘ t

case mpr
α : Type u_1
β : Type v
inst✝ : DecidableEq α
f : α → β
s : Multiset α
t : Multiset β
b : β
⊢ map f s = b ::ₘ t → ∃ a ∈ s, f a = b ∧ map f (s.erase a) = t

Proof state:
case mpr.intro.intro.intro
α : Type u_1
β : Type v
inst✝ : DecidableEq α
f : α → β
t : Multiset β
a : α
u : Multiset α
h1 : a ∈ a ::ₘ u
h : map f u = t
this : f a ∈ map f (a ::ₘ u)
⊢ ∃ a_1 ∈ a ::ₘ u, f a_1 = f a ∧ map f ((a ::ₘ u).erase a_1) = t

Tactic:
refine ⟨a, mem_cons_self _ _, rfl, ?_⟩

Result:
case mpr.intro.intro.intro
α : Type u_1
β : Type v
inst✝ : DecidableEq α
f : α → β
t : Multiset β
a : α
u : Multiset α
h1 : a ∈ a ::ₘ u
h : map f u = t
this : f a ∈ map f (a ::ₘ u)
⊢ map f ((a ::ₘ u).erase a) = t

Proof state:
case mpr.intro.intro.intro
α : Type u_1
β : Type v
inst✝ : DecidableEq α
f : α → β
t : Multiset β
a : α
u : Multiset α
h1 : a ∈ a ::ₘ u
h : map f (a ::ₘ u) = f a ::ₘ t
this : f a ∈ map f (a ::ₘ u)
⊢ ∃ a_1 ∈ a ::ₘ u, f a_1 = f a ∧ map f ((a ::ₘ u).erase a_1) = t

Tactic:
rw [map_cons, cons_inj_right] at h

Result:
case mpr.intro.intro.intro
α : Type u_1
β : Type v
inst✝ : DecidableEq α
f : α → β
t : Multiset β
a : α
u : Multiset α
h1 : a ∈ a ::ₘ u
h : map f u = t
this : f a ∈ map f (a ::ₘ u)
⊢ ∃ a_1 ∈ a ::ₘ u, f a_1 = f a ∧ map f ((a ::ₘ u).erase a_1) = t

Proof state:
α : Type u_1
β : Type v
inst✝ : DecidableEq α
f : α → β
s : Multiset α
t : Multiset β
b : β
h : map f s = b ::ₘ t
⊢ b ∈ map f s

Tactic:
rw [h]

Result:
α : Type u_1
β : Type v
inst✝ : DecidableEq α
f : α → β
s : Multiset α
t : Multiset β
b : β
h : map f s = b ::ₘ t
⊢ b ∈ b ::ₘ t

Proof state:
case mpr
α : Type u_1
β : Type v
inst✝ : DecidableEq α
f : α → β
s : Multiset α
t : Multiset β
b : β
h : map f s = b ::ₘ t
this : b ∈ map f s
⊢ ∃ a ∈ s, f a = b ∧ map f (s.erase a) = t

Tactic:
obtain ⟨a, h1, rfl⟩ := mem_map.mp this

Result:
case mpr.intro.intro
α : Type u_1
β : Type v
inst✝ : DecidableEq α
f : α → β
s : Multiset α
t : Multiset β
a : α
h1 : a ∈ s
h : map f s = f a ::ₘ t
this : f a ∈ map f s
⊢ ∃ a_1 ∈ s, f a_1 = f a ∧ map f (s.erase a_1) = t

Proof state:
case mpr
α : Type u_1
β : Type v
inst✝ : DecidableEq α
f : α → β
s : Multiset α
t : Multiset β
b : β
h : map f s = b ::ₘ t
⊢ ∃ a ∈ s, f a = b ∧ map f (s.erase a) = t

Tactic:
have : b ∈ s.map f := by
  rw [h]
  exact mem_cons_self _ _

Result:
case mpr
α : Type u_1
β : Type v
inst✝ : DecidableEq α
f : α → β
s : Multiset α
t : Multiset β
b : β
h : map f s = b ::ₘ t
this : b ∈ map f s
⊢ ∃ a ∈ s, f a = b ∧ map f (s.erase a) = t

Proof state:
case mpr.intro.intro
α : Type u_1
β : Type v
inst✝ : DecidableEq α
f : α → β
s : Multiset α
t : Multiset β
a : α
h1 : a ∈ s
h : map f s = f a ::ₘ t
this : f a ∈ map f s
⊢ ∃ a_1 ∈ s, f a_1 = f a ∧ map f (s.erase a_1) = t

Tactic:
obtain ⟨u, rfl⟩ := exists_cons_of_mem h1

Result:
case mpr.intro.intro.intro
α : Type u_1
β : Type v
inst✝ : DecidableEq α
f : α → β
t : Multiset β
a : α
u : Multiset α
h1 : a ∈ a ::ₘ u
h : map f (a ::ₘ u) = f a ::ₘ t
this : f a ∈ map f (a ::ₘ u)
⊢ ∃ a_1 ∈ a ::ₘ u, f a_1 = f a ∧ map f ((a ::ₘ u).erase a_1) = t

Proof state:
case mpr
α : Type u_1
β : Type v
inst✝ : DecidableEq α
f : α → β
s : Multiset α
t : Multiset β
b : β
⊢ map f s = b ::ₘ t → ∃ a ∈ s, f a = b ∧ map f (s.erase a) = t

Tactic:
intro h

Result:
case mpr
α : Type u_1
β : Type v
inst✝ : DecidableEq α
f : α → β
s : Multiset α
t : Multiset β
b : β
h : map f s = b ::ₘ t
⊢ ∃ a ∈ s, f a = b ∧ map f (s.erase a) = t

Proof state:
case mp.intro.intro.intro
α : Type u_1
β : Type v
inst✝ : DecidableEq α
f : α → β
s : Multiset α
a : α
ha : a ∈ s
⊢ map f s = f a ::ₘ map f (s.erase a)

Tactic:
rw [← map_cons, Multiset.cons_erase ha]

Result:
no goals

Proof state:
α : Type u_1
β : Type v
inst✝ : DecidableEq α
f : α → β
s : Multiset α
t : Multiset β
b : β
h : map f s = b ::ₘ t
⊢ b ∈ b ::ₘ t

Tactic:
exact mem_cons_self _ _

Result:
no goals