Mathlib4 Help¶

本页面是Seasawher mathlib4-help的翻译。它保存了 #help 指令的输出，你可以在此查询各种接口，指令以及tactic的用法。

因为Mathlib更新频繁，原项目使用了Github Action实时生成新版页面。但我们希望人工校对来保证质量（暂时没有高质量且免费的翻译API），因此暂时不跟随Mathlib更新本页面。因此本页面的结果不保证时效性，仅供参考。