Error on rw?: "found an applicable rewrite lemma"

Stream: new members

[Dan Abramov]

I often see this sort-of-maybe-error when I try to rw?:

found an applicable rewrite lemma, but the corresponding tactic failed:
  (expose_names; rw [SetCoe.ext_iff] at this)
  -- a.choose x = d.choose x

It may be possible to correct this proof by adding type annotations, explicitly specifying implicit arguments, or eliminating unnecessary function abstractions.

It looks like this:

Screenshot 2025-09-02 at 23.53.36.png

I was wondering if there's any idea of what might be causing this. The message itself is confusing — what is the "corresponding tactic"? Why did it fail?

Applying the suggestion works just fine:

Screenshot 2025-09-02 at 23.56.27.png

Also, what's up with this expose_names;? Feels like some internal leaking in accidentally.

[Dan Abramov]

The most annoying thing with this one is I have to copy and paste the suggestion because it's not clickable anymore.

[Rado Kirov]

Somehow, it never occured to me to use rw? despite using apply? and exact? a lot, so haven't seen this error.

Also, what's up with this expose_names;? Feels like some internal leaking in accidentally.

I have only seen this happen with exact? when it needs to use a hypothesis, but I have accidentally shadowed it by another one with the same name.

[Luna]

Has there been any further updates on this? I'm running into this problem quite often as well.

For example:

import Mathlib.Topology.Instances.Real.Lemmas

open Set Filter Topology

example (u : ℕ → ℝ) (M : Set ℝ) (x : ℝ) (hux : Tendsto u atTop (𝓝 x))
    (huM : ∀ᶠ n in atTop, u n ∈ M) : x ∈ closure M := by
  rw [mem_closure_iff_clusterPt]
  unfold ClusterPt
  unfold Tendsto at hux
  unfold Filter.Eventually at huM
  rw [← le_principal_iff] at huM
  simp only at huM

  apply neBot_of_le (f := (map u atTop))
  apply le_inf
  · exact hux
  · exact?  -- <<< ERROR here
-- found a proof, but the corresponding tactic failed:
--  (expose_names; exact fun ⦃U⦄ a => huM fun ⦃a_1⦄ => a)

[Jovan Gerbscheid]

This is somewhat orthogonal to the conversation, but I would suggest trying rw??. This is a point-and-click rewrite search tactic that rewrites at the location you select with a shift-click, unlike rw? which tries to rewrite anywhere.

[Filippo A. E. Nuccio]

Luna said:

Has there been any further updates on this? I'm running into this problem quite often as well.

A lot of unfold often gets into the way: if you do

import Mathlib.Topology.Instances.Real.Lemmas

open Set Filter Topology

example (u : ℕ → ℝ) (M : Set ℝ) (x : ℝ) (hux : Tendsto u atTop (𝓝 x))
    (huM : ∀ᶠ n in atTop, u n ∈ M) : x ∈ closure M := by
  rw [mem_closure_iff_clusterPt]
  apply neBot_of_le (f := (map u atTop))
  apply le_inf
  · exact hux
  · exact?

(which is exactly your proof, where I've just removed all the unfold, the subsequent rw and simp only), you get

Try this:
  exact le_principal_iff.mpr huM

that indeed closes the proof.