M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type ?u.3263012
inst✝¹ : CommMonoid N
P : Type ?u.3263018
inst✝ : CommMonoid P
x : M
y : { x // x ∈ S }
⊢ mk (x * ↑y) (1 * y) = mk x 1
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type ?u.3263012
inst✝¹ : CommMonoid N
P : Type ?u.3263018
inst✝ : CommMonoid P
x : M
y : { x // x ∈ S }
⊢ mk x y * ↑(Submonoid.LocalizationMap.toMap (monoidOf S)) ↑y = ↑(Submonoid.LocalizationMap.toMap (monoidOf S)) x
rw [← mk_one_eq_monoidOf_mk, ← mk_one_eq_monoidOf_mk, mk_mul x y y 1, mul_comm y 1]
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type ?u.3263012
inst✝¹ : CommMonoid N
P : Type ?u.3263018
inst✝ : CommMonoid P
x : M
y : { x // x ∈ S }
⊢ mk (x * ↑y) (1 * y) = mk (x * 1) (1 * 1)
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type ?u.3263012
inst✝¹ : CommMonoid N
P : Type ?u.3263018
inst✝ : CommMonoid P
x : M
y : { x // x ∈ S }
⊢ mk (x * ↑y) (1 * y) = mk x 1
conv => rhs ; rw [← mul_one 1] ; rw [← mul_one x]
no goals
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type ?u.3263012
inst✝¹ : CommMonoid N
P : Type ?u.3263018
inst✝ : CommMonoid P
x : M
y : { x // x ∈ S }
⊢ mk (x * ↑y) (1 * y) = mk (x * 1) (1 * 1)
exact mk_eq_mk_iff.2 (Con.symm _ <| (Localization.r S).mul (Con.refl _ (x, 1)) <| one_rel _)