case inl
R : Type u_3
inst✝¹¹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
P : Type ?u.431142
inst✝⁸ : CommRing P
Rₘ : Type u_1
Sₘ : Type ?u.431151
inst✝⁷ : CommRing Rₘ
inst✝⁶ : CommRing Sₘ
inst✝⁵ : Algebra R Rₘ
inst✝⁴ : IsLocalization M Rₘ
inst✝³ : Algebra S Sₘ
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst✝¹ : Algebra Rₘ S
inst✝ : IsScalarTower R Rₘ S
x : S
hx : IsIntegral Rₘ x
h✝ : Subsingleton Rₘ
⊢ ∃ m, IsIntegral R (m • x)

case inr
R : Type u_3
inst✝¹¹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
P : Type ?u.431142
inst✝⁸ : CommRing P
Rₘ : Type u_1
Sₘ : Type ?u.431151
inst✝⁷ : CommRing Rₘ
inst✝⁶ : CommRing Sₘ
inst✝⁵ : Algebra R Rₘ
inst✝⁴ : IsLocalization M Rₘ
inst✝³ : Algebra S Sₘ
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst✝¹ : Algebra Rₘ S
inst✝ : IsScalarTower R Rₘ S
x : S
hx : IsIntegral Rₘ x
nontriv : Nontrivial Rₘ
⊢ ∃ m, IsIntegral R (m • x)
R : Type u_3
inst✝¹¹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
P : Type ?u.431142
inst✝⁸ : CommRing P
Rₘ : Type u_1
Sₘ : Type ?u.431151
inst✝⁷ : CommRing Rₘ
inst✝⁶ : CommRing Sₘ
inst✝⁵ : Algebra R Rₘ
inst✝⁴ : IsLocalization M Rₘ
inst✝³ : Algebra S Sₘ
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst✝¹ : Algebra Rₘ S
inst✝ : IsScalarTower R Rₘ S
x : S
hx : IsIntegral Rₘ x
⊢ ∃ m, IsIntegral R (m • x)
cases' subsingleton_or_nontrivial Rₘ with _ nontriv <;> skip
case inr.intro.intro
R : Type u_3
inst✝¹¹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
P : Type ?u.431142
inst✝⁸ : CommRing P
Rₘ : Type u_1
Sₘ : Type ?u.431151
inst✝⁷ : CommRing Rₘ
inst✝⁶ : CommRing Sₘ
inst✝⁵ : Algebra R Rₘ
inst✝⁴ : IsLocalization M Rₘ
inst✝³ : Algebra S Sₘ
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst✝¹ : Algebra Rₘ S
inst✝ : IsScalarTower R Rₘ S
x : S
nontriv : Nontrivial Rₘ
p : Rₘ[X]
hp₁ : Monic p
hp₂ : eval₂ (_root_.algebraMap Rₘ S) x p = 0
⊢ ∃ m, IsIntegral R (m • x)
case inr
R : Type u_3
inst✝¹¹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
P : Type ?u.431142
inst✝⁸ : CommRing P
Rₘ : Type u_1
Sₘ : Type ?u.431151
inst✝⁷ : CommRing Rₘ
inst✝⁶ : CommRing Sₘ
inst✝⁵ : Algebra R Rₘ
inst✝⁴ : IsLocalization M Rₘ
inst✝³ : Algebra S Sₘ
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst✝¹ : Algebra Rₘ S
inst✝ : IsScalarTower R Rₘ S
x : S
hx : IsIntegral Rₘ x
nontriv : Nontrivial Rₘ
⊢ ∃ m, IsIntegral R (m • x)
obtain ⟨p, hp₁, hp₂⟩ := hx
case inr.intro.intro.refine_3
R : Type u_3
inst✝¹¹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
P : Type ?u.431142
inst✝⁸ : CommRing P
Rₘ : Type u_1
Sₘ : Type ?u.431151
inst✝⁷ : CommRing Rₘ
inst✝⁶ : CommRing Sₘ
inst✝⁵ : Algebra R Rₘ
inst✝⁴ : IsLocalization M Rₘ
inst✝³ : Algebra S Sₘ
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst✝¹ : Algebra Rₘ S
inst✝ : IsScalarTower R Rₘ S
x : S
nontriv : Nontrivial Rₘ
p : Rₘ[X]
hp₁ : Monic p
hp₂ : eval₂ (_root_.algebraMap Rₘ S) x p = 0
this :
  ∃ q,
    Polynomial.map (_root_.algebraMap R Rₘ) q =
        scaleRoots p (↑(_root_.algebraMap R Rₘ) ↑(commonDenom M (support p) (coeff p))) ∧
      natDegree q = natDegree (scaleRoots p (↑(_root_.algebraMap R Rₘ) ↑(commonDenom M (support p) (coeff p)))) ∧
        Monic q
