# Zulip Chat Archive

## Stream: new members

### Topic: convincing lean something is ok

#### Ned Summers (Aug 20 2018 at 15:15):

I'm trying to construct a function `f : a → b`

(as part of an instance of a structure) with two types a and b and non-trivially I have that for some type c defined differently in fact `b=c`

(and I can prove that if needed).

How can I let lean know that in fact, what might appear to be of type `a → c`

(being given by `λ x , y`

, for some `y : c`

) is in fact totally fine and fulfils the requirement for being of type `a → b`

?

#### Simon Hudon (Aug 20 2018 at 15:18):

One way do it is to use `cast`

. It does get in the way when trying to reason about the function but it does what you said. You could do it as `cast (by subst c) f`

#### Simon Hudon (Aug 20 2018 at 15:21):

I sometimes define local notations for this kind of cast:

local prefix `♯`:0 := cast (by cc <|> solve_by_elim)

#### Ned Summers (Aug 21 2018 at 09:48):

Ah ok, thanks. I'm not familiar with using subst, how would I include a proof that b = c in this? Currently, I'm being told "subst tactic failed, given expression is not a local constant". Apologies, I am very much a beginning.

#### Ned Summers (Aug 21 2018 at 10:21):

Never mind, managed to get that sorted!

#### Ned Summers (Aug 21 2018 at 10:39):

I'm not sure if this is what you originally meant, Simon, but I ended up solving this with `λ x , cast( ... ) y`

, using my proof in the brackets. However, if I also had properties previously expressed about y, how do I go about using these for the cast version?

For example (fairly close to what I'm doing), if y were in the center of a group, is it possible to prove that for some other member x, cast _ y * x = x * cast _ y? Or do we lose this information in casting?

#### Kevin Buzzard (Aug 21 2018 at 13:31):

Maybe you should take a look at https://leanprover.github.io/theorem_proving_in_lean/tactics.html#rewriting

Last updated: May 08 2021 at 09:11 UTC