specifying implicit type

Stream: Berkeley Lean Seminar

[Sean Gonzales]

I am using the following line of code in a proof:
exact normal.is_integral _inst_4.to_normal (x : L),
I'm receiving an error since the theorem normal.is_integral is expecting a hypothesis of type normal F ↥K but my hypothesis _inst_4.to_normal is of type normal F L. I assumed writing x : L would specify that we should be using L rather than K, but I'm still receiving the same error. How do I specify the type?

[Junyan Xu]

I presume x.1 should work, and (↑x : L) might work.

[Kyle Miller]

(For that suggestion doesn't help for whatever reason, consider a #mwe if you can!)

[Thomas Browning]

A bad way is to start with have := @normal.is_integral, and then fill in the blanks one by one, allowing you to specify all of the types.