obtain doesn't work with placeholders

[Ruben-VandeVelde]

Example from #4707:

    obtain ⟨k, ⟨f⟩⟩ := IH ?_ s' ?_

doesn't work - no proof obligations are created for the placeholders (lean reports "no goals to be solved"), but omitting the proofs reports "don't know how to synthesize placeholder for argument 'h'".

    have := IH ?_ s' ?_
    obtain ⟨k, ⟨f⟩⟩ := this

works as expected.

[digama0]

duplicate of leanprover-community/batteries#116