Brackets after unification symbol?

Stream: new members

[Anton Lorenzen]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Anton Lorenzen]

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

[Anton Lorenzen]

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