@highergeometer@mathstodon.xyz
Post #1365984
2025-05-19 03:25 UTC
@tao @ProfKinyon @xenaproject It may well be the fact that I was working with a slightly crippled system. I couldn't get Lean 4 Web to import all the tactics you did in your example video where you tackled that other Equational implication.
Replies (1)
-
@tao@mathstodon.xyz 2025-05-19 03:27
@highergeometer @ProfKinyon @xenaproject Ah, yes, canonical is a very new tactic that does not currently ship with the default installation of Lean, one has to build it separately. The other tactics should all be present, though.