SetLike docs using Lean 3 or 4 syntax?

Stream: new members

[Martin C. Martin]

Mathlib4's SetLike/Basic.lean contains this example usage in a comment:

instance : SetLike (MySubobject X) X :=
  ⟨MySubobject.carrier, λ p q h, by cases p; cases q; congr'⟩

Is that proper Lean 4 syntax? OneShot translated my equivalent to:

  ⟨MySubobject.carrier, fun p q h => by cases p <;> cases q <;> congr⟩

Which is correct?

[Ruben Van de Velde]

Most likely you'll get a warning that the <;> is unnecessary (though it will work)

[Ruben Van de Velde]

<;> and ; are only different if the tactic before it created multiple goals, which I'm guessing cases doesn't do in this case

[Kyle Miller]

Lean 3's ; is Lean 4's <;>, but I think the Lean 3 should have been written as by { cases p, cases q, congr' } (too frequently people used ; to avoid needing to reach for the braces)

[Kyle Miller]

I think the Lean 4 could be by cases p; cases q; congr! since p and q are structures, and since congr! is the analogue of congr' (it might make a difference if the structures have things like Decidable fields)

[Anne Baanen]

I tested Kyle's suggestion on Subgroup and that worked. So: #7986.