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