case a
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
β : OreLocalization R S → Prop
c : ∀ (r : R) (s : { x // x ∈ S }), β (r /ₒ s)
⊢ ∀ (a : R × { x // x ∈ S }), β (Quotient.mk (oreEqv R S) a)
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
β : OreLocalization R S → Prop
c : ∀ (r : R) (s : { x // x ∈ S }), β (r /ₒ s)
⊢ ∀ (q : OreLocalization R S), β q
apply Quotient.ind
case a.mk
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
β : OreLocalization R S → Prop
c : ∀ (r : R) (s : { x // x ∈ S }), β (r /ₒ s)
r : R
s : { x // x ∈ S }
⊢ β (Quotient.mk (oreEqv R S) (r, s))
case a
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
β : OreLocalization R S → Prop
c : ∀ (r : R) (s : { x // x ∈ S }), β (r /ₒ s)
⊢ ∀ (a : R × { x // x ∈ S }), β (Quotient.mk (oreEqv R S) a)
rintro ⟨r, s⟩
no goals
case a.mk
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
β : OreLocalization R S → Prop
c : ∀ (r : R) (s : { x // x ∈ S }), β (r /ₒ s)
r : R
s : { x // x ∈ S }
⊢ β (Quotient.mk (oreEqv R S) (r, s))
exact c r s