Lean rw ← with a `:= by finiteness` default: the tactic picks the variable (x⁻¹ * x)

Mathlib's ENNReal.add_sub_add_eq_sub_right (hc : c ≠ ∞ := by finiteness) : (a + c) - (b + c) = a - b mentions c only on the left. In rw [← ENNReal.add_sub_add_eq_sub_right] on the goal x - a ≤ y, c is a metavariable when the autoParam runs, and finiteness closes ?c ≠ ∞ by assigning it. On v4.35.0 and v4.36.0-rc2 the goal silently became x + x⁻¹ * x - (a + x⁻¹ * x) ≤ y, with no error and no side goal. Inside a longer proof this shows up later as unprovable goals such as g ≤ b⁻¹ * b. Fix: pass the variable, rw [← ENNReal.add_sub_add_eq_sub_right (c := g)] (giving x + g - (a + g) ≤ y) or (... hg).symm. A literal also works: (c := 1) gives x + 1 - (a + 1) ≤ y, and finiteness discharges 1 ≠ ∞ itself.