Defanging the unnecessary seqFocus linter

Stream: mathlib4

[Gabriel Ebner]

With the latest Lean nightly, this linter triggers a lot more easily. A common case is the following:

cases h <;> simp_all <;> rfl

Quite often, simp_all manages to close one of the two goals, but the other one requires rfl to see through the defeq. The linter then complains that the second <;> should be replaced by a ;.

cases h <;> simp_all
rfl

I don't think that's an improvement. The intention here is to clean up all left over goals from simp using rfl, no matter whether there's one or two. The proof shouldn't break if simp suddenly proves more or less.

[Mario Carneiro]

Note that the linter was originally designed for right-assoc <;> and needed to be adjusted for left-assoc, which I have done now

[Mario Carneiro]

but it doesn't fix this issue. This linter is working exactly as it was intended to, and cases h <;> simp_all; rfl works as a proof

[Mario Carneiro]

If you really want to write cases h <;> simp_all <;> rfl then you will need to set set_option linter.unnecessarySeqFocus false in ...