case ofFractionRing.ofFractionRing
K : Type u
inst✝⁵ : CommRing K
G₀ : Type ?u.685775
L : Type ?u.685778
R : Type u_2
S : Type u_3
F : Type u_1
inst✝⁴ : CommGroupWithZero G₀
inst✝³ : Field L
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : MonoidHomClass F R[X] S[X]
φ : F
hφ : R[X]⁰ ≤ Submonoid.comap φ S[X]⁰
hf : Function.Injective ↑φ
x y : FractionRing R[X]
h : ↑(map φ hφ) { toFractionRing := x } = ↑(map φ hφ) { toFractionRing := y }
⊢ { toFractionRing := x } = { toFractionRing := y }
K : Type u
inst✝⁵ : CommRing K
G₀ : Type ?u.685775
L : Type ?u.685778
R : Type u_2
S : Type u_3
F : Type u_1
inst✝⁴ : CommGroupWithZero G₀
inst✝³ : Field L
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : MonoidHomClass F R[X] S[X]
φ : F
hφ : R[X]⁰ ≤ Submonoid.comap φ S[X]⁰
hf : Function.Injective ↑φ
⊢ Function.Injective ↑(map φ hφ)
rintro ⟨x⟩ ⟨y⟩ h
case ofFractionRing.ofFractionRing.H
K : Type u
inst✝⁵ : CommRing K
G₀ : Type ?u.685775
L : Type ?u.685778
R : Type u_2
S : Type u_3
F : Type u_1
inst✝⁴ : CommGroupWithZero G₀
inst✝³ : Field L
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : MonoidHomClass F R[X] S[X]
φ : F
hφ : R[X]⁰ ≤ Submonoid.comap φ S[X]⁰
hf : Function.Injective ↑φ
y : FractionRing R[X]
y✝ : R[X] × { x // x ∈ R[X]⁰ }
h : ↑(map φ hφ) { toFractionRing := Localization.mk y✝.fst y✝.snd } = ↑(map φ hφ) { toFractionRing := y }
⊢ { toFractionRing := Localization.mk y✝.fst y✝.snd } = { toFractionRing := y }
case ofFractionRing.ofFractionRing
K : Type u
inst✝⁵ : CommRing K
G₀ : Type ?u.685775
L : Type ?u.685778
R : Type u_2
S : Type u_3
F : Type u_1
inst✝⁴ : CommGroupWithZero G₀
inst✝³ : Field L
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : MonoidHomClass F R[X] S[X]
φ : F
hφ : R[X]⁰ ≤ Submonoid.comap φ S[X]⁰
hf : Function.Injective ↑φ
x y : FractionRing R[X]
h : ↑(map φ hφ) { toFractionRing := x } = ↑(map φ hφ) { toFractionRing := y }
⊢ { toFractionRing := x } = { toFractionRing := y }
induction x using Localization.induction_on
case ofFractionRing.ofFractionRing.H.H
K : Type u
inst✝⁵ : CommRing K
G₀ : Type ?u.685775
L : Type ?u.685778
R : Type u_2
S : Type u_3
F : Type u_1
inst✝⁴ : CommGroupWithZero G₀
inst✝³ : Field L
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : MonoidHomClass F R[X] S[X]
φ : F
hφ : R[X]⁰ ≤ Submonoid.comap φ S[X]⁰
hf : Function.Injective ↑φ
y✝¹ y✝ : R[X] × { x // x ∈ R[X]⁰ }
h :
  ↑(map φ hφ) { toFractionRing := Localization.mk y✝¹.fst y✝¹.snd } =
    ↑(map φ hφ) { toFractionRing := Localization.mk y✝.fst y✝.snd }
⊢ { toFractionRing := Localization.mk y✝¹.fst y✝¹.snd } = { toFractionRing := Localization.mk y✝.fst y✝.snd }
case ofFractionRing.ofFractionRing.H
K : Type u
inst✝⁵ : CommRing K
G₀ : Type ?u.685775
L : Type ?u.685778
R : Type u_2
S : Type u_3
F : Type u_1
inst✝⁴ : CommGroupWithZero G₀
inst✝³ : Field L
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : MonoidHomClass F R[X] S[X]
φ : F
hφ : R[X]⁰ ≤ Submonoid.comap φ S[X]⁰
hf : Function.Injective ↑φ
y : FractionRing R[X]
y✝ : R[X] × { x // x ∈ R[X]⁰ }
h : ↑(map φ hφ) { toFractionRing := Localization.mk y✝.fst y✝.snd } = ↑(map φ hφ) { toFractionRing := y }
⊢ { toFractionRing := Localization.mk y✝.fst y✝.snd } = { toFractionRing := y }
induction y using Localization.induction_on
no goals
case ofFractionRing.ofFractionRing.H.H
K : Type u
inst✝⁵ : CommRing K
G₀ : Type ?u.685775
L : Type ?u.685778
R : Type u_2
S : Type u_3
F : Type u_1
inst✝⁴ : CommGroupWithZero G₀
inst✝³ : Field L
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : MonoidHomClass F R[X] S[X]
φ : F
hφ : R[X]⁰ ≤ Submonoid.comap φ S[X]⁰
hf : Function.Injective ↑φ
y✝¹ y✝ : R[X] × { x // x ∈ R[X]⁰ }
h :
  ↑(map φ hφ) { toFractionRing := Localization.mk y✝¹.fst y✝¹.snd } =
    ↑(map φ hφ) { toFractionRing := Localization.mk y✝.fst y✝.snd }
⊢ { toFractionRing := Localization.mk y✝¹.fst y✝¹.snd } = { toFractionRing := Localization.mk y✝.fst y✝.snd }
simpa only [map_apply_ofFractionRing_mk, ofFractionRing_injective.eq_iff,
  Localization.mk_eq_mk_iff, Localization.r_iff_exists, mul_cancel_left_coe_nonZeroDivisors,
  exists_const, ← map_mul, hf.eq_iff] using h