Strange instance problem with distributive lattice

Stream: general

[Chase Meadors]

The following gives a strange type mismatch error:

import order.complete_lattice
example {α : Type*} [distrib_lattice α] [complete_lattice α] {x y z : α} :
  x ⊓ (y ⊔ z) = x ⊓ y ⊔ x ⊓ z := inf_sup_left

Replacing inf_sup_left with the more explicit @inf_sup_left α _ x y z yields a very very long type mismatch error.

Upon inspection, removing the [complete_lattice α] instance from the hypothesis makes everything fine. What could be going on here?

[Sebastien Gouezel]

You have two different lattice structures (coming from your two instances), for which the operations are completely unrelated. So Lean is confused.

[Chase Meadors]

Hm, the class tree is a bit complicated here, but I thought both extended has_sup and has_inf all the way down, so that these operators would be unambiguous. My ignorance of the more technical aspects of type classes might be showing here though; I'm not 100% sure what you mean.
In context, I'd like to work with a complete lattice that is distributive, and rewrite somewhere with this lemma.

[Eric Wieser]

The fact that both extend has_sup is exactly the problem. Your lemma doesn't have anything that says the two sups are the same.

[Eric Wieser]

Just like if you take two integers as an argument, lean won't assume they are equal

[Chase Meadors]

Oh, I see! That makes sense. I'm specifying two (potentially completely unrelated) structures on α.

[Rémy Degenne]

There is a docs#complete_distrib_lattice class, which might interest you

[Rémy Degenne]

for other code that you may have I mean. It is not useful for that example.

[Chase Meadors]

Right. In my case I want to specifically avoid the _infinite_ distributive property, as that's part of / related to the conclusions. But this discussion clears things up and I think I can find a way to make things work now.