solve each goal in "by" mode

Stream: general

[Kenny Lau]

In by mode, i.e. by xxx; yyy; zzz, is there a way to not apply the tactics to every goal?

[Mario Carneiro]

you can use seq_focus, i.e. xxx; [yyy, zzz], or use a big tactic block by { xxx, yyy, zzz }

[Kenny Lau]

aha

[Kenny Lau]

I was trying focus [yyy, zzz] but it failed

[Kenny Lau]

turns out you don't say focus

[Kenny Lau]

how would you write this?

by simp [reduce.step, h] at H; cases L; injections;
    [cc, { rw ← h_2, from list.suffix_append _ _ } ]

[Mario Carneiro]

begin
  simp [reduce.step, h] at H,
  cases L; injections, {cc},
  rw ← h_2,
  exact list.suffix_append _ _
end

[Kenny Lau]

but it's three lines longer, lol

[Kenny Lau]

four lines longer. i can't count

[Mario Carneiro]

If you have to represent complicated control flow, you probably shouldn't be using by

[Mario Carneiro]

at some point it's saving lines by just deleting newlines