Joachim Breitner and Lean FRO describe the proof behind con-leche checker