Restricting a function f : α → N to the unit group Nˣ

Stream: Is there code for X?

[Mitchell Lee]

Any monoid homomorphism f : M →* N can be restricted to the unit group Nˣ, provided we have (hf : ∀ (x : M), IsUnit (f x)). This is IsUnit.liftRight.

What if the M is replaced by an arbitrary type α, and the monoid homomorphism f by an arbitrary function α → N?

[Johan Commelin]

In that case I don't think there is API for that

[Eric Wieser]

Does the lift tactic work?

[Mitchell Lee]

Ah, I didn't know about that one; thanks