Display target before assumptions not always respected

[MoritzBeroRoos]

Description

There are situations (e.g. in messages) where the Infoview setting Display target before assumptions is not respected.
E.g. click on the underscore in the following:

theorem bla (a : False) : 1 = 2 := by sorry

theorem bla2 : 1 = 2 := by
  let := 1
  rw [bla (by _)]

The infoview shows the message

unsolved goals
this : Nat := 1
⊢ False

although i have set the setting to true.
This makes for a lot of scrolling in proofs with large contextes before i can finally see the goal.

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.