"Fill goal" works incorrectly in presence of ==<, >== and `qed

[marat-rkh]

Invoke "Fill goal" on the following code:

Expected result:

Actual result:

Note that `qed lost its `. Also the last {?} is after the qed, not before it. These are bugs.

[ice1000]

It's the pretty printer

[valis]

I thought it just syntactically inserts the expression. Why does it invoke pretty printer?

[ice1000]

Oh, sorry, I remembered it wrongly.

[ice1000]

https://github.com/JetBrains/intellij-arend/blob/1c110f1081154aa297aeb8f3a0e8af0c48803965/src/main/kotlin/org/arend/quickfix/GoalFillingQuickFix.kt#L13