R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type ?u.817480
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
x y : { x // x ∈ M }
⊢ mk' S (↑y * ↑x) (y * x) = 1
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type ?u.817480
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
x y : { x // x ∈ M }
⊢ mk' S (↑x) y * mk' S (↑y) x = 1
rw [← mk'_mul, mul_comm]
no goals
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type ?u.817480
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
x y : { x // x ∈ M }
⊢ mk' S (↑y * ↑x) (y * x) = 1
exact mk'_self _ _