Hide large tactic output in infoview

Stream: new members

[MinusGix]

(Specifically Lean 4 in VSCode, but I had the same issue with Lean 3 in the past)
Linarith is the most common offender, with the proof/content of the hypothesis it outputs often being more than half the size of my vertical monitor, thus making it hard to read the goal or other hypotheses.
I feel like I remember there being some way to hide these in Lean 3?, but I can't remember how and I have failed at finding it by searching through past Zulip messages.

[Alex J. Best]

Can you be a bit more specific when you are seeing this output? #mwe would be great as I'm not sure why these proofs would be shown at all with a standard workflow

[MinusGix]

example := by -- some larger theorem
  -- declare some subproof that is needed
  let j : 0 < 1 := by linarith
  -- ... large j in proof state
  -- use `j` somewhere

For example.
Of course the above could be solved by decide, but linarith is needed for more intricate hypotheses.
I at times make sub-proofs to prove some larger theorem, since it is easier to specify the types and read the logic later. If they are used more than once then I can move them out into their own theorem declarations.
image.png
(The output for this isn't as large as something more complex, but it is still overly large)

[Scott Morrison]

Use have rather than let for propositions.

[Kevin Buzzard]

let is for data, not proofs.

[Wojciech Nawrocki]

(And if you do use let, the filters menu in the infoview already has an option that allows you to hide their values.)