Coercing typeclass instances?

Stream: lean4

[Shreyas Srinivas]

I need help with the following #mwe. This is based on me trying to work with sets and pushing away finiteness issues until they are really needed at multiple places. I am not comfortable with HEq wizardry yet. Is that what I need here?

import Mathlib.Tactic


example (Q : Type) [instFin : Fintype Q]
  (s : Set Q) : Set.Finite s := by
  apply Set.Finite.intro
  apply instFin -- fails. ↑s is `@Set.Elem Q s`, the set of elements of s

example (Q : Type) [instFin : Fintype Q]
  (s : Set Q) : Set.Finite s := by
  apply Set.Finite.intro
  have h : s = @Set.Elem Q s := by rfl
  apply (h ▸ instFin) -- also fails. I can see why. In the lhs of `h`, `s` already got coerced

-- Additional question below
example (Q : Type) [instFin : Fintype Q]
  (s : Set Q) : Set.Finite s := by
  apply Set.Finite.intro
  have h : s = @Set.Elem Q s := by rfl
  apply (@Fintype.mk) -- why doesn't `apply` produce goals for implicit types?

[Kyle Miller]

The idiomatic expression is

example (Q : Type) [Fintype Q]
  (s : Set Q) : Set.Finite s := s.toFinite

[Shreyas Srinivas]

Thanks a lot :) that works :tada: