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