Finset / Multiset / Set issue

Stream: mathlib4

[John Talbot]

Could anyone give some advice about why the following proof fails?

import Mathlib.Data.Finset.Basic

variable {α : Type*} {a : α}

def null (f : Set α → ℕ) (s : Set α) [NeZero (f s)] : ℕ := 0

lemma null_set (f : Set α → ℕ) (s : Set α) (_h : a ∈ s) [NeZero (f s)] :
    null f s = 0 := rfl

lemma null_finset (f : Set α → ℕ) (s : Finset α) (h : a ∈ s) [NeZero (f s)] :
    null f s = 0 := by
  exact null_set f _ h  -- failed to synthesize NeZero (f (Membership.mem s.val))
-- exact null_set f s h            -- Goals accomplished!
-- exact null_set f _ (by exact h) -- Goals accomplished!
-- exact @null_set _ _ _ _ h ‹_›   -- Goals accomplished!
-- rfl                             -- Goals accomplished!

[John Talbot]

Sorry posted prematurely!
In particular how do we arrive at the Membership.mem s.val in the typeclass resolution?

[Riccardo Brasca]

Because Lean has no way of guessing what you mean by _. This is because s is a Finset, not a Set.

[Riccardo Brasca]

In particular, it cannot guess it from h, since h is not of type "a belongs to a set"

[Riccardo Brasca]

OK, maybe not exactly this, but the issue due to s : Finset α

[John Talbot]

Thanks! But I don't see a coercion from Finset to Multiset so I was surprised to see s.val appear?

[Riccardo Brasca]

To understand that you have to look at the trace

[Riccardo Brasca]

Give my 10 minutes

[John Talbot]

Thanks!

[Aaron Liu]

docs#Finset.instCoeTCSet

[Aaron Liu]

wait you were looking for the multiset

[John Talbot]

No - I was just naively expecting the Finset to be coerced to a Set

[Aaron Liu]

The reason s.val appears is because it's unfolding the membership instance
docs#Finset.instMembership

[John Talbot]

So it looks for a Set α and finds Membership.mem s.val?

[Aaron Liu]

I think so

[Riccardo Brasca]

The underscore in null_set f _ h means "Lean, please figure out what the _ is looking at the other variables". Lean knows that the underscore has type Set α and looks at h to guess it. Since h hasn't type x ∈ X for a set X it unfold h, hoping to get to something of the form x ∈ X, so it gets to a ∈ s.val. Now it goes back to check the required NeZero instance, and it complains.

[Riccardo Brasca]

There must be a trace to see off all of this, but I am not 100% sure which option is required.

[Aaron Liu]

I tried trace.Meta.isDefEq, trace.Elab.app.propagateExpectedType, trace.Elab.step, trace.Elab.step.result, trace.Elab.app.args, which told me a lot but didn't tell me enough

[John Talbot]

Thanks both! I will investigate those trace options.