case h
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
T : Type u_2
inst✝ : Monoid T
f : R →* T
fS : { x // x ∈ S } →* Tˣ
hf : ∀ (s : { x // x ∈ S }), ↑f ↑s = ↑(↑fS s)
φ : OreLocalization R S →* T
huniv : ∀ (r : R), ↑φ (↑numeratorHom r) = ↑f r
x : OreLocalization R S
⊢ ↑φ x = ↑(universalMulHom f fS hf) x
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
T : Type u_2
inst✝ : Monoid T
f : R →* T
fS : { x // x ∈ S } →* Tˣ
hf : ∀ (s : { x // x ∈ S }), ↑f ↑s = ↑(↑fS s)
φ : OreLocalization R S →* T
huniv : ∀ (r : R), ↑φ (↑numeratorHom r) = ↑f r
⊢ φ = universalMulHom f fS hf
ext x
case h.c
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
T : Type u_2
inst✝ : Monoid T
f : R →* T
fS : { x // x ∈ S } →* Tˣ
hf : ∀ (s : { x // x ∈ S }), ↑f ↑s = ↑(↑fS s)
φ : OreLocalization R S →* T
huniv : ∀ (r : R), ↑φ (↑numeratorHom r) = ↑f r
r : R
s : { x // x ∈ S }
⊢ ↑φ (r /ₒ s) = ↑(universalMulHom f fS hf) (r /ₒ s)
case h
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
T : Type u_2
inst✝ : Monoid T
f : R →* T
fS : { x // x ∈ S } →* Tˣ
hf : ∀ (s : { x // x ∈ S }), ↑f ↑s = ↑(↑fS s)
φ : OreLocalization R S →* T
huniv : ∀ (r : R), ↑φ (↑numeratorHom r) = ↑f r
x : OreLocalization R S
⊢ ↑φ x = ↑(universalMulHom f fS hf) x
induction' x using OreLocalization.ind with r s
no goals
case h.c
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
T : Type u_2
inst✝ : Monoid T
f : R →* T
fS : { x // x ∈ S } →* Tˣ
hf : ∀ (s : { x // x ∈ S }), ↑f ↑s = ↑(↑fS s)
φ : OreLocalization R S →* T
huniv : ∀ (r : R), ↑φ (↑numeratorHom r) = ↑f r
r : R
s : { x // x ∈ S }
⊢ ↑φ (r /ₒ s) = ↑(universalMulHom f fS hf) (r /ₒ s)
rw [universalMulHom_apply, ← huniv r, numeratorHom_apply, ← mul_one (φ (r /ₒ s)), ←
  Units.val_one, ← mul_right_inv (fS s), Units.val_mul, ← mul_assoc, ← hf, ← huniv, ← φ.map_mul,
  numeratorHom_apply, OreLocalization.mul_cancel]