beginner question on decomposing Sigma types

Stream: general

[Jonas Frey]

I have a very basic beginner question:

Of the following two proofs, the first one works but the second one doesn't:

example (A B : Prop) : A ∧ B → B ∧ A := by
  intro p
  cases p with
  | intro x y =>
    constructor
    assumption
    assumption

example (A B : Type) : A × B → B × A := by
  intro p
  cases p with
  | intro x y =>
    constructor
    assumption
    assumption

What's the easiest way to decompose a product or Sigma in the context into two named hypotheses? I think in earlier lean versions I could do something like cases p with x y, but that doesn't seem to work anymore.

[Kyle Miller]

A new syntax is cases' p with x y.

When you use cases .. with, what you need after | is the name of the constructor. For And, that's intro, and for Prod, that's mk.

example (A B : Type) : A × B → B × A := by
  intro p
  cases p with
  | mk x y =>
    constructor
    assumption
    assumption

[Kyle Miller]

There's also let for pattern matching:

example (A B : Type) : A × B → B × A := by
  intro p
  let ⟨x, y⟩ := p
  constructor
  assumption
  assumption

[Kyle Miller]

As well as intro:

example (A B : Type) : A × B → B × A := by
  intro ⟨x, y⟩
  constructor
  assumption
  assumption

[Jonas Frey]

Ahh thanks! the last one looks like the slickest solution

[Jonas Frey]

OK another question: how do I select / focus on the other goal at the end of the following?

def pcons (A : Type) : Type := Σ p : Prop, p → A
def dpcons (A : Type) : Type := Σ p : Prop, Σ q : Prop, p → PProd q A

def abc (A : Type) : (pcons (pcons A)) → dpcons A := by
  intro ⟨a, b⟩
  constructor

[Jonas Frey]

I want to give a as first component of the pair, but it's asking me for the second component first apparently?

(i figured it out, with case fst =>)