Typeclass synthetization error when using unfold

Stream: lean4

[Emilie (Shad Amethyst)]

I've encountered this strange issue, where I was given finite : Set.Finite s, and a function f : ↑s → β, and so some of the theorems used require Finite ↑s instead of Set.Finite s.
However, whenever I would use unfold Set.Finite at finite, errors would pop up. I randomly then tried to do rw [Set.Finite] at finite, and things suddenly worked. Here's a MWE:

import Mathlib.Topology.Filter

-- `Filter.iInter_mem` here requires `Finite ↑s`:

-- Works
example {α : Type*} {s : Set (Set α)} {f : Filter α} (finite : s.Finite) (h : ∀ x ∈ s, x ∈ f) :
    ⋂ i : s, i ∈ f := by
  rw [Set.Finite] at finite
  rw [Filter.iInter_mem]
  simpa using h

-- Fails
example {α : Type*} {s : Set (Set α)} {f : Filter α} (finite : s.Finite) (h : ∀ x ∈ s, x ∈ f) :
    ⋂ i : s, i ∈ f := by
  unfold Set.Finite at finite
  rw [Filter.iInter_mem] -- Failed to synthesize instance `Finite ↑s`
  simpa using h

#print-ing either theorem oddly yields the same function body.

[Eric Wieser]

Adding have _ := finite after the unfold line fixes it, so this looks like a caching issue

[Emilie (Shad Amethyst)]

That was my solution at first, but it makes the mathlib linter unhappy

[Kevin Buzzard]

haveI?

[Eric Wieser]

I think the next step here is probably to make a Mathlib-free #mwe