小试牛刀:我的第一个数学证明-Lean-Lang

import Mathlib
import Mathlib.Tactic.Ring

#check ℝ

example : { a b :Nat }->(a+b)^2 = a^2+b^2+2*a*b := by
 intro a b
 ring

example : ∀ a b : ℝ , a^2 - b^2 = (a+b)*(a-b) := by
 intro a b
 ring