Nested Inductive Type Resolution with Match Syntax Issue

Stream: new members

[Andrew Elsey]

Hi, essentially I have a nested inductive type with several type parameters. In the picture below, it is the prod case. The prod case has two nested arguments which determine the type parameters of the constructed term. The problem is when I go to write any function which matches on the constructors. I can't even write the case for the nested constructor without getting a type resolution error. To be more explicit, the function expects the matched value to be (fm K dim id_vec), but it's claiming the prod constructor stores a value of (fm K (dim1 + dim2) (add_maps id1 id2), where ideally I'd like Lean simply to figure out that (dim1 + dim2 = dim). Is there any way I can provide a proof of this or any attribute I'm unaware of? Anyone run into any similar problems? Note: I can, as shown in the second picture, use tactic mode to write function bodies instead of matching, so something works, but, unfortunately, I do need the match syntax for the recursion. Thank you to anyone with any insight here.

image.png

image.png

[Kevin Buzzard]

Can you post a #mwe rather than screenshots?

[Eric Wieser]

At a minimum you should move K [inhabited K] [field K] before the colon, unless the deriv you're not showing does something surprising

[Andrew Elsey]

Eric Wieser said:

At a minimum you should move K [inhabited K] [field K] before the colon, unless the deriv you're not showing does something surprising

I've been trying placing the K in several places (also as a variable, etc). That didn't seem to change the underlying problem, however. Oh well. Might just have to do a different approach. Thank you.

[Eric Wieser]

You'd likely get better help if you could provide a #mwe