rewriting at specific part

Stream: new members

[Calle Sönne]

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]

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]

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

[Calle Sönne]

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

[Kevin Buzzard]

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

[Patrick Massot]

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