R : Type u_2
inst✝⁹ : CommRing R
M : Submonoid R
S : Type ?u.399271
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type ?u.399527
inst✝⁶ : CommRing P
Rₘ : Type u_1
Sₘ : Type ?u.399536
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ₘ
p : Rₘ[X]
hp : leadingCoeff p ∈ RingHom.range (algebraMap R Rₘ)
⊢ ∀ (n : ℕ),
    coeff (scaleRoots p (↑(algebraMap R Rₘ) ↑(commonDenom M (support p) (coeff p)))) n ∈ Set.range ↑(algebraMap R Rₘ)
R : Type u_2
inst✝⁹ : CommRing R
M : Submonoid R
S : Type ?u.399271
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type ?u.399527
inst✝⁶ : CommRing P
Rₘ : Type u_1
Sₘ : Type ?u.399536
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ₘ
p : Rₘ[X]
hp : leadingCoeff p ∈ RingHom.range (algebraMap R Rₘ)
⊢ scaleRoots p (↑(algebraMap R Rₘ) ↑(commonDenom M (support p) (coeff p))) ∈ lifts (algebraMap R Rₘ)
rw [Polynomial.lifts_iff_coeff_lifts]
R : Type u_2
inst✝⁹ : CommRing R
M : Submonoid R
S : Type ?u.399271
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type ?u.399527
inst✝⁶ : CommRing P
Rₘ : Type u_1
Sₘ : Type ?u.399536
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ₘ
p : Rₘ[X]
hp : leadingCoeff p ∈ RingHom.range (algebraMap R Rₘ)
n : ℕ
⊢ coeff (scaleRoots p (↑(algebraMap R Rₘ) ↑(commonDenom M (support p) (coeff p)))) n ∈ Set.range ↑(algebraMap R Rₘ)
R : Type u_2
inst✝⁹ : CommRing R
M : Submonoid R
S : Type ?u.399271
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type ?u.399527
inst✝⁶ : CommRing P
Rₘ : Type u_1
Sₘ : Type ?u.399536
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ₘ
p : Rₘ[X]
hp : leadingCoeff p ∈ RingHom.range (algebraMap R Rₘ)
⊢ ∀ (n : ℕ),
    coeff (scaleRoots p (↑(algebraMap R Rₘ) ↑(commonDenom M (support p) (coeff p)))) n ∈ Set.range ↑(algebraMap R Rₘ)
intro n
R : Type u_2
inst✝⁹ : CommRing R
M : Submonoid R
S : Type ?u.399271
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type ?u.399527
inst✝⁶ : CommRing P
Rₘ : Type u_1
Sₘ : Type ?u.399536
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ₘ
p : Rₘ[X]
hp : leadingCoeff p ∈ RingHom.range (algebraMap R Rₘ)
n : ℕ
⊢ coeff p n * ↑(algebraMap R Rₘ) ↑(commonDenom M (support p) (coeff p)) ^ (natDegree p - n) ∈
    Set.range ↑(algebraMap R Rₘ)
R : Type u_2
inst✝⁹ : CommRing R
M : Submonoid R
S : Type ?u.399271
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type ?u.399527
inst✝⁶ : CommRing P
Rₘ : Type u_1
Sₘ : Type ?u.399536
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ₘ
p : Rₘ[X]
hp : leadingCoeff p ∈ RingHom.range (algebraMap R Rₘ)
n : ℕ
⊢ coeff (scaleRoots p (↑(algebraMap R Rₘ) ↑(commonDenom M (support p) (coeff p)))) n ∈ Set.range ↑(algebraMap R Rₘ)
rw [Polynomial.coeff_scaleRoots]
case pos
R : Type u_2
inst✝⁹ : CommRing R
M : Submonoid R
S : Type ?u.399271
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type ?u.399527
inst✝⁶ : CommRing P
Rₘ : Type u_1
Sₘ : Type ?u.399536
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ₘ
p : Rₘ[X]
hp : leadingCoeff p ∈ RingHom.range (algebraMap R Rₘ)
n : ℕ
h₁ : n ∈ support p
⊢ coeff p n * ↑(algebraMap R Rₘ) ↑(commonDenom M (support p) (coeff p)) ^ (natDegree p - n) ∈
    Set.range ↑(algebraMap R Rₘ)

case neg
R : Type u_2
inst✝⁹ : CommRing R
M : Submonoid R
S : Type ?u.399271
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type ?u.399527
inst✝⁶ : CommRing P
Rₘ : Type u_1
Sₘ : Type ?u.399536
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ₘ
p : Rₘ[X]
hp : leadingCoeff p ∈ RingHom.range (algebraMap R Rₘ)
n : ℕ
h₁ : ¬n ∈ support p
⊢ coeff p n * ↑(algebraMap R Rₘ) ↑(commonDenom M (support p) (coeff p)) ^ (natDegree p - n) ∈
    Set.range ↑(algebraMap R Rₘ)
