R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r : R
hr : r ∈ S
⊢ ∃ u v, 1 * ↑u = r * v ∧ ↑1 * ↑u = ↑{ val := r, property := hr } * v
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r : R
hr : r ∈ S
⊢ r /ₒ { val := r, property := hr } = 1
rw [OreLocalization.one_def, oreDiv_eq_iff]
no goals
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r : R
hr : r ∈ S
⊢ ∃ u v, 1 * ↑u = r * v ∧ ↑1 * ↑u = ↑{ val := r, property := hr } * v
exact ⟨⟨r, hr⟩, 1, by simp, by simp⟩
no goals
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r : R
hr : r ∈ S
⊢ 1 * ↑{ val := r, property := hr } = r * 1
simp
no goals
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r : R
hr : r ∈ S
⊢ ↑1 * ↑{ val := r, property := hr } = ↑{ val := r, property := hr } * 1
simp