style proposal: avoid superfluous `<;>`

Stream: mathlib4

[Kim Morrison]

I think very often <;> is used solely to squeeze everything into one line, and I don't think we should do that.

Sometimes <;> is actually helpful. e.g. in src#Set.OrdConnected.strictConvex

  cases' hxy.lt_or_lt with hlt hlt <;> [skip; rw [openSegment_symm]] <;>
    exact
      (openSegment_subset_Ioo hlt).trans
        (isOpen_Ioo.subset_interior_iff.2 <| Ioo_subset_Icc_self.trans <| hs.out ‹_› ‹_›)

would be awkward without <;>. Similarly in Imo20221Q1:

  cases' hCA with hCA hCA <;> [right; left] <;>
    exact ⟨a, (hCA ha).2, b, (hCA hb).2, hab, h₁ a (hCA ha).1 b (hCA hb).1 hab⟩

But most are not like that:

apply mono_lie_left <;> [exact le_sup_left; exact le_sup_right]

split_ifs with h <;> [simp only [h, mod_zero, gcd_zero_right]; rfl]

by_cases hc : c = 0 <;> [simp only [hc, mul_zero, or_true]; simp [mul_left_inj', hc]]

I think these are less readable, and for no good reason (new lines characters are expensive?), and would encourage us to encourage or require that <;> is not used when the same proof logic could be achieved with either \. or all_goals.

[Johan Commelin]

So maybe the "rule" is that we shouldn't use <;> [tac1, tac2, ...] at the end of a proof?

[Mario Carneiro]

Speaking only for myself, I have a personal preference for the <;> [tac1; tac2] style to close trivial side goals, as well as to prove very short case splits. In lean 3 this was often accomplished by using e.g. {refl} at the end of a line after, say, an induction with a trivial base case; but in lean 4 this formatting leads to induction e; · rfl which looks pretty weird with a bullet in the middle of the line. I often use several tactics on the same line as a means of doing "semantic line breaking", where multiple tactics coordinate into one higher level idea. I'm aware not everyone is a fan of this style though.

[Kim Morrison]

Okay. I'm happy to leave it at that. This one is not a big deal.

[Mario Carneiro]

I'd be okay with being overruled on this point by the other mathlib maintainers though, I don't trust my own opinion in this regard to be reflective of mathlib maintainer consensus because a lot of people think I write too-golfed proofs

[Mario Carneiro]

I just wanted to put the counter point out there so that people had something to upvote if they disagree