bot_eq_zero in complete lattice

Stream: mathlib4

[Peter Nelson]

The following seems to be missing lemmas, but I am a bit suspicious. Is there a reason they shouldn't exist?

import Mathlib

lemma bot_eq_zero''' {R : Type*} [AddCommMonoid R] [CompleteLattice R] [IsOrderedAddMonoid R]
  [CanonicallyOrderedAdd R] : (⊥ : R) = 0 :=
  -- `exact?`, `simp` and all versions of `bot_eq_zero` fail here
  bot_le.antisymm <| zero_le _

@[simp]
lemma bot_eq_zero'''' {R : Type*} [AddCommMonoid R] [CompleteLinearOrder R] [IsOrderedAddMonoid R]
  [CanonicallyOrderedAdd R] : (⊥ : R) = 0 :=
  -- `exact?`, `simp` and all existing versions of `bot_eq_zero` fail here
  bot_eq_zero'''

[Eric Wieser]

You're in trouble for the first one, there's an instance diamond

[Eric Wieser]

docs#CanonicallyOrderedAdd.toOrderBot is a bad instance

[Eric Wieser]

(it used to be ok, but #17444 unbundled it which made it bad)

[Yaël Dillies]

Oh yeah, I have fixed that instance once already :raised:

[Eric Wieser]

(cc @Yuyang Zhao)

[Peter Nelson]

I don't think I've wrapped my head around this. What does the 'good' version of this look like?

[Eric Wieser]

The good version is that CanonicallyOrderedAdd.toOrderBot is deleted and your statements above are solved with bot_eq_zero

[Peter Nelson]

Ok, I can remove it. Is it better as a def or just removed completely?

[Peter Nelson]

The latter involves fixing a few proofs that use lemmas about OrderBot.

[Yuyang Zhao]

#24094 remove them.

[Eric Wieser]

As does #24090

[Eric Wieser]

@Peter Nelson, you made the mistake of not linking to the PR from the Zulip thread to prevent someone else repeating your work, while @Yuyang Zhao, you forgot to link in the other direction!

[Yuyang Zhao]

How about merging your changes that avoid OrderBot assumptions into #24094 and adding co-authored-by? @Peter Nelson

[Peter Nelson]

Doh! I got distracted while working on the PR and forgot to link it. Thanks for adding me and my code to yours anyway, @Yuyang Zhao .

[vxctyxeha]

:tada: