@zkproofs Yeah, tactics proofs are very write only for me. I guess you can kind of "embrace it", since you just need to be able to read the definition right, since you're confident the theorem is actually true.
@zkproofs I guess, an automated proof is not a substitute for explanation. (Nor is a pen and paper proof I guess)