no goals
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type ?u.915559
inst✝ : CommMonoid P
f : LocalizationMap S N
x₁ x₂ : M
y : { x // x ∈ S }
⊢ ↑(toMap f) x₁ * mk' f x₂ y = mk' f (x₁ * x₂) y
rw [← mk'_one, ← mk'_mul, one_mul]