no goals
M : Type u_2
inst✝² : CommMonoidWithZero M
S : Submonoid M
N : Type ?u.3333984
inst✝¹ : CommMonoidWithZero N
P : Type ?u.3333990
inst✝ : CommMonoidWithZero P
p : Type u_1
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
⊢ liftOn 0 f H = f 0 1
rw [← mk_zero 1, liftOn_mk]