case ofFractionRing.ofFractionRing
K : Type u
inst✝⁵ : CommRing K
G₀ : Type u_2
L : Type ?u.969727
R : Type u_1
S : Type ?u.969733
F : Type ?u.969736
inst✝⁴ : CommGroupWithZero G₀
inst✝³ : Field L
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Nontrivial R
φ : R[X] →*₀ G₀
hφ : Function.Injective ↑φ
hφ' : optParam (R[X]⁰ ≤ Submonoid.comap φ G₀⁰) (_ : R[X]⁰ ≤ Submonoid.comap φ G₀⁰)
x y : FractionRing R[X]
⊢ ↑(liftMonoidWithZeroHom φ hφ') { toFractionRing := x } = ↑(liftMonoidWithZeroHom φ hφ') { toFractionRing := y } →
    { toFractionRing := x } = { toFractionRing := y }
K : Type u
inst✝⁵ : CommRing K
G₀ : Type u_2
L : Type ?u.969727
R : Type u_1
S : Type ?u.969733
F : Type ?u.969736
inst✝⁴ : CommGroupWithZero G₀
inst✝³ : Field L
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Nontrivial R
φ : R[X] →*₀ G₀
hφ : Function.Injective ↑φ
hφ' : optParam (R[X]⁰ ≤ Submonoid.comap φ G₀⁰) (_ : R[X]⁰ ≤ Submonoid.comap φ G₀⁰)
⊢ Function.Injective ↑(liftMonoidWithZeroHom φ hφ')
rintro ⟨x⟩ ⟨y⟩
case ofFractionRing.ofFractionRing.H
K : Type u
inst✝⁵ : CommRing K
G₀ : Type u_2
L : Type ?u.969727
R : Type u_1
S : Type ?u.969733
F : Type ?u.969736
inst✝⁴ : CommGroupWithZero G₀
inst✝³ : Field L
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Nontrivial R
φ : R[X] →*₀ G₀
hφ : Function.Injective ↑φ
hφ' : optParam (R[X]⁰ ≤ Submonoid.comap φ G₀⁰) (_ : R[X]⁰ ≤ Submonoid.comap φ G₀⁰)
y : FractionRing R[X]
a : R[X] × { x // x ∈ R[X]⁰ }
⊢ ↑(liftMonoidWithZeroHom φ hφ') { toFractionRing := Localization.mk a.fst a.snd } =
      ↑(liftMonoidWithZeroHom φ hφ') { toFractionRing := y } →
    { toFractionRing := Localization.mk a.fst a.snd } = { toFractionRing := y }
case ofFractionRing.ofFractionRing
K : Type u
inst✝⁵ : CommRing K
G₀ : Type u_2
L : Type ?u.969727
R : Type u_1
S : Type ?u.969733
F : Type ?u.969736
inst✝⁴ : CommGroupWithZero G₀
inst✝³ : Field L
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Nontrivial R
φ : R[X] →*₀ G₀
hφ : Function.Injective ↑φ
hφ' : optParam (R[X]⁰ ≤ Submonoid.comap φ G₀⁰) (_ : R[X]⁰ ≤ Submonoid.comap φ G₀⁰)
x y : FractionRing R[X]
⊢ ↑(liftMonoidWithZeroHom φ hφ') { toFractionRing := x } = ↑(liftMonoidWithZeroHom φ hφ') { toFractionRing := y } →
    { toFractionRing := x } = { toFractionRing := y }
induction' x using Localization.induction_on with a
case ofFractionRing.ofFractionRing.H.H
K : Type u
inst✝⁵ : CommRing K
G₀ : Type u_2
L : Type ?u.969727
R : Type u_1
S : Type ?u.969733
F : Type ?u.969736
inst✝⁴ : CommGroupWithZero G₀
inst✝³ : Field L
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Nontrivial R
φ : R[X] →*₀ G₀
hφ : Function.Injective ↑φ
hφ' : optParam (R[X]⁰ ≤ Submonoid.comap φ G₀⁰) (_ : R[X]⁰ ≤ Submonoid.comap φ G₀⁰)
a a' : R[X] × { x // x ∈ R[X]⁰ }
⊢ ↑(liftMonoidWithZeroHom φ hφ') { toFractionRing := Localization.mk a.fst a.snd } =
      ↑(liftMonoidWithZeroHom φ hφ') { toFractionRing := Localization.mk a'.fst a'.snd } →
    { toFractionRing := Localization.mk a.fst a.snd } = { toFractionRing := Localization.mk a'.fst a'.snd }
case ofFractionRing.ofFractionRing.H
K : Type u
inst✝⁵ : CommRing K
G₀ : Type u_2
L : Type ?u.969727
R : Type u_1
S : Type ?u.969733
F : Type ?u.969736
inst✝⁴ : CommGroupWithZero G₀
inst✝³ : Field L
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Nontrivial R
φ : R[X] →*₀ G₀
hφ : Function.Injective ↑φ
hφ' : optParam (R[X]⁰ ≤ Submonoid.comap φ G₀⁰) (_ : R[X]⁰ ≤ Submonoid.comap φ G₀⁰)
y : FractionRing R[X]
a : R[X] × { x // x ∈ R[X]⁰ }
⊢ ↑(liftMonoidWithZeroHom φ hφ') { toFractionRing := Localization.mk a.fst a.snd } =
      ↑(liftMonoidWithZeroHom φ hφ') { toFractionRing := y } →
    { toFractionRing := Localization.mk a.fst a.snd } = { toFractionRing := y }
induction' y using Localization.induction_on with a'
case ofFractionRing.ofFractionRing.H.H
K : Type u
inst✝⁵ : CommRing K
G₀ : Type u_2
L : Type ?u.969727
R : Type u_1
S : Type ?u.969733
F : Type ?u.969736
inst✝⁴ : CommGroupWithZero G₀
inst✝³ : Field L
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Nontrivial R
φ : R[X] →*₀ G₀
hφ : Function.Injective ↑φ
hφ' : optParam (R[X]⁰ ≤ Submonoid.comap φ G₀⁰) (_ : R[X]⁰ ≤ Submonoid.comap φ G₀⁰)
a a' : R[X] × { x // x ∈ R[X]⁰ }
⊢ ↑φ a.fst / ↑φ ↑a.snd = ↑φ a'.fst / ↑φ ↑a'.snd →
    { toFractionRing := Localization.mk a.fst a.snd } = { toFractionRing := Localization.mk a'.fst a'.snd }
case ofFractionRing.ofFractionRing.H.H
K : Type u
inst✝⁵ : CommRing K
G₀ : Type u_2
L : Type ?u.969727
R : Type u_1
S : Type ?u.969733
F : Type ?u.969736
inst✝⁴ : CommGroupWithZero G₀
inst✝³ : Field L
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Nontrivial R
φ : R[X] →*₀ G₀
hφ : Function.Injective ↑φ
hφ' : optParam (R[X]⁰ ≤ Submonoid.comap φ G₀⁰) (_ : R[X]⁰ ≤ Submonoid.comap φ G₀⁰)
a a' : R[X] × { x // x ∈ R[X]⁰ }
⊢ ↑(liftMonoidWithZeroHom φ hφ') { toFractionRing := Localization.mk a.fst a.snd } =
      ↑(liftMonoidWithZeroHom φ hφ') { toFractionRing := Localization.mk a'.fst a'.snd } →
    { toFractionRing := Localization.mk a.fst a.snd } = { toFractionRing := Localization.mk a'.fst a'.snd }
simp_rw [liftMonoidWithZeroHom_apply_ofFractionRing_mk]
case ofFractionRing.ofFractionRing.H.H
K : Type u
inst✝⁵ : CommRing K
G₀ : Type u_2
L : Type ?u.969727
R : Type u_1
S : Type ?u.969733
F : Type ?u.969736
inst✝⁴ : CommGroupWithZero G₀
inst✝³ : Field L
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Nontrivial R
φ : R[X] →*₀ G₀
hφ : Function.Injective ↑φ
hφ' : optParam (R[X]⁰ ≤ Submonoid.comap φ G₀⁰) (_ : R[X]⁰ ≤ Submonoid.comap φ G₀⁰)
a a' : R[X] × { x // x ∈ R[X]⁰ }
h : ↑φ a.fst / ↑φ ↑a.snd = ↑φ a'.fst / ↑φ ↑a'.snd
⊢ { toFractionRing := Localization.mk a.fst a.snd } = { toFractionRing := Localization.mk a'.fst a'.snd }
case ofFractionRing.ofFractionRing.H.H
K : Type u
inst✝⁵ : CommRing K
G₀ : Type u_2
L : Type ?u.969727
R : Type u_1
S : Type ?u.969733
F : Type ?u.969736
inst✝⁴ : CommGroupWithZero G₀
inst✝³ : Field L
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Nontrivial R
φ : R[X] →*₀ G₀
hφ : Function.Injective ↑φ
hφ' : optParam (R[X]⁰ ≤ Submonoid.comap φ G₀⁰) (_ : R[X]⁰ ≤ Submonoid.comap φ G₀⁰)
a a' : R[X] × { x // x ∈ R[X]⁰ }
⊢ ↑φ a.fst / ↑φ ↑a.snd = ↑φ a'.fst / ↑φ ↑a'.snd →
    { toFractionRing := Localization.mk a.fst a.snd } = { toFractionRing := Localization.mk a'.fst a'.snd }
intro h
case ofFractionRing.ofFractionRing.H.H.e_toFractionRing
K : Type u
inst✝⁵ : CommRing K
G₀ : Type u_2
L : Type ?u.969727
R : Type u_1
S : Type ?u.969733
F : Type ?u.969736
inst✝⁴ : CommGroupWithZero G₀
inst✝³ : Field L
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Nontrivial R
φ : R[X] →*₀ G₀
hφ : Function.Injective ↑φ
hφ' : optParam (R[X]⁰ ≤ Submonoid.comap φ G₀⁰) (_ : R[X]⁰ ≤ Submonoid.comap φ G₀⁰)
a a' : R[X] × { x // x ∈ R[X]⁰ }
h : ↑φ a.fst / ↑φ ↑a.snd = ↑φ a'.fst / ↑φ ↑a'.snd
⊢ Localization.mk a.fst a.snd = Localization.mk a'.fst a'.snd
case ofFractionRing.ofFractionRing.H.H
K : Type u
inst✝⁵ : CommRing K
G₀ : Type u_2
L : Type ?u.969727
R : Type u_1
S : Type ?u.969733
F : Type ?u.969736
inst✝⁴ : CommGroupWithZero G₀
inst✝³ : Field L
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Nontrivial R
φ : R[X] →*₀ G₀
hφ : Function.Injective ↑φ
hφ' : optParam (R[X]⁰ ≤ Submonoid.comap φ G₀⁰) (_ : R[X]⁰ ≤ Submonoid.comap φ G₀⁰)
a a' : R[X] × { x // x ∈ R[X]⁰ }
h : ↑φ a.fst / ↑φ ↑a.snd = ↑φ a'.fst / ↑φ ↑a'.snd
⊢ { toFractionRing := Localization.mk a.fst a.snd } = { toFractionRing := Localization.mk a'.fst a'.snd }
congr 1
case ofFractionRing.ofFractionRing.H.H.e_toFractionRing
K : Type u
inst✝⁵ : CommRing K
G₀ : Type u_2
L : Type ?u.969727
R : Type u_1
S : Type ?u.969733
F : Type ?u.969736
inst✝⁴ : CommGroupWithZero G₀
inst✝³ : Field L
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Nontrivial R
φ : R[X] →*₀ G₀
hφ : Function.Injective ↑φ
hφ' : optParam (R[X]⁰ ≤ Submonoid.comap φ G₀⁰) (_ : R[X]⁰ ≤ Submonoid.comap φ G₀⁰)
a a' : R[X] × { x // x ∈ R[X]⁰ }
h : ↑φ a.fst / ↑φ ↑a.snd = ↑φ a'.fst / ↑φ ↑a'.snd
⊢ ↑(a'.fst, a'.snd).snd * (a.fst, a.snd).fst = ↑(a.fst, a.snd).snd * (a'.fst, a'.snd).fst
case ofFractionRing.ofFractionRing.H.H.e_toFractionRing
K : Type u
inst✝⁵ : CommRing K
G₀ : Type u_2
L : Type ?u.969727
R : Type u_1
S : Type ?u.969733
F : Type ?u.969736
inst✝⁴ : CommGroupWithZero G₀
inst✝³ : Field L
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Nontrivial R
φ : R[X] →*₀ G₀
hφ : Function.Injective ↑φ
hφ' : optParam (R[X]⁰ ≤ Submonoid.comap φ G₀⁰) (_ : R[X]⁰ ≤ Submonoid.comap φ G₀⁰)
a a' : R[X] × { x // x ∈ R[X]⁰ }
h : ↑φ a.fst / ↑φ ↑a.snd = ↑φ a'.fst / ↑φ ↑a'.snd
⊢ Localization.mk a.fst a.snd = Localization.mk a'.fst a'.snd
refine Localization.mk_eq_mk_iff.mpr (Localization.r_of_eq (M := R[X]) ?_)
case ofFractionRing.ofFractionRing.H.H.e_toFractionRing.refine_3
K : Type u
inst✝⁵ : CommRing K
G₀ : Type u_2
L : Type ?u.969727
R : Type u_1
S : Type ?u.969733
F : Type ?u.969736
inst✝⁴ : CommGroupWithZero G₀
inst✝³ : Field L
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Nontrivial R
φ : R[X] →*₀ G₀
hφ : Function.Injective ↑φ
hφ' : optParam (R[X]⁰ ≤ Submonoid.comap φ G₀⁰) (_ : R[X]⁰ ≤ Submonoid.comap φ G₀⁰)
a a' : R[X] × { x // x ∈ R[X]⁰ }
h : ↑φ a.fst / ↑φ ↑a.snd = ↑φ a'.fst / ↑φ ↑a'.snd
this : ↑φ a.fst * ↑φ ↑a'.snd = ↑φ a'.fst * ↑φ ↑a.snd
⊢ ↑(a'.fst, a'.snd).snd * (a.fst, a.snd).fst = ↑(a.fst, a.snd).snd * (a'.fst, a'.snd).fst

case ofFractionRing.ofFractionRing.H.H.e_toFractionRing.refine_1
K : Type u
inst✝⁵ : CommRing K
G₀ : Type u_2
L : Type ?u.969727
R : Type u_1
S : Type ?u.969733
F : Type ?u.969736
inst✝⁴ : CommGroupWithZero G₀
inst✝³ : Field L
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Nontrivial R
φ : R[X] →*₀ G₀
hφ : Function.Injective ↑φ
hφ' : optParam (R[X]⁰ ≤ Submonoid.comap φ G₀⁰) (_ : R[X]⁰ ≤ Submonoid.comap φ G₀⁰)
a a' : R[X] × { x // x ∈ R[X]⁰ }
h : ↑φ a.fst / ↑φ ↑a.snd = ↑φ a'.fst / ↑φ ↑a'.snd
⊢ ↑φ ↑a.snd ≠ 0

case ofFractionRing.ofFractionRing.H.H.e_toFractionRing.refine_2
K : Type u
inst✝⁵ : CommRing K
G₀ : Type u_2
L : Type ?u.969727
R : Type u_1
S : Type ?u.969733
F : Type ?u.969736
inst✝⁴ : CommGroupWithZero G₀
inst✝³ : Field L
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Nontrivial R
φ : R[X] →*₀ G₀
hφ : Function.Injective ↑φ
hφ' : optParam (R[X]⁰ ≤ Submonoid.comap φ G₀⁰) (_ : R[X]⁰ ≤ Submonoid.comap φ G₀⁰)
a a' : R[X] × { x // x ∈ R[X]⁰ }
h : ↑φ a.fst / ↑φ ↑a.snd = ↑φ a'.fst / ↑φ ↑a'.snd
⊢ ↑φ ↑a'.snd ≠ 0
case ofFractionRing.ofFractionRing.H.H.e_toFractionRing
K : Type u
inst✝⁵ : CommRing K
G₀ : Type u_2
L : Type ?u.969727
R : Type u_1
S : Type ?u.969733
F : Type ?u.969736
inst✝⁴ : CommGroupWithZero G₀
inst✝³ : Field L
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Nontrivial R
φ : R[X] →*₀ G₀
hφ : Function.Injective ↑φ
hφ' : optParam (R[X]⁰ ≤ Submonoid.comap φ G₀⁰) (_ : R[X]⁰ ≤ Submonoid.comap φ G₀⁰)
a a' : R[X] × { x // x ∈ R[X]⁰ }
h : ↑φ a.fst / ↑φ ↑a.snd = ↑φ a'.fst / ↑φ ↑a'.snd
⊢ ↑(a'.fst, a'.snd).snd * (a.fst, a.snd).fst = ↑(a.fst, a.snd).snd * (a'.fst, a'.snd).fst
have := mul_eq_mul_of_div_eq_div _ _ ?_ ?_ h
case ofFractionRing.ofFractionRing.H.H.e_toFractionRing.refine_1
K : Type u
inst✝⁵ : CommRing K
G₀ : Type u_2
L : Type ?u.969727
R : Type u_1
S : Type ?u.969733
F : Type ?u.969736
inst✝⁴ : CommGroupWithZero G₀
inst✝³ : Field L
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Nontrivial R
φ : R[X] →*₀ G₀
hφ : Function.Injective ↑φ
hφ' : optParam (R[X]⁰ ≤ Submonoid.comap φ G₀⁰) (_ : R[X]⁰ ≤ Submonoid.comap φ G₀⁰)
a a' : R[X] × { x // x ∈ R[X]⁰ }
h : ↑φ a.fst / ↑φ ↑a.snd = ↑φ a'.fst / ↑φ ↑a'.snd
⊢ ↑φ ↑a.snd ≠ 0

case ofFractionRing.ofFractionRing.H.H.e_toFractionRing.refine_2
K : Type u
inst✝⁵ : CommRing K
G₀ : Type u_2
L : Type ?u.969727
R : Type u_1
S : Type ?u.969733
F : Type ?u.969736
inst✝⁴ : CommGroupWithZero G₀
inst✝³ : Field L
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Nontrivial R
φ : R[X] →*₀ G₀
hφ : Function.Injective ↑φ
hφ' : optParam (R[X]⁰ ≤ Submonoid.comap φ G₀⁰) (_ : R[X]⁰ ≤ Submonoid.comap φ G₀⁰)
a a' : R[X] × { x // x ∈ R[X]⁰ }
h : ↑φ a.fst / ↑φ ↑a.snd = ↑φ a'.fst / ↑φ ↑a'.snd
⊢ ↑φ ↑a'.snd ≠ 0
case ofFractionRing.ofFractionRing.H.H.e_toFractionRing.refine_3
K : Type u
inst✝⁵ : CommRing K
G₀ : Type u_2
L : Type ?u.969727
R : Type u_1
S : Type ?u.969733
F : Type ?u.969736
inst✝⁴ : CommGroupWithZero G₀
inst✝³ : Field L
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Nontrivial R
φ : R[X] →*₀ G₀
hφ : Function.Injective ↑φ
hφ' : optParam (R[X]⁰ ≤ Submonoid.comap φ G₀⁰) (_ : R[X]⁰ ≤ Submonoid.comap φ G₀⁰)
a a' : R[X] × { x // x ∈ R[X]⁰ }
h : ↑φ a.fst / ↑φ ↑a.snd = ↑φ a'.fst / ↑φ ↑a'.snd
this : ↑φ a.fst * ↑φ ↑a'.snd = ↑φ a'.fst * ↑φ ↑a.snd
⊢ ↑(a'.fst, a'.snd).snd * (a.fst, a.snd).fst = ↑(a.fst, a.snd).snd * (a'.fst, a'.snd).fst

case ofFractionRing.ofFractionRing.H.H.e_toFractionRing.refine_1
K : Type u
inst✝⁵ : CommRing K
G₀ : Type u_2
L : Type ?u.969727
R : Type u_1
S : Type ?u.969733
F : Type ?u.969736
inst✝⁴ : CommGroupWithZero G₀
inst✝³ : Field L
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Nontrivial R
φ : R[X] →*₀ G₀
hφ : Function.Injective ↑φ
hφ' : optParam (R[X]⁰ ≤ Submonoid.comap φ G₀⁰) (_ : R[X]⁰ ≤ Submonoid.comap φ G₀⁰)
a a' : R[X] × { x // x ∈ R[X]⁰ }
h : ↑φ a.fst / ↑φ ↑a.snd = ↑φ a'.fst / ↑φ ↑a'.snd
⊢ ↑φ ↑a.snd ≠ 0

case ofFractionRing.ofFractionRing.H.H.e_toFractionRing.refine_2
K : Type u
inst✝⁵ : CommRing K
G₀ : Type u_2
L : Type ?u.969727
R : Type u_1
S : Type ?u.969733
F : Type ?u.969736
inst✝⁴ : CommGroupWithZero G₀
inst✝³ : Field L
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Nontrivial R
φ : R[X] →*₀ G₀
hφ : Function.Injective ↑φ
hφ' : optParam (R[X]⁰ ≤ Submonoid.comap φ G₀⁰) (_ : R[X]⁰ ≤ Submonoid.comap φ G₀⁰)
a a' : R[X] × { x // x ∈ R[X]⁰ }
h : ↑φ a.fst / ↑φ ↑a.snd = ↑φ a'.fst / ↑φ ↑a'.snd
⊢ ↑φ ↑a'.snd ≠ 0
rwa [← map_mul, ← map_mul, hφ.eq_iff, mul_comm, mul_comm a'.fst] at this
no goals
case ofFractionRing.ofFractionRing.H.H.e_toFractionRing.refine_1
K : Type u
inst✝⁵ : CommRing K
G₀ : Type u_2
L : Type ?u.969727
R : Type u_1
S : Type ?u.969733
F : Type ?u.969736
inst✝⁴ : CommGroupWithZero G₀
inst✝³ : Field L
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Nontrivial R
φ : R[X] →*₀ G₀
hφ : Function.Injective ↑φ
hφ' : optParam (R[X]⁰ ≤ Submonoid.comap φ G₀⁰) (_ : R[X]⁰ ≤ Submonoid.comap φ G₀⁰)
a a' : R[X] × { x // x ∈ R[X]⁰ }
h : ↑φ a.fst / ↑φ ↑a.snd = ↑φ a'.fst / ↑φ ↑a'.snd
⊢ ↑φ ↑a.snd ≠ 0

case ofFractionRing.ofFractionRing.H.H.e_toFractionRing.refine_2
K : Type u
inst✝⁵ : CommRing K
G₀ : Type u_2
L : Type ?u.969727
R : Type u_1
S : Type ?u.969733
F : Type ?u.969736
inst✝⁴ : CommGroupWithZero G₀
inst✝³ : Field L
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Nontrivial R
φ : R[X] →*₀ G₀
hφ : Function.Injective ↑φ
hφ' : optParam (R[X]⁰ ≤ Submonoid.comap φ G₀⁰) (_ : R[X]⁰ ≤ Submonoid.comap φ G₀⁰)
a a' : R[X] × { x // x ∈ R[X]⁰ }
h : ↑φ a.fst / ↑φ ↑a.snd = ↑φ a'.fst / ↑φ ↑a'.snd
⊢ ↑φ ↑a'.snd ≠ 0
all_goals exact map_ne_zero_of_mem_nonZeroDivisors _ hφ (SetLike.coe_mem _)
no goals
case ofFractionRing.ofFractionRing.H.H.e_toFractionRing.refine_2
K : Type u
inst✝⁵ : CommRing K
G₀ : Type u_2
L : Type ?u.969727
R : Type u_1
S : Type ?u.969733
F : Type ?u.969736
inst✝⁴ : CommGroupWithZero G₀
inst✝³ : Field L
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Nontrivial R
φ : R[X] →*₀ G₀
hφ : Function.Injective ↑φ
hφ' : optParam (R[X]⁰ ≤ Submonoid.comap φ G₀⁰) (_ : R[X]⁰ ≤ Submonoid.comap φ G₀⁰)
a a' : R[X] × { x // x ∈ R[X]⁰ }
h : ↑φ a.fst / ↑φ ↑a.snd = ↑φ a'.fst / ↑φ ↑a'.snd
⊢ ↑φ ↑a'.snd ≠ 0
exact map_ne_zero_of_mem_nonZeroDivisors _ hφ (SetLike.coe_mem _)