no goals
M : Type u_1
inst✝² : CommMonoidWithZero M
S : Submonoid M
N : Type ?u.3329406
inst✝¹ : CommMonoidWithZero N
P : Type ?u.3329412
inst✝ : CommMonoidWithZero P
x : { x // x ∈ S }
⊢ ↑(0, 1).snd * (0, x).fst = ↑(0, x).snd * (0, 1).fst
simp