# 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

After quite a bit of searching, I did find a number of things to try that seem to cover most of what I need here:

constructor    -- unfolds the definition of an inductive type
apply funext   -- unfolds equivalence of functions
funext v       -- does the same but more efficiently, introducing variables
apply congrArg FooClass.mk -- unfolds an equivalence of a classes into equivalence of the arguments of its constructor
apply propext  -- unfolds an = into an iff