-- Mathlib/Data/Multiset/MapFold.lean
theorem map_erase_of_mem [DecidableEq α] [DecidableEq β] (f : α → β)
    (s : Multiset α) {x : α} (h : x ∈ s) : (s.erase x).map f = (s.map f).erase (f x)

Proof state:
case cons.inl
α : Type u_1
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
y : α
s : Multiset α
ih : y ∈ s → map f (s.erase y) = (map f s).erase (f y)
h : y ∈ y ::ₘ s
⊢ map f ((y ::ₘ s).erase y) = (map f (y ::ₘ s)).erase (f y)

Tactic:
simp

Result:
no goals

Proof state:
case cons.inr
α : Type u_1
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
x y : α
s : Multiset α
ih : x ∈ s → map f (s.erase x) = (map f s).erase (f x)
hxy : y ≠ x
h : x ∈ s
⊢ map f ((y ::ₘ s).erase x) = (map f (y ::ₘ s)).erase (f x)

Tactic:
rw [s.erase_cons_tail hxy, map_cons, map_cons, ih h, erase_cons_tail_of_mem (mem_map_of_mem f h)]

Result:
no goals

Proof state:
α : Type u_1
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
s : Multiset α
x : α
h : x ∈ s
⊢ map f (s.erase x) = (map f s).erase (f x)

Tactic:
induction' s using Multiset.induction_on with y s ih

Result:
case empty
α : Type u_1
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
x : α
h : x ∈ 0
⊢ map f (erase 0 x) = (map f 0).erase (f x)

case cons
α : Type u_1
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
x y : α
s : Multiset α
ih : x ∈ s → map f (s.erase x) = (map f s).erase (f x)
h : x ∈ y ::ₘ s
⊢ map f ((y ::ₘ s).erase x) = (map f (y ::ₘ s)).erase (f x)

Proof state:
case cons
α : Type u_1
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
x y : α
s : Multiset α
ih : x ∈ s → map f (s.erase x) = (map f s).erase (f x)
h : x ∈ y ::ₘ s
⊢ map f ((y ::ₘ s).erase x) = (map f (y ::ₘ s)).erase (f x)

Tactic:
rcases eq_or_ne y x with rfl | hxy

Result:
case cons.inl
α : Type u_1
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
y : α
s : Multiset α
ih : y ∈ s → map f (s.erase y) = (map f s).erase (f y)
h : y ∈ y ::ₘ s
⊢ map f ((y ::ₘ s).erase y) = (map f (y ::ₘ s)).erase (f y)

case cons.inr
α : Type u_1
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
x y : α
s : Multiset α
ih : x ∈ s → map f (s.erase x) = (map f s).erase (f x)
h : x ∈ y ::ₘ s
hxy : y ≠ x
⊢ map f ((y ::ₘ s).erase x) = (map f (y ::ₘ s)).erase (f x)

Proof state:
case empty
α : Type u_1
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
x : α
h : x ∈ 0
⊢ map f (erase 0 x) = (map f 0).erase (f x)

Tactic:
simp

Result:
no goals

Proof state:
case cons.inr
α : Type u_1
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
x y : α
s : Multiset α
ih : x ∈ s → map f (s.erase x) = (map f s).erase (f x)
h : x ∈ y ::ₘ s
hxy : y ≠ x
⊢ map f ((y ::ₘ s).erase x) = (map f (y ::ₘ s)).erase (f x)

Tactic:
replace h : x ∈ s := by simpa [hxy.symm] using h

Result:
case cons.inr
α : Type u_1
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
x y : α
s : Multiset α
ih : x ∈ s → map f (s.erase x) = (map f s).erase (f x)
hxy : y ≠ x
h : x ∈ s
⊢ map f ((y ::ₘ s).erase x) = (map f (y ::ₘ s)).erase (f x)

Proof state:
α : Type u_1
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
x y : α
s : Multiset α
ih : x ∈ s → map f (s.erase x) = (map f s).erase (f x)
h : x ∈ y ::ₘ s
hxy : y ≠ x
⊢ x ∈ s

Tactic:
simpa [hxy.symm] using h

Result:
no goals