case empty
α : Type u_1
β : Type u_2
γ : Type ?u.127295
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Injective f
x : α
⊢ map f (erase 0 x) = erase (map f 0) (f x)

case cons
α : Type u_1
β : Type u_2
γ : Type ?u.127295
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Injective f
x y : α
s : Multiset α
ih : map f (erase s x) = erase (map f s) (f x)
⊢ map f (erase (y ::ₘ s) x) = erase (map f (y ::ₘ s)) (f x)
α : Type u_1
β : Type u_2
γ : Type ?u.127295
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Injective f
x : α
s : Multiset α
⊢ map f (erase s x) = erase (map f s) (f x)
induction' s using Multiset.induction_on with y s ih
case pos
α : Type u_1
β : Type u_2
γ : Type ?u.127295
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Injective f
x y : α
s : Multiset α
ih : map f (erase s x) = erase (map f s) (f x)
hxy : y = x
⊢ map f (erase (y ::ₘ s) x) = erase (map f (y ::ₘ s)) (f x)

case neg
α : Type u_1
β : Type u_2
γ : Type ?u.127295
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Injective f
x y : α
s : Multiset α
ih : map f (erase s x) = erase (map f s) (f x)
hxy : ¬y = x
⊢ map f (erase (y ::ₘ s) x) = erase (map f (y ::ₘ s)) (f x)
case cons
α : Type u_1
β : Type u_2
γ : Type ?u.127295
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Injective f
x y : α
s : Multiset α
ih : map f (erase s x) = erase (map f s) (f x)
⊢ map f (erase (y ::ₘ s) x) = erase (map f (y ::ₘ s)) (f x)
by_cases hxy : y = x
no goals
case empty
α : Type u_1
β : Type u_2
γ : Type ?u.127295
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Injective f
x : α
⊢ map f (erase 0 x) = erase (map f 0) (f x)
simp
case pos.refl
α : Type u_1
β : Type u_2
γ : Type ?u.127295
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Injective f
x : α
s : Multiset α
ih : map f (erase s x) = erase (map f s) (f x)
⊢ map f (erase (x ::ₘ s) x) = erase (map f (x ::ₘ s)) (f x)
case pos
α : Type u_1
β : Type u_2
γ : Type ?u.127295
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Injective f
x y : α
s : Multiset α
ih : map f (erase s x) = erase (map f s) (f x)
hxy : y = x
⊢ map f (erase (y ::ₘ s) x) = erase (map f (y ::ₘ s)) (f x)
cases hxy
no goals
case pos.refl
α : Type u_1
β : Type u_2
γ : Type ?u.127295
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Injective f
x : α
s : Multiset α
ih : map f (erase s x) = erase (map f s) (f x)
⊢ map f (erase (x ::ₘ s) x) = erase (map f (x ::ₘ s)) (f x)
simp
no goals
case neg
α : Type u_1
β : Type u_2
γ : Type ?u.127295
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Injective f
x y : α
s : Multiset α
ih : map f (erase s x) = erase (map f s) (f x)
hxy : ¬y = x
⊢ map f (erase (y ::ₘ s) x) = erase (map f (y ::ₘ s)) (f x)
rw [s.erase_cons_tail hxy, map_cons, map_cons, (s.map f).erase_cons_tail (hf.ne hxy), ih]