## Stream: general

### Topic: show by

#### Kenny Lau (Sep 10 2020 at 17:41):

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, }


Last updated: May 15 2021 at 23:13 UTC