⊢ ∃ m, IsIntegral R (m • x)

case inr.intro.intro.refine_1
R : Type u_3
inst✝¹¹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
P : Type ?u.431142
inst✝⁸ : CommRing P
Rₘ : Type u_1
Sₘ : Type ?u.431151
inst✝⁷ : CommRing Rₘ
inst✝⁶ : CommRing Sₘ
inst✝⁵ : Algebra R Rₘ
inst✝⁴ : IsLocalization M Rₘ
inst✝³ : Algebra S Sₘ
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst✝¹ : Algebra Rₘ S
inst✝ : IsScalarTower R Rₘ S
x : S
nontriv : Nontrivial Rₘ
p : Rₘ[X]
hp₁ : Monic p
hp₂ : eval₂ (_root_.algebraMap Rₘ S) x p = 0
⊢ leadingCoeff p ∈ RingHom.range (_root_.algebraMap R Rₘ)

case inr.intro.intro.refine_2
R : Type u_3
inst✝¹¹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
P : Type ?u.431142
inst✝⁸ : CommRing P
Rₘ : Type u_1
Sₘ : Type ?u.431151
inst✝⁷ : CommRing Rₘ
inst✝⁶ : CommRing Sₘ
inst✝⁵ : Algebra R Rₘ
inst✝⁴ : IsLocalization M Rₘ
inst✝³ : Algebra S Sₘ
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst✝¹ : Algebra Rₘ S
inst✝ : IsScalarTower R Rₘ S
x : S
nontriv : Nontrivial Rₘ
p : Rₘ[X]
hp₁ : Monic p
hp₂ : eval₂ (_root_.algebraMap Rₘ S) x p = 0
⊢ Monic (scaleRoots p (↑(_root_.algebraMap R Rₘ) ↑(commonDenom M (support p) (coeff p))))
case inr.intro.intro
R : Type u_3
inst✝¹¹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
P : Type ?u.431142
inst✝⁸ : CommRing P
Rₘ : Type u_1
Sₘ : Type ?u.431151
inst✝⁷ : CommRing Rₘ
inst✝⁶ : CommRing Sₘ
inst✝⁵ : Algebra R Rₘ
inst✝⁴ : IsLocalization M Rₘ
inst✝³ : Algebra S Sₘ
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst✝¹ : Algebra Rₘ S
inst✝ : IsScalarTower R Rₘ S
x : S
nontriv : Nontrivial Rₘ
p : Rₘ[X]
hp₁ : Monic p
hp₂ : eval₂ (_root_.algebraMap Rₘ S) x p = 0
⊢ ∃ m, IsIntegral R (m • x)
have :=
  lifts_and_natDegree_eq_and_monic (IsLocalization.scaleRoots_commonDenom_mem_lifts M p ?_) ?_
case inr.intro.intro.refine_3.intro.intro.intro
R : Type u_3
inst✝¹¹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
P : Type ?u.431142
inst✝⁸ : CommRing P
Rₘ : Type u_1
Sₘ : Type ?u.431151
inst✝⁷ : CommRing Rₘ
inst✝⁶ : CommRing Sₘ
inst✝⁵ : Algebra R Rₘ
inst✝⁴ : IsLocalization M Rₘ
inst✝³ : Algebra S Sₘ
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst✝¹ : Algebra Rₘ S
inst✝ : IsScalarTower R Rₘ S
x : S
nontriv : Nontrivial Rₘ
p : Rₘ[X]
hp₁ : Monic p
hp₂ : eval₂ (_root_.algebraMap Rₘ S) x p = 0
p' : R[X]
hp'₁ :
  Polynomial.map (_root_.algebraMap R Rₘ) p' =
    scaleRoots p (↑(_root_.algebraMap R Rₘ) ↑(commonDenom M (support p) (coeff p)))
hp'₂ : Monic p'
⊢ ∃ m, IsIntegral R (m • x)

