at [Expressions](https://leanprover-community.github.io/lean4-metaprogramming-book/md/main/03_expressions.html#expressions) > letE n t v b is a let binder (let ($n : $t) := $v in $b). I don't think there is a syntax for `let` followed by `in`.