M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type ?u.78772
inst✝¹ : CommMonoid N
P : Type ?u.78778
inst✝ : CommMonoid P
⊢ mk 1 1 = One.one
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type ?u.78772
inst✝¹ : CommMonoid N
P : Type ?u.78778
inst✝ : CommMonoid P
⊢ mk 1 1 = Localization.one S
rw [Localization.one]
no goals
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type ?u.78772
inst✝¹ : CommMonoid N
P : Type ?u.78778
inst✝ : CommMonoid P
⊢ mk 1 1 = One.one
rfl