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