induction cases on the same line

Stream: mathlib4

[Jeremy Tan]

In #22533 I have some instances of induction where one or more of the initial cases are presented on the same line as the induction.

induction n with | zero => simp [geomSum] | succ n ih =>

It is legal syntax, but is this style an acceptable variant?

(@Yury G. Kudryashov, https://github.com/leanprover-community/mathlib4/pull/22533#discussion_r1997766857)

[Yury G. Kudryashov]

Note: Jeremy uses this syntax to replace something like

induction' n with n ih; · simp

[Kyle Miller]

I'm not sure I like having multiple cases on the same line like this, but that's style that's up for debate.

More importantly, I think in the future

induction x with | label a b c =>
tac1
tac2

will be an error if there's no indentation. This would be to support empty tactic blocks, without giving strange behavior. I don't know for certain yet.

Two future-proof options: (1) indent, or (2) use induction x with | label a b c => ?_ if you don't want to indent the following lines.

[Damiano Testa]

I might have been the one introducing the weird induction' ...; · simp syntax when I was cleaning up mathlib for adopting the multiGoal linter.

[Damiano Testa]

My personal preference would be to indent, though.