Rewrite one side of eq

Stream: lean4

[Marcus Rossel]

Say I have:

example (f : α → β) (g : β → α) (h : f ∘ g = id) (b : β) : f (g b) = b := by
  have hb : id b = b := id.def b

How can I use hb to rewrite only the right side of the equation f (g b) = b?

---

For context, the (important part of the) goal state is:

hb : id b = b
⊢ f (g b) = b

[Eric Rodriguez]

if you just want some way to solve it, rw [show f (g b) = (f ∘ g) b from rfl, h, id.def]. I don't know that there's anything like nth_rewrite or occs in lean4 (my light skim suggests not), though; you could also try something like rw [←hb, show f (g (id b)) = (f ∘ g) b from rfl, h] but that's still just workarounds