case refine'_1
α : Type u_1
β : Type u_2
ι : Type ?u.27283
f : α →₀ ℕ
g : α → β
⊢ Multiset.map g (↑toMultiset 0) = ↑toMultiset (mapDomain g 0)

case refine'_2
α : Type u_1
β : Type u_2
ι : Type ?u.27283
f : α →₀ ℕ
g : α → β
⊢ ∀ (a : α) (b : ℕ) (f : α →₀ ℕ),
    ¬a ∈ f.support →
      b ≠ 0 →
        Multiset.map g (↑toMultiset f) = ↑toMultiset (mapDomain g f) →
          Multiset.map g (↑toMultiset (single a b + f)) = ↑toMultiset (mapDomain g (single a b + f))
α : Type u_1
β : Type u_2
ι : Type ?u.27283
f : α →₀ ℕ
g : α → β
⊢ Multiset.map g (↑toMultiset f) = ↑toMultiset (mapDomain g f)
refine' f.induction _ _
no goals
case refine'_1
α : Type u_1
β : Type u_2
ι : Type ?u.27283
f : α →₀ ℕ
g : α → β
⊢ Multiset.map g (↑toMultiset 0) = ↑toMultiset (mapDomain g 0)
rw [toMultiset_zero, Multiset.map_zero, mapDomain_zero, toMultiset_zero]
case refine'_2
α : Type u_1
β : Type u_2
ι : Type ?u.27283
f✝ : α →₀ ℕ
g : α → β
a : α
n : ℕ
f : α →₀ ℕ
a✝¹ : ¬a ∈ f.support
a✝ : n ≠ 0
ih : Multiset.map g (↑toMultiset f) = ↑toMultiset (mapDomain g f)
⊢ Multiset.map g (↑toMultiset (single a n + f)) = ↑toMultiset (mapDomain g (single a n + f))
case refine'_2
α : Type u_1
β : Type u_2
ι : Type ?u.27283
f : α →₀ ℕ
g : α → β
⊢ ∀ (a : α) (b : ℕ) (f : α →₀ ℕ),
    ¬a ∈ f.support →
      b ≠ 0 →
        Multiset.map g (↑toMultiset f) = ↑toMultiset (mapDomain g f) →
          Multiset.map g (↑toMultiset (single a b + f)) = ↑toMultiset (mapDomain g (single a b + f))
intro a n f _ _ ih
case refine'_2
α : Type u_1
β : Type u_2
ι : Type ?u.27283
f✝ : α →₀ ℕ
g : α → β
a : α
n : ℕ
f : α →₀ ℕ
a✝¹ : ¬a ∈ f.support
a✝ : n ≠ 0
ih : Multiset.map g (↑toMultiset f) = ↑toMultiset (mapDomain g f)
⊢ n • ↑(Multiset.mapAddMonoidHom g) {a} + ↑toMultiset (mapDomain g f) = n • {g a} + ↑toMultiset (mapDomain g f)
case refine'_2
α : Type u_1
β : Type u_2
ι : Type ?u.27283
f✝ : α →₀ ℕ
g : α → β
a : α
n : ℕ
f : α →₀ ℕ
a✝¹ : ¬a ∈ f.support
a✝ : n ≠ 0
ih : Multiset.map g (↑toMultiset f) = ↑toMultiset (mapDomain g f)
⊢ Multiset.map g (↑toMultiset (single a n + f)) = ↑toMultiset (mapDomain g (single a n + f))
rw [toMultiset_add, Multiset.map_add, ih, mapDomain_add, mapDomain_single,
  toMultiset_single, toMultiset_add, toMultiset_single, ← Multiset.coe_mapAddMonoidHom,
  (Multiset.mapAddMonoidHom g).map_nsmul]
no goals
case refine'_2
α : Type u_1
β : Type u_2
ι : Type ?u.27283
f✝ : α →₀ ℕ
g : α → β
a : α
n : ℕ
f : α →₀ ℕ
a✝¹ : ¬a ∈ f.support
a✝ : n ≠ 0
ih : Multiset.map g (↑toMultiset f) = ↑toMultiset (mapDomain g f)
⊢ n • ↑(Multiset.mapAddMonoidHom g) {a} + ↑toMultiset (mapDomain g f) = n • {g a} + ↑toMultiset (mapDomain g f)
rfl