no goals
α : Type ?u.30089
M : Type u
N : Type v
P : Type w
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
f : M →* N
g : M → Nˣ
h : ∀ (x : M), ↑(g x) = ↑f x
x : M
⊢ ↑f x * ↑(↑(liftRight f g h) x)⁻¹ = 1
rw [Units.mul_inv_eq_iff_eq_mul, one_mul, coe_liftRight]