The classical congruence result of Lucas for the binomial coefficients "n choose m" modulo a prime p shows that looking at the base-p representations of n and m is often an efficient way to determine divisibility properties of the binomial coefficients modulo p. Many authors have studied divisibility properties of famous combinatorial sequences along these lines. For instance, Alter and Kubota (1971) studied the Catalan numbers modulo p. Deutsch and Sagan (2006) looked at a variety of other sequences, such as the Motzkin numbers, central Delannoy numbers, Apery numbers, etc. Rowland and Yassawi (2015) and Rowland and Zeilbeger (2014) showed that finite automata may be the most appropriate way to describe congruence properties of these types of sequences. In this talk we show how to combine the method of Rowland and Zeilberger with the theorem prover Walnut, which can prove many properties of so-called "automatic sequences", to give very quick, fully automated proofs of some of these congruence properties. In some cases we can prove stronger properties regarding the patterns appearing in these sequences modulo p than have been obtained so far using conventional proof techniques.