batteries
batteries copied to clipboard
rcases doesn't seem to support ?_ placeholders
import Std.Tactic.RCases
theorem aux (h : 0 < 2) : ∃ n : Nat, n = 2 := ⟨2, rfl⟩
example : True := by
rcases aux ?_ with ⟨x, h⟩
trivial
I would expect a side goal to be created (like in lean3), but get "don't know how to synthesize placeholder for argument 'h'"
Currently my workaround is
have := aux ?_
rcases this with ⟨x, h⟩
which is kind of annoying.