Simp failure involving `Fin.getElem_fin`

Stream: mathlib4

[Geoffrey Irving]

Before a Mathlib upgrade to v4.11.0-rc2, roughly this code succeeded in simplifying. Now it does not. Anyone know why it wouldn't be inferring? Something delicate is going on, as if I inline exp_series into simp_failure it works.

import Mathlib.Algebra.Order.Ring.Nat

def exp_series (A : Type) (term : ℕ → A) (n : ℕ) : Array A :=
  (Array.range n).map (fun n ↦ term n)

lemma simp_failure (A : Type) (term : ℕ → A) (n : ℕ) (k : Fin (exp_series A term n).size)
    (good : A → Prop) : good (exp_series A term n)[k] := by
  simp only [exp_series]
  simp only [Fin.getElem_fin]  -- I'd like this to turn ...[k] into ...[(k : ℕ)], but it fails
  sorry

[Kevin Buzzard]

Maybe you're a victim of the fact that def is now more irreducible than before.

Examples of fixes:

abbrev exp_series (A : Type) (term : ℕ → A) (n : ℕ) : Array A :=

or

  simp only [exp_series] at k ⊢

(because there's some type mismatch with k otherwise) or

erw [Fin.getElem_fin]

[Geoffrey Irving]

Thanks, those (and other) workarounds work, but I'm still curious if there's some way to fix Fin.getElem_fin to work with simp such that the unmodified code would have worked.

[Kevin Buzzard]

I think the issue is that the type of k still involves exp_series and Lean can't see through this any more.