This is why I prefer Agda, where everything comes down to pattern matching.

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"

	▲	solomonb 10 days ago \| parent [-]
		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.