Rewrite type of term in function definition

Stream: new members

[Alex Keizer]

Is there a way to rewrite the type of a term in a function definition?

I'm getting the following error

type mismatch
  foo
has type
  motive Foo : Sort u
but is expected to have type
  motive Bar : Sort u

But I have a theorem that states

Foo = Bar

So is there a way to use this theorem to resolve the type mismatch?

EDIT: Forgot to mention, I'm working with lean 4

[Martin Dvořák]

If the theorem is called foobar and you have this error when applying something to your goal, just write:
rw foobar,

[Martin Dvořák]

Oh, sorry, you were probably asking about something else, right?

[Martin Dvořák]

Usually, it is better to post your code than to post your error.

[Reid Barton]

or ideally, post both

[Alex Keizer]

Yeah, I'm talking about a function definition, rather than a proof.

def List.Nil {α : Type} : List α
  := W.mk (A.Nil) (λ emp => Empty.rec (λ_ => List α) emp)

def List.rec {α : Type} {motive : List α → Sort u}
  (mNil : motive List.Nil)
  (mCons : (hd : α) → (tl: List α) → motive tl → motive (List.Cons hd tl))
    : (t : List α) → motive t
| W.mk (A.Nil) f => mNil  -- <-- mNil is of type `motive List.Nil`, but `motive W.mk Flist_A.Nil f)` is expected
| W.mk (A.Cons hd) f => _ -- not important yet

[Alex Keizer]

So I have a term mNil of type motive List.Nil which I want to return from my function that is declared to return motive W.mk ...,
which seems fine as List.Nil is equal to W.mk ...

[Alex Keizer]

I could of course change the type of mNil, but the goal is to hide the internal machinery, so that it seems like List.Nil and List.Cons are actual constructors, rather than wrappers around W ...

[Alex Keizer]

With List.rec the normal high-level recursor that one would expect an inductive type to have

[Alex Keizer]

Here is a more minimal example:

inductive Foo
  | X : (Empty → Nat) → Foo

def bar : Foo
  := Foo.X (λ emp => 1)

theorem foobar (foo : Foo):
  foo = bar :=
  by
    unfold bar
    cases foo
    apply congrArg
    funext x
    cases x

def func (motive : Foo → Type) (foo : Foo) (mBar : motive bar) : motive foo
  := mBar -- ERROR

Where the error is again

type mismatch
  mBar
has type
  motive bar : Type
but is expected to have type
  motive foo : Type

[Reid Barton]

You can use Eq.rec or something, but you're heading down a dark path

[Alex Keizer]

Thanks for the pointer, I'll see what I can work out