bad bahavior of isDefEq with introElem and DataArray

[lecopivo]

There is some bad interaction between introElem for DataArray and isDefEq.

The following code run out of heartbeats

import SciLean

open SciLean

open Lean Meta Qq in
#eval show MetaM Unit from do

  let X : Q(Type) := q(Float → DataArrayN Float (Idx 10))
  withLocalDecl `x default X fun x => do
  let x : Q($X) := x
  let HX := q(IsDifferentiable Float $x)
  withLocalDecl `hx default HX fun hx => do

  let H := q(IsDifferentiable Float fun w => ⊞ i => ($x w)[i])
  let h ← mkFreshExprMVar H 
  IO.println (← isDefEq hx h)

Somehow deciding defeq for IsDifferentiable Float fun w => ⊞ i => ($x w)[i] =?= IsDifferentiable Float x is hard and Lean starts unfolding everything.

[lecopivo]

This code runs slow as the definition IsDifferentiableAt gets unfolded in isDefEq too much

import SciLean

namespace SciLean

set_option profiler true in

example 
  (x : Float → DataArrayN Float (Idx 10)) (hx : IsDifferentiable Float x)
  : IsDifferentiable Float (fun w => ⊞ i => (x w)[i]) := 
by
  fprop

it takes roughly 500ms

[lecopivo]

Seems to be fixed now