M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type ?u.76919
inst✝¹ : CommMonoid N
P : Type ?u.76925
inst✝ : CommMonoid P
a c : M
b d : { x // x ∈ S }
⊢ Mul.mul (mk a b) (mk c d) = mk (a * c) (b * d)
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type ?u.76919
inst✝¹ : CommMonoid N
P : Type ?u.76925
inst✝ : CommMonoid P
a c : M
b d : { x // x ∈ S }
⊢ Localization.mul S (mk a b) (mk c d) = mk (a * c) (b * d)
rw [Localization.mul]
no goals
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type ?u.76919
inst✝¹ : CommMonoid N
P : Type ?u.76925
inst✝ : CommMonoid P
a c : M
b d : { x // x ∈ S }
⊢ Mul.mul (mk a b) (mk c d) = mk (a * c) (b * d)
rfl