style guide

Stream: mathlib4

[Heather Macbeth]

When you have a lot of hypotheses, do extra lines of hypotheses get indented 2 or 4 spaces? That is, is the whitespace convention

lemma bop_of_baz (hyp : Hyp) (more_hyp : MoreHyp)
  (yet_more_hyp : YetMoreHyp) :
    17 = 43 := by
  proof_line_1
  proof_line_2

or

lemma bop_of_baz (hyp : Hyp) (more_hyp : MoreHyp)
    (yet_more_hyp : YetMoreHyp) :
    17 = 43 := by
  proof_line_1
  proof_line_2

[Gabriel Ebner]

The second one is what I prefer, and what the pretty-printer (and by extension mathport) produces.