Fin.find? and decide in v4.26.0

Stream: lean4

[Joseph Tooby-Smith]

I'm bumping PhysLean to v4.26.0, in which Mathlib's Fin.find has been replaced with Fin.find? in Batteries. The latter does not seem to work nicely with decide. In particular,

import Mathlib

example :  let c : Finset (Finset (Fin 2)) := {{0, 1}}
     Fin.find? (fun j => ({0, j} ∈ c.1)) = some 1 := by
  decide -- does not work in v4.26.0

does not work, whilst in v4.24.0 (for example):

import Mathlib

example :  let c : Finset (Finset (Fin 2)) := {{0, 1}}
    Fin.find (fun j => ({0, j} ∈ c.1)) = some 1 := by
  decide -- works in v4.24.0

worked (see here). There are a number of results in PhysLean which were using decide and somewhere along the lines used Fin.find. Is there a known solution to this?

[Bhavik Mehta]

Does decide +kernel work?

[Damiano Testa]

As Bhavik points out, it seems to be a reducibility setting. Also with_unfolding_all decide works.

[Joseph Tooby-Smith]

Weird adding +kernel works on the online playground, but not locally - I must be missing an import.

[Joseph Tooby-Smith]

Actually, this does not work on Mathlib stable on the online playground (see here), only on the latest version.

[Joseph Tooby-Smith]

Here is a Mathlib independent version which works on Mathlib latest i.e. v4.27.0-rc1 but not on Mathlib stable i.e. v4.26.0:

import Batteries.Data.Fin.Basic

example :  Fin.find? (fun j : Fin 7 => 5 < j) = some 6 := by
  decide +kernel

[Damiano Testa]

To fix the bump, does simp +decide work?

[Joseph Tooby-Smith]

No it doesn't, not on my examples above, nor on my 'real case'. One option would be to just bump straight to v4.27.0-rc1, but ideally I would like to have a version on a stable bump.