## Stream: new members

### Topic: Rewrite failed

#### Pim Otte (Aug 14 2022 at 14:42):

In the below sample, I've deduced that finset.univ = {a} (off the type t\alpha). However, the rewrite failed and I have no clue why. They should both be finset.univ of t\alpha, as far as I can see with the widget, and I don't know what else it could be. In addition, the whole usage of unfreezing and the induction tactic is based on other usage in mathlib, but I don't really understand what I've done there, so it could be wrong :sweat_smile: Any pointers?

import data.finsupp.basic

open nat

open_locale big_operators

noncomputable theory

def multinomial {α : Type*} [fintype α] [has_le α] : (ℕ) → (α → ℕ) → ℕ :=  λ n, (λ (k : α → ℕ), (factorial n)*∏ i, choose (∑ j in {j' ∈ fintype.elems α | j' ≤ i}, (k j)) (k i))

def multinomial_theorem (α : Type*) [hα : fintype α] [hα₁ : decidable_eq α] [hα₂ : has_le α] [hα₃ : nonempty α] {R : Type*} [comm_ring R] (x: α →₀ R) (n : ℕ) :
(∑ i, x i)^n = ∑ k : α → (fin (n+1)), ite ((∑ i, k i) = n) ((multinomial n (λ i, ((k i) : ℕ)))*(∏ i, (x i)^(((k i) : ℕ)))) 0 :=
begin
unfreezingI
{
induction hα using fintype.induction_subsingleton_or_nontrivial with tα htα htα₁ htα₂ htα₃,
},
{
simp,
cases finset.nonempty.bex (@finset.univ_nonempty tα _ _) with a ha,
rw (fintype.univ_of_subsingleton a),
}
end


#### Junyan Xu (Aug 14 2022 at 16:24):

I think the problem here is probably that the fintype instance in fintype.univ_of_subsingleton (that comes from the subsingleton instance htα₁) is not defeq to the fintype instance htα in finset.univ in your goal. I think in order to apply induction more easily, you may want to generalize your definition to use an arbitrary finset instead of only finset.univ of a fintype. However, there are other problems in your definition, which I'll detail in the multinomial topic.

Last updated: Dec 20 2023 at 11:08 UTC