You can absolutely use pattern matching in Lean instead of tactics, if you prefer to write the proof that is closer to "what is going on under the hood"

yeah i didn't mean to imply you cannot do that, but tactics seem to be highly encouraged.

I'm actually a big fan of Lean, I just like it more as a programming language for writing programs with dependent types then as a proof checker.