R : Type u_1
inst✝¹ : Ring R
S : Submonoid R
inst✝ : OreSet S
hS : S ≤ R⁰
r₁ r₂ : R
h : ∃ u v, r₂ * ↑u = r₁ * v ∧ ↑1 * ↑u = ↑1 * v
⊢ r₁ = r₂
R : Type u_1
inst✝¹ : Ring R
S : Submonoid R
inst✝ : OreSet S
hS : S ≤ R⁰
r₁ r₂ : R
h : ↑numeratorHom r₁ = ↑numeratorHom r₂
⊢ r₁ = r₂
rw [numeratorHom_apply, numeratorHom_apply, oreDiv_eq_iff] at h
case intro.intro.intro
R : Type u_1
inst✝¹ : Ring R
S : Submonoid R
inst✝ : OreSet S
hS : S ≤ R⁰
r₁ r₂ : R
u : { x // x ∈ S }
v : R
h₁ : r₂ * ↑u = r₁ * v
h₂ : ↑1 * ↑u = ↑1 * v
⊢ r₁ = r₂
R : Type u_1
inst✝¹ : Ring R
S : Submonoid R
inst✝ : OreSet S
hS : S ≤ R⁰
r₁ r₂ : R
h : ∃ u v, r₂ * ↑u = r₁ * v ∧ ↑1 * ↑u = ↑1 * v
⊢ r₁ = r₂
rcases h with ⟨u, v, h₁, h₂⟩
case intro.intro.intro
R : Type u_1
inst✝¹ : Ring R
S : Submonoid R
inst✝ : OreSet S
hS : S ≤ R⁰
r₁ r₂ : R
u : { x // x ∈ S }
v : R
h₁ : r₂ * ↑u = r₁ * v
h₂ : ↑u = v
⊢ r₁ = r₂
case intro.intro.intro
R : Type u_1
inst✝¹ : Ring R
S : Submonoid R
inst✝ : OreSet S
hS : S ≤ R⁰
r₁ r₂ : R
u : { x // x ∈ S }
v : R
h₁ : r₂ * ↑u = r₁ * v
h₂ : ↑1 * ↑u = ↑1 * v
⊢ r₁ = r₂
simp only [S.coe_one, one_mul] at h₂
no goals
case intro.intro.intro
R : Type u_1
inst✝¹ : Ring R
S : Submonoid R
inst✝ : OreSet S
hS : S ≤ R⁰
r₁ r₂ : R
u : { x // x ∈ S }
v : R
h₁ : r₂ * ↑u = r₁ * v
h₂ : ↑u = v
⊢ r₁ = r₂
rwa [← h₂, mul_cancel_right_mem_nonZeroDivisors (hS (SetLike.coe_mem u)), eq_comm] at h₁