show by

Stream: general

[Kenny Lau]

I just noticed that the by is redundant in show if you have a tactic block:

theorem foo {a b c d : ℕ} (hab : a = b) (hcd : c = d) : a + c = b + d :=
show _, { rw hab, rw hcd, }