case h
α : Type u_2
β : Type u_1
γ : Type ?u.423906
inst✝ : AddZeroClass β
f g : Multiset α →+ β
h : ∀ (x : α), ↑f {x} = ↑g {x}
s : Multiset α
⊢ ↑f s = ↑g s
α : Type u_2
β : Type u_1
γ : Type ?u.423906
inst✝ : AddZeroClass β
f g : Multiset α →+ β
h : ∀ (x : α), ↑f {x} = ↑g {x}
⊢ f = g
ext s
case h.empty
α : Type u_2
β : Type u_1
γ : Type ?u.423906
inst✝ : AddZeroClass β
f g : Multiset α →+ β
h : ∀ (x : α), ↑f {x} = ↑g {x}
⊢ ↑f 0 = ↑g 0

case h.cons
α : Type u_2
β : Type u_1
γ : Type ?u.423906
inst✝ : AddZeroClass β
f g : Multiset α →+ β
h : ∀ (x : α), ↑f {x} = ↑g {x}
a : α
s : Multiset α
ih : ↑f s = ↑g s
⊢ ↑f (a ::ₘ s) = ↑g (a ::ₘ s)
case h
α : Type u_2
β : Type u_1
γ : Type ?u.423906
inst✝ : AddZeroClass β
f g : Multiset α →+ β
h : ∀ (x : α), ↑f {x} = ↑g {x}
s : Multiset α
⊢ ↑f s = ↑g s
induction' s using Multiset.induction_on with a s ih
no goals
case h.empty
α : Type u_2
β : Type u_1
γ : Type ?u.423906
inst✝ : AddZeroClass β
f g : Multiset α →+ β
h : ∀ (x : α), ↑f {x} = ↑g {x}
⊢ ↑f 0 = ↑g 0
simp only [_root_.map_zero]
no goals
case h.cons
α : Type u_2
β : Type u_1
γ : Type ?u.423906
inst✝ : AddZeroClass β
f g : Multiset α →+ β
h : ∀ (x : α), ↑f {x} = ↑g {x}
a : α
s : Multiset α
ih : ↑f s = ↑g s
⊢ ↑f (a ::ₘ s) = ↑g (a ::ₘ s)
simp only [← singleton_add, _root_.map_add, ih, h]