Zulip Chat Archive

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*) [ : 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 :=
    induction  using fintype.induction_subsingleton_or_nontrivial with  htα htα₁ htα₂ htα₃,
      cases finset.nonempty.bex (@finset.univ_nonempty  _ _) with a ha,
      rw (fintype.univ_of_subsingleton a),

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