The algorithms presented in Lower Your Guards analyze pattern matching defi- nitions and detect uncovered cases, but also inaccessible and redundant right hand sides. Their implementation in the GHC spotted previously unknown bugs in real world code. While empirical validation over a large corpus of Haskell code corrob- orates the claim of correctness, the authors lack a precise formalization as well as a proof of that claim. This thesis establishes a precise notion of correctness and presents formal proofs that these algorithms are indeed correct. These proofs are formalized in Lean 3.