Definitional equality and local instance

Stream: general

[Chase Meadors]

Consider:

import order.complete_lattice
import order.lattice_intervals
example {α : Type} [complete_lattice α] (a k : α) (hak : a < k) : Prop :=
begin
  haveI : bounded_lattice ↥(set.Icc a k) := set.Icc.bounded_lattice (le_of_lt hak),
  have : (⟨a, ⟨le_refl a, le_of_lt hak⟩⟩ : set.Icc a k) < ⊤,
  exact hak,
end

I have a local instance that requires a hypothesis.
After I introduce it with haveI, it seems to "work" since \top (from order_top inferred from bounded_lattice) is acknowledged on the next line.
Now I want to prove the simple goal, which is trivial since \top in this bounded lattice is exactly k (or, ⟨k, whatever⟩). I feel like exact hak should close the goal but it doesn't work.
Drilling down with things like rw ←subtype.coe_lt_coe, simp gets down to a < ↑⊤, so it seems that it can't figure out what ↑⊤ is, even though it "should know". Am I missing something about how to work with local instances like this?

[Sebastien Gouezel]

You need to use letI instead of haveI.

[Sebastien Gouezel]

Otherwise, Lean records that there is an instance, but forgets the details of its definition.

[Chase Meadors]

Oh. Sure enough, that works!
What's the use of haveI then?

[Johan Commelin]

for propositions

[Chase Meadors]

Oh, I think I understand. Since you'd use have and let for propositions and data, respectively, it's the same here.