Lean server keeps consuming more memory as it reprocesses a large definition

import Std.Data.HashSet

set_option autoImplicit false

open String (Pos Iterator)
open Std (HashSet)

#eval Lean.versionString -- "4.16.0-nightly-2025-01-23"

inductive Node where
  | done
  | fail
  | epsilon (next : Nat)
  | char (c : Char) (next : Nat)
  | split (next₁ next₂ : Nat)
  | save (offset : Nat) (next : Nat)
  | sparse (cs : Char) (next : Nat)
deriving Repr

structure NFA where
  nodes : Array Node
  start : Nat
deriving Repr

def get (nfa : NFA) (i : Nat) (h : i < nfa.nodes.size) : Node :=
  nfa.nodes[i]

instance : GetElem NFA Nat Node (fun nfa i => i < nfa.nodes.size) where
  getElem nfa i h := get nfa i h

structure SearchState' (nfa : NFA) where
  states : HashSet (Fin nfa.nodes.size)
  updates : Vector (List (Nat × Pos)) nfa.nodes.size

abbrev εStack' (nfa : NFA) := List (List (Nat × Pos) × Fin nfa.nodes.size)

-- Run `top` and press Shift + M to see most memory-consuming processes.
-- Editing this comment will cause Lean server to re-check `εClosure'.induct'`,
-- leading to additional 1-2GB of memory consumption.
-- Don't forget monitoring the memory usage and restart the server before your system hangs with high memory pressure :)
theorem εClosure'.induct' (nfa : NFA) (it : Iterator)
  (motive : Option (List (Nat × Pos)) → SearchState' nfa → εStack' nfa → Prop)
  (base : ∀ matched next, motive matched next [])
  (visited :
    ∀ matched next update state stack',
    state ∈ next.states →
    motive matched next stack' →
    motive matched next ((update, state) :: stack'))
  (epsilon : ∀ matched next update state stack' state',
    state ∉ next.states → nfa[state] = .epsilon state' →
    let next' := ⟨next.states.insert state, next.updates⟩;
    motive matched next' ((update, state') :: stack') →
    motive matched next ((update, state) :: stack'))
  (split : ∀ matched next update state stack' state₁ state₂,
    state ∉ next.states → nfa[state] = .split state₁ state₂ →
    let next' := ⟨next.states.insert state, next.updates⟩;
    motive matched next' ((update, state₁) :: (update, state₂) :: stack') →
    motive matched next ((update, state) :: stack'))
  (save : ∀ matched next update state stack' offset state',
    state ∉ next.states → nfa[state] = .save offset state' →
    let next' := ⟨next.states.insert state, next.updates⟩;
    motive matched next' ((update ++ [(offset, it.pos)], state') :: stack') →
    motive matched next ((update, state) :: stack'))
  (done : ∀ matched next update state stack',
    state ∉ next.states → nfa[state] = .done →
    let next' := ⟨next.states.insert state, next.updates.set state update⟩;
    motive (matched <|> .some update) next' stack' →
    motive matched next ((update, state) :: stack'))
  (char : ∀ matched next update state stack' c (state' : Fin nfa.nodes.size),
    state ∉ next.states → nfa[state] = .char c state' →
    let next' := ⟨next.states.insert state, next.updates.set state update⟩;
    motive matched next' stack' →
    motive matched next ((update, state) :: stack'))
  (sparse : ∀ matched next update state stack' cs (state' : Fin nfa.nodes.size),
    state ∉ next.states → nfa[state] = .sparse cs state' →
    let next' := ⟨next.states.insert state, next.updates.set state update⟩;
    motive matched next' stack' →
    motive matched next ((update, state) :: stack'))
  (fail : ∀ matched next update state stack',
    state ∉ next.states → nfa[state] = .fail →
    let next' := ⟨next.states.insert state, next.updates⟩;
    motive matched next' stack' →
    motive matched next ((update, state) :: stack')) :
  ∀ matched next stack, motive matched next stack := sorry