no goals
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type ?u.3266990
inst✝¹ : CommMonoid N
P : Type ?u.3266996
inst✝ : CommMonoid P
p : Sort u
f : M → { x // x ∈ S } → p
H : ∀ {a c : M} {b d : { x // x ∈ S }}, ↑(r S) (a, b) (c, d) → f a b = f c d
a : M
b : { x // x ∈ S }
⊢ liftOn (Submonoid.LocalizationMap.mk' (monoidOf S) a b) f H = f a b
rw [← mk_eq_monoidOf_mk', liftOn_mk]