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