Interactive unfold issue

Stream: mathlib4

[Patrick Massot]

@Jovan Gerbscheid I wanted to advertise unfold? in MIL but the example I wanted actually doesn’t work.

import Mathlib.Tactic

def mkVectorSpace {K X : Type*} [Field K] [AddCommGroup X] (ρ : K →+* AddMonoid.End X) : Module K X where
  smul a x := ρ a x
  one_smul x := by sorry
  mul_smul := _
  smul_zero := _
  smul_add := _
  add_smul := _
  zero_smul := _

And try to start proving one_smul. This is a typical case where beginners are completely stuck because ρ does not appear in the goal. I wanted to say: type unfold?, shift-click on the bullet and select ρ 1. But it creates a rw that doesn’t work. Why not creating a change instead? Note that one_smul x := by change ρ 1 x = _ ; sorry does work.

[Jovan Gerbscheid]

I see, the problem is that the notation 1 • x which is used in the goal, and put in the rw tactic, doesn't elaborate to the expression with ρ that we want. Emitting a change tactic instead of a rw [show .. = .. from rfl] seems reasonable too. However, I'm not sure how to make the underscores appear in the expression, such as in ρ 1 x = _.

[Jovan Gerbscheid]

It would also be nice to be able to evaluate whether a pasted tactic will succeed, before actually pasting it.

[Patrick Massot]

Yes, that’s an elaboration issue. About the change version, generating the underscore for parts that didn’t change isn’t essential, although it would be nice. And indeed evaluating whether the pasted tactic will succeed would be much more user-friendly.

[Kyle Miller]

For _-insertion, you could annotate the unchanged subexpressions with some metadata and create a delaborator keyed to that metadata that returns _