Data.Nat.Choose.Multinomial

Stream: mathlib4

[Moritz Firsching]

In port/Data.Nat.Choose.Multinomial , mathlib4#2361, there are a couple of places, where there were instances missing, and @Xavier Roblot pointed out those can be fixed by adding haves with the correct instances, but suggested to check back on zulip if this is the right way to do it. One problem with it, that this leads to lines like this:

      have : IsEmpty (Finset.sym (∅ : Finset α) (succ n)) :=
        Finset.instIsEmptySubtypeMemFinsetInstMembershipFinsetEmptyCollectionInstEmptyCollectionFinset

which go over the 100 character limit. Is just adding those instances the correct thing to do here?

Perhaps related, the last thing missing in the proof is

Multiset.multinomial ↑0 = 1

where this was automatic before, but now cannot be unified for a reason that I don't understand.

[Eric Wieser]

Does turning on etaExperiement cause that instance to be found automatically?

[Moritz Firsching]

If this is done by inserting the line

set_option synthInstance.etaExperiment true in

before the theorem, then no, the instance can still not be found automatically, i.e. when removing the correspondings haves it doesn't work

[Kevin Buzzard]

Another issue with have is that a linter might complain that the have is unused, and if this happens then usually it's fixed by changing to haveI (which means inline have, not instance have, in Lean 4)

[Moritz Firsching]

I fixed the last issue on this one, and it was merged.
However I'm still unsure if adding those instances is the way to go. Porting notes are there in any case.