convincing lean something is ok

Stream: new members

[Ned Summers]

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]

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]

I sometimes define local notations for this kind of cast:

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

[Ned Summers]

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]

Never mind, managed to get that sorted!

[Ned Summers]

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]

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