How to tell Lean preorders from different sources are same?

Stream: mathlib4

[Wen Yang]

import Mathlib.Data.Set.Intervals.Image
import Mathlib.Order.CompleteLatticeIntervals
import Mathlib.Topology.Order.Basic

open TopologicalSpace Function Set Topology
universe u

variable {α : Type u} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α]
  {δ : Type*} [LinearOrder δ] [TopologicalSpace δ] [OrderClosedTopology δ]

theorem A [BoundedOrder α] {f : α → δ} (hf_c : Continuous f)
    (hf : f ⊥ ≤ f ⊤) (hf_i : Injective f) : StrictMono f := sorry

theorem B {a b : α} {f : α → δ}
    (hab : a ≤ b) (hfab : f a ≤ f b)
    (hf_c : ContinuousOn f (Icc a b)) (hf_i : InjOn f (Icc a b)) :
    StrictMonoOn f (Icc a b) := by
  haveI := Icc.completeLinearOrder hab
  refine StrictMono.of_restrict ?_
  set g : Icc a b → δ := Set.restrict (Icc a b) f
  have hgab : g ⊥ ≤ g ⊤ := by sorry
  exact A (f := g) hf_c.restrict hgab hf_i.injective

Error occurs in the last line:

type mismatch
  A (ContinuousOn.restrict hf_c) hgab (InjOn.injective hf_i)
has type
  StrictMono g : Prop
but is expected to have type
  StrictMono g : Prop

The reason is that the first StrictMono g is

@StrictMono (↑(Icc a b)) δ PartialOrder.toPreorder PartialOrder.toPreorder g : Prop

while the second StrictMono g is

@StrictMono (↑(Icc a b)) δ (Subtype.preorder fun x ↦ x ∈ Icc a b) PartialOrder.toPreorder g : Prop

It seems that Lean does not realize that the Preorder obtained from PartialOrder on Icc a b and the Subtype.preorder inherited from α are the same.
What should I do?

[Junyan Xu]

Just replace haveI := Icc.completeLinearOrder hab by letI.

[Wen Yang]

Junyan Xu 发言道：

Just replace haveI := Icc.completeLinearOrder hab by letI.

It works! It is really amazing! Thank you very much! :smiley:

[Junyan Xu]

I'm sorry it took so long to get the question answered. It's a pretty common mistake so I'd expect it got answered quickly. What's happening here is that haveI behaves like lemma/theorem which are intended for proofs, so they forget the term (proof) and only remember its type (statement), while letI behaves like def, which is intended for data, so they remember the term (data) as well as its type. In this particular case, haveI := Icc.completeLinearOrder hab forgets the term Icc.completeLinearOrder hab and only remembers its type CompleteLinearOrder ↑(Icc a b); if you try have : this = Icc.completeLinearOrder hab := rfl you will also get a type mismatch error.

[Kevin Buzzard]

If there were a core linter for this then the problem would basically go away