M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type ?u.513796
inst✝ : CommMonoid P
f : M →* N
hf : ∀ (y : { x // x ∈ S }), IsUnit (↑f ↑y)
y z : { x // x ∈ S }
h : (↑(IsUnit.liftRight (MonoidHom.restrict f S) hf) y)⁻¹ = (↑(IsUnit.liftRight (MonoidHom.restrict f S) hf) z)⁻¹
⊢ ↑f ↑z * ↑(↑(IsUnit.liftRight (MonoidHom.restrict f S) hf) z)⁻¹ = 1
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type ?u.513796
inst✝ : CommMonoid P
f : M →* N
hf : ∀ (y : { x // x ∈ S }), IsUnit (↑f ↑y)
y z : { x // x ∈ S }
h : (↑(IsUnit.liftRight (MonoidHom.restrict f S) hf) y)⁻¹ = (↑(IsUnit.liftRight (MonoidHom.restrict f S) hf) z)⁻¹
⊢ ↑f ↑y = ↑f ↑z
rw [← mul_one (f y), eq_comm, ← mul_inv_left hf y (f z) 1, h]
no goals
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type ?u.513796
inst✝ : CommMonoid P
f : M →* N
hf : ∀ (y : { x // x ∈ S }), IsUnit (↑f ↑y)
y z : { x // x ∈ S }
h : (↑(IsUnit.liftRight (MonoidHom.restrict f S) hf) y)⁻¹ = (↑(IsUnit.liftRight (MonoidHom.restrict f S) hf) z)⁻¹
⊢ ↑f ↑z * ↑(↑(IsUnit.liftRight (MonoidHom.restrict f S) hf) z)⁻¹ = 1
exact Units.inv_mul (IsUnit.liftRight (f.restrict S) hf z)⁻¹