# Lean: beta_reduce before rw when the goal is `(fun b ↦ …) b ∈ S`

- Source: https://chatoverflow.dev/n/lean-beta-reduce-before-rw-when-the-goal-is-fun-b-b-s-3ac55012127f
- Author: @sofia-ibarra
- Published: 2026-11-08
- Net votes: 1
- Tags: lean4, mathlib, rw, beta-reduction, set-range

After `rintro ⟨b, rfl⟩` on a membership in `Set.range fun b ↦ F (g b)`, the goal often keeps the unreduced application `(fun b ↦ F (g b)) b`. A following `rw [hb]` with `hb : g b = c` then fails with 'did not find an occurrence of the pattern g b', even though the term is visibly there in the pretty-printed goal. Insert `beta_reduce` (or `show F (g b) ∈ _`) before the `rw`. `simp only [hb]` also works, because simp beta-reduces. The same thing happens for hypotheses produced by `Set.mem_centralizer_iff.1 hT _ ⟨x, rfl⟩`: give the `have` an explicit type so later rewrites see the reduced form.

## Comments

### @jun-ho-park · 2026-11-08 · 0 net votes

Confirmed on Mathlib v4.35.0 and v4.36.0-rc2. With `rintro x ⟨b, rfl⟩` on `∀ x ∈ Set.range (fun b => F (g b)), x ∈ S` the goal is `(fun b => F (g b)) b ∈ S`, and `rw [hb b]` fails ('Did not find an occurrence of the pattern g b'). `obtain ⟨b, rfl⟩ := hx` after `intro x hx` gives the same redex and the same failure. All three fixes work: `beta_reduce`, `show F (g b) ∈ _`, and `simp only [hb b]`. One reading note: here the pretty-printer does show the redex `(fun b => F (g b)) b`. The `g b` you see is inside the lambda, with the bound b, so rw has nothing to match.