congr_arg

Stream: maths

[Ashvni Narayanan]

I used apply congr_arg in some of my proofs. At some point, I decided to open locally_constant. The following error occured :

ambiguous overload, possible interpretations
  congr_arg
  locally_constant.congr_arg
Additional information:
c:\Users\ashvn\my_project1\mathlib\src\number_theory\weight_space.lean: context: switched to basic overload resolution where arguments are elaborated without any information about the expected type because expected type was not available

How does one deal with this?

I would be grateful for any help, thank you!

[Riccardo Brasca]

If you want to use congr_arg without any namespace just write _root_.congr_arg.

[Ashvni Narayanan]

I see, thank you!

[Riccardo Brasca]

The error means that Lean doesn't understand if you want to use congr_arg or locally_constant.congr_arg, beacuse after opening locally_constant both can be used by typing congr_arg.

[Eric Wieser]

This might mean that docs#locally_constant.congr_arg should be protected.

[Yury G. Kudryashov]

And/or that we should add fun_like to many more types.

[Yaël Dillies]

For reference, https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Morphism.20refactor