Typing issue in Lean 4 through Equiv

Stream: lean4

[Arien Malec]

I'm working through logic.equiv.option & there's some Lean 3 code:

if h : (e (some x)).is_some
  then option.get h

which to my mind scans like Rust's if letthrough an Equiv?

On the Lean 3 side, h has type h : ↥((⇑e (some x)).is_some), (e is e : option α ≃ option β & x is α).

in Lean 4 the resulting type for h is h : isSome (toFun e (some x)) = true doesn't let Lean 4 know that Option.get h is typed β

(the error is

type mismatch
  Option.get ?m.2294
has type
  isSome ?m.2294 = true → ?m.2127 : Type ?u.2126
but is expected to have type
  β : Type ?u.1989

)

Any pointers?

(branch arienmmalec/port-equivfunctor has the in progress port for Mathlib.Control.EquivFunctor)

[Sebastian Ullrich]

Take a look at Option.get's signature: it takes two explicit parameters

[Scott Morrison]

I think we probably ought to add a (deprecated?) shim that we can #align to, or if someone is brave, backport this change.