非零自然数大于零的Lean证明优化及Mathlib4查询困惑

• 直接调用已有引理：Mathlib4中存在完全匹配需求的引理Nat.pos_of_ne_zero，可以直接替代手动匹配的实现，代码如下：

def Nat.zero_lt (n:Nat)(p:n ≠ 0) : 0 < n :=
  Nat.pos_of_ne_zero p

• 战术模式简化实现：如果偏好战术风格，也可以用更简洁的写法：

def Nat.zero_lt (n:Nat)(p:n ≠ 0) : 0 < n :=
by
  apply Nat.pos_of_ne_zero
  exact p

或者一步到位：

def Nat.zero_lt (n:Nat)(p:n ≠ 0) : 0 < n :=
  exact Nat.pos_of_ne_zero p

• 引理检索小技巧：在Lean环境中，可通过#check Nat.pos_of_ne_zero查看引理的类型签名；也可以用#find (n:Nat) → n≠0 → 0<n命令搜索匹配类型的引理，这种方式比单纯查阅文档更高效。

内容的提问来源于stack exchange，提问作者redjamjar