unfolding inherited infix

Stream: general

[Peter Nelson]

I am trying to define an instance by adding a field to an existing instance, in an example like the following

import order.lattice_intervals
open set

instance Icc.distrib_lattice {α : Type} [distrib_lattice α] {a b : α} :
  distrib_lattice (Icc a b) :=
{ le_sup_inf := λ x y z, by {cases x with x₀ hx, cases y with y₀ hy, cases z with z₀ hz, sorry },
.. Icc.lattice}

Before the sorry, my goal is
⊢ (⟨x₀, hx⟩ ⊔ ⟨y₀, hy⟩) ⊓ (⟨x₀, hx⟩ ⊔ ⟨z₀, hz⟩) ≤ ⟨x₀, hx⟩ ⊔ ⟨y₀, hy⟩ ⊓ ⟨z₀, hz⟩.

I can't find any rewrite/simp/unfold-type statement to access the definition of ⊔, that is, ⟨x₀, hx⟩ ⊔ ⟨y₀, hy⟩ = ⟨x₀ ⊔ y₀, _⟩. How do I do this?

Similarly, is there a way to handle goals like this without the cases?

(This is a MWE; in fact le_sup_inf := λ x y z, distrib_lattice.le_sup_infworks above; but only because of defeq. How would I handle a less trivial goal?).

[Eric Wieser]

docs#subtype.coe_le_coe (in reverse) should make progress

[Eric Wieser]

I think you can maybe just docs#function.injective.distrib_lattice here with f = coe