vscode-lean
vscode-lean copied to clipboard
Spacing at end of "Try this" line
Given
squeeze_simpa [model_with_corners.left_inv] using hx },
if I click on the suggested output it erases the space between hx and }. This breaks mathlib style convention.