Surprise noncomputable building an ∃ from a Subtype

Stream: lean4

[Robert Maxton]

Seems to be another case of https://github.com/leanprover/lean4/issues/2104; I've already added my MWE to the thread.

import Mathlib.Tactic.Common

structure Iso (α : Type) (β : Type) :=
  (to_fun : α → β)
  (inv_fun : β → α)
  (left_inv : inv_fun ∘ to_fun = id)
  (right_inv : to_fun ∘ inv_fun = id)

def HasInverse {α β: Type} (f: α → β) := ∃ (g: β → α), (g ∘ f = id) ∧ (f ∘ g = id)

def Invertible (α β: Type) := {f: α → β // HasInverse f}

theorem Invertible.ofIso {α β: Type} (iso: Iso α β): Invertible α β :=
  ⟨iso.to_fun, ⟨iso.inv_fun, ⟨iso.left_inv, iso.right_inv⟩⟩⟩

instance : Coe (Iso α β) (Invertible α β) := ⟨Invertible.ofIso⟩

gives a weird ... 'noncomputable' because it depends on 'Invertible.ofIso' error. Replacing the reference with its definition

instance : Coe (Iso α β) (Invertible α β) := ⟨λ i ↦ ⟨i.to_fun, ⟨i.inv_fun, ⟨i.left_inv, i.right_inv⟩⟩⟩⟩

works as a workaround.

[Kim Morrison]

Invertible.ofIso should be a def, not a theorem.

[Robert Maxton]

Scott Morrison said:

Invertible.ofIso should be a def, not a theorem.

... ah. I see. In retrospect it should have been obvious that, since theorems don't require a noncomputable modifier, they would probably be assumed noncomputable. Oops.