no goals
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type u_1
f : M × { x // x ∈ S } → M × { x // x ∈ S } → α
wd : ∀ (p q p' q' : M × { x // x ∈ S }), p ≈ p' → q ≈ q' → f p q = f p' q'
m m' : M
s s' : { x // x ∈ S }
⊢ liftOn₂ (mk m s) (mk m' s') f wd = f (m, s) (m', s')
convert Quotient.liftOn₂_mk f wd _ _