R : Type u_2
inst✝⁹ : CommRing R
M : Submonoid R
S : Type ?u.399271
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type ?u.399527
inst✝⁶ : CommRing P
Rₘ : Type u_1
Sₘ : Type ?u.399536
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ₘ
p : Rₘ[X]
hp : leadingCoeff p ∈ RingHom.range (algebraMap R Rₘ)
n : ℕ
⊢ coeff p n * ↑(algebraMap R Rₘ) ↑(commonDenom M (support p) (coeff p)) ^ (natDegree p - n) ∈
    Set.range ↑(algebraMap R Rₘ)
by_cases h₁ : n ∈ p.support
case pos
R : Type u_2
inst✝⁹ : CommRing R
M : Submonoid R
S : Type ?u.399271
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type ?u.399527
inst✝⁶ : CommRing P
Rₘ : Type u_1
Sₘ : Type ?u.399536
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ₘ
p : Rₘ[X]
hp : leadingCoeff p ∈ RingHom.range (algebraMap R Rₘ)
n : ℕ
h₁ : n ∈ support p
h₂ : n = natDegree p
⊢ coeff p n * ↑(algebraMap R Rₘ) ↑(commonDenom M (support p) (coeff p)) ^ (natDegree p - n) ∈
    Set.range ↑(algebraMap R Rₘ)

case neg
R : Type u_2
inst✝⁹ : CommRing R
M : Submonoid R
S : Type ?u.399271
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type ?u.399527
inst✝⁶ : CommRing P
Rₘ : Type u_1
Sₘ : Type ?u.399536
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ₘ
p : Rₘ[X]
hp : leadingCoeff p ∈ RingHom.range (algebraMap R Rₘ)
n : ℕ
h₁ : n ∈ support p
h₂ : ¬n = natDegree p
⊢ coeff p n * ↑(algebraMap R Rₘ) ↑(commonDenom M (support p) (coeff p)) ^ (natDegree p - n) ∈
    Set.range ↑(algebraMap R Rₘ)

case neg
R : Type u_2
inst✝⁹ : CommRing R
M : Submonoid R
S : Type ?u.399271
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type ?u.399527
inst✝⁶ : CommRing P
Rₘ : Type u_1
Sₘ : Type ?u.399536
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ₘ
p : Rₘ[X]
hp : leadingCoeff p ∈ RingHom.range (algebraMap R Rₘ)
n : ℕ
h₁ : ¬n ∈ support p
⊢ coeff p n * ↑(algebraMap R Rₘ) ↑(commonDenom M (support p) (coeff p)) ^ (natDegree p - n) ∈
    Set.range ↑(algebraMap R Rₘ)
case pos
R : Type u_2
inst✝⁹ : CommRing R
M : Submonoid R
S : Type ?u.399271
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type ?u.399527
inst✝⁶ : CommRing P
Rₘ : Type u_1
Sₘ : Type ?u.399536
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ₘ
p : Rₘ[X]
hp : leadingCoeff p ∈ RingHom.range (algebraMap R Rₘ)
n : ℕ
h₁ : n ∈ support p
⊢ coeff p n * ↑(algebraMap R Rₘ) ↑(commonDenom M (support p) (coeff p)) ^ (natDegree p - n) ∈
    Set.range ↑(algebraMap R Rₘ)

case neg
R : Type u_2
inst✝⁹ : CommRing R
M : Submonoid R
S : Type ?u.399271
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type ?u.399527
inst✝⁶ : CommRing P
Rₘ : Type u_1
Sₘ : Type ?u.399536
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ₘ
p : Rₘ[X]
hp : leadingCoeff p ∈ RingHom.range (algebraMap R Rₘ)
n : ℕ
h₁ : ¬n ∈ support p
⊢ coeff p n * ↑(algebraMap R Rₘ) ↑(commonDenom M (support p) (coeff p)) ^ (natDegree p - n) ∈
    Set.range ↑(algebraMap R Rₘ)
by_cases h₂ : n = p.natDegree
no goals
case pos
R : Type u_2
inst✝⁹ : CommRing R
M : Submonoid R
S : Type ?u.399271
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type ?u.399527
inst✝⁶ : CommRing P
Rₘ : Type u_1
Sₘ : Type ?u.399536
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ₘ
p : Rₘ[X]
hp : leadingCoeff p ∈ RingHom.range (algebraMap R Rₘ)
n : ℕ
h₁ : n ∈ support p
h₂ : n = natDegree p
⊢ coeff p n * ↑(algebraMap R Rₘ) ↑(commonDenom M (support p) (coeff p)) ^ (natDegree p - n) ∈
    Set.range ↑(algebraMap R Rₘ)