case inr.intro.intro.refine_1
R : Type u_3
inst✝¹¹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
P : Type ?u.431142
inst✝⁸ : CommRing P
Rₘ : Type u_1
Sₘ : Type ?u.431151
inst✝⁷ : CommRing Rₘ
inst✝⁶ : CommRing Sₘ
inst✝⁵ : Algebra R Rₘ
inst✝⁴ : IsLocalization M Rₘ
inst✝³ : Algebra S Sₘ
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst✝¹ : Algebra Rₘ S
inst✝ : IsScalarTower R Rₘ S
x : S
nontriv : Nontrivial Rₘ
p : Rₘ[X]
hp₁ : Monic p
hp₂ : eval₂ (_root_.algebraMap Rₘ S) x p = 0
⊢ leadingCoeff p ∈ RingHom.range (_root_.algebraMap R Rₘ)

case inr.intro.intro.refine_2
R : Type u_3
inst✝¹¹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
P : Type ?u.431142
inst✝⁸ : CommRing P
Rₘ : Type u_1
Sₘ : Type ?u.431151
inst✝⁷ : CommRing Rₘ
inst✝⁶ : CommRing Sₘ
inst✝⁵ : Algebra R Rₘ
inst✝⁴ : IsLocalization M Rₘ
inst✝³ : Algebra S Sₘ
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst✝¹ : Algebra Rₘ S
inst✝ : IsScalarTower R Rₘ S
x : S
nontriv : Nontrivial Rₘ
p : Rₘ[X]
hp₁ : Monic p
hp₂ : eval₂ (_root_.algebraMap Rₘ S) x p = 0
⊢ Monic (scaleRoots p (↑(_root_.algebraMap R Rₘ) ↑(commonDenom M (support p) (coeff p))))
case inr.intro.intro.refine_3
R : Type u_3
inst✝¹¹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
P : Type ?u.431142
inst✝⁸ : CommRing P
Rₘ : Type u_1
Sₘ : Type ?u.431151
inst✝⁷ : CommRing Rₘ
inst✝⁶ : CommRing Sₘ
inst✝⁵ : Algebra R Rₘ
inst✝⁴ : IsLocalization M Rₘ
inst✝³ : Algebra S Sₘ
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst✝¹ : Algebra Rₘ S
inst✝ : IsScalarTower R Rₘ S
x : S
nontriv : Nontrivial Rₘ
p : Rₘ[X]
hp₁ : Monic p
hp₂ : eval₂ (_root_.algebraMap Rₘ S) x p = 0
this :
  ∃ q,
    Polynomial.map (_root_.algebraMap R Rₘ) q =
        scaleRoots p (↑(_root_.algebraMap R Rₘ) ↑(commonDenom M (support p) (coeff p))) ∧
      natDegree q = natDegree (scaleRoots p (↑(_root_.algebraMap R Rₘ) ↑(commonDenom M (support p) (coeff p)))) ∧
        Monic q
⊢ ∃ m, IsIntegral R (m • x)

case inr.intro.intro.refine_1
R : Type u_3
inst✝¹¹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
P : Type ?u.431142
inst✝⁸ : CommRing P
Rₘ : Type u_1
Sₘ : Type ?u.431151
inst✝⁷ : CommRing Rₘ
inst✝⁶ : CommRing Sₘ
inst✝⁵ : Algebra R Rₘ
inst✝⁴ : IsLocalization M Rₘ
inst✝³ : Algebra S Sₘ
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst✝¹ : Algebra Rₘ S
inst✝ : IsScalarTower R Rₘ S
x : S
nontriv : Nontrivial Rₘ
p : Rₘ[X]
hp₁ : Monic p
hp₂ : eval₂ (_root_.algebraMap Rₘ S) x p = 0
⊢ leadingCoeff p ∈ RingHom.range (_root_.algebraMap R Rₘ)

