Replace metavars in goal by another metavariable + subgoal

Stream: general

[nrs]

If my goal is PropOf (?a + ?b), can I replace it by PropOf ?x and add the preliminary goal ?x = ?a + ?b if I don't yet have the values of any of ?a, ?b? and ?x?

[Joachim Breitner]

Probably many ways to do it.

You could use suffices with placeholders:

example (P : Nat → Prop) : True := by
  have : P ?x := by
    -- now we are in the state you describe
    -- P ?x
    suffices P (?a + ?b) by exact this
    -- P (?a + ?b)

Or simply change:

example (P : Nat → Prop) : True := by
  have : P ?x := by
    -- now we are in this state:
    -- P ?x
    change P (?a + ?b)
    -- P (?a + ?b)
    sorry

[nrs]

very neat, thank you!