Converse of linear_equiv.congr_arg

Stream: Is there code for X?

[Winston Yin]

Given a linear equiv f : M ≃ₗ[R] M₂, is there an easy way to prove x = y from f.to_fun x = f.to_fun y (note the latter is without forall x y)? In the same vein, I want to apply f.symm to both sides of x = y using linear_equiv.congr_arg, but all the arguments are implicit...

[Eric Wieser]

I think you want f.injective

[Eric Wieser]

docs#linear_equiv.injective

[Winston Yin]

But let's say I'm still trying to apply a linear map g to x = y. How can I use linear_equiv.congr_arg to achieve that?

[Winston Yin]

Should I use the congr_arg for regular functions?

[Eric Wieser]

Can you give a mwe?

[Eric Wieser]

You might be after tactic#apply_fun, which somewhat turns this problem on its head as "I need this goal state, tell me what I have to prove"

[Winston Yin]

tactic#apply_fun is the easiest in my case. Thanks! Btw, how did you link to the doc?

[Eric Wieser]

By typing exactly what you see on your screen. In general though, when not on mobile you can quote someone's post to see how they typed it