case inr.intro.intro.refine_2
R : Type u_3
inst✝¹¹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
P : Type ?u.431142
inst✝⁸ : CommRing P
Rₘ : Type u_1
Sₘ : Type ?u.431151
inst✝⁷ : CommRing Rₘ
inst✝⁶ : CommRing Sₘ
inst✝⁵ : Algebra R Rₘ
inst✝⁴ : IsLocalization M Rₘ
inst✝³ : Algebra S Sₘ
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst✝¹ : Algebra Rₘ S
inst✝ : IsScalarTower R Rₘ S
x : S
nontriv : Nontrivial Rₘ
p : Rₘ[X]
hp₁ : Monic p
hp₂ : eval₂ (_root_.algebraMap Rₘ S) x p = 0
⊢ Monic (scaleRoots p (↑(_root_.algebraMap R Rₘ) ↑(commonDenom M (support p) (coeff p))))
obtain ⟨p', hp'₁, -, hp'₂⟩ := this
case inl
R : Type u_3
inst✝¹¹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
P : Type ?u.431142
inst✝⁸ : CommRing P
Rₘ : Type u_1
Sₘ : Type ?u.431151
inst✝⁷ : CommRing Rₘ
inst✝⁶ : CommRing Sₘ
inst✝⁵ : Algebra R Rₘ
inst✝⁴ : IsLocalization M Rₘ
inst✝³ : Algebra S Sₘ
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst✝¹ : Algebra Rₘ S
inst✝ : IsScalarTower R Rₘ S
x : S
hx : IsIntegral Rₘ x
h✝ : Subsingleton Rₘ
this : Subsingleton S
⊢ ∃ m, IsIntegral R (m • x)
case inl
R : Type u_3
inst✝¹¹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
P : Type ?u.431142
inst✝⁸ : CommRing P
Rₘ : Type u_1
Sₘ : Type ?u.431151
inst✝⁷ : CommRing Rₘ
inst✝⁶ : CommRing Sₘ
inst✝⁵ : Algebra R Rₘ
inst✝⁴ : IsLocalization M Rₘ
inst✝³ : Algebra S Sₘ
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst✝¹ : Algebra Rₘ S
inst✝ : IsScalarTower R Rₘ S
x : S
hx : IsIntegral Rₘ x
h✝ : Subsingleton Rₘ
⊢ ∃ m, IsIntegral R (m • x)
haveI := (_root_.algebraMap Rₘ S).codomain_trivial
no goals
case inl
R : Type u_3
inst✝¹¹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
P : Type ?u.431142
inst✝⁸ : CommRing P
Rₘ : Type u_1
Sₘ : Type ?u.431151
inst✝⁷ : CommRing Rₘ
inst✝⁶ : CommRing Sₘ
inst✝⁵ : Algebra R Rₘ
inst✝⁴ : IsLocalization M Rₘ
inst✝³ : Algebra S Sₘ
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst✝¹ : Algebra Rₘ S
inst✝ : IsScalarTower R Rₘ S
x : S
hx : IsIntegral Rₘ x
h✝ : Subsingleton Rₘ
this : Subsingleton S
⊢ ∃ m, IsIntegral R (m • x)
exact ⟨1, Polynomial.X, Polynomial.monic_X, Subsingleton.elim _ _⟩
case inr.intro.intro.refine_3.intro.intro.intro
R : Type u_3
inst✝¹¹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
P : Type ?u.431142
inst✝⁸ : CommRing P
Rₘ : Type u_1
Sₘ : Type ?u.431151
inst✝⁷ : CommRing Rₘ
inst✝⁶ : CommRing Sₘ
inst✝⁵ : Algebra R Rₘ
inst✝⁴ : IsLocalization M Rₘ
inst✝³ : Algebra S Sₘ
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst✝¹ : Algebra Rₘ S
inst✝ : IsScalarTower R Rₘ S
x : S
nontriv : Nontrivial Rₘ
p : Rₘ[X]
hp₁ : Monic p
hp₂ : eval₂ (_root_.algebraMap Rₘ S) x p = 0
p' : R[X]
hp'₁ :
  Polynomial.map (_root_.algebraMap R Rₘ) p' =
    scaleRoots p (↑(_root_.algebraMap R Rₘ) ↑(commonDenom M (support p) (coeff p)))
hp'₂ : Monic p'
⊢ eval₂ (_root_.algebraMap R S) (commonDenom M (support p) (coeff p) • x) p' = 0
case inr.intro.intro.refine_3.intro.intro.intro
R : Type u_3
inst✝¹¹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
P : Type ?u.431142
inst✝⁸ : CommRing P
Rₘ : Type u_1
Sₘ : Type ?u.431151
inst✝⁷ : CommRing Rₘ
inst✝⁶ : CommRing Sₘ
inst✝⁵ : Algebra R Rₘ
inst✝⁴ : IsLocalization M Rₘ
inst✝³ : Algebra S Sₘ
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst✝¹ : Algebra Rₘ S
inst✝ : IsScalarTower R Rₘ S
x : S
nontriv : Nontrivial Rₘ
p : Rₘ[X]
hp₁ : Monic p
hp₂ : eval₂ (_root_.algebraMap Rₘ S) x p = 0
p' : R[X]
hp'₁ :
  Polynomial.map (_root_.algebraMap R Rₘ) p' =
    scaleRoots p (↑(_root_.algebraMap R Rₘ) ↑(commonDenom M (support p) (coeff p)))
