case c
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r : R
s : { x // x ∈ S }
⊢ 1 * (r /ₒ s) = r /ₒ s
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
x : OreLocalization R S
⊢ 1 * x = x
induction' x using OreLocalization.ind with r s
no goals
case c
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r : R
s : { x // x ∈ S }
⊢ 1 * (r /ₒ s) = r /ₒ s
simp [OreLocalization.one_def, oreDiv_mul_char (1 : R) r (1 : S) s r 1 (by simp)]
no goals
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r : R
s : { x // x ∈ S }
⊢ r * ↑1 = ↑1 * r
simp