Quantum Hoare Logic (QHL) provides a rigorous framework for reasoning about quantum programs using Hoare triples, but its reliance on Hermitian matrices severely limits scalability. We propose an automata-based approach to automate the generation of proof trees for QHL triples by encoding Hermitian matrices via sets of eigenvectors and eigenvalues using level-synchronized tree automata (LSTAs). Our method exploits the structural compactness of LSTAs to represent an exponential number of quantum basis vectors using a linear-size automaton. This compact encoding supports key proof rules of QHL—including initialization, unitary transformation, and loop reasoning—while facilitating automation through existing tree automata operations. We further adapt quantum gate transformation techniques and develop a specialized inclusion-checking procedure to verify the Loewner order, critical for applying the rule of consequence. As a proof-of-concept, we demonstrate our framework on a quantum repeat-until-success coin-flip protocol. This example highlights the automated construction of aQHL proof trees, showcasing how the system can compute unknown projectors and compose local triples into a full proof using automata manipulations. Our current framework supports applied QHL (aQHL), with ongoing work extending toward full QHL automation. The results show promising steps toward scalable, mechanical verification of quantum programs.