R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type ?u.919061
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type u_2
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
g : R →+* P
h : ∀ (y : { x // x ∈ M }), IsUnit (↑g ↑y)
y : { x // x ∈ M }
w z₁ z₂ : P
⊢ w + ↑(MonoidHom.restrict (↑g) M) y * z₁ = ↑(MonoidHom.restrict (↑g) M) y * z₂ ↔ w + ↑g ↑y * z₁ = ↑g ↑y * z₂
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type ?u.919061
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type u_2
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
g : R →+* P
h : ∀ (y : { x // x ∈ M }), IsUnit (↑g ↑y)
y : { x // x ∈ M }
w z₁ z₂ : P
⊢ w * ↑(↑(IsUnit.liftRight (MonoidHom.restrict (↑g) M) h) y)⁻¹ + z₁ = z₂ ↔ w + ↑g ↑y * z₁ = ↑g ↑y * z₂
rw [mul_comm, ← one_mul z₁, ← Units.inv_mul (IsUnit.liftRight (g.toMonoidHom.restrict M) h y),
  mul_assoc, ← mul_add, Units.inv_mul_eq_iff_eq_mul, Units.inv_mul_cancel_left,
  IsUnit.coe_liftRight]
no goals
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type ?u.919061
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type u_2
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
g : R →+* P
h : ∀ (y : { x // x ∈ M }), IsUnit (↑g ↑y)
y : { x // x ∈ M }
w z₁ z₂ : P
⊢ w + ↑(MonoidHom.restrict (↑g) M) y * z₁ = ↑(MonoidHom.restrict (↑g) M) y * z₂ ↔ w + ↑g ↑y * z₁ = ↑g ↑y * z₂
simp [RingHom.toMonoidHom_eq_coe, MonoidHom.restrict_apply]