M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type ?u.325903
inst✝ : CommMonoid P
f : M →* N
h : ∀ (y : { x // x ∈ S }), IsUnit (↑f ↑y)
y : { x // x ∈ S }
w z : N
⊢ ↑(↑(IsUnit.liftRight (MonoidHom.restrict f S) h) y)⁻¹ * w = z ↔ w = ↑f ↑y * z
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type ?u.325903
inst✝ : CommMonoid P
f : M →* N
h : ∀ (y : { x // x ∈ S }), IsUnit (↑f ↑y)
y : { x // x ∈ S }
w z : N
⊢ w * ↑(↑(IsUnit.liftRight (MonoidHom.restrict f S) h) y)⁻¹ = z ↔ w = ↑f ↑y * z
rw [mul_comm]
no goals
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type ?u.325903
inst✝ : CommMonoid P
f : M →* N
h : ∀ (y : { x // x ∈ S }), IsUnit (↑f ↑y)
y : { x // x ∈ S }
w z : N
⊢ ↑(↑(IsUnit.liftRight (MonoidHom.restrict f S) h) y)⁻¹ * w = z ↔ w = ↑f ↑y * z
exact Units.inv_mul_eq_iff_eq_mul (IsUnit.liftRight (f.restrict S) h y)