Require strict indentation in nested by-s

[AdrienChampion]

This makes the non-bracketed tactic sequence parser following a nested by require strict
indentation.

Mentored by @digama0, this PR introduces Tactic.tacticSeqIndentGt which is the same as
Tactic.tacticSeq (by's current tactic sequence parser) but with checkColGt "strict indentation" right before the non-bracketed tactic sequence.

It does not use leading_parser but instead builds a Tactic.tacticSeq node, the idea being
that antiquotations should not have to care whether the tactic sequence allows non-strict
indentation or not. It also makes the change relatively shallow and local.

Motivation

Currently, the first element of a non-bracketed tactic sequences after a by can be indented
arbitrarily. The parser will accept the sequence as long as its tail has the same indentation as the
first element:

theorem easy : True := by
skip
skip
sorry

No problem for top-level bys, but things can get confusing (especially for newcomers) for nested
bys:

theorem easy : True := by
  have : True := by
  sorry -- recognized as the first element of the tactic sequence for `have`

  -- cannot write anything legal here
  -- - same indentation as `have` ⇒ part of the `have` tactic sequence ⇒ "no goals to be solved"
  -- - smaller indentation ⇒ not recognized as a tactic for top-level `by` ⇒ syntax error

This PR turns it into an error:

theorem easy : True := by
  have : True := by
  sorry -- expected '{' or strict indentation

to force

theorem easy : True := by
  have : True := by
    sorry
  sorry

[Kha]

The "expected command" error message is not great, but we have that issue in many other places. I suppose we could add a colGt-like parser combinator that unconditionally runs the inner parser, then complains about the indentation afterwards (but still at the initial position).

[AdrienChampion]

Fixed stage2: where structure fields set the position, causing by to require strict indentation, which two structure definitions in the codebase did not respect.

So I should clarify that the following is not allowed anymore:

... where
  field1 := by
  long
  unindented
  proof
  field2 := by
  still
  no
  indentation

I would say it's good for this to be banned as it's perfectly unreadable to me. But reasonable minds might disagree (separating fields by an empty line would arguably make this readable), so another approach would be for field definitions to be parsed with withoutPosition termParser (thanks @digama0 for pointing this out).

[Kha]

Looks fine to me