case h.e'_2.h.e'_5
R : Type u_2
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_1
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type ?u.3731
inst✝¹ : CommSemiring P
x : R
inst✝ : Away x S
⊢ ↑(algebraMap R S) x = mk' S (↑{ val := x, property := (_ : x ∈ Submonoid.powers x) }) 1
R : Type u_2
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_1
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type ?u.3731
inst✝¹ : CommSemiring P
x : R
inst✝ : Away x S
⊢ ↑(algebraMap R S) x * invSelf x = 1
convert IsLocalization.mk'_mul_mk'_eq_one (M := Submonoid.powers x) (S := S) _ 1
case h.e'_2.h.e'_5
R : Type u_2
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_1
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type ?u.3731
inst✝¹ : CommSemiring P
x : R
inst✝ : Away x S
⊢ mk' S (↑{ val := x, property := (_ : x ∈ Submonoid.powers x) }) 1 = ↑(algebraMap R S) x
case h.e'_2.h.e'_5
R : Type u_2
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_1
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type ?u.3731
inst✝¹ : CommSemiring P
x : R
inst✝ : Away x S
⊢ ↑(algebraMap R S) x = mk' S (↑{ val := x, property := (_ : x ∈ Submonoid.powers x) }) 1
symm
no goals
case h.e'_2.h.e'_5
R : Type u_2
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_1
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type ?u.3731
inst✝¹ : CommSemiring P
x : R
inst✝ : Away x S
⊢ mk' S (↑{ val := x, property := (_ : x ∈ Submonoid.powers x) }) 1 = ↑(algebraMap R S) x
apply IsLocalization.mk'_one