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

Question

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?)

Answer 1

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