case refine'_1
α : Type u_1
β : Type ?u.51824
ι : Type ?u.51827
inst✝ : DecidableEq α
f : α →₀ ℕ
⊢ Multiset.toFinset (↑toMultiset 0) = 0.support

case refine'_2
α : Type u_1
β : Type ?u.51824
ι : Type ?u.51827
inst✝ : DecidableEq α
f : α →₀ ℕ
⊢ ∀ (a : α) (b : ℕ) (f : α →₀ ℕ),
    ¬a ∈ f.support →
      b ≠ 0 →
        Multiset.toFinset (↑toMultiset f) = f.support →
          Multiset.toFinset (↑toMultiset (single a b + f)) = (single a b + f).support
α : Type u_1
β : Type ?u.51824
ι : Type ?u.51827
inst✝ : DecidableEq α
f : α →₀ ℕ
⊢ Multiset.toFinset (↑toMultiset f) = f.support
refine' f.induction _ _
no goals
case refine'_1
α : Type u_1
β : Type ?u.51824
ι : Type ?u.51827
inst✝ : DecidableEq α
f : α →₀ ℕ
⊢ Multiset.toFinset (↑toMultiset 0) = 0.support
rw [toMultiset_zero, Multiset.toFinset_zero, support_zero]
case refine'_2
α : Type u_1
β : Type ?u.51824
ι : Type ?u.51827
inst✝ : DecidableEq α
f✝ : α →₀ ℕ
a : α
n : ℕ
f : α →₀ ℕ
ha : ¬a ∈ f.support
hn : n ≠ 0
ih : Multiset.toFinset (↑toMultiset f) = f.support
⊢ Multiset.toFinset (↑toMultiset (single a n + f)) = (single a n + f).support
case refine'_2
α : Type u_1
β : Type ?u.51824
ι : Type ?u.51827
inst✝ : DecidableEq α
f : α →₀ ℕ
⊢ ∀ (a : α) (b : ℕ) (f : α →₀ ℕ),
    ¬a ∈ f.support →
      b ≠ 0 →
        Multiset.toFinset (↑toMultiset f) = f.support →
          Multiset.toFinset (↑toMultiset (single a b + f)) = (single a b + f).support
intro a n f ha hn ih
case refine'_2
α : Type u_1
β : Type ?u.51824
ι : Type ?u.51827
inst✝ : DecidableEq α
f✝ : α →₀ ℕ
a : α
n : ℕ
f : α →₀ ℕ
ha : ¬a ∈ f.support
hn : n ≠ 0
ih : Multiset.toFinset (↑toMultiset f) = f.support
⊢ Disjoint (single a n).support f.support
case refine'_2
α : Type u_1
β : Type ?u.51824
ι : Type ?u.51827
inst✝ : DecidableEq α
f✝ : α →₀ ℕ
a : α
n : ℕ
f : α →₀ ℕ
ha : ¬a ∈ f.support
hn : n ≠ 0
ih : Multiset.toFinset (↑toMultiset f) = f.support
⊢ Multiset.toFinset (↑toMultiset (single a n + f)) = (single a n + f).support
rw [toMultiset_add, Multiset.toFinset_add, ih, toMultiset_single, support_add_eq,
  support_single_ne_zero _ hn, Multiset.toFinset_nsmul _ _ hn, Multiset.toFinset_singleton]
case refine'_2
α : Type u_1
β : Type ?u.51824
ι : Type ?u.51827
inst✝ : DecidableEq α
f✝ : α →₀ ℕ
a : α
n : ℕ
f : α →₀ ℕ
ha : ¬a ∈ f.support
hn : n ≠ 0
ih : Multiset.toFinset (↑toMultiset f) = f.support
⊢ Disjoint {a} f.support
case refine'_2
α : Type u_1
β : Type ?u.51824
ι : Type ?u.51827
inst✝ : DecidableEq α
f✝ : α →₀ ℕ
a : α
n : ℕ
f : α →₀ ℕ
ha : ¬a ∈ f.support
hn : n ≠ 0
ih : Multiset.toFinset (↑toMultiset f) = f.support
⊢ Disjoint (single a n).support f.support
refine' Disjoint.mono_left support_single_subset _
no goals
case refine'_2
α : Type u_1
β : Type ?u.51824
ι : Type ?u.51827
inst✝ : DecidableEq α
f✝ : α →₀ ℕ
a : α
n : ℕ
f : α →₀ ℕ
ha : ¬a ∈ f.support
hn : n ≠ 0
ih : Multiset.toFinset (↑toMultiset f) = f.support
⊢ Disjoint {a} f.support
rwa [Finset.disjoint_singleton_left]