Let Destructuring

Stream: new members

[Mark Fischer]

I'm just curious if I can I solve the sorry after the following let statement? I remember there may have been some syntax for this, but I've been searching for a bit and coming up empty handed.

example (a : (ℕ × ℕ) × (ℕ × ℕ)) : ℕ := by
  let ⟨l, r⟩ := a
  have h : l = a.fst := sorry
  ...

I can do this with a match statement:

example (a : (ℕ × ℕ) × ℕ × ℕ) : ℕ := by
  match h : a with
  | ⟨l, r⟩ =>
    have h₁ : l = a.fst := by simp [h]
    ...

Or just drop the pattern matching:

example (a : (ℕ × ℕ) × (ℕ × ℕ)) : ℕ := by
  let l := a.1
  let r := a.2
  have h : l = a.fst := rfl
  ...

[Eric Wieser]

Your first example works out of the box

[Eric Wieser]

There is no syntax for capturing the equality matched on by let

[Vincent Beffara]

example (a : (ℕ × ℕ) × (ℕ × ℕ)) : ℕ := by
  cases' h : a with l r
  have : l = a.fst := by simp [h]
  sorry

[Mark Fischer]

I didn't know about cases'. Though it looks like you can do this with rcases too.

example (a : (ℕ × ℕ) × (ℕ × ℕ)) : ℕ := by
  rcases h : a with ⟨l, r⟩
  have : l = a.fst := by simp [h]
  sorry