α : Type u_1
β : Type u_2
γ : Type ?u.111985
f g : α → β
s : Multiset α
h : ∀ (x : α), x ∈ s → f x = g x
⊢ map f s = map g s
α : Type u_1
β : Type u_2
γ : Type ?u.111985
f g : α → β
s t : Multiset α
⊢ s = t → (∀ (x : α), x ∈ t → f x = g x) → map f s = map g t
rintro rfl h
case h
α : Type u_1
β : Type u_2
γ : Type ?u.111985
f g : α → β
a✝ : List α
h : ∀ (x : α), x ∈ Quot.mk Setoid.r a✝ → f x = g x
⊢ map f (Quot.mk Setoid.r a✝) = map g (Quot.mk Setoid.r a✝)
α : Type u_1
β : Type u_2
γ : Type ?u.111985
f g : α → β
s : Multiset α
h : ∀ (x : α), x ∈ s → f x = g x
⊢ map f s = map g s
induction s using Quot.inductionOn
no goals
case h
α : Type u_1
β : Type u_2
γ : Type ?u.111985
f g : α → β
a✝ : List α
h : ∀ (x : α), x ∈ Quot.mk Setoid.r a✝ → f x = g x
⊢ map f (Quot.mk Setoid.r a✝) = map g (Quot.mk Setoid.r a✝)
exact congr_arg _ (List.map_congr h)