rwa [h₂, Polynomial.coeff_natDegree, tsub_self, pow_zero, _root_.mul_one]
case neg
R : Type u_2
inst✝⁹ : CommRing R
M : Submonoid R
S : Type ?u.399271
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type ?u.399527
inst✝⁶ : CommRing P
Rₘ : Type u_1
Sₘ : Type ?u.399536
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ₘ
p : Rₘ[X]
hp : leadingCoeff p ∈ RingHom.range (algebraMap R Rₘ)
n : ℕ
h₁ : n ∈ support p
h₂ : ¬n = natDegree p
this : n + 1 ≤ natDegree p
⊢ coeff p n * ↑(algebraMap R Rₘ) ↑(commonDenom M (support p) (coeff p)) ^ (natDegree p - n) ∈
    Set.range ↑(algebraMap R Rₘ)
case neg
R : Type u_2
inst✝⁹ : CommRing R
M : Submonoid R
S : Type ?u.399271
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type ?u.399527
inst✝⁶ : CommRing P
Rₘ : Type u_1
Sₘ : Type ?u.399536
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ₘ
p : Rₘ[X]
hp : leadingCoeff p ∈ RingHom.range (algebraMap R Rₘ)
n : ℕ
h₁ : n ∈ support p
h₂ : ¬n = natDegree p
⊢ coeff p n * ↑(algebraMap R Rₘ) ↑(commonDenom M (support p) (coeff p)) ^ (natDegree p - n) ∈
    Set.range ↑(algebraMap R Rₘ)
have : n + 1 ≤ p.natDegree := lt_of_le_of_ne (Polynomial.le_natDegree_of_mem_supp _ h₁) h₂
case neg
R : Type u_2
inst✝⁹ : CommRing R
M : Submonoid R
S : Type ?u.399271
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type ?u.399527
inst✝⁶ : CommRing P
Rₘ : Type u_1
Sₘ : Type ?u.399536
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ₘ
p : Rₘ[X]
hp : leadingCoeff p ∈ RingHom.range (algebraMap R Rₘ)
n : ℕ
h₁ : n ∈ support p
h₂ : ¬n = natDegree p
this : n + 1 ≤ natDegree p
⊢ ↑(algebraMap R Rₘ) (↑(commonDenom M (support p) (coeff p)) ^ (natDegree p - n - 1)) *
      (↑(algebraMap R Rₘ) ↑(commonDenom M (support p) (coeff p)) * coeff p n) ∈
    Set.range ↑(algebraMap R Rₘ)
case neg
R : Type u_2
inst✝⁹ : CommRing R
M : Submonoid R
S : Type ?u.399271
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type ?u.399527
inst✝⁶ : CommRing P
Rₘ : Type u_1
Sₘ : Type ?u.399536
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ₘ
p : Rₘ[X]
hp : leadingCoeff p ∈ RingHom.range (algebraMap R Rₘ)
n : ℕ
h₁ : n ∈ support p
h₂ : ¬n = natDegree p
this : n + 1 ≤ natDegree p
⊢ coeff p n * ↑(algebraMap R Rₘ) ↑(commonDenom M (support p) (coeff p)) ^ (natDegree p - n) ∈
    Set.range ↑(algebraMap R Rₘ)
rw [← tsub_add_cancel_of_le (le_tsub_of_add_le_left this), pow_add, pow_one, mul_comm,
  _root_.mul_assoc, ← map_pow]
case neg
R : Type u_2
inst✝⁹ : CommRing R
M : Submonoid R
S : Type ?u.399271
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type ?u.399527
inst✝⁶ : CommRing P
Rₘ : Type u_1
Sₘ : Type ?u.399536
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ₘ
p : Rₘ[X]
hp : leadingCoeff p ∈ RingHom.range (algebraMap R Rₘ)
n : ℕ
h₁ : n ∈ support p
h₂ : ¬n = natDegree p
this : n + 1 ≤ natDegree p
⊢ ↑(algebraMap R Rₘ) (↑(commonDenom M (support p) (coeff p)) ^ (natDegree p - n - 1)) *
      (↑(algebraMap R Rₘ) ↑(commonDenom M (support p) (coeff p)) * coeff p n) ∈
    RingHom.range (algebraMap R Rₘ)
