> So, even though 1+1=3 is surely false, we could prove it in Lean like so: “Let’s assume that ¬(1+1=3). But this leads to a contradiction: coll_conj and ¬coll_conj. We can therefore deduce that our assumption must be false, so 1+1=3.”

I was following along with the logic, but got completely lost here. Can anyone explain how does the assumption "1 plus 1 is equal to three is false" lead to a contradiction? What is the contradiction here exactly?