Reduce Goal to Equality with Unfolding

Stream: lean4

[Marcus Rossel]

How would I go about reducing a given proof goal up to the point where it has the form _ = _ while unfolding definitions and introducing quantified variables? For example, in the following:

def P := ∀ x y : Nat, x + y = y + x

example : P := by
  to_eq

How could I implement to_eq, such that it turns the goal into x + y = y + x (while introducing x and y)? I feel like it's some combination involving MVarId.intros and Meta.reduce, but I can't find the right incantation.

[Kyle Miller]

repeat intro?

[Marcus Rossel]

Oh, so intro will try to see through definitions, but intros won't?

[Kyle Miller]

Yes (well, intros doesn't look through definitions to see how many times to intro).

Here's an intros! tactic that does the same thing as repeat intro, but it does it all at once:

open Lean Elab Tactic Meta in
elab "intros!" : tactic => liftMetaTactic fun g => do
  forallTelescopeReducing (← g.getType) fun args ty => do
    let g' ← mkFreshExprSyntheticOpaqueMVar ty
    g.assign <| ← mkLambdaFVars args g'
    return [g'.mvarId!]

def P := ∀ x y : Nat, x + y = y + x

example : P := by
  intros!
  rw [Nat.add_comm]