Why `erw` doesn't work for `frobenius`?

Stream: new members

[Jiang Jiedong]

Hi everyone,
I encountered the following example:

import Mathlib

example {R : Type*} [CommRing R] {p : ℕ} [Fact (Nat.Prime p)] (pchar : CharP R p) (x y : R) :
    (x + y) ^ p = x ^ p + y ^ p := by
  -- exact frobenius_add R p x y
  erw [frobenius_add R p x y] -- failed

The exact frobenius_add R p x y tactic will close the goal but erw does not work. Does anyone has some clue for this? Thank you!

[Kyle Miller]

I'm not sure, but I think it would be best to do rw [<- frobenius_def (x + y), frobenius_add] (I did not test this)

[Jiang Jiedong]

Kyle Miller said:

<- frobenius_def (x + y)

Thank you! This works. But still I'm curious about what is special about this frobenius that makes erw cannot see through it. (But exact and rfl can)

[Kyle Miller]

It's more that erw isn't seeing it in the expression. Tactics like exact and rfl just need to check definitional equality, but erw needs to locate a term to rewrite.

[Kyle Miller]

One of my guesses is that frobenius is a ring homomorphism, so applying it involves a coercion, and somehow that's obstructing rw from seeing the pattern.

[Kyle Miller]

But more likely is that rw uses "key matching" when looking for a term to rewrite. It only considers doing a rewrite if the theorem's LHS and the target subexpression have the same "key".

[Kyle Miller]

Yeah, in this case (x + y) ^ p has the key HPow.hPow, but the LHS of frobenius_add is going to be the name of the coercion function for ring homomorphisms.

[Kyle Miller]

(I wonder if erw should turn off key matching? There's also no configuration option to turn it off yet.)