Eta expansion in the pattern lambda calculus
This is not a complete answer; it is a comment that got too large.

If you extend typed lambda calculus with products with projective eliminators (ie, product eliminators fst(e) and snd(e)), there are no basically issues whatsoever. The reason it took so long to figure out is because it turns out to be more natural to do eta expansions rather than eta reductions.  See Barry Jay's The Virtues of Eta Expansion.

If you want products to have a pattern-style eliminator 

let (a,b) = e in t 


Then matters are more complex. The primary difficulty with pattern matching are the commuting conversions. That is, these calculi have the equation 

C[let (a,b) = e in t] === let (a,b) = e in C[t]


and figuring out (a)  which context C[-] to use and (b) how to orient this equation gets tricky. IMO, the state of the art for rewriting-style approaches are Sam Lindley's  Extensional Rewriting with Sums and Gabriel Scherer's Deciding Equivalence with Sums and the Empty Type, both of which consider the typed lambda calculus with both products and sums.