A verified tensor library in Lean