This is one of the laws where greedy completion has been shown (via extensive SAT-solver calculations) to work, but only barely. As such, the proof of anti-implications from these laws could be extremely lengthy, to the extent that Lean may struggle to verify them. See this discussion.