M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type ?u.45548
inst✝¹ : CommMonoid N
P : Type ?u.45554
inst✝ : CommMonoid P
x y : M × { x // x ∈ S }
⊢ ↑(r' S) x y ↔ ∃ c, ↑c * (↑y.snd * x.fst) = ↑c * (↑x.snd * y.fst)
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type ?u.45548
inst✝¹ : CommMonoid N
P : Type ?u.45554
inst✝ : CommMonoid P
x y : M × { x // x ∈ S }
⊢ ↑(r S) x y ↔ ∃ c, ↑c * (↑y.snd * x.fst) = ↑c * (↑x.snd * y.fst)
rw [r_eq_r' S]
no goals
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type ?u.45548
inst✝¹ : CommMonoid N
P : Type ?u.45554
inst✝ : CommMonoid P
x y : M × { x // x ∈ S }
⊢ ↑(r' S) x y ↔ ∃ c, ↑c * (↑y.snd * x.fst) = ↑c * (↑x.snd * y.fst)
rfl