Sage Binder (Jun 10 2025 at 21:23): Sage Binder (Jun 10 2025 at 21:23):When an existing theorem directly matches a goal, which of the following is preferred?
have "..." using my_theorem .
have "..." by (rule my_theorem)
I prefer the latter, but that's mostly personal preference.
Mathias Fleury (Jun 11 2025 at 09:26):I try to skip those steps...
Mathias Fleury (Jun 11 2025 at 09:27):note H = my_theorem[of ...] would also work
Mathias Fleury (Jun 11 2025 at 09:28):The rule version has the advantage to have an implicit standard applied, which can be useful to discharge assumptions
Last updated: Jun 21 2025 at 01:46 UTC