hp'₂ : Monic p'
⊢ ∃ m, IsIntegral R (m • x)
refine' ⟨IsLocalization.commonDenom M p.support p.coeff, p', hp'₂, _⟩
case inr.intro.intro.refine_3.intro.intro.intro
R : Type u_3
inst✝¹¹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
P : Type ?u.431142
inst✝⁸ : CommRing P
Rₘ : Type u_1
Sₘ : Type ?u.431151
inst✝⁷ : CommRing Rₘ
inst✝⁶ : CommRing Sₘ
inst✝⁵ : Algebra R Rₘ
inst✝⁴ : IsLocalization M Rₘ
inst✝³ : Algebra S Sₘ
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst✝¹ : Algebra Rₘ S
inst✝ : IsScalarTower R Rₘ S
x : S
nontriv : Nontrivial Rₘ
p : Rₘ[X]
hp₁ : Monic p
hp₂ : eval₂ (_root_.algebraMap Rₘ S) x p = 0
p' : R[X]
hp'₁ :
  Polynomial.map (_root_.algebraMap R Rₘ) p' =
    scaleRoots p (↑(_root_.algebraMap R Rₘ) ↑(commonDenom M (support p) (coeff p)))
hp'₂ : Monic p'
⊢ eval₂ (_root_.algebraMap Rₘ S)
      (↑(_root_.algebraMap Rₘ S) (↑(_root_.algebraMap R Rₘ) ↑(commonDenom M (support p) (coeff p))) * x)
      (scaleRoots p (↑(_root_.algebraMap R Rₘ) ↑(commonDenom M (support p) (coeff p)))) =
    0
case inr.intro.intro.refine_3.intro.intro.intro
R : Type u_3
inst✝¹¹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
P : Type ?u.431142
inst✝⁸ : CommRing P
Rₘ : Type u_1
Sₘ : Type ?u.431151
inst✝⁷ : CommRing Rₘ
inst✝⁶ : CommRing Sₘ
inst✝⁵ : Algebra R Rₘ
inst✝⁴ : IsLocalization M Rₘ
inst✝³ : Algebra S Sₘ
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst✝¹ : Algebra Rₘ S
inst✝ : IsScalarTower R Rₘ S
x : S
nontriv : Nontrivial Rₘ
p : Rₘ[X]
hp₁ : Monic p
hp₂ : eval₂ (_root_.algebraMap Rₘ S) x p = 0
p' : R[X]
hp'₁ :
  Polynomial.map (_root_.algebraMap R Rₘ) p' =
    scaleRoots p (↑(_root_.algebraMap R Rₘ) ↑(commonDenom M (support p) (coeff p)))
hp'₂ : Monic p'
⊢ eval₂ (_root_.algebraMap R S) (commonDenom M (support p) (coeff p) • x) p' = 0
rw [IsScalarTower.algebraMap_eq R Rₘ S, ← Polynomial.eval₂_map, hp'₁, Submonoid.smul_def,
  Algebra.smul_def, IsScalarTower.algebraMap_apply R Rₘ S]
no goals
case inr.intro.intro.refine_3.intro.intro.intro
R : Type u_3
inst✝¹¹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
P : Type ?u.431142
inst✝⁸ : CommRing P
Rₘ : Type u_1
Sₘ : Type ?u.431151
inst✝⁷ : CommRing Rₘ
inst✝⁶ : CommRing Sₘ
inst✝⁵ : Algebra R Rₘ
inst✝⁴ : IsLocalization M Rₘ
inst✝³ : Algebra S Sₘ
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst✝¹ : Algebra Rₘ S
inst✝ : IsScalarTower R Rₘ S
x : S
nontriv : Nontrivial Rₘ
p : Rₘ[X]
hp₁ : Monic p
hp₂ : eval₂ (_root_.algebraMap Rₘ S) x p = 0
p' : R[X]
hp'₁ :
  Polynomial.map (_root_.algebraMap R Rₘ) p' =
    scaleRoots p (↑(_root_.algebraMap R Rₘ) ↑(commonDenom M (support p) (coeff p)))
