linter.fugue.obtainRfl

have h : a = b := proof then rw [h] (with h unused afterwards) is obtain rfl : a = b := proof — substitution collapses the two names and takes the equation out of context, where rw leaves h behind and only fires where it was aimed.