Strange recursion depth error

Stream: mathlib4

[Gareth Ma]

Sorry that this code is not exactly minimal, but it's kind of hard to golf.

import Mathlib.Tactic
open Nat Finset
variable {n m k : Nat}

/- Projection map -/
def f₁ (a : Fin n.succ) (ha : ↑a ≠ n) : Fin n := ⟨a.val, lt_of_le_of_ne (lt_succ.mp a.isLt) ha⟩

/- Embeds a n-tuple into an (n + 1)-tuple where the final value is k -/
def f₂
  (g : Fin n → Fin k.succ) (_ : g ∈ Finset.univ.filter StrictMono) :
  Fin n.succ → Fin k.succ :=
  fun a ↦ if ha : ↑a ≠ n then g (f₁ a ha) else k

example : card (univ.filter (fun (s : Fin 2 → Fin 26) ↦ StrictMono s))
  = card (univ.filter (fun (s : Fin 3 → Fin 26) ↦ StrictMono s ∧ s 2 = 25)) :=
by
  refine Finset.card_congr f₂ ?_ ?_ ?_
  · intro a ha
    rw [mem_filter] at *
    constructor <;> try constructor
    · apply mem_univ -- maximum recursion depth has been reached
  · sorry
  · sorry

It says maximum recursion depth has been reached at the annotated point, even though the goal is literally f₂ a ha✝ ∈ univ, and I am not sure why.

[Gareth Ma]

Also though not related to the error, if anyone has a better proof idea or to rewrite the statement please tell me :D

[Mario Carneiro]

it will probably help to generalize the "big number" 26 because lean is probably computing something 26 or 26^2 times

[Gareth Ma]

Oh that worked, if I replace 26 with k or something. That's interesting..

[Gareth Ma]

Thanks!

[Mario Carneiro]

MWE

def test : Prop :=
  -- expensive to whnf
  if 100 ∈ List.range 1000000 then True else False

example : True := by
  have : test := sorry
              -- ^^^^^
-- maximum recursion depth has been reached (use `set_option maxRecDepth <num>` to increase limit)

[Gareth Ma]

Generalising the numbers to variables is probably the correct way, but is there a "no whnf" tag / option?

[Mario Carneiro]

another trick I noticed was to use have : Fintype (Fin 2 → Fin 26) := inferInstance at the beginning of the proof

[Bhavik Mehta]

I just ran into something similar when porting, since it (including Mario's mwe) works in Lean 3 :/