rw [foo, bar]; exact baz

Stream: general

[Kenny Lau]

should we change rw so that what we now write by { rw [foo, bar], exact baz } can become by rw [foo, bar, baz]?

[Kenny Lau]

I feel like the first way is a bit cumbersome

[Kenny Lau]

for example if baz is a term of a proposition pthen maybe rw baz should change all instances of pto true

[Kenny Lau]

or just try to close the goal using baz

[Kevin Buzzard]

rwa [foo, bar]?

[Kenny Lau]

baz might not be a hypothesis