https://leanprover.github.io/live/latest/#code=import%20data.list%0Aopen%20list%0A%0Asection%20test_dependent%0A%0Avariables%20%7B%CE%B1%20:%20Type%7D%20%7Bl%20:%20list%20%CE%B1%7D%20%5Bdecidable_eq%20%CE%B1%5D%0A%20%20%20%20%20%20%20%20%20%20%7BP%20:%20%CE%B1%20%E2%86%92%20Prop%7D%20%5Bdecidable_pred%20P%5D%0A%20%20%20%20%20%20%20%20%20%20%7BQ%20:%20%CE%B1%20%E2%86%92%20Prop%7D%20%5Bdecidable_pred%20Q%5D%0A%20%20%20%20%20%20%20%20%20%20%7BR%20:%20%CE%B1%20%E2%86%92%20Prop%7D%20%5Bdecidable_pred%20R%5D%0A%0Alemma%20filter_partition%0A%20%20(h%20:%20%E2%88%80x,%20%C2%ACQ%20x%20%E2%86%94%20R%20x)%20:%0A%20%20length%20(filter%20P%20l)%20=%0A%20%20length%20(filter%20P%20(filter%20Q%20l))%20+%0A%20%20length%20(filter%20P%20(filter%20R%20l))%20:=%0Abegin%0A%20%20induction%20l%20with%20hd,%0A%20%20%20%20%7Bsimp%20only%20%5Badd_zero,%20list.filter_nil,%20list.length%5D%7D,%0A%20%20%20%20%7B%0A%20%20%20%20%20%20by_cases%20h%E2%82%81%20:%20R%20hd,%0A%20%20%20%20%20%20%20%20%7B%0A%20%20%20%20%20%20%20%20%20%20have%20:%20%C2%ACQ%20hd,%20from%20(h%20_).2%20h%E2%82%81,%0A%20%20%20%20%20%20%20%20%20%20by_cases%20h%E2%82%82%20:%20P%20hd;%20simp*,%0A%20%20%20%20%20%20%20%20%7D,%0A%20%20%20%20%20%20%20%20%7B%0A%20%20%20%20%20%20%20%20%20%20have%20:%20Q%20hd,%20from%20(not_iff_comm.1%20(h%20_)).1%20h%E2%82%81,%0A%20%20%20%20%20%20%20%20%20%20by_cases%20h%E2%82%82%20:%20P%20hd;%20simp*%0A%20%20%20%20%20%20%20%20%7D%0A%20%20%20%20%7D%0Aend%0A%0Alemma%20filter_partition_dependent%0A%20%20%7BP%20:%20%7Bx%20//%20x%20%E2%88%88%20l%7D%20%E2%86%92%20Prop%7D%20%5Bdecidable_pred%20P%5D%0A%20%20(h%20:%20%E2%88%80x,%20%C2%ACQ%20x%20%E2%86%94%20R%20x)%20:%0A%20%20length%20(filter%20(%CE%BB%20(x%20:%20%7Bx%20//%20x%20%E2%88%88%20l%7D),%20P%20x)%20(attach%20l))%20=%0A%20%20length%20(filter%20(%CE%BB%20(x%20:%20%7Bx%20//%20x%20%E2%88%88%20filter%20Q%20l%7D),%20P%20%E2%9F%A8x.1,%20mem_of_mem_filter%20x.2%E2%9F%A9)%20(attach%20(filter%20Q%20l)))%20+%0A%20%20length%20(filter%20(%CE%BB%20(x%20:%20%7Bx%20//%20x%20%E2%88%88%20filter%20R%20l%7D),%20P%20%E2%9F%A8x.1,%20mem_of_mem_filter%20x.2%E2%9F%A9)%20(attach%20(filter%20R%20l)))%20:=%0Abegin%0A%20%20resetI,%20induction%20l%20with%20hd%20tl%20ih,%0A%20%20%20%20%7Bsimp%20%5Battach%5D%7D,%0A%20%20%20%20%7B%0A%20%20%20%20%20%20--%20ih%20:%20%E2%88%80%20%7BP%20:%20%7Bx%20//%20x%20%E2%88%88%20tl%7D%20%E2%86%92%20Prop%7D%0A%20%20%20%20%20%20--%20but%20P%20:%20%7Bx%20//%20x%20%E2%88%88%20l%7D%0A%20%20%20%20%20%20admit%0A%20%20%20%20%7D%0Aend%0A%0Aend%20test_dependent