hitting the dreaded motive rw error in 3.6.10

Stream: Analysis I

[Rado Kirov]

I am trying to do a simple rewrite using a proof Fin 0 = \emptyset using rw [this] see screenshot. I understand now what the error says - Fin 0 is used also in the type of A, but is there a way to tell Lean rewrite that too? Simp [this] makes no progress either.

Screenshot 2025-07-30 at 9.48.49 PM.png

Screenshot 2025-07-30 at 9.49.02 PM.png

[Aaron Liu]

Try revert A and then rewrite

[Aaron Liu]

That's what I do and it usually works

[Rado Kirov]

Nice, that worked for me too.

[Kyle Miller]

Most of the time, "motive not type correct" means that after doing the rewrite, one of the subterms has a type that couldn't be rewritten. The rewrite tactic can only rewrite subterms, not types of subterms.

In this case, see how the error message says that A has type (Fin 0).subtype -> Set but it's expected to have type _a.toSubtype -> Set? That _a represents the subterm that's being rewritten; it starts as Fin 0, and it will become \emptyset.

Since A is a local variable, this suggests that a solution could be to revert it. The effect of doing this is that now the type of A is in the goal. Since the type is now a subterm, it's something that rw can rewrite.

[Rado Kirov]

Makes sense, sounds like revert A is something I need to add to my bag of tricks.

The rewrite tactic can only rewrite subterms, not types of subterms.

I was testing this with some contrived examples - but it does seem here https://live.lean-lang.org/#codez=JYWwDg9gTgLgBAWQIYwBYBtgCMBQATAUwDM4BzACgH0AuOATQEpbBUQjmoF44AGOHNA6ARBwk6dAC8CUCOQCetRrVJxZcTjw5wsqqEXQ4CADyTh0BOOUO0AGgwuoba+kzJxDTjZ2044cKAHc4AG1UAF0ReEMfP0Cg0QkpCFCcHCA that Lean can make x: X turn into x: Y with rw. So maybe the limitation above is more of rw can't rewrite at two places at once - the goal and local definitions?

[Aaron Liu]

Rado Kirov said:

Makes sense, sounds like revert A is something I need to add to my bag of tricks.

The rewrite tactic can only rewrite subterms, not types of subterms.

I was testing this with some contrived examples - but it does seem here https://live.lean-lang.org/#codez=JYWwDg9gTgLgBAWQIYwBYBtgCMBQATAUwDM4BzACgH0AuOATQEpbBUQjmoF44AGOHNA6ARBwk6dAC8CUCOQCetRrVJxZcTjw5wsqqEXQ4CADyTh0BOOUO0AGgwuoba+kzJxDTjZ2044cKAHc4AG1UAF0ReEMfP0Cg0QkpCFCcHCA that Lean can make x: X turn into x: Y with rw. So maybe the limitation above is more of rw can't rewrite at two places at once - the goal and local definitions?

That's because you are rewriting the type of x, not x itself

[Rado Kirov]

Right, but that's what I wanted in the original question - rewrite Fin 0 both in the goal and in the type of A which would have allowed for the whole thing to continue to type-check.

The problem is these are two rewrites, so something like rw [h] at \goal A could have worked, if the rw works simultaneously across both places (which I guess it doesn't).

[Aaron Liu]

yeah you can't rewrite simultaneously in multiple places

[Aaron Liu]

you have to put them together into a single expression

[Aaron Liu]

so that's what revert x will do