hp'₂ : Monic p'
⊢ eval₂ (_root_.algebraMap Rₘ S)
      (↑(_root_.algebraMap Rₘ S) (↑(_root_.algebraMap R Rₘ) ↑(commonDenom M (support p) (coeff p))) * x)
      (scaleRoots p (↑(_root_.algebraMap R Rₘ) ↑(commonDenom M (support p) (coeff p)))) =
    0
exact Polynomial.scaleRoots_eval₂_eq_zero _ hp₂
case inr.intro.intro.refine_1
R : Type u_3
inst✝¹¹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
P : Type ?u.431142
inst✝⁸ : CommRing P
Rₘ : Type u_1
Sₘ : Type ?u.431151
inst✝⁷ : CommRing Rₘ
inst✝⁶ : CommRing Sₘ
inst✝⁵ : Algebra R Rₘ
inst✝⁴ : IsLocalization M Rₘ
inst✝³ : Algebra S Sₘ
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst✝¹ : Algebra Rₘ S
inst✝ : IsScalarTower R Rₘ S
x : S
nontriv : Nontrivial Rₘ
p : Rₘ[X]
hp₁ : Monic p
hp₂ : eval₂ (_root_.algebraMap Rₘ S) x p = 0
⊢ 1 ∈ RingHom.range (_root_.algebraMap R Rₘ)
case inr.intro.intro.refine_1
R : Type u_3
inst✝¹¹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
P : Type ?u.431142
inst✝⁸ : CommRing P
Rₘ : Type u_1
Sₘ : Type ?u.431151
inst✝⁷ : CommRing Rₘ
inst✝⁶ : CommRing Sₘ
inst✝⁵ : Algebra R Rₘ
inst✝⁴ : IsLocalization M Rₘ
inst✝³ : Algebra S Sₘ
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst✝¹ : Algebra Rₘ S
inst✝ : IsScalarTower R Rₘ S
x : S
nontriv : Nontrivial Rₘ
p : Rₘ[X]
hp₁ : Monic p
hp₂ : eval₂ (_root_.algebraMap Rₘ S) x p = 0
⊢ leadingCoeff p ∈ RingHom.range (_root_.algebraMap R Rₘ)
rw [hp₁.leadingCoeff]
no goals
case inr.intro.intro.refine_1
R : Type u_3
inst✝¹¹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
P : Type ?u.431142
inst✝⁸ : CommRing P
Rₘ : Type u_1
Sₘ : Type ?u.431151
inst✝⁷ : CommRing Rₘ
inst✝⁶ : CommRing Sₘ
inst✝⁵ : Algebra R Rₘ
inst✝⁴ : IsLocalization M Rₘ
inst✝³ : Algebra S Sₘ
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst✝¹ : Algebra Rₘ S
inst✝ : IsScalarTower R Rₘ S
x : S
nontriv : Nontrivial Rₘ
p : Rₘ[X]
hp₁ : Monic p
hp₂ : eval₂ (_root_.algebraMap Rₘ S) x p = 0
⊢ 1 ∈ RingHom.range (_root_.algebraMap R Rₘ)
exact one_mem _
no goals
case inr.intro.intro.refine_2
R : Type u_3
inst✝¹¹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
P : Type ?u.431142
inst✝⁸ : CommRing P
Rₘ : Type u_1
Sₘ : Type ?u.431151
inst✝⁷ : CommRing Rₘ
inst✝⁶ : CommRing Sₘ
inst✝⁵ : Algebra R Rₘ
inst✝⁴ : IsLocalization M Rₘ
inst✝³ : Algebra S Sₘ
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst✝¹ : Algebra Rₘ S
inst✝ : IsScalarTower R Rₘ S
x : S
nontriv : Nontrivial Rₘ
p : Rₘ[X]
hp₁ : Monic p
hp₂ : eval₂ (_root_.algebraMap Rₘ S) x p = 0
⊢ Monic (scaleRoots p (↑(_root_.algebraMap R Rₘ) ↑(commonDenom M (support p) (coeff p))))
rwa [Polynomial.monic_scaleRoots_iff]