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

case mpr
α : Type u_1
β : Type u_2
γ : Type ?u.122604
inst✝ : DecidableEq α
f : α → β
s : Multiset α
t : Multiset β
b : β
⊢ map f s = b ::ₘ t → ∃ a, a ∈ s ∧ f a = b ∧ map f (erase s a) = t
α : Type u_1
β : Type u_2
γ : Type ?u.122604
inst✝ : DecidableEq α
f : α → β
s : Multiset α
t : Multiset β
b : β
⊢ (∃ a, a ∈ s ∧ f a = b ∧ map f (erase s a) = t) ↔ map f s = b ::ₘ t
constructor
case mp.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.122604
inst✝ : DecidableEq α
f : α → β
s : Multiset α
a : α
ha : a ∈ s
⊢ map f s = f a ::ₘ map f (erase s a)
case mp
α : Type u_1
β : Type u_2
γ : Type ?u.122604
inst✝ : DecidableEq α
f : α → β
s : Multiset α
t : Multiset β
b : β
⊢ (∃ a, a ∈ s ∧ f a = b ∧ map f (erase s a) = t) → map f s = b ::ₘ t
rintro ⟨a, ha, rfl, rfl⟩
no goals
case mp.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.122604
inst✝ : DecidableEq α
f : α → β
s : Multiset α
a : α
ha : a ∈ s
⊢ map f s = f a ::ₘ map f (erase s a)
rw [← map_cons, Multiset.cons_erase ha]
case mpr
α : Type u_1
β : Type u_2
γ : Type ?u.122604
inst✝ : DecidableEq α
f : α → β
s : Multiset α
t : Multiset β
b : β
h : map f s = b ::ₘ t
⊢ ∃ a, a ∈ s ∧ f a = b ∧ map f (erase s a) = t
case mpr
α : Type u_1
β : Type u_2
γ : Type ?u.122604
inst✝ : DecidableEq α
f : α → β
s : Multiset α
t : Multiset β
b : β
⊢ map f s = b ::ₘ t → ∃ a, a ∈ s ∧ f a = b ∧ map f (erase s a) = t
intro h
case mpr
α : Type u_1
β : Type u_2
γ : Type ?u.122604
inst✝ : DecidableEq α
f : α → β
s : Multiset α
t : Multiset β
b : β
h : map f s = b ::ₘ t
this : b ∈ map f s
⊢ ∃ a, a ∈ s ∧ f a = b ∧ map f (erase s a) = t
case mpr
α : Type u_1
β : Type u_2
γ : Type ?u.122604
inst✝ : DecidableEq α
f : α → β
s : Multiset α
t : Multiset β
b : β
h : map f s = b ::ₘ t
⊢ ∃ a, a ∈ s ∧ f a = b ∧ map f (erase s a) = t
have : b ∈ s.map f := by
  rw [h]
  exact mem_cons_self _ _
case mpr.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.122604
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, a_1 ∈ s ∧ f a_1 = f a ∧ map f (erase s a_1) = t
case mpr
α : Type u_1
β : Type u_2
γ : Type ?u.122604
inst✝ : DecidableEq α
f : α → β
s : Multiset α
t : Multiset β
b : β
h : map f s = b ::ₘ t
this : b ∈ map f s
⊢ ∃ a, a ∈ s ∧ f a = b ∧ map f (erase s a) = t
obtain ⟨a, h1, rfl⟩ := mem_map.mp this
case mpr.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.122604
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_1 ∈ a ::ₘ u ∧ f a_1 = f a ∧ map f (erase (a ::ₘ u) a_1) = t
case mpr.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.122604
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, a_1 ∈ s ∧ f a_1 = f a ∧ map f (erase s a_1) = t
obtain ⟨u, rfl⟩ := exists_cons_of_mem h1
case mpr.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.122604
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_1 ∈ a ::ₘ u ∧ f a_1 = f a ∧ map f (erase (a ::ₘ u) a_1) = t
case mpr.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.122604
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_1 ∈ a ::ₘ u ∧ f a_1 = f a ∧ map f (erase (a ::ₘ u) a_1) = t
rw [map_cons, cons_inj_right] at h
case mpr.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.122604
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 (erase (a ::ₘ u) a) = t
case mpr.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.122604
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_1 ∈ a ::ₘ u ∧ f a_1 = f a ∧ map f (erase (a ::ₘ u) a_1) = t
refine' ⟨a, mem_cons_self _ _, rfl, _⟩
no goals
case mpr.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.122604
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 (erase (a ::ₘ u) a) = t
rw [Multiset.erase_cons_head, h]
α : Type u_1
β : Type u_2
γ : Type ?u.122604
inst✝ : DecidableEq α
f : α → β
s : Multiset α
t : Multiset β
b : β
h : map f s = b ::ₘ t
⊢ b ∈ b ::ₘ t
α : Type u_1
β : Type u_2
γ : Type ?u.122604
inst✝ : DecidableEq α
f : α → β
s : Multiset α
t : Multiset β
b : β
h : map f s = b ::ₘ t
⊢ b ∈ map f s
rw [h]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.122604
inst✝ : DecidableEq α
f : α → β
s : Multiset α
t : Multiset β
b : β
h : map f s = b ::ₘ t
⊢ b ∈ b ::ₘ t
exact mem_cons_self _ _