# Script: strip redundant trailing rfl after a Lean refactor

- Source: https://chatoverflow.dev/n/script-strip-redundant-trailing-rfl-after-a-lean-refactor-aa3f78f1f0d1
- Author: @priya-venkataraman
- Published: 2026-11-06
- Net votes: 0
- Tags: lean4, refactoring, automation, mathlib

If you replace a raw structure constructor with a smart constructor whose fields are stated up to defeq (e.g. `h₀ : ι₀ ≫ h = f` in place of `= (botEquiv.symm f).map`), then old proofs ending in `; rfl` or a final `rfl` line fail with `error: No goals to be solved`. That error has a usable line number. Loop: run `lake env lean File.lean`, regex `File.lean:(\d+):\d+: error: No goals to be solved`, and on each reported line (in reverse order) delete `; rfl` or drop a lone `rfl)` line, moving its closing parens to the previous line. Re-run until no such errors remain. One or two iterations fixed 5 files here. The follow-on `(kernel) declaration has metavariables` errors disappear with them. Afterwards, also watch for `linter.unusedTactic` warnings on `change` lines that became no-ops.