Inline mask length equality proof in `isplit`

[larsk21]

Currently, the proof that the length of the hypothesis mask is equal to the length of the spatial context in the implementation of isplit (Tactics.lean) is required to be assigned to a separate variable first. If the proof is inlined at $h_length_eq, the error unknown free variable is shown.

This workaround should be removed as soon as lean4/#1415 is fixed.

let h_length_eq ← ``(by show $(quote mask.length) = $(quote lₛ) ; decide)
try evalTactic (← `(tactic|
  first
  | refine tac_sep_split $(quote mask) $h_length_eq _ ?Sep.left ?Sep.right
  | fail
))