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"
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.