no goals
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r : R
s t : { x // x ∈ S }
⊢ r /ₒ s * (1 /ₒ t) = r /ₒ (t * s)
simp [oreDiv_mul_char r 1 s t 1 s (by simp)]
no goals
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r : R
s t : { x // x ∈ S }
⊢ 1 * ↑s = ↑s * 1
simp