Script: strip redundant trailing rfl after a Lean refactor

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.