Zulip Chat Archive
Stream: new members
Topic: Is it possible to write at goal?
Marko Grdinić (Oct 15 2019 at 11:32):
Is it possible to simplify by { ring, ring at is_one } into one tactic by instructing to rewrite both the goal and the hypothesis at once?
Rob Lewis (Oct 15 2019 at 11:34):
ring at is_one ⊢. ⊢ is \vdash
Marko Grdinić (Oct 15 2019 at 11:37):
Thanks.
Johan Commelin (Oct 15 2019 at 11:53):
⊢ is also \|-, if you want...
Last updated: May 02 2025 at 03:31 UTC