Typos intro.lean

[nsd4fr]

Linen 218 "The proof is produced the rfl inference rule."

Presumably is

"The proof is produced with the rfl inference rule."

Line 224

"rule rule ..."

Line 233

"... Checke ..."

Line 327

There is a right parenthesis with no left parenthesis

Line 397

Extra space between "assistant" and "or"

Line 498

"...slooppy. Inded..."