no goals
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type ?u.417122
inst✝ : CommMonoid P
f : M →* N
h : ∀ (y : { x // x ∈ S }), IsUnit (↑f ↑y)
x₁ x₂ : M
y₁ y₂ : { x // x ∈ S }
⊢ ↑f x₁ * ↑(↑(IsUnit.liftRight (MonoidHom.restrict f S) h) y₁)⁻¹ =
      ↑f x₂ * ↑(↑(IsUnit.liftRight (MonoidHom.restrict f S) h) y₂)⁻¹ ↔
    ↑f (x₁ * ↑y₂) = ↑f (x₂ * ↑y₁)
rw [mul_inv_right h, mul_assoc, mul_comm _ (f y₂), ← mul_assoc, mul_inv_left h, mul_comm x₂,
  f.map_mul, f.map_mul]