M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type ?u.129008
inst✝¹ : CommMonoid N
P : Type ?u.129014
inst✝ : CommMonoid P
a : { x // x ∈ S }
⊢ 1 = mk (↑a) a
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type ?u.129008
inst✝¹ : CommMonoid N
P : Type ?u.129014
inst✝ : CommMonoid P
a : { x // x ∈ S }
⊢ mk (↑a) a = 1
symm
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type ?u.129008
inst✝¹ : CommMonoid N
P : Type ?u.129014
inst✝ : CommMonoid P
a : { x // x ∈ S }
⊢ ↑(r S) (1, 1) (↑a, a)
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type ?u.129008
inst✝¹ : CommMonoid N
P : Type ?u.129014
inst✝ : CommMonoid P
a : { x // x ∈ S }
⊢ 1 = mk (↑a) a
rw [← mk_one, mk_eq_mk_iff]
no goals
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type ?u.129008
inst✝¹ : CommMonoid N
P : Type ?u.129014
inst✝ : CommMonoid P
a : { x // x ∈ S }
⊢ ↑(r S) (1, 1) (↑a, a)
exact one_rel a