equality by components

Stream: general

[Reid Barton]

If my goal is of the form ⟨x, y⟩ = ⟨x', y'⟩, is there a tactic that will replace it with two new goals x = x' and y = y'?

[Reid Barton]

oh, congr did it.

[Reid Barton]

I'm also wondering how I could do this when the left and/or right hand side is not already a constructor application, and I want to eta expand first. (But in my actual case the right hand side was just a variable, and I could use induction.)

[Mario Carneiro]

Lean doesn't have definitional eta for products fyi