elaboration of pow

Stream: general

[Bhavik Mehta]

In Data.Nat.Choose.Bounds, the statement of docs#Nat.choose_le_pow is subtly different from the Lean 3 version. In particular, in the Lean 3 version the cast happens before the pow, whereas in Lean 4 the pow happens in Nat, and then is cast to α. (And this isn't just because of a mistake in porting - (n ^ r : α) just elaborates differently). And this change in how the theorem is stated just bit me in porting the exponential ramsey project!

Does the change to pow (https://github.com/leanprover/lean4/pull/2778) affect this? Do we want to turn the statements back into what they used to be?

[Kyle Miller]

I just checked, and the statement will change once the Lean version bump #8366 lands in mathlib, without modification. Here will be the new statement:

Nat.choose_le_pow.{u_1} {α : Type u_1} [inst✝ : LinearOrderedSemifield α] (r n : ℕ) :
    ↑(choose n r) ≤ ↑n ^ r / ↑r !

I got that from hovering over the lemma.

[Bhavik Mehta]

Ah perfect, so back to the Lean 3 version!