style when the := makes the line too long

Stream: mathlib4

[Emily Riehl]

I have an open PR which failed the style linter bc the := makes the line too long. I returned before this and started a new line with two indents and then :=. But now I fail the style linter for having this on a new line.

I can make this pass by splitting the type of the defined term across two lines but I thought I'd ask what is actually preferred here.

[Yaël Dillies]

Can you tell us which PR?

[Floris van Doorn]

In this case I indeed split up the type into two lines.

[Jon Eugster]

I think when the line is too long you should always split up after the : separating the arguments from the type and then split the type/arguments as necessary. And use 4 spaces until the proof starts.

I usually choose where to split the type by what looks nice, for example the ∧ below is a natural separation of two parts

theorem Nat.my_statement
    (a : Nat) (h : 0 < n) :
    1 < a + 1 ∧
    a - 1 ≠ 0 := by
  skip
  sorry

[Eric Wieser]

I'd maybe argue for

theorem Nat.my_statement
    (a : Nat) (h : 0 < n) :
    1 < a + 1 ∧
      a - 1 ≠ 0 := by
  skip
  sorry

which I think is also what the pretty-printer thinks