What am I doing wrong with comprehension coercion?

Stream: general

[Sina]

What am I doing wrong here? I want to specialize Schröder-Bernstein to two simple functions between Icc (0 : ℝ) 1 and Ico (0 : ℝ) 1, but I get the following error

argument
  f
has type
  ↑(Icc 0 1) → ↑(Ico 0 1) : Type
but is expected to have type
  ↑(Icc 0 1) → ↑(Ico 0 1) : Type

Here's my mwe:

import Mathlib.Tactic
open Set
open Function
noncomputable section

theorem schroeder_bernstein (f : α → β) (g : β → α) :
Injective f →  Injective g →  ∃ (h : α → β), Bijective h :=
by
    sorry

def f : Icc (0 : ℝ) 1 → Ico (0 : ℝ) 1 := fun x =>
  ⟨x.val/2, by
    obtain ⟨x, hx⟩ := x; simp at hx ⊢; constructor <;> linarith⟩

lemma inj_f : Injective f := by
  intro x y h
  simp [f] at h
  ext
  linarith

def g : Ico (0 : ℝ) 1 → Icc (0 : ℝ) 1 := fun x =>
  ⟨x.val, by
    obtain ⟨x, hx⟩ := x; simp at hx ⊢; constructor <;> linarith⟩

lemma inj_g : Injective g := by
  intro x y h
  simp [g] at h
  ext
  linarith

theorem my_bij : ∃ (h : Icc 0 1 → Ico 0 1), Bijective h :=
by
  exact schroeder_bernstein f g inj_f inj_g
  --apply schroeder_bernstein f g

[Eric Wieser]

Your final statement ∃ (h : Icc 0 1 → Ico 0 1) is about the natural numbers; is this what you wanted?

[Sina]

Eric Wieser said:

Your final statement ∃ (h : Icc 0 1 → Ico 0 1) is about the natural numbers; is this what you wanted?

Oh, I see. When I change it to ∃ (h : Icc (0 : ℝ) 1 → Ico (0 : ℝ) 1), Bijective h it works. Thanks! For future, how do i detect such silly mistakes? Or, how did you find this out? I think the error message was not very helpful in this case.

[Eric Wieser]

Here I just guessed because this type of thing happens all the time, but you can check by hovering over the error message

[Eric Wieser]

In this case, hovering over the two 0s will show you that they are different

[Sina]

Eric Wieser said:

In this case, hovering over the two 0s will show you that they are different

This is great! I almost never did this, but seems very useful.