## Stream: new members

### Topic: rewriting at specific part

#### 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 .

#### 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.

#### Kevin Buzzard (Feb 25 2019 at 10:36):

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

#### Calle Sönne (Feb 25 2019 at 10:38):

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

#### 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

#### 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