Commit 2020-05-14 00:19 f7cb3634

refactor(order/lattice): adjust proofs to avoid choice (#2666) For foundational category theoretic reasons, I'd like these lattice properties to avoid choice. In particular, I'd like the proof here: https://github.com/leanprover-community/mathlib/pull/2665 to be intuitionistic. For most of them it was very easy, eg changing finish to simp. For sup_assoc and inf_assoc it's a bit more complex though - for inf_assoc I wrote out a term mode proof, and for sup_assoc I used ifinish. I realise ifinish is deprecated because it isn't always intuitionistic, but in this case it did give an intuitionistic proof. I think both should be proved the same way, but I'm including one of each to see which is preferred.