case neg
R : Type u_2
inst✝⁹ : CommRing R
M : Submonoid R
S : Type ?u.399271
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type ?u.399527
inst✝⁶ : CommRing P
Rₘ : Type u_1
Sₘ : Type ?u.399536
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ₘ
p : Rₘ[X]
hp : leadingCoeff p ∈ RingHom.range (algebraMap R Rₘ)
n : ℕ
h₁ : n ∈ support p
h₂ : ¬n = natDegree p
this : n + 1 ≤ natDegree p
⊢ ↑(algebraMap R Rₘ) (↑(commonDenom M (support p) (coeff p)) ^ (natDegree p - n - 1)) *
      (↑(algebraMap R Rₘ) ↑(commonDenom M (support p) (coeff p)) * coeff p n) ∈
    Set.range ↑(algebraMap R Rₘ)
change _ ∈ (algebraMap R Rₘ).range
case neg.a
R : Type u_2
inst✝⁹ : CommRing R
M : Submonoid R
S : Type ?u.399271
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type ?u.399527
inst✝⁶ : CommRing P
Rₘ : Type u_1
Sₘ : Type ?u.399536
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ₘ
p : Rₘ[X]
hp : leadingCoeff p ∈ RingHom.range (algebraMap R Rₘ)
n : ℕ
h₁ : n ∈ support p
h₂ : ¬n = natDegree p
this : n + 1 ≤ natDegree p
⊢ ↑(algebraMap R Rₘ) (↑(commonDenom M (support p) (coeff p)) ^ (natDegree p - n - 1)) ∈ RingHom.range (algebraMap R Rₘ)

case neg.a
R : Type u_2
inst✝⁹ : CommRing R
M : Submonoid R
S : Type ?u.399271
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type ?u.399527
inst✝⁶ : CommRing P
Rₘ : Type u_1
Sₘ : Type ?u.399536
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ₘ
p : Rₘ[X]
hp : leadingCoeff p ∈ RingHom.range (algebraMap R Rₘ)
n : ℕ
h₁ : n ∈ support p
h₂ : ¬n = natDegree p
this : n + 1 ≤ natDegree p
⊢ ↑(algebraMap R Rₘ) ↑(commonDenom M (support p) (coeff p)) * coeff p n ∈ RingHom.range (algebraMap R Rₘ)
case neg
R : Type u_2
inst✝⁹ : CommRing R
M : Submonoid R
S : Type ?u.399271
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type ?u.399527
inst✝⁶ : CommRing P
Rₘ : Type u_1
Sₘ : Type ?u.399536
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ₘ
p : Rₘ[X]
hp : leadingCoeff p ∈ RingHom.range (algebraMap R Rₘ)
n : ℕ
h₁ : n ∈ support p
h₂ : ¬n = natDegree p
this : n + 1 ≤ natDegree p
⊢ ↑(algebraMap R Rₘ) (↑(commonDenom M (support p) (coeff p)) ^ (natDegree p - n - 1)) *
      (↑(algebraMap R Rₘ) ↑(commonDenom M (support p) (coeff p)) * coeff p n) ∈
    RingHom.range (algebraMap R Rₘ)
