R : Type u_1
inst✝³ : Ring R
inst✝² : Nontrivial R
inst✝¹ : OreSet R⁰
inst✝ : NoZeroDivisors R
⊢ (if hr : 0 = 0 then 0 else ↑1 /ₒ { val := 0, property := (_ : ∀ (x : R), x * 0 = 0 → x = 0) }) = 0 /ₒ 1
R : Type u_1
inst✝³ : Ring R
inst✝² : Nontrivial R
inst✝¹ : OreSet R⁰
inst✝ : NoZeroDivisors R
⊢ 0⁻¹ = 0
rw [OreLocalization.zero_def, OreLocalization.inv_def]
no goals
R : Type u_1
inst✝³ : Ring R
inst✝² : Nontrivial R
inst✝¹ : OreSet R⁰
inst✝ : NoZeroDivisors R
⊢ (if hr : 0 = 0 then 0 else ↑1 /ₒ { val := 0, property := (_ : ∀ (x : R), x * 0 = 0 → x = 0) }) = 0 /ₒ 1
simp