# How to unfold definitions in Lean / find the right theorems to apply?

After a few days playing around with Lean4, I notice I keep running into the problem of how to find the right theorems to apply. The situation below is one I run into particularly often, so perhaps I simply have not found the right tactic yet.

Note, that there is - of course - simpler proof for this particular theorem, but for the sake of the example assume I'm looking for the indicated unfolding steps.

example (x y : α × β) : x = y ↔ (x.1 = y.1 ∧ x.2 = y.2) := by
constructor
. intro
constructor
. admit -- what can I do to unfold =' into its definition here?
. congr -- I found that this one helps to solve the goal, but I wanted to unfold the assumption!
. intro
. admit -- what can I do to unfold =' into its definition here?


I suspected there would be something of the kind apply Eq or some kind of intro based on a constructor, or some extensionality principle. But I can't find it.

I also find it a bit difficult to explain what I'm looking for really. The manuals do not go very deeply into giving examples of how to do proofs. (Is there a good reference with examples, perhaps?)

• Asking on the Lean Zulip is probably the most helpful. Sep 23, 2022 at 20:46
• Thanks, I'll have a look there as well. Sep 23, 2022 at 21:01

constructor    -- unfolds the definition of an inductive type