apply mul_mem
no goals
case neg.a
R : Type u_2
inst✝⁹ : CommRing R
M : Submonoid R
S : Type ?u.399271
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type ?u.399527
inst✝⁶ : CommRing P
Rₘ : Type u_1
Sₘ : Type ?u.399536
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ₘ
p : Rₘ[X]
hp : leadingCoeff p ∈ RingHom.range (algebraMap R Rₘ)
n : ℕ
h₁ : n ∈ support p
h₂ : ¬n = natDegree p
this : n + 1 ≤ natDegree p
⊢ ↑(algebraMap R Rₘ) (↑(commonDenom M (support p) (coeff p)) ^ (natDegree p - n - 1)) ∈ RingHom.range (algebraMap R Rₘ)
exact RingHom.mem_range_self _ _
case neg.a
R : Type u_2
inst✝⁹ : CommRing R
M : Submonoid R
S : Type ?u.399271
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type ?u.399527
inst✝⁶ : CommRing P
Rₘ : Type u_1
Sₘ : Type ?u.399536
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ₘ
p : Rₘ[X]
hp : leadingCoeff p ∈ RingHom.range (algebraMap R Rₘ)
n : ℕ
h₁ : n ∈ support p
h₂ : ¬n = natDegree p
this : n + 1 ≤ natDegree p
⊢ ↑(commonDenom M (support p) (coeff p)) • coeff p n ∈ RingHom.range (algebraMap R Rₘ)
case neg.a
R : Type u_2
inst✝⁹ : CommRing R
M : Submonoid R
S : Type ?u.399271
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type ?u.399527
inst✝⁶ : CommRing P
Rₘ : Type u_1
Sₘ : Type ?u.399536
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ₘ
p : Rₘ[X]
hp : leadingCoeff p ∈ RingHom.range (algebraMap R Rₘ)
n : ℕ
h₁ : n ∈ support p
h₂ : ¬n = natDegree p
this : n + 1 ≤ natDegree p
⊢ ↑(algebraMap R Rₘ) ↑(commonDenom M (support p) (coeff p)) * coeff p n ∈ RingHom.range (algebraMap R Rₘ)
rw [← Algebra.smul_def]
no goals
case neg.a
R : Type u_2
inst✝⁹ : CommRing R
M : Submonoid R
S : Type ?u.399271
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type ?u.399527
inst✝⁶ : CommRing P
Rₘ : Type u_1
Sₘ : Type ?u.399536
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ₘ
p : Rₘ[X]
hp : leadingCoeff p ∈ RingHom.range (algebraMap R Rₘ)
n : ℕ
h₁ : n ∈ support p
h₂ : ¬n = natDegree p
this : n + 1 ≤ natDegree p
⊢ ↑(commonDenom M (support p) (coeff p)) • coeff p n ∈ RingHom.range (algebraMap R Rₘ)
exact ⟨_, IsLocalization.map_integerMultiple M p.support p.coeff ⟨n, h₁⟩⟩
case neg
R : Type u_2
inst✝⁹ : CommRing R
M : Submonoid R
S : Type ?u.399271
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type ?u.399527
inst✝⁶ : CommRing P
Rₘ : Type u_1
Sₘ : Type ?u.399536
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ₘ
p : Rₘ[X]
hp : leadingCoeff p ∈ RingHom.range (algebraMap R Rₘ)
n : ℕ
h₁ : coeff p n = 0
⊢ coeff p n * ↑(algebraMap R Rₘ) ↑(commonDenom M (support p) (coeff p)) ^ (natDegree p - n) ∈
    Set.range ↑(algebraMap R Rₘ)
case neg
R : Type u_2
inst✝⁹ : CommRing R
M : Submonoid R
S : Type ?u.399271
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type ?u.399527
inst✝⁶ : CommRing P
Rₘ : Type u_1
Sₘ : Type ?u.399536
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ₘ
p : Rₘ[X]
hp : leadingCoeff p ∈ RingHom.range (algebraMap R Rₘ)
n : ℕ
h₁ : ¬n ∈ support p
⊢ coeff p n * ↑(algebraMap R Rₘ) ↑(commonDenom M (support p) (coeff p)) ^ (natDegree p - n) ∈
    Set.range ↑(algebraMap R Rₘ)
rw [Polynomial.not_mem_support_iff] at h₁
case neg
R : Type u_2
inst✝⁹ : CommRing R
M : Submonoid R
S : Type ?u.399271
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type ?u.399527
inst✝⁶ : CommRing P
Rₘ : Type u_1
Sₘ : Type ?u.399536
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ₘ
p : Rₘ[X]
hp : leadingCoeff p ∈ RingHom.range (algebraMap R Rₘ)
n : ℕ
h₁ : coeff p n = 0
⊢ 0 ∈ Set.range ↑(algebraMap R Rₘ)
case neg
R : Type u_2
inst✝⁹ : CommRing R
M : Submonoid R
S : Type ?u.399271
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type ?u.399527
inst✝⁶ : CommRing P
Rₘ : Type u_1
Sₘ : Type ?u.399536
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ₘ
p : Rₘ[X]
hp : leadingCoeff p ∈ RingHom.range (algebraMap R Rₘ)
n : ℕ
h₁ : coeff p n = 0
⊢ coeff p n * ↑(algebraMap R Rₘ) ↑(commonDenom M (support p) (coeff p)) ^ (natDegree p - n) ∈
    Set.range ↑(algebraMap R Rₘ)
rw [h₁, MulZeroClass.zero_mul]
no goals
case neg
R : Type u_2
inst✝⁹ : CommRing R
M : Submonoid R
S : Type ?u.399271
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type ?u.399527
inst✝⁶ : CommRing P
Rₘ : Type u_1
Sₘ : Type ?u.399536
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ₘ
p : Rₘ[X]
hp : leadingCoeff p ∈ RingHom.range (algebraMap R Rₘ)
n : ℕ
h₁ : coeff p n = 0
⊢ 0 ∈ Set.range ↑(algebraMap R Rₘ)
exact zero_mem (algebraMap R Rₘ).range