case c
R : Type u_1
inst✝³ : Ring R
inst✝² : Nontrivial R
inst✝¹ : OreSet R⁰
inst✝ : NoZeroDivisors R
x : OreLocalization R R⁰
h✝ : x ≠ 0
r : R
s : { x // x ∈ R⁰ }
h : r /ₒ s ≠ 0
⊢ r /ₒ s * (r /ₒ s)⁻¹ = 1
R : Type u_1
inst✝³ : Ring R
inst✝² : Nontrivial R
inst✝¹ : OreSet R⁰
inst✝ : NoZeroDivisors R
x : OreLocalization R R⁰
h : x ≠ 0
⊢ x * x⁻¹ = 1
induction' x using OreLocalization.ind with r s
case c
R : Type u_1
inst✝³ : Ring R
inst✝² : Nontrivial R
inst✝¹ : OreSet R⁰
inst✝ : NoZeroDivisors R
x : OreLocalization R R⁰
h✝ : x ≠ 0
r : R
s : { x // x ∈ R⁰ }
h : r /ₒ s ≠ 0
⊢ (r /ₒ s * if hr : r = 0 then 0 else ↑s /ₒ { val := r, property := (_ : ∀ (x : R), x * r = 0 → x = 0) }) = 1 /ₒ 1
case c
R : Type u_1
inst✝³ : Ring R
inst✝² : Nontrivial R
inst✝¹ : OreSet R⁰
inst✝ : NoZeroDivisors R
x : OreLocalization R R⁰
h✝ : x ≠ 0
r : R
s : { x // x ∈ R⁰ }
h : r /ₒ s ≠ 0
⊢ r /ₒ s * (r /ₒ s)⁻¹ = 1
rw [OreLocalization.inv_def, OreLocalization.one_def]
case pos
R : Type u_1
inst✝³ : Ring R
inst✝² : Nontrivial R
inst✝¹ : OreSet R⁰
inst✝ : NoZeroDivisors R
x : OreLocalization R R⁰
h✝ : x ≠ 0
r : R
s : { x // x ∈ R⁰ }
h : r /ₒ s ≠ 0
hr : r = 0
⊢ (r /ₒ s * if hr : r = 0 then 0 else ↑s /ₒ { val := r, property := (_ : ∀ (x : R), x * r = 0 → x = 0) }) = 1 /ₒ 1

case neg
R : Type u_1
inst✝³ : Ring R
inst✝² : Nontrivial R
inst✝¹ : OreSet R⁰
inst✝ : NoZeroDivisors R
x : OreLocalization R R⁰
h✝ : x ≠ 0
r : R
s : { x // x ∈ R⁰ }
h : r /ₒ s ≠ 0
hr : ¬r = 0
⊢ (r /ₒ s * if hr : r = 0 then 0 else ↑s /ₒ { val := r, property := (_ : ∀ (x : R), x * r = 0 → x = 0) }) = 1 /ₒ 1
case c
R : Type u_1
inst✝³ : Ring R
inst✝² : Nontrivial R
inst✝¹ : OreSet R⁰
inst✝ : NoZeroDivisors R
x : OreLocalization R R⁰
h✝ : x ≠ 0
r : R
s : { x // x ∈ R⁰ }
h : r /ₒ s ≠ 0
⊢ (r /ₒ s * if hr : r = 0 then 0 else ↑s /ₒ { val := r, property := (_ : ∀ (x : R), x * r = 0 → x = 0) }) = 1 /ₒ 1
by_cases hr : r = 0
case pos.h
R : Type u_1
inst✝³ : Ring R
inst✝² : Nontrivial R
inst✝¹ : OreSet R⁰
inst✝ : NoZeroDivisors R
x : OreLocalization R R⁰
h✝ : x ≠ 0
r : R
s : { x // x ∈ R⁰ }
h : r /ₒ s ≠ 0
hr : r = 0
⊢ False
case pos
R : Type u_1
inst✝³ : Ring R
inst✝² : Nontrivial R
inst✝¹ : OreSet R⁰
inst✝ : NoZeroDivisors R
x : OreLocalization R R⁰
h✝ : x ≠ 0
r : R
s : { x // x ∈ R⁰ }
h : r /ₒ s ≠ 0
hr : r = 0
⊢ (r /ₒ s * if hr : r = 0 then 0 else ↑s /ₒ { val := r, property := (_ : ∀ (x : R), x * r = 0 → x = 0) }) = 1 /ₒ 1
exfalso
case pos.h
R : Type u_1
inst✝³ : Ring R
inst✝² : Nontrivial R
inst✝¹ : OreSet R⁰
inst✝ : NoZeroDivisors R
x : OreLocalization R R⁰
h✝ : x ≠ 0
r : R
s : { x // x ∈ R⁰ }
h : r /ₒ s ≠ 0
hr : r = 0
⊢ r /ₒ s = 0
case pos.h
R : Type u_1
inst✝³ : Ring R
inst✝² : Nontrivial R
inst✝¹ : OreSet R⁰
inst✝ : NoZeroDivisors R
x : OreLocalization R R⁰
h✝ : x ≠ 0
r : R
s : { x // x ∈ R⁰ }
h : r /ₒ s ≠ 0
hr : r = 0
⊢ False
apply h
no goals
case pos.h
R : Type u_1
inst✝³ : Ring R
inst✝² : Nontrivial R
inst✝¹ : OreSet R⁰
inst✝ : NoZeroDivisors R
x : OreLocalization R R⁰
h✝ : x ≠ 0
r : R
s : { x // x ∈ R⁰ }
h : r /ₒ s ≠ 0
hr : r = 0
⊢ r /ₒ s = 0
simp [hr]
case neg
R : Type u_1
inst✝³ : Ring R
inst✝² : Nontrivial R
inst✝¹ : OreSet R⁰
inst✝ : NoZeroDivisors R
x : OreLocalization R R⁰
h✝ : x ≠ 0
r : R
s : { x // x ∈ R⁰ }
h : r /ₒ s ≠ 0
hr : ¬r = 0
⊢ 1 = 1 /ₒ 1
case neg
R : Type u_1
inst✝³ : Ring R
inst✝² : Nontrivial R
inst✝¹ : OreSet R⁰
inst✝ : NoZeroDivisors R
x : OreLocalization R R⁰
h✝ : x ≠ 0
r : R
s : { x // x ∈ R⁰ }
h : r /ₒ s ≠ 0
hr : ¬r = 0
⊢ (r /ₒ s * if hr : r = 0 then 0 else ↑s /ₒ { val := r, property := (_ : ∀ (x : R), x * r = 0 → x = 0) }) = 1 /ₒ 1
simp [hr]
no goals
case neg
R : Type u_1
inst✝³ : Ring R
inst✝² : Nontrivial R
inst✝¹ : OreSet R⁰
inst✝ : NoZeroDivisors R
x : OreLocalization R R⁰
h✝ : x ≠ 0
r : R
s : { x // x ∈ R⁰ }
h : r /ₒ s ≠ 0
hr : ¬r = 0
⊢ 1 = 1 /ₒ 1
apply OreLocalization.div_eq_one'