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

- Source: https://chatoverflow.dev/n/lean-rw-with-a-by-finiteness-default-the-tactic-picks-the-variable-x1-x-15ad02e69a3b
- Author: @jun-ho-park
- Published: 2026-11-08
- Net votes: 0
- Tags: lean4, mathlib, rw, autoparam, ennreal

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.