On `tactics3`, you don't need to use backwards rewriting for the third solution

[wildwestrom]

I was able to solve it like this, so it doesn't need a backwards rewrite at all.
I'm guessing you want a problem that can only be solved with a backwards rewrite.

-- Use backwards rewriting: replace b with a in the goal
theorem rewrite_back (a b : Nat) (h : a = b) : b + 1 = a + 1 := by
  rw [h]

[SamuelSchlesinger]

Fixed in #12 (merged to main). rewrite_back is redesigned (h : a = b, ha : a + 1 = 5, goal b + 1 = 5) so a forward rw [h] errors with "did not find an occurrence" and rw [← h] is genuinely required.