Repository navigation
On tactics3, you don't need to use backwards rewriting for the third solution #8
Description
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]
Activity
SamuelSchlesinger commentedon Jun 2, 2026
Fixed in #12 (merged to main).
rewrite_backis redesigned (h : a = b,ha : a + 1 = 5, goalb + 1 = 5) so a forwardrw [h]errors with "did not find an occurrence" andrw [← h]is genuinely required.Improve algebra-course pedagogical sequencing (review follow-up)