Stream: Beginner Questions

Topic: Just a small stylistic question about trivial proofs

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)

Fabian Huch (Jun 11 2025 at 07:30):

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

Manuel Eberl (Sep 17 2025 at 11:44):

There's also the "fact" method for that sort of thing. Can take a theorem as a parameter, or can figure it out automatically if there's a suitable fact in the context

Last updated: Oct 12 2025 at 20:20 UTC