Problems with meta variable in goal

Stream: new members

[Eric Mark Martin]

Hey, I’m new to lean but having some trouble where an exact I’m providing won’t unify because the goal has a metavariable in it

[Johan Commelin]

Could you provide a minimal (non-)working example (MWE), please?

[Johan Commelin]

As in, copy-paste your code

```lean
code goes here (you get syntax-highlighting!)
```

[Johan Commelin]

That will make it a lot easier for us to help you

[Johan Commelin]

Also: welcome :wink:

[Eric Mark Martin]

Thank so much—I’m actually having a lot of trouble getting a mwe which is part of the difficulty—I can’t tell why it lets me do what I want sometimes but not here

[Eric Mark Martin]

The proof is actually for a class so I don’t want to paste it here online

[Eric Mark Martin]

I think the error message that captures the gist of the issue though is

invalid apply tactic, failed to unify
  Expr.Num x ~ Expr.Num ?m_1
with
  ?m_2 ~ ?m_2

[Eric Mark Martin]

Where Expr.num x ~ Expr.Num ?m_1 is my goal as a result of an existential introduction

[Kevin Buzzard]

If you're not going to post any code it's difficult to help. Try explicitly writing some type ascriptions in some clever places (ie write (_ : nat) instead of _) and see if it helps

[Kevin Buzzard]

Maybe the elaborater is doing things in a silly order and needs some hints