Zulip Chat Archive

Stream: new members

Topic: rewriting at specific part


view this post on Zulip Calle Sönne (Feb 25 2019 at 10:21):

I have following goal:
r * ↑b ^ n * ↑b < ↑b + ↑⌊r * ↑b ^ n⌋ * ↑b I want to rewrite to r * ↑b ^ n * ↑b < 1*↑b + ↑⌊r * ↑b ^ n⌋ * ↑b
How do I do that? Using rw will rewrite all the b:s.
End goal is r * ↑b ^ n * ↑b < (1 + ↑⌊r * ↑b ^ n⌋) * ↑b .

view this post on Zulip Johan Commelin (Feb 25 2019 at 10:27):

Either you use some form of conv { to_rhs, congr, skip, rw }, or you write
suffices : whatever_you_want, and hope that simp can prove your goal starting from whatever_you_want.

view this post on Zulip Kevin Buzzard (Feb 25 2019 at 10:36):

See what happens if you write suffices : (end_goal), simpa using this [or simp [this]]

view this post on Zulip Calle Sönne (Feb 25 2019 at 10:38):

Thank you! simp failed, but it was easy to prove with rw

view this post on Zulip Kevin Buzzard (Feb 25 2019 at 10:50):

I suspect convert would also have been useful. suffices : blah, convert this, then pick up the pieces

view this post on Zulip Patrick Massot (Feb 25 2019 at 11:34):

My first reaction would have been rw [show b + ⌊r * b ^ n⌋ * b = (1 + ⌊r * b ^ n⌋) * b , by ring]. But I guess the general context would have oriented me towards using a calc block


Last updated: May 11 2021 at 23:11 UTC