2
$\begingroup$

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

New contributor
Pieter Cuijpers is a new contributor to this site. Take care in asking for clarification, commenting, and answering. Check out our Code of Conduct.
$\endgroup$
2
  • $\begingroup$ Asking on the Lean Zulip is probably the most helpful. $\endgroup$
    – Jason Rute
    Sep 23 at 20:46
  • $\begingroup$ Thanks, I'll have a look there as well. $\endgroup$ Sep 23 at 21:01

1 Answer 1

2
$\begingroup$

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
New contributor
Pieter Cuijpers is a new contributor to this site. Take care in asking for clarification, commenting, and answering. Check out our Code of Conduct.
$\endgroup$

Your Answer

Pieter Cuijpers is a new contributor. Be nice, and check out our Code of Conduct.

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.