How prove things about Exists.choose terms?

Stream: new members

[Scott Carnahan]

I am stuck on the following theorem:

import Mathlib.Data.Nat.Factorial.Basic
import Mathlib.Data.Polynomial.Eval
import Mathlib.RingTheory.Polynomial.Pochhammer

class BinomialSemiring (R: Type _) extends Semiring R where
  /-- Multiplication by factorials is injective -/
  inj_smul_factorial : ∀ (n:ℕ) (r s: R), n.factorial * r = n.factorial * s → r = s
  /-- All Pochhammer evaluations are divisible by the suitable factorials -/
  exist_binomial_coeffs : ∀ (r:R) (n:ℕ), ∃ (x:R), n.factorial * x = Polynomial.eval r (pochhammer R n)

open Classical

noncomputable def multichoose {R:Type _} [BinomialSemiring R] (r:R) : ℕ → R :=
  λ n ↦ (BinomialSemiring.exist_binomial_coeffs r n).choose

theorem factorial_mul_multichoose_eq_pochhammer [BinomialSemiring R] (r:R) (n:ℕ) : n.factorial * multichoose r n = Polynomial.eval r (pochhammer R n) := by
    sorry

If I use unfold multichoose I get the goal ↑(Nat.factorial n) * Exists.choose (_ : ∃ x, ↑(Nat.factorial n) * x = Polynomial.eval r (pochhammer R n)) = Polynomial.eval r (pochhammer R n) and I don't know how to collapse the left side.

[Ruben Van de Velde]

Does docs#Exists.choose_spec help?

[Kevin Buzzard]

theorem factorial_mul_multichoose_eq_pochhammer {R:Type _} [BinomialSemiring R]
    (r:R) (n:ℕ) : n.factorial * multichoose r n = Polynomial.eval r (pochhammer R n) :=
  (BinomialSemiring.exist_binomial_coeffs r n).choose_spec

[Kevin Buzzard]

The only thing you know about the output of Exists.choose is Exists.choose_spec. Even if you proved the exists statement with "let x=37 and now show that this works" Lean forgets that x=37 (because this showed up in a proof).

[Scott Carnahan]

It worked! Thank you very much.

[Junyan Xu]

In mathlib the usual practice would be defining this class with fields

multichoose : R → ℕ → R
factorial_mul_multichoose : ∀ n : ℕ, ∀ r, n.factorial * multichoose r n = (pochhammer R n).eval r

[Scott Carnahan]

@Junyan Xu Should that code go in the part with class BinomialSemiring ?

[Scott Carnahan]

Okay, I see now. That is quite nice, since it gets rid of the non-computable part.

[Eric Wieser]

Junyan Xu said:

In mathlib the usual practice would be defining this class with fields

To elaborate a little more: if there's a _unique_ choice of multichoose, then you'd use the above. If there's no unique choice, then the noncomputable version might still be preferred