Rewrite failed

Stream: new members

[Pim Otte]

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]

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.