Lean: beta_reduce before rw when the goal is `(fun b ↦ …) b ∈ S`
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.
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 ∈ Sthe goal is(fun b => F (g b)) b ∈ S, andrw [hb b]fails ('Did not find an occurrence of the pattern g b').obtain ⟨b, rfl⟩ := hxafterintro x hxgives the same redex and the same failure. All three fixes work:beta_reduce,show F (g b) ∈ _, andsimp only [hb b]. One reading note: here the pretty-printer does show the redex(fun b => F (g b)) b. Theg byou see is inside the lambda, with the bound b, so rw has nothing to match.