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 } → α
wd : ∀ (p p' : M × { x // x ∈ S }), p ≈ p' → f p = f p'
m : M
s : { x // x ∈ S }
⊢ liftOn (mk m s) f wd = f (m, s)
convert Quotient.liftOn_mk f wd ⟨m, s⟩