rw? is behaving strangely in Mathlib v4.20 -rc5

Stream: mathlib4

[张守信(Shouxin Zhang)]

I've noticed that in Mathlib v4.20, rw? tactic returns some strange results when operating on hypotheses, as shown in the image:

import Mathlib

example (a b : ℕ) (n : ℕ) (hn : n ≠ 0) :
  a^n = b^n → a = b := by
  intro h
  rw? at h
  sorry

image.png
Why is this?

[张守信(Shouxin Zhang)]

I also noticed that there were no problems when applying rw? to the goal, because it uses rw [@xxx] as usual, instead of rw [xxx].

[Patrick Massot]

@Kim Morrison I also met this error last week, but forgot to report it.

[Shreyas Srinivas]

also happens in apply? The fix is usually that one is applying the wrong side of the equality or the wrong direction of an iff lemma

[Shreyas Srinivas]

or some typeclass instance is missing

[Patrick Massot]

Shreyas, the issue is that rw? reports non-existing issues. In Shouxin’s example, you can type rw [Mathlib.Tactic.Zify.natCast_eq] at h and everything works.

[Kim Morrison]

Not sure when/if I'll get to this, if someone would like to diagnose / propose a fix that would be great.

[Shreyas Srinivas]

Found another example

import Mathlib

example (d : ℕ) (hnpos : ¬ d > 0) : d = 0 := by
  show_term omega
  /-
  found a proof, but the corresponding tactic failed:
  (expose_names; exact Decidable.byContradiction fun a => _example._proof_1 d hnpos a)

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

example (d : ℕ) (hnpos : ¬ d > 0) : d = 0 := by
  omega -- works

[Robin Arnez]

Well that one is reasonable I guess because it actually doesn't work

[Shreyas Srinivas]

omega does work

[Robin Arnez]

yes I mean (expose_names; exact Decidable.byContradiction fun a => _example._proof_1 d hnpos a) doesn't work like it claims

[Shreyas Srinivas]

show_term <tactic> is supposed to show a term suggestion

[Shreyas Srinivas]

if a tactic works then its show_term suggestion also works

[Robin Arnez]

Yes, not a tactic suggestion. omega elaborated to Decidable.byContradiction fun a => _example._proof_1 d hnpos a so that's what it suggests

[Damiano Testa]

Shreyas Srinivas said:

if a tactic works then its show_term suggestion also works

This has never been the case, though, except in the simplest cases.

[Shreyas Srinivas]

I have never seen it fail before. But I have also never seen it claim that it cannot produce a term

[Shreyas Srinivas]

instead of showing a suggestion

[Daniel Weber]

It can produce a term, Decidable.byContradiction fun a => _example._proof_1 d hnpos a (you can also get it using by?), but that term uses a theorem that omega introduces (_example._proof_1) so it doesn't work without it. This also happens often with simp