rw? and expose_names

Stream: lean4

[Michael Stoll]

Since a while ago, rw? and friends sometimes produce suggestions that involve expose_names and frequently come with the added caveat "found an applicable rewrite lemma, but the corresponding tactic failed" (which leads to no clickable "Try this:"). However, there are cases where

• the expose_names is actually unnecessary;
• the suggested rw [...] with or without expose_names works perfectly well.

Here is a Mathlib-free example.

def B (n : Nat) : Prop := n = 0

example (A : Prop) (n : Nat) : A ∧ B n ↔ A := by
  refine ⟨fun H ↦ ?_, ?_⟩
  · rw? at H
    -- found an applicable rewrite lemma, but the corresponding tactic failed:
    -- (expose_names; rw [and_congr_left_eq (congrFun rfl)] at H)
    sorry
  sorry

but rw [and_comm] at H (say) just works.

It seems to be relevant that there is B n and not just some C : Prop in the term.

This looks like a bug to me.

[Jovan Gerbscheid]

I haven't implemented the expose_names feature yet in my rw?? tactic, but apparently I shouldn't copy exactly what rw? does :sweat_smile: