case refine'_1
α : Type u_1
β : Type ?u.29111
ι : Type ?u.29114
inst✝ : CommMonoid α
f : α →₀ ℕ
⊢ Multiset.prod (↑toMultiset 0) = prod 0 fun a n => a ^ n

case refine'_2
α : Type u_1
β : Type ?u.29111
ι : Type ?u.29114
inst✝ : CommMonoid α
f : α →₀ ℕ
⊢ ∀ (a : α) (b : ℕ) (f : α →₀ ℕ),
    ¬a ∈ f.support →
      b ≠ 0 →
        (Multiset.prod (↑toMultiset f) = prod f fun a n => a ^ n) →
          Multiset.prod (↑toMultiset (single a b + f)) = prod (single a b + f) fun a n => a ^ n
α : Type u_1
β : Type ?u.29111
ι : Type ?u.29114
inst✝ : CommMonoid α
f : α →₀ ℕ
⊢ Multiset.prod (↑toMultiset f) = prod f fun a n => a ^ n
refine' f.induction _ _
no goals
case refine'_1
α : Type u_1
β : Type ?u.29111
ι : Type ?u.29114
inst✝ : CommMonoid α
f : α →₀ ℕ
⊢ Multiset.prod (↑toMultiset 0) = prod 0 fun a n => a ^ n
rw [toMultiset_zero, Multiset.prod_zero, Finsupp.prod_zero_index]
case refine'_2
α : Type u_1
β : Type ?u.29111
ι : Type ?u.29114
inst✝ : CommMonoid α
f✝ : α →₀ ℕ
a : α
n : ℕ
f : α →₀ ℕ
a✝¹ : ¬a ∈ f.support
a✝ : n ≠ 0
ih : Multiset.prod (↑toMultiset f) = prod f fun a n => a ^ n
⊢ Multiset.prod (↑toMultiset (single a n + f)) = prod (single a n + f) fun a n => a ^ n
case refine'_2
α : Type u_1
β : Type ?u.29111
ι : Type ?u.29114
inst✝ : CommMonoid α
f : α →₀ ℕ
⊢ ∀ (a : α) (b : ℕ) (f : α →₀ ℕ),
    ¬a ∈ f.support →
      b ≠ 0 →
        (Multiset.prod (↑toMultiset f) = prod f fun a n => a ^ n) →
          Multiset.prod (↑toMultiset (single a b + f)) = prod (single a b + f) fun a n => a ^ n
intro a n f _ _ ih
case refine'_2
α : Type u_1
β : Type ?u.29111
ι : Type ?u.29114
inst✝ : CommMonoid α
f✝ : α →₀ ℕ
a : α
n : ℕ
f : α →₀ ℕ
a✝¹ : ¬a ∈ f.support
a✝ : n ≠ 0
ih : Multiset.prod (↑toMultiset f) = prod f fun a n => a ^ n
⊢ a ^ 0 = 1
case refine'_2
α : Type u_1
β : Type ?u.29111
ι : Type ?u.29114
inst✝ : CommMonoid α
f✝ : α →₀ ℕ
a : α
n : ℕ
f : α →₀ ℕ
a✝¹ : ¬a ∈ f.support
a✝ : n ≠ 0
ih : Multiset.prod (↑toMultiset f) = prod f fun a n => a ^ n
⊢ Multiset.prod (↑toMultiset (single a n + f)) = prod (single a n + f) fun a n => a ^ n
rw [toMultiset_add, Multiset.prod_add, ih, toMultiset_single, Multiset.prod_nsmul,
  Finsupp.prod_add_index' pow_zero pow_add, Finsupp.prod_single_index, Multiset.prod_singleton]
no goals
case refine'_2
α : Type u_1
β : Type ?u.29111
ι : Type ?u.29114
inst✝ : CommMonoid α
f✝ : α →₀ ℕ
a : α
n : ℕ
f : α →₀ ℕ
a✝¹ : ¬a ∈ f.support
a✝ : n ≠ 0
ih : Multiset.prod (↑toMultiset f) = prod f fun a n => a ^ n
⊢ a ^ 0 = 1
exact pow_zero a