problem with change

Stream: mathlib4

[Patrick Massot]

Is the change tactic meant to work in mathlib4? It doesn't seem to like

import Mathlib.Tactic.Basic
open Prod

theorem lex_def (r : α → α → Prop) (s : β → β → Prop) {p q : α × β} :
    Prod.Lex r s p q ↔ r p.1 q.1 ∨ p.1 = q.1 ∧ s p.2 q.2 :=
  ⟨fun h => by cases h <;> simp [*], fun h =>
    match p, q, h with
    | (a, b), (c, d), Or.inl h => Lex.left _ _ h
    | (a, b), (c, d), Or.inr ⟨e, h⟩ => by
      change a = c at e
      subst e <;> exact lex.right _ h⟩

By the way, trying to jump to definition on change jumps, to the definition of Iff...

[Mario Carneiro]

change is just show now

[Patrick Massot]

Then someone should tell mathport about it.

[Mario Carneiro]

change e defined in Mathlib.Tactic.Basic as an alias for show e, but the at form and change .. with .. are both defined without implementation in lean 4 core. These are just missing an implementation (and they should either be PR'd to lean 4 or moved to mathlib4).

[Patrick Massot]

Switching from change to show doesn't fix anything

[Patrick Massot]

It only makes a new weird error message: expected '⟩'

[Patrick Massot]

And trying to jump to the definition of show still jumps to the definition of Iff

[Mario Carneiro]

that is, change e at h does not exist currently

[Patrick Massot]

Oh, I thought you meant we need show e at h

[Patrick Massot]

What is the workaround then?

[Mario Carneiro]

(it should really be on the tactic porting list, I think it was missed because it is one of the few tactics that has syntax but no elab in lean 4 core)

[Mario Carneiro]

no workaround other than revert/intro

[Mario Carneiro]

or rw

[Mario Carneiro]

or have I guess for the change e at h case

[Patrick Massot]

Ok thanks. I guess this gives us a rather urgent tactic porting target.

[Ruben Van de Velde]

replace h : _ := h, if that exists already?

[Mario Carneiro]

it does exist

[Mario Carneiro]

reported as lean4#1745, I'll work on it