Unpacking existential hypothesis

Stream: new members

[Martin Huschenbett]

Hi there,

I'm pretty new to Lean but have some experience with Coq. I'm using Lean 4.22.

I'm doing a proof and have an existentially quantified hypothesis that I would like to "unpack". More specifically, my hypothesis is of the form h: exists x y, P /\ Q and I would like to replace it with x: S; y: T; h1: P; h2: Q.

Currently, my code looks something like this:

cases h; case intro x h =>
cases h; case intro y h =>
cases h; case intro h1 h2 =>
clear h
-- Rest  of the proof, using x, y, h1, and h2.

Is there a way to make this more concise, similar to what the destruct h as [x [y [h1 h2]]] tactic in Coq would do?

Many thanks, Martin.

[Anand Rao Tadipatri]

The obtain tactic in Lean allows you to do this.

example {P Q : Prop} (h : ∃ (x : S) (y : T), P ∧ Q) : True := by
  obtain ⟨x, y, ⟨h1, h2⟩⟩ := h
  sorry

[Martin Huschenbett]

That's exactly what I was looking for. Thank you so much!