(deterministic) timeout at 'whnf', maximum number of heartbe

Stream: mathlib4

[Christopher Hoskin]

Hello,

I'm fairly new to mathlib4 porting. I've nearly got Analysis.NormedSpace.MStructure building, but it fails towards the end with

./././Mathlib/Analysis/NormedSpace/MStructure.lean:302:0: error: (deterministic) timeout at 'whnf', maximum number of heartbeats (800000) has been reached (use 'set_option maxHeartbeats <num>' to set the limit)
./././Mathlib/Analysis/NormedSpace/MStructure.lean:302:0: error: (deterministic) timeout at 'whnf', maximum number of heartbeats (800000) has been reached (use 'set_option maxHeartbeats <num>' to set the limit)
./././Mathlib/Analysis/NormedSpace/MStructure.lean:344:0: error: IR check failed at 'IsLprojection.instBooleanAlgebraSubtypeIsLprojection._rarg', error: unknown declaration 'IsLprojection.instDistribLatticeSubtypeIsLprojection'
error: external command `/home/runner/.elan/toolchains/leanprover--lean4---nightly-2023-03-09/bin/lean` exited with code 1

Please see: https://github.com/leanprover-community/mathlib4/pull/2915

Any suggestions as to what I've done wrong?

Thanks,

Christopher