## Stream: new members

### Topic: Brackets after unification symbol?

#### Anton Lorenzen (Feb 16 2020 at 16:17):

In a goal, what does ?m_1[⟨h2_fst, h2_snd⟩] mean? Here h2 : \Sigma s, j was case-splitted into h2_fst and h2_snd and I get an error if I try to unify ?m_1 with h2_fst.

#### Kevin Buzzard (Feb 16 2020 at 16:18):

m_1 is a metavariable which depends on other things and which Lean doesn't know

#### Kevin Buzzard (Feb 16 2020 at 16:18):

When did it appear? I try to avoid them in tactic mode

#### Kevin Buzzard (Feb 16 2020 at 16:19):

Maybe you can squeeze in a .1 somewhere and make it go away

#### Anton Lorenzen (Feb 16 2020 at 16:21):

Lol, not case-splitting and using .2 instead solved the proof

#### Anton Lorenzen (Feb 16 2020 at 16:23):

I am completely baffled by this, but this actually seems to work

Last updated: May 15 2021 at 02:11 UTC