[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
p : S[X]
i : ℕ
h : coeff p i = 0
⊢ coeffIntegerNormalization M p i = 0
[PROOFSTEP]
simp only [coeffIntegerNormalization, h, mem_support_iff, eq_self_iff_true, not_true, Ne.def, dif_neg, not_false_iff]
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
p : S[X]
i : ℕ
h : coeffIntegerNormalization M p i ≠ 0
⊢ i ∈ support p
[PROOFSTEP]
contrapose h
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
p : S[X]
i : ℕ
h : ¬i ∈ support p
⊢ ¬coeffIntegerNormalization M p i ≠ 0
[PROOFSTEP]
rw [Ne.def, Classical.not_not, coeffIntegerNormalization, dif_neg h]
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
p : S[X]
i : ℕ
⊢ coeff (integerNormalization M p) i = coeffIntegerNormalization M p i
[PROOFSTEP]
simp (config := { contextual := true }) [integerNormalization, coeff_monomial,
  coeffIntegerNormalization_of_not_mem_support]
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
p : S[X]
⊢ ∃ b, ∀ (i : ℕ), ↑(algebraMap R S) (coeff (integerNormalization M p) i) = ↑b • coeff p i
[PROOFSTEP]
use Classical.choose (exist_integer_multiples_of_finset M (p.support.image p.coeff))
[GOAL]
case h
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
p : S[X]
⊢ ∀ (i : ℕ),
    ↑(algebraMap R S) (coeff (integerNormalization M p) i) =
      ↑(choose (_ : ∃ b, ∀ (a : S), a ∈ Finset.image (coeff p) (support p) → IsInteger R (↑b • a))) • coeff p i
[PROOFSTEP]
intro i
[GOAL]
case h
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
p : S[X]
i : ℕ
⊢ ↑(algebraMap R S) (coeff (integerNormalization M p) i) =
    ↑(choose (_ : ∃ b, ∀ (a : S), a ∈ Finset.image (coeff p) (support p) → IsInteger R (↑b • a))) • coeff p i
[PROOFSTEP]
rw [integerNormalization_coeff, coeffIntegerNormalization]
[GOAL]
case h
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
p : S[X]
i : ℕ
⊢ ↑(algebraMap R S)
      (if hi : i ∈ support p then
        choose
          (_ :
            IsInteger R
              (↑(choose (_ : ∃ b, ∀ (a : S), a ∈ Finset.image (coeff p) (support p) → IsInteger R (↑b • a))) •
                coeff p i))
      else 0) =
    ↑(choose (_ : ∃ b, ∀ (a : S), a ∈ Finset.image (coeff p) (support p) → IsInteger R (↑b • a))) • coeff p i
[PROOFSTEP]
split_ifs with hi
[GOAL]
case pos
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
p : S[X]
i : ℕ
hi : i ∈ support p
⊢ ↑(algebraMap R S)
      (if hi : i ∈ support p then
        choose
          (_ :
            IsInteger R
              (↑(choose (_ : ∃ b, ∀ (a : S), a ∈ Finset.image (coeff p) (support p) → IsInteger R (↑b • a))) •
                coeff p i))
      else 0) =
    ↑(choose (_ : ∃ b, ∀ (a : S), a ∈ Finset.image (coeff p) (support p) → IsInteger R (↑b • a))) • coeff p i
[PROOFSTEP]
rw [dif_pos hi]
[GOAL]
case pos
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
p : S[X]
i : ℕ
hi : i ∈ support p
⊢ ↑(algebraMap R S)
      (choose
        (_ :
          IsInteger R
            (↑(choose (_ : ∃ b, ∀ (a : S), a ∈ Finset.image (coeff p) (support p) → IsInteger R (↑b • a))) •
              coeff p i))) =
    ↑(choose (_ : ∃ b, ∀ (a : S), a ∈ Finset.image (coeff p) (support p) → IsInteger R (↑b • a))) • coeff p i
[PROOFSTEP]
exact
  Classical.choose_spec
    (Classical.choose_spec (exist_integer_multiples_of_finset M (p.support.image p.coeff)) (p.coeff i)
      (Finset.mem_image.mpr ⟨i, hi, rfl⟩))
[GOAL]
case neg
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
p : S[X]
i : ℕ
hi : ¬i ∈ support p
⊢ ↑(algebraMap R S)
      (if hi : i ∈ support p then
        choose
          (_ :
            IsInteger R
              (↑(choose (_ : ∃ b, ∀ (a : S), a ∈ Finset.image (coeff p) (support p) → IsInteger R (↑b • a))) •
                coeff p i))
      else 0) =
    ↑(choose (_ : ∃ b, ∀ (a : S), a ∈ Finset.image (coeff p) (support p) → IsInteger R (↑b • a))) • coeff p i
[PROOFSTEP]
rw [dif_neg hi]
[GOAL]
case neg
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
p : S[X]
i : ℕ
hi : ¬i ∈ support p
⊢ ↑(algebraMap R S) 0 =
    ↑(choose (_ : ∃ b, ∀ (a : S), a ∈ Finset.image (coeff p) (support p) → IsInteger R (↑b • a))) • coeff p i
[PROOFSTEP]
rw [RingHom.map_zero, not_mem_support_iff.mp hi, smul_zero]
  -- Porting note: was `convert (smul_zero _).symm, ...`
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
p : S[X]
b : { x // x ∈ M }
hb : ∀ (i : ℕ), ↑(algebraMap R S) (coeff (integerNormalization M p) i) = ↑b • coeff p i
i : ℕ
⊢ coeff (Polynomial.map (algebraMap R S) (integerNormalization M p)) i = coeff (↑b • p) i
[PROOFSTEP]
rw [coeff_map, coeff_smul]
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
p : S[X]
b : { x // x ∈ M }
hb : ∀ (i : ℕ), ↑(algebraMap R S) (coeff (integerNormalization M p) i) = ↑b • coeff p i
i : ℕ
⊢ ↑(algebraMap R S) (coeff (integerNormalization M p) i) = ↑b • coeff p i
[PROOFSTEP]
exact hb i
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Type u_3
inst✝² : CommRing P
inst✝¹ : IsLocalization M S
R' : Type u_4
inst✝ : CommRing R'
g : S →+* R'
p : S[X]
x : R'
hx : eval₂ g x p = 0
b : { x // x ∈ M }
hb : Polynomial.map (algebraMap R S) (integerNormalization M p) = ↑b • p
⊢ eval₂ g x (Polynomial.map (algebraMap R S) (integerNormalization M p)) = 0
[PROOFSTEP]
rw [hb, ← IsScalarTower.algebraMap_smul S (b : R) p, eval₂_smul, hx, mul_zero]
[GOAL]
R : Type u_1
inst✝⁸ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
P : Type u_3
inst✝⁵ : CommRing P
inst✝⁴ : IsLocalization M S
R' : Type u_4
inst✝³ : CommRing R'
inst✝² : Algebra R R'
inst✝¹ : Algebra S R'
inst✝ : IsScalarTower R S R'
p : S[X]
x : R'
hx : ↑(aeval x) p = 0
⊢ ↑(aeval x) (integerNormalization M p) = 0
[PROOFSTEP]
rw [aeval_def, IsScalarTower.algebraMap_eq R S R', integerNormalization_eval₂_eq_zero _ _ _ hx]
[GOAL]
R : Type u_1
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type u_3
inst✝⁶ : CommRing P
A : Type u_4
K : Type u_5
C : Type u_6
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : CommRing C
p : K[X]
⊢ integerNormalization (nonZeroDivisors A) p = 0 ↔ p = 0
[PROOFSTEP]
refine' Polynomial.ext_iff.trans (Polynomial.ext_iff.trans _).symm
[GOAL]
R : Type u_1
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type u_3
inst✝⁶ : CommRing P
A : Type u_4
K : Type u_5
C : Type u_6
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : CommRing C
p : K[X]
⊢ (∀ (n : ℕ), coeff p n = coeff 0 n) ↔ ∀ (n : ℕ), coeff (integerNormalization (nonZeroDivisors A) p) n = coeff 0 n
[PROOFSTEP]
obtain ⟨⟨b, nonzero⟩, hb⟩ := integerNormalization_spec (nonZeroDivisors A) p
[GOAL]
case intro.mk
R : Type u_1
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type u_3
inst✝⁶ : CommRing P
A : Type u_4
K : Type u_5
C : Type u_6
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : CommRing C
p : K[X]
b : A
nonzero : b ∈ nonZeroDivisors A
hb :
  ∀ (i : ℕ),
    ↑(algebraMap A K) (coeff (integerNormalization (nonZeroDivisors A) p) i) =
      ↑{ val := b, property := nonzero } • coeff p i
⊢ (∀ (n : ℕ), coeff p n = coeff 0 n) ↔ ∀ (n : ℕ), coeff (integerNormalization (nonZeroDivisors A) p) n = coeff 0 n
[PROOFSTEP]
constructor
[GOAL]
case intro.mk.mp
R : Type u_1
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type u_3
inst✝⁶ : CommRing P
A : Type u_4
K : Type u_5
C : Type u_6
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : CommRing C
p : K[X]
b : A
nonzero : b ∈ nonZeroDivisors A
hb :
  ∀ (i : ℕ),
    ↑(algebraMap A K) (coeff (integerNormalization (nonZeroDivisors A) p) i) =
      ↑{ val := b, property := nonzero } • coeff p i
⊢ (∀ (n : ℕ), coeff p n = coeff 0 n) → ∀ (n : ℕ), coeff (integerNormalization (nonZeroDivisors A) p) n = coeff 0 n
[PROOFSTEP]
intro h i
[GOAL]
case intro.mk.mpr
R : Type u_1
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type u_3
inst✝⁶ : CommRing P
A : Type u_4
K : Type u_5
C : Type u_6
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : CommRing C
p : K[X]
b : A
nonzero : b ∈ nonZeroDivisors A
hb :
  ∀ (i : ℕ),
    ↑(algebraMap A K) (coeff (integerNormalization (nonZeroDivisors A) p) i) =
      ↑{ val := b, property := nonzero } • coeff p i
⊢ (∀ (n : ℕ), coeff (integerNormalization (nonZeroDivisors A) p) n = coeff 0 n) → ∀ (n : ℕ), coeff p n = coeff 0 n
[PROOFSTEP]
intro h i
[GOAL]
case intro.mk.mp
R : Type u_1
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type u_3
inst✝⁶ : CommRing P
A : Type u_4
K : Type u_5
C : Type u_6
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : CommRing C
p : K[X]
b : A
nonzero : b ∈ nonZeroDivisors A
hb :
  ∀ (i : ℕ),
    ↑(algebraMap A K) (coeff (integerNormalization (nonZeroDivisors A) p) i) =
      ↑{ val := b, property := nonzero } • coeff p i
h : ∀ (n : ℕ), coeff p n = coeff 0 n
i : ℕ
⊢ coeff (integerNormalization (nonZeroDivisors A) p) i = coeff 0 i
[PROOFSTEP]
rw [coeff_zero, ← to_map_eq_zero_iff (K := K), hb i, h i, coeff_zero, smul_zero]
[GOAL]
case intro.mk.mpr
R : Type u_1
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type u_3
inst✝⁶ : CommRing P
A : Type u_4
K : Type u_5
C : Type u_6
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : CommRing C
p : K[X]
b : A
nonzero : b ∈ nonZeroDivisors A
hb :
  ∀ (i : ℕ),
    ↑(algebraMap A K) (coeff (integerNormalization (nonZeroDivisors A) p) i) =
      ↑{ val := b, property := nonzero } • coeff p i
h : ∀ (n : ℕ), coeff (integerNormalization (nonZeroDivisors A) p) n = coeff 0 n
i : ℕ
⊢ coeff p i = coeff 0 i
[PROOFSTEP]
have hi := h i
[GOAL]
case intro.mk.mpr
R : Type u_1
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type u_3
inst✝⁶ : CommRing P
A : Type u_4
K : Type u_5
C : Type u_6
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : CommRing C
p : K[X]
b : A
nonzero : b ∈ nonZeroDivisors A
hb :
  ∀ (i : ℕ),
    ↑(algebraMap A K) (coeff (integerNormalization (nonZeroDivisors A) p) i) =
      ↑{ val := b, property := nonzero } • coeff p i
h : ∀ (n : ℕ), coeff (integerNormalization (nonZeroDivisors A) p) n = coeff 0 n
i : ℕ
hi : coeff (integerNormalization (nonZeroDivisors A) p) i = coeff 0 i
⊢ coeff p i = coeff 0 i
[PROOFSTEP]
rw [Polynomial.coeff_zero, ← @to_map_eq_zero_iff A _ K, hb i, Algebra.smul_def] at hi 
[GOAL]
case intro.mk.mpr
R : Type u_1
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type u_3
inst✝⁶ : CommRing P
A : Type u_4
K : Type u_5
C : Type u_6
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : CommRing C
p : K[X]
b : A
nonzero : b ∈ nonZeroDivisors A
hb :
  ∀ (i : ℕ),
    ↑(algebraMap A K) (coeff (integerNormalization (nonZeroDivisors A) p) i) =
      ↑{ val := b, property := nonzero } • coeff p i
h : ∀ (n : ℕ), coeff (integerNormalization (nonZeroDivisors A) p) n = coeff 0 n
i : ℕ
hi : ↑(algebraMap A K) ↑{ val := b, property := nonzero } * coeff p i = 0
⊢ coeff p i = coeff 0 i
[PROOFSTEP]
apply Or.resolve_left (eq_zero_or_eq_zero_of_mul_eq_zero hi)
[GOAL]
case intro.mk.mpr
R : Type u_1
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type u_3
inst✝⁶ : CommRing P
A : Type u_4
K : Type u_5
C : Type u_6
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : CommRing C
p : K[X]
b : A
nonzero : b ∈ nonZeroDivisors A
hb :
  ∀ (i : ℕ),
    ↑(algebraMap A K) (coeff (integerNormalization (nonZeroDivisors A) p) i) =
      ↑{ val := b, property := nonzero } • coeff p i
h : ∀ (n : ℕ), coeff (integerNormalization (nonZeroDivisors A) p) n = coeff 0 n
i : ℕ
hi : ↑(algebraMap A K) ↑{ val := b, property := nonzero } * coeff p i = 0
⊢ ¬↑(algebraMap A K) ↑{ val := b, property := nonzero } = 0
[PROOFSTEP]
intro h
[GOAL]
case intro.mk.mpr
R : Type u_1
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type u_3
inst✝⁶ : CommRing P
A : Type u_4
K : Type u_5
C : Type u_6
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : CommRing C
p : K[X]
b : A
nonzero : b ∈ nonZeroDivisors A
hb :
  ∀ (i : ℕ),
    ↑(algebraMap A K) (coeff (integerNormalization (nonZeroDivisors A) p) i) =
      ↑{ val := b, property := nonzero } • coeff p i
h✝ : ∀ (n : ℕ), coeff (integerNormalization (nonZeroDivisors A) p) n = coeff 0 n
i : ℕ
hi : ↑(algebraMap A K) ↑{ val := b, property := nonzero } * coeff p i = 0
h : ↑(algebraMap A K) ↑{ val := b, property := nonzero } = 0
⊢ False
[PROOFSTEP]
apply mem_nonZeroDivisors_iff_ne_zero.mp nonzero
[GOAL]
case intro.mk.mpr
R : Type u_1
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type u_3
inst✝⁶ : CommRing P
A : Type u_4
K : Type u_5
C : Type u_6
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : CommRing C
p : K[X]
b : A
nonzero : b ∈ nonZeroDivisors A
hb :
  ∀ (i : ℕ),
    ↑(algebraMap A K) (coeff (integerNormalization (nonZeroDivisors A) p) i) =
      ↑{ val := b, property := nonzero } • coeff p i
h✝ : ∀ (n : ℕ), coeff (integerNormalization (nonZeroDivisors A) p) n = coeff 0 n
i : ℕ
hi : ↑(algebraMap A K) ↑{ val := b, property := nonzero } * coeff p i = 0
h : ↑(algebraMap A K) ↑{ val := b, property := nonzero } = 0
⊢ b = 0
[PROOFSTEP]
exact to_map_eq_zero_iff.mp h
[GOAL]
R : Type u_1
inst✝¹² : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹¹ : CommRing S
inst✝¹⁰ : Algebra R S
P : Type u_3
inst✝⁹ : CommRing P
A : Type u_4
K : Type u_5
C : Type u_6
inst✝⁸ : CommRing A
inst✝⁷ : IsDomain A
inst✝⁶ : Field K
inst✝⁵ : Algebra A K
inst✝⁴ : IsFractionRing A K
inst✝³ : CommRing C
inst✝² : Algebra A C
inst✝¹ : Algebra K C
inst✝ : IsScalarTower A K C
x : C
⊢ IsAlgebraic A x ↔ IsAlgebraic K x
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u_1
inst✝¹² : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹¹ : CommRing S
inst✝¹⁰ : Algebra R S
P : Type u_3
inst✝⁹ : CommRing P
A : Type u_4
K : Type u_5
C : Type u_6
inst✝⁸ : CommRing A
inst✝⁷ : IsDomain A
inst✝⁶ : Field K
inst✝⁵ : Algebra A K
inst✝⁴ : IsFractionRing A K
inst✝³ : CommRing C
inst✝² : Algebra A C
inst✝¹ : Algebra K C
inst✝ : IsScalarTower A K C
x : C
⊢ IsAlgebraic A x → IsAlgebraic K x
[PROOFSTEP]
rintro ⟨p, hp, px⟩
[GOAL]
case mpr
R : Type u_1
inst✝¹² : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹¹ : CommRing S
inst✝¹⁰ : Algebra R S
P : Type u_3
inst✝⁹ : CommRing P
A : Type u_4
K : Type u_5
C : Type u_6
inst✝⁸ : CommRing A
inst✝⁷ : IsDomain A
inst✝⁶ : Field K
inst✝⁵ : Algebra A K
inst✝⁴ : IsFractionRing A K
inst✝³ : CommRing C
inst✝² : Algebra A C
inst✝¹ : Algebra K C
inst✝ : IsScalarTower A K C
x : C
⊢ IsAlgebraic K x → IsAlgebraic A x
[PROOFSTEP]
rintro ⟨p, hp, px⟩
[GOAL]
case mp.intro.intro
R : Type u_1
inst✝¹² : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹¹ : CommRing S
inst✝¹⁰ : Algebra R S
P : Type u_3
inst✝⁹ : CommRing P
A : Type u_4
K : Type u_5
C : Type u_6
inst✝⁸ : CommRing A
inst✝⁷ : IsDomain A
inst✝⁶ : Field K
inst✝⁵ : Algebra A K
inst✝⁴ : IsFractionRing A K
inst✝³ : CommRing C
inst✝² : Algebra A C
inst✝¹ : Algebra K C
inst✝ : IsScalarTower A K C
x : C
p : A[X]
hp : p ≠ 0
px : ↑(aeval x) p = 0
⊢ IsAlgebraic K x
[PROOFSTEP]
refine' ⟨p.map (algebraMap A K), fun h => hp (Polynomial.ext fun i => _), _⟩
[GOAL]
case mp.intro.intro.refine'_1
R : Type u_1
inst✝¹² : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹¹ : CommRing S
inst✝¹⁰ : Algebra R S
P : Type u_3
inst✝⁹ : CommRing P
A : Type u_4
K : Type u_5
C : Type u_6
inst✝⁸ : CommRing A
inst✝⁷ : IsDomain A
inst✝⁶ : Field K
inst✝⁵ : Algebra A K
inst✝⁴ : IsFractionRing A K
inst✝³ : CommRing C
inst✝² : Algebra A C
inst✝¹ : Algebra K C
inst✝ : IsScalarTower A K C
x : C
p : A[X]
hp : p ≠ 0
px : ↑(aeval x) p = 0
h : Polynomial.map (algebraMap A K) p = 0
i : ℕ
⊢ coeff p i = coeff 0 i
[PROOFSTEP]
have : algebraMap A K (p.coeff i) = 0 := _root_.trans (Polynomial.coeff_map _ _).symm (by simp [h])
[GOAL]
R : Type u_1
inst✝¹² : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹¹ : CommRing S
inst✝¹⁰ : Algebra R S
P : Type u_3
inst✝⁹ : CommRing P
A : Type u_4
K : Type u_5
C : Type u_6
inst✝⁸ : CommRing A
inst✝⁷ : IsDomain A
inst✝⁶ : Field K
inst✝⁵ : Algebra A K
inst✝⁴ : IsFractionRing A K
inst✝³ : CommRing C
inst✝² : Algebra A C
inst✝¹ : Algebra K C
inst✝ : IsScalarTower A K C
x : C
p : A[X]
hp : p ≠ 0
px : ↑(aeval x) p = 0
h : Polynomial.map (algebraMap A K) p = 0
i : ℕ
⊢ coeff (Polynomial.map (algebraMap A K) p) i = 0
[PROOFSTEP]
simp [h]
[GOAL]
case mp.intro.intro.refine'_1
R : Type u_1
inst✝¹² : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹¹ : CommRing S
inst✝¹⁰ : Algebra R S
P : Type u_3
inst✝⁹ : CommRing P
A : Type u_4
K : Type u_5
C : Type u_6
inst✝⁸ : CommRing A
inst✝⁷ : IsDomain A
inst✝⁶ : Field K
inst✝⁵ : Algebra A K
inst✝⁴ : IsFractionRing A K
inst✝³ : CommRing C
inst✝² : Algebra A C
inst✝¹ : Algebra K C
inst✝ : IsScalarTower A K C
x : C
p : A[X]
hp : p ≠ 0
px : ↑(aeval x) p = 0
h : Polynomial.map (algebraMap A K) p = 0
i : ℕ
this : ↑(algebraMap A K) (coeff p i) = 0
⊢ coeff p i = coeff 0 i
[PROOFSTEP]
exact to_map_eq_zero_iff.mp this
[GOAL]
case mp.intro.intro.refine'_2
R : Type u_1
inst✝¹² : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹¹ : CommRing S
inst✝¹⁰ : Algebra R S
P : Type u_3
inst✝⁹ : CommRing P
A : Type u_4
K : Type u_5
C : Type u_6
inst✝⁸ : CommRing A
inst✝⁷ : IsDomain A
inst✝⁶ : Field K
inst✝⁵ : Algebra A K
inst✝⁴ : IsFractionRing A K
inst✝³ : CommRing C
inst✝² : Algebra A C
inst✝¹ : Algebra K C
inst✝ : IsScalarTower A K C
x : C
p : A[X]
hp : p ≠ 0
px : ↑(aeval x) p = 0
⊢ ↑(aeval x) (Polynomial.map (algebraMap A K) p) = 0
[PROOFSTEP]
exact (Polynomial.aeval_map_algebraMap K _ _).trans px
[GOAL]
case mpr.intro.intro
R : Type u_1
inst✝¹² : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹¹ : CommRing S
inst✝¹⁰ : Algebra R S
P : Type u_3
inst✝⁹ : CommRing P
A : Type u_4
K : Type u_5
C : Type u_6
inst✝⁸ : CommRing A
inst✝⁷ : IsDomain A
inst✝⁶ : Field K
inst✝⁵ : Algebra A K
inst✝⁴ : IsFractionRing A K
inst✝³ : CommRing C
inst✝² : Algebra A C
inst✝¹ : Algebra K C
inst✝ : IsScalarTower A K C
x : C
p : K[X]
hp : p ≠ 0
px : ↑(aeval x) p = 0
⊢ IsAlgebraic A x
[PROOFSTEP]
exact ⟨integerNormalization _ p, mt integerNormalization_eq_zero_iff.mp hp, integerNormalization_aeval_eq_zero _ p px⟩
[GOAL]
R✝ : Type u_1
inst✝¹⁷ : CommRing R✝
M✝ : Submonoid R✝
S✝ : Type u_2
inst✝¹⁶ : CommRing S✝
inst✝¹⁵ : Algebra R✝ S✝
P : Type u_3
inst✝¹⁴ : CommRing P
Rₘ✝ : Type u_4
Sₘ✝ : Type u_5
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ₘ✝
R : Type u_6
S : Type u_7
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
f : R →+* S
x : S
p : R[X]
hf : eval₂ f x p = 0
M : Submonoid R
hM : leadingCoeff p ∈ M
Rₘ : Type u_8
Sₘ : Type u_9
inst✝⁵ : CommRing Rₘ
inst✝⁴ : CommRing Sₘ
inst✝³ : Algebra R Rₘ
inst✝² : IsLocalization M Rₘ
inst✝¹ : Algebra S Sₘ
inst✝ : IsLocalization (Submonoid.map f M) Sₘ
⊢ IsIntegralElem (IsLocalization.map Sₘ f (_ : M ≤ Submonoid.comap f (Submonoid.map f M))) (↑(algebraMap S Sₘ) x)
[PROOFSTEP]
by_cases triv : (1 : Rₘ) = 0
[GOAL]
case pos
R✝ : Type u_1
inst✝¹⁷ : CommRing R✝
M✝ : Submonoid R✝
S✝ : Type u_2
inst✝¹⁶ : CommRing S✝
inst✝¹⁵ : Algebra R✝ S✝
P : Type u_3
inst✝¹⁴ : CommRing P
Rₘ✝ : Type u_4
Sₘ✝ : Type u_5
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ₘ✝
R : Type u_6
S : Type u_7
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
f : R →+* S
x : S
p : R[X]
hf : eval₂ f x p = 0
M : Submonoid R
hM : leadingCoeff p ∈ M
Rₘ : Type u_8
Sₘ : Type u_9
inst✝⁵ : CommRing Rₘ
inst✝⁴ : CommRing Sₘ
inst✝³ : Algebra R Rₘ
inst✝² : IsLocalization M Rₘ
inst✝¹ : Algebra S Sₘ
inst✝ : IsLocalization (Submonoid.map f M) Sₘ
triv : 1 = 0
⊢ IsIntegralElem (IsLocalization.map Sₘ f (_ : M ≤ Submonoid.comap f (Submonoid.map f M))) (↑(algebraMap S Sₘ) x)
[PROOFSTEP]
exact ⟨0, ⟨_root_.trans leadingCoeff_zero triv.symm, eval₂_zero _ _⟩⟩
[GOAL]
case neg
R✝ : Type u_1
inst✝¹⁷ : CommRing R✝
M✝ : Submonoid R✝
S✝ : Type u_2
inst✝¹⁶ : CommRing S✝
inst✝¹⁵ : Algebra R✝ S✝
P : Type u_3
inst✝¹⁴ : CommRing P
Rₘ✝ : Type u_4
Sₘ✝ : Type u_5
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ₘ✝
R : Type u_6
S : Type u_7
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
f : R →+* S
x : S
p : R[X]
hf : eval₂ f x p = 0
M : Submonoid R
hM : leadingCoeff p ∈ M
Rₘ : Type u_8
Sₘ : Type u_9
inst✝⁵ : CommRing Rₘ
inst✝⁴ : CommRing Sₘ
inst✝³ : Algebra R Rₘ
inst✝² : IsLocalization M Rₘ
inst✝¹ : Algebra S Sₘ
inst✝ : IsLocalization (Submonoid.map f M) Sₘ
triv : ¬1 = 0
⊢ IsIntegralElem (IsLocalization.map Sₘ f (_ : M ≤ Submonoid.comap f (Submonoid.map f M))) (↑(algebraMap S Sₘ) x)
[PROOFSTEP]
haveI : Nontrivial Rₘ := nontrivial_of_ne 1 0 triv
[GOAL]
case neg
R✝ : Type u_1
inst✝¹⁷ : CommRing R✝
M✝ : Submonoid R✝
S✝ : Type u_2
inst✝¹⁶ : CommRing S✝
inst✝¹⁵ : Algebra R✝ S✝
P : Type u_3
inst✝¹⁴ : CommRing P
Rₘ✝ : Type u_4
Sₘ✝ : Type u_5
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ₘ✝
R : Type u_6
S : Type u_7
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
f : R →+* S
x : S
p : R[X]
hf : eval₂ f x p = 0
M : Submonoid R
hM : leadingCoeff p ∈ M
Rₘ : Type u_8
Sₘ : Type u_9
inst✝⁵ : CommRing Rₘ
inst✝⁴ : CommRing Sₘ
inst✝³ : Algebra R Rₘ
inst✝² : IsLocalization M Rₘ
inst✝¹ : Algebra S Sₘ
inst✝ : IsLocalization (Submonoid.map f M) Sₘ
triv : ¬1 = 0
this : Nontrivial Rₘ
⊢ IsIntegralElem (IsLocalization.map Sₘ f (_ : M ≤ Submonoid.comap f (Submonoid.map f M))) (↑(algebraMap S Sₘ) x)
[PROOFSTEP]
obtain ⟨b, hb⟩ := isUnit_iff_exists_inv.mp (map_units Rₘ ⟨p.leadingCoeff, hM⟩)
[GOAL]
case neg.intro
R✝ : Type u_1
inst✝¹⁷ : CommRing R✝
M✝ : Submonoid R✝
S✝ : Type u_2
inst✝¹⁶ : CommRing S✝
inst✝¹⁵ : Algebra R✝ S✝
P : Type u_3
inst✝¹⁴ : CommRing P
Rₘ✝ : Type u_4
Sₘ✝ : Type u_5
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ₘ✝
R : Type u_6
S : Type u_7
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
f : R →+* S
x : S
p : R[X]
hf : eval₂ f x p = 0
M : Submonoid R
hM : leadingCoeff p ∈ M
Rₘ : Type u_8
Sₘ : Type u_9
inst✝⁵ : CommRing Rₘ
inst✝⁴ : CommRing Sₘ
inst✝³ : Algebra R Rₘ
inst✝² : IsLocalization M Rₘ
inst✝¹ : Algebra S Sₘ
inst✝ : IsLocalization (Submonoid.map f M) Sₘ
triv : ¬1 = 0
this : Nontrivial Rₘ
b : Rₘ
hb : ↑(algebraMap R Rₘ) ↑{ val := leadingCoeff p, property := hM } * b = 1
⊢ IsIntegralElem (IsLocalization.map Sₘ f (_ : M ≤ Submonoid.comap f (Submonoid.map f M))) (↑(algebraMap S Sₘ) x)
[PROOFSTEP]
refine' ⟨p.map (algebraMap R Rₘ) * C b, ⟨_, _⟩⟩
[GOAL]
case neg.intro.refine'_1
R✝ : Type u_1
inst✝¹⁷ : CommRing R✝
M✝ : Submonoid R✝
S✝ : Type u_2
inst✝¹⁶ : CommRing S✝
inst✝¹⁵ : Algebra R✝ S✝
P : Type u_3
inst✝¹⁴ : CommRing P
Rₘ✝ : Type u_4
Sₘ✝ : Type u_5
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ₘ✝
R : Type u_6
S : Type u_7
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
f : R →+* S
x : S
p : R[X]
hf : eval₂ f x p = 0
M : Submonoid R
hM : leadingCoeff p ∈ M
Rₘ : Type u_8
Sₘ : Type u_9
inst✝⁵ : CommRing Rₘ
inst✝⁴ : CommRing Sₘ
inst✝³ : Algebra R Rₘ
inst✝² : IsLocalization M Rₘ
inst✝¹ : Algebra S Sₘ
inst✝ : IsLocalization (Submonoid.map f M) Sₘ
triv : ¬1 = 0
this : Nontrivial Rₘ
b : Rₘ
hb : ↑(algebraMap R Rₘ) ↑{ val := leadingCoeff p, property := hM } * b = 1
⊢ Monic (Polynomial.map (algebraMap R Rₘ) p * ↑C b)
[PROOFSTEP]
refine' monic_mul_C_of_leadingCoeff_mul_eq_one _
[GOAL]
case neg.intro.refine'_1
R✝ : Type u_1
inst✝¹⁷ : CommRing R✝
M✝ : Submonoid R✝
S✝ : Type u_2
inst✝¹⁶ : CommRing S✝
inst✝¹⁵ : Algebra R✝ S✝
P : Type u_3
inst✝¹⁴ : CommRing P
Rₘ✝ : Type u_4
Sₘ✝ : Type u_5
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ₘ✝
R : Type u_6
S : Type u_7
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
f : R →+* S
x : S
p : R[X]
hf : eval₂ f x p = 0
M : Submonoid R
hM : leadingCoeff p ∈ M
Rₘ : Type u_8
Sₘ : Type u_9
inst✝⁵ : CommRing Rₘ
inst✝⁴ : CommRing Sₘ
inst✝³ : Algebra R Rₘ
inst✝² : IsLocalization M Rₘ
inst✝¹ : Algebra S Sₘ
inst✝ : IsLocalization (Submonoid.map f M) Sₘ
triv : ¬1 = 0
this : Nontrivial Rₘ
b : Rₘ
hb : ↑(algebraMap R Rₘ) ↑{ val := leadingCoeff p, property := hM } * b = 1
⊢ leadingCoeff (Polynomial.map (algebraMap R Rₘ) p) * b = 1
[PROOFSTEP]
rwa [leadingCoeff_map_of_leadingCoeff_ne_zero (algebraMap R Rₘ)]
[GOAL]
case neg.intro.refine'_1
R✝ : Type u_1
inst✝¹⁷ : CommRing R✝
M✝ : Submonoid R✝
S✝ : Type u_2
inst✝¹⁶ : CommRing S✝
inst✝¹⁵ : Algebra R✝ S✝
P : Type u_3
inst✝¹⁴ : CommRing P
Rₘ✝ : Type u_4
Sₘ✝ : Type u_5
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ₘ✝
R : Type u_6
S : Type u_7
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
f : R →+* S
x : S
p : R[X]
hf : eval₂ f x p = 0
M : Submonoid R
hM : leadingCoeff p ∈ M
Rₘ : Type u_8
Sₘ : Type u_9
inst✝⁵ : CommRing Rₘ
inst✝⁴ : CommRing Sₘ
inst✝³ : Algebra R Rₘ
inst✝² : IsLocalization M Rₘ
inst✝¹ : Algebra S Sₘ
inst✝ : IsLocalization (Submonoid.map f M) Sₘ
triv : ¬1 = 0
this : Nontrivial Rₘ
b : Rₘ
hb : ↑(algebraMap R Rₘ) ↑{ val := leadingCoeff p, property := hM } * b = 1
⊢ ↑(algebraMap R Rₘ) (leadingCoeff p) ≠ 0
[PROOFSTEP]
refine' fun hfp => zero_ne_one (_root_.trans (zero_mul b).symm (hfp ▸ hb) : (0 : Rₘ) = 1)
[GOAL]
case neg.intro.refine'_2
R✝ : Type u_1
inst✝¹⁷ : CommRing R✝
M✝ : Submonoid R✝
S✝ : Type u_2
inst✝¹⁶ : CommRing S✝
inst✝¹⁵ : Algebra R✝ S✝
P : Type u_3
inst✝¹⁴ : CommRing P
Rₘ✝ : Type u_4
Sₘ✝ : Type u_5
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ₘ✝
R : Type u_6
S : Type u_7
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
f : R →+* S
x : S
p : R[X]
hf : eval₂ f x p = 0
M : Submonoid R
hM : leadingCoeff p ∈ M
Rₘ : Type u_8
Sₘ : Type u_9
inst✝⁵ : CommRing Rₘ
inst✝⁴ : CommRing Sₘ
inst✝³ : Algebra R Rₘ
inst✝² : IsLocalization M Rₘ
inst✝¹ : Algebra S Sₘ
inst✝ : IsLocalization (Submonoid.map f M) Sₘ
triv : ¬1 = 0
this : Nontrivial Rₘ
b : Rₘ
hb : ↑(algebraMap R Rₘ) ↑{ val := leadingCoeff p, property := hM } * b = 1
⊢ eval₂ (IsLocalization.map Sₘ f (_ : M ≤ Submonoid.comap f (Submonoid.map f M))) (↑(algebraMap S Sₘ) x)
      (Polynomial.map (algebraMap R Rₘ) p * ↑C b) =
    0
[PROOFSTEP]
refine' eval₂_mul_eq_zero_of_left _ _ _ _
[GOAL]
case neg.intro.refine'_2
R✝ : Type u_1
inst✝¹⁷ : CommRing R✝
M✝ : Submonoid R✝
S✝ : Type u_2
inst✝¹⁶ : CommRing S✝
inst✝¹⁵ : Algebra R✝ S✝
P : Type u_3
inst✝¹⁴ : CommRing P
Rₘ✝ : Type u_4
Sₘ✝ : Type u_5
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ₘ✝
R : Type u_6
S : Type u_7
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
f : R →+* S
x : S
p : R[X]
hf : eval₂ f x p = 0
M : Submonoid R
hM : leadingCoeff p ∈ M
Rₘ : Type u_8
Sₘ : Type u_9
inst✝⁵ : CommRing Rₘ
inst✝⁴ : CommRing Sₘ
inst✝³ : Algebra R Rₘ
inst✝² : IsLocalization M Rₘ
inst✝¹ : Algebra S Sₘ
inst✝ : IsLocalization (Submonoid.map f M) Sₘ
triv : ¬1 = 0
this : Nontrivial Rₘ
b : Rₘ
hb : ↑(algebraMap R Rₘ) ↑{ val := leadingCoeff p, property := hM } * b = 1
⊢ eval₂ (IsLocalization.map Sₘ f (_ : M ≤ Submonoid.comap f (Submonoid.map f M))) (↑(algebraMap S Sₘ) x)
      (Polynomial.map (algebraMap R Rₘ) p) =
    0
[PROOFSTEP]
erw [eval₂_map, IsLocalization.map_comp, ← hom_eval₂ _ f (algebraMap S Sₘ) x]
[GOAL]
case neg.intro.refine'_2
R✝ : Type u_1
inst✝¹⁷ : CommRing R✝
M✝ : Submonoid R✝
S✝ : Type u_2
inst✝¹⁶ : CommRing S✝
inst✝¹⁵ : Algebra R✝ S✝
P : Type u_3
inst✝¹⁴ : CommRing P
Rₘ✝ : Type u_4
Sₘ✝ : Type u_5
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ₘ✝
R : Type u_6
S : Type u_7
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
f : R →+* S
x : S
p : R[X]
hf : eval₂ f x p = 0
M : Submonoid R
hM : leadingCoeff p ∈ M
Rₘ : Type u_8
Sₘ : Type u_9
inst✝⁵ : CommRing Rₘ
inst✝⁴ : CommRing Sₘ
inst✝³ : Algebra R Rₘ
inst✝² : IsLocalization M Rₘ
inst✝¹ : Algebra S Sₘ
inst✝ : IsLocalization (Submonoid.map f M) Sₘ
triv : ¬1 = 0
this : Nontrivial Rₘ
b : Rₘ
hb : ↑(algebraMap R Rₘ) ↑{ val := leadingCoeff p, property := hM } * b = 1
⊢ ↑(algebraMap S Sₘ) (eval₂ f x p) = 0
[PROOFSTEP]
exact _root_.trans (congr_arg (algebraMap S Sₘ) hf) (RingHom.map_zero _)
[GOAL]
R : Type u_1
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type u_3
inst✝⁶ : CommRing P
Rₘ : Type u_4
Sₘ : Type u_5
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ₘ
H : Algebra.IsIntegral R S
⊢ RingHom.IsIntegral
    (IsLocalization.map Sₘ (algebraMap R S)
      (_ : M ≤ Submonoid.comap (algebraMap R S) (Algebra.algebraMapSubmonoid S M)))
[PROOFSTEP]
intro x
[GOAL]
R : Type u_1
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type u_3
inst✝⁶ : CommRing P
Rₘ : Type u_4
Sₘ : Type u_5
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ₘ
H : Algebra.IsIntegral R S
x : Sₘ
⊢ RingHom.IsIntegralElem
    (IsLocalization.map Sₘ (algebraMap R S)
      (_ : M ≤ Submonoid.comap (algebraMap R S) (Algebra.algebraMapSubmonoid S M)))
    x
[PROOFSTEP]
obtain ⟨⟨s, ⟨u, hu⟩⟩, hx⟩ := surj (Algebra.algebraMapSubmonoid S M) x
[GOAL]
case intro.mk.mk
R : Type u_1
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type u_3
inst✝⁶ : CommRing P
Rₘ : Type u_4
Sₘ : Type u_5
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ₘ
H : Algebra.IsIntegral R S
x : Sₘ
s u : S
hu : u ∈ Algebra.algebraMapSubmonoid S M
hx :
  x * ↑(algebraMap S Sₘ) ↑(s, { val := u, property := hu }).snd =
    ↑(algebraMap S Sₘ) (s, { val := u, property := hu }).fst
⊢ RingHom.IsIntegralElem
    (IsLocalization.map Sₘ (algebraMap R S)
      (_ : M ≤ Submonoid.comap (algebraMap R S) (Algebra.algebraMapSubmonoid S M)))
    x
[PROOFSTEP]
obtain ⟨v, hv⟩ := hu
[GOAL]
case intro.mk.mk.intro
R : Type u_1
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type u_3
inst✝⁶ : CommRing P
Rₘ : Type u_4
Sₘ : Type u_5
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ₘ
H : Algebra.IsIntegral R S
x : Sₘ
s u : S
v : R
hv : v ∈ ↑M ∧ ↑(algebraMap R S) v = u
hx :
  x * ↑(algebraMap S Sₘ) ↑(s, { val := u, property := (_ : ∃ a, a ∈ ↑M ∧ ↑(algebraMap R S) a = u) }).snd =
    ↑(algebraMap S Sₘ) (s, { val := u, property := (_ : ∃ a, a ∈ ↑M ∧ ↑(algebraMap R S) a = u) }).fst
⊢ RingHom.IsIntegralElem
    (IsLocalization.map Sₘ (algebraMap R S)
      (_ : M ≤ Submonoid.comap (algebraMap R S) (Algebra.algebraMapSubmonoid S M)))
    x
[PROOFSTEP]
obtain ⟨v', hv'⟩ := isUnit_iff_exists_inv'.1 (map_units Rₘ ⟨v, hv.1⟩)
[GOAL]
case intro.mk.mk.intro.intro
R : Type u_1
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type u_3
inst✝⁶ : CommRing P
Rₘ : Type u_4
Sₘ : Type u_5
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ₘ
H : Algebra.IsIntegral R S
x : Sₘ
s u : S
v : R
hv : v ∈ ↑M ∧ ↑(algebraMap R S) v = u
hx :
  x * ↑(algebraMap S Sₘ) ↑(s, { val := u, property := (_ : ∃ a, a ∈ ↑M ∧ ↑(algebraMap R S) a = u) }).snd =
    ↑(algebraMap S Sₘ) (s, { val := u, property := (_ : ∃ a, a ∈ ↑M ∧ ↑(algebraMap R S) a = u) }).fst
v' : Rₘ
hv' : v' * ↑(algebraMap R Rₘ) ↑{ val := v, property := (_ : v ∈ ↑M) } = 1
⊢ RingHom.IsIntegralElem
    (IsLocalization.map Sₘ (algebraMap R S)
      (_ : M ≤ Submonoid.comap (algebraMap R S) (Algebra.algebraMapSubmonoid S M)))
    x
[PROOFSTEP]
refine' @isIntegral_of_isIntegral_mul_unit Rₘ _ _ _ (localizationAlgebra M S) x (algebraMap S Sₘ u) v' _ _
[GOAL]
case intro.mk.mk.intro.intro.refine'_1
R : Type u_1
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type u_3
inst✝⁶ : CommRing P
Rₘ : Type u_4
Sₘ : Type u_5
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ₘ
H : Algebra.IsIntegral R S
x : Sₘ
s u : S
v : R
hv : v ∈ ↑M ∧ ↑(algebraMap R S) v = u
hx :
  x * ↑(algebraMap S Sₘ) ↑(s, { val := u, property := (_ : ∃ a, a ∈ ↑M ∧ ↑(algebraMap R S) a = u) }).snd =
    ↑(algebraMap S Sₘ) (s, { val := u, property := (_ : ∃ a, a ∈ ↑M ∧ ↑(algebraMap R S) a = u) }).fst
v' : Rₘ
hv' : v' * ↑(algebraMap R Rₘ) ↑{ val := v, property := (_ : v ∈ ↑M) } = 1
⊢ ↑(algebraMap Rₘ Sₘ) v' * ↑(algebraMap S Sₘ) u = 1
[PROOFSTEP]
replace hv' := congr_arg (@algebraMap Rₘ Sₘ _ _ (localizationAlgebra M S)) hv'
[GOAL]
case intro.mk.mk.intro.intro.refine'_1
R : Type u_1
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type u_3
inst✝⁶ : CommRing P
Rₘ : Type u_4
Sₘ : Type u_5
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ₘ
H : Algebra.IsIntegral R S
x : Sₘ
s u : S
v : R
hv : v ∈ ↑M ∧ ↑(algebraMap R S) v = u
hx :
  x * ↑(algebraMap S Sₘ) ↑(s, { val := u, property := (_ : ∃ a, a ∈ ↑M ∧ ↑(algebraMap R S) a = u) }).snd =
    ↑(algebraMap S Sₘ) (s, { val := u, property := (_ : ∃ a, a ∈ ↑M ∧ ↑(algebraMap R S) a = u) }).fst
v' : Rₘ
hv' : ↑(algebraMap Rₘ Sₘ) (v' * ↑(algebraMap R Rₘ) ↑{ val := v, property := (_ : v ∈ ↑M) }) = ↑(algebraMap Rₘ Sₘ) 1
⊢ ↑(algebraMap Rₘ Sₘ) v' * ↑(algebraMap S Sₘ) u = 1
[PROOFSTEP]
rw [RingHom.map_mul, RingHom.map_one, ← RingHom.comp_apply _ (algebraMap R Rₘ)] at hv' 
[GOAL]
case intro.mk.mk.intro.intro.refine'_1
R : Type u_1
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type u_3
inst✝⁶ : CommRing P
Rₘ : Type u_4
Sₘ : Type u_5
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ₘ
H : Algebra.IsIntegral R S
x : Sₘ
s u : S
v : R
hv : v ∈ ↑M ∧ ↑(algebraMap R S) v = u
hx :
  x * ↑(algebraMap S Sₘ) ↑(s, { val := u, property := (_ : ∃ a, a ∈ ↑M ∧ ↑(algebraMap R S) a = u) }).snd =
    ↑(algebraMap S Sₘ) (s, { val := u, property := (_ : ∃ a, a ∈ ↑M ∧ ↑(algebraMap R S) a = u) }).fst
v' : Rₘ
hv' :
  ↑(algebraMap Rₘ Sₘ) v' *
      ↑(RingHom.comp (algebraMap Rₘ Sₘ) (algebraMap R Rₘ)) ↑{ val := v, property := (_ : v ∈ ↑M) } =
    1
⊢ ↑(algebraMap Rₘ Sₘ) v' * ↑(algebraMap S Sₘ) u = 1
[PROOFSTEP]
erw [IsLocalization.map_comp (show _ ≤ (Algebra.algebraMapSubmonoid S M).comap _ from M.le_comap_map)] at hv' 
[GOAL]
case intro.mk.mk.intro.intro.refine'_1
R : Type u_1
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type u_3
inst✝⁶ : CommRing P
Rₘ : Type u_4
Sₘ : Type u_5
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ₘ
H : Algebra.IsIntegral R S
x : Sₘ
s u : S
v : R
hv : v ∈ ↑M ∧ ↑(algebraMap R S) v = u
hx :
  x * ↑(algebraMap S Sₘ) ↑(s, { val := u, property := (_ : ∃ a, a ∈ ↑M ∧ ↑(algebraMap R S) a = u) }).snd =
    ↑(algebraMap S Sₘ) (s, { val := u, property := (_ : ∃ a, a ∈ ↑M ∧ ↑(algebraMap R S) a = u) }).fst
v' : Rₘ
hv' :
  ↑(algebraMap Rₘ Sₘ) v' * ↑(RingHom.comp (algebraMap S Sₘ) (algebraMap R S)) ↑{ val := v, property := (_ : v ∈ ↑M) } =
    1
⊢ ↑(algebraMap Rₘ Sₘ) v' * ↑(algebraMap S Sₘ) u = 1
[PROOFSTEP]
exact hv.2 ▸ hv'
[GOAL]
case intro.mk.mk.intro.intro.refine'_2
R : Type u_1
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type u_3
inst✝⁶ : CommRing P
Rₘ : Type u_4
Sₘ : Type u_5
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ₘ
H : Algebra.IsIntegral R S
x : Sₘ
s u : S
v : R
hv : v ∈ ↑M ∧ ↑(algebraMap R S) v = u
hx :
  x * ↑(algebraMap S Sₘ) ↑(s, { val := u, property := (_ : ∃ a, a ∈ ↑M ∧ ↑(algebraMap R S) a = u) }).snd =
    ↑(algebraMap S Sₘ) (s, { val := u, property := (_ : ∃ a, a ∈ ↑M ∧ ↑(algebraMap R S) a = u) }).fst
v' : Rₘ
hv' : v' * ↑(algebraMap R Rₘ) ↑{ val := v, property := (_ : v ∈ ↑M) } = 1
⊢ IsIntegral Rₘ (x * ↑(algebraMap S Sₘ) u)
[PROOFSTEP]
obtain ⟨p, hp⟩ := H s
[GOAL]
case intro.mk.mk.intro.intro.refine'_2.intro
R : Type u_1
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type u_3
inst✝⁶ : CommRing P
Rₘ : Type u_4
Sₘ : Type u_5
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ₘ
H : Algebra.IsIntegral R S
x : Sₘ
s u : S
v : R
hv : v ∈ ↑M ∧ ↑(algebraMap R S) v = u
hx :
  x * ↑(algebraMap S Sₘ) ↑(s, { val := u, property := (_ : ∃ a, a ∈ ↑M ∧ ↑(algebraMap R S) a = u) }).snd =
    ↑(algebraMap S Sₘ) (s, { val := u, property := (_ : ∃ a, a ∈ ↑M ∧ ↑(algebraMap R S) a = u) }).fst
v' : Rₘ
hv' : v' * ↑(algebraMap R Rₘ) ↑{ val := v, property := (_ : v ∈ ↑M) } = 1
p : R[X]
hp : Monic p ∧ eval₂ (algebraMap R S) s p = 0
⊢ IsIntegral Rₘ (x * ↑(algebraMap S Sₘ) u)
[PROOFSTEP]
exact hx.symm ▸ is_integral_localization_at_leadingCoeff p hp.2 (hp.1.symm ▸ M.one_mem)
[GOAL]
R : Type u_1
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type u_3
inst✝⁶ : CommRing P
Rₘ : Type u_4
Sₘ : Type u_5
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ₘ)
[PROOFSTEP]
rw [Polynomial.lifts_iff_coeff_lifts]
[GOAL]
R : Type u_1
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type u_3
inst✝⁶ : CommRing P
Rₘ : Type u_4
Sₘ : Type u_5
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ₘ)
[PROOFSTEP]
intro n
[GOAL]
R : Type u_1
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type u_3
inst✝⁶ : CommRing P
Rₘ : Type u_4
Sₘ : Type u_5
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ₘ)
[PROOFSTEP]
rw [Polynomial.coeff_scaleRoots]
[GOAL]
R : Type u_1
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type u_3
inst✝⁶ : CommRing P
Rₘ : Type u_4
Sₘ : Type u_5
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ₘ)
[PROOFSTEP]
by_cases h₁ : n ∈ p.support
[GOAL]
case pos
R : Type u_1
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type u_3
inst✝⁶ : CommRing P
Rₘ : Type u_4
Sₘ : Type u_5
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_1
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type u_3
inst✝⁶ : CommRing P
Rₘ : Type u_4
Sₘ : Type u_5
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ₘ)
[PROOFSTEP]
by_cases h₂ : n = p.natDegree
[GOAL]
case pos
R : Type u_1
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type u_3
inst✝⁶ : CommRing P
Rₘ : Type u_4
Sₘ : Type u_5
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ₘ)
[PROOFSTEP]
rwa [h₂, Polynomial.coeff_natDegree, tsub_self, pow_zero, _root_.mul_one]
[GOAL]
case neg
R : Type u_1
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type u_3
inst✝⁶ : CommRing P
Rₘ : Type u_4
Sₘ : Type u_5
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ₘ)
[PROOFSTEP]
have : n + 1 ≤ p.natDegree := lt_of_le_of_ne (Polynomial.le_natDegree_of_mem_supp _ h₁) h₂
[GOAL]
case neg
R : Type u_1
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type u_3
inst✝⁶ : CommRing P
Rₘ : Type u_4
Sₘ : Type u_5
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ₘ)
[PROOFSTEP]
rw [← tsub_add_cancel_of_le (le_tsub_of_add_le_left this), pow_add, pow_one, mul_comm, _root_.mul_assoc, ← map_pow]
[GOAL]
case neg
R : Type u_1
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type u_3
inst✝⁶ : CommRing P
Rₘ : Type u_4
Sₘ : Type u_5
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ₘ)
[PROOFSTEP]
change _ ∈ (algebraMap R Rₘ).range
[GOAL]
case neg
R : Type u_1
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type u_3
inst✝⁶ : CommRing P
Rₘ : Type u_4
Sₘ : Type u_5
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ₘ)
[PROOFSTEP]
apply mul_mem
[GOAL]
case neg.a
R : Type u_1
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type u_3
inst✝⁶ : CommRing P
Rₘ : Type u_4
Sₘ : Type u_5
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ₘ)
[PROOFSTEP]
exact RingHom.mem_range_self _ _
[GOAL]
case neg.a
R : Type u_1
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type u_3
inst✝⁶ : CommRing P
Rₘ : Type u_4
Sₘ : Type u_5
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ₘ)
[PROOFSTEP]
rw [← Algebra.smul_def]
[GOAL]
case neg.a
R : Type u_1
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type u_3
inst✝⁶ : CommRing P
Rₘ : Type u_4
Sₘ : Type u_5
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ₘ)
[PROOFSTEP]
exact ⟨_, IsLocalization.map_integerMultiple M p.support p.coeff ⟨n, h₁⟩⟩
[GOAL]
case neg
R : Type u_1
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type u_3
inst✝⁶ : CommRing P
Rₘ : Type u_4
Sₘ : Type u_5
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ₘ)
[PROOFSTEP]
rw [Polynomial.not_mem_support_iff] at h₁ 
[GOAL]
case neg
R : Type u_1
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type u_3
inst✝⁶ : CommRing P
Rₘ : Type u_4
Sₘ : Type u_5
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ₘ)
[PROOFSTEP]
rw [h₁, zero_mul]
[GOAL]
case neg
R : Type u_1
inst✝⁹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type u_3
inst✝⁶ : CommRing P
Rₘ : Type u_4
Sₘ : Type u_5
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ₘ)
[PROOFSTEP]
exact zero_mem (algebraMap R Rₘ).range
[GOAL]
R : Type u_1
inst✝¹¹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
P : Type u_3
inst✝⁸ : CommRing P
Rₘ : Type u_4
Sₘ : Type u_5
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)
[PROOFSTEP]
cases' subsingleton_or_nontrivial Rₘ with _ nontriv
[GOAL]
case inl
R : Type u_1
inst✝¹¹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
P : Type u_3
inst✝⁸ : CommRing P
Rₘ : Type u_4
Sₘ : Type u_5
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)
[PROOFSTEP]
skip
[GOAL]
case inr
R : Type u_1
inst✝¹¹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
P : Type u_3
inst✝⁸ : CommRing P
Rₘ : Type u_4
Sₘ : Type u_5
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)
[PROOFSTEP]
skip
[GOAL]
case inl
R : Type u_1
inst✝¹¹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
P : Type u_3
inst✝⁸ : CommRing P
Rₘ : Type u_4
Sₘ : Type u_5
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)
[PROOFSTEP]
haveI := (_root_.algebraMap Rₘ S).codomain_trivial
[GOAL]
case inl
R : Type u_1
inst✝¹¹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
P : Type u_3
inst✝⁸ : CommRing P
Rₘ : Type u_4
Sₘ : Type u_5
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)
[PROOFSTEP]
exact ⟨1, Polynomial.X, Polynomial.monic_X, Subsingleton.elim _ _⟩
[GOAL]
case inr
R : Type u_1
inst✝¹¹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
P : Type u_3
inst✝⁸ : CommRing P
Rₘ : Type u_4
Sₘ : Type u_5
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)
[PROOFSTEP]
obtain ⟨p, hp₁, hp₂⟩ := hx
[GOAL]
case inr.intro.intro
R : Type u_1
inst✝¹¹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
P : Type u_3
inst✝⁸ : CommRing P
Rₘ : Type u_4
Sₘ : Type u_5
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)
[PROOFSTEP]
have := lifts_and_natDegree_eq_and_monic (IsLocalization.scaleRoots_commonDenom_mem_lifts M p ?_) ?_
[GOAL]
case inr.intro.intro.refine_3
R : Type u_1
inst✝¹¹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
P : Type u_3
inst✝⁸ : CommRing P
Rₘ : Type u_4
Sₘ : Type u_5
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_1
inst✝¹¹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
P : Type u_3
inst✝⁸ : CommRing P
Rₘ : Type u_4
Sₘ : Type u_5
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_1
inst✝¹¹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
P : Type u_3
inst✝⁸ : CommRing P
Rₘ : Type u_4
Sₘ : Type u_5
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))))
[PROOFSTEP]
obtain ⟨p', hp'₁, -, hp'₂⟩ := this
[GOAL]
case inr.intro.intro.refine_3.intro.intro.intro
R : Type u_1
inst✝¹¹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
P : Type u_3
inst✝⁸ : CommRing P
Rₘ : Type u_4
Sₘ : Type u_5
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)
[PROOFSTEP]
refine' ⟨IsLocalization.commonDenom M p.support p.coeff, p', hp'₂, _⟩
[GOAL]
case inr.intro.intro.refine_3.intro.intro.intro
R : Type u_1
inst✝¹¹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
P : Type u_3
inst✝⁸ : CommRing P
Rₘ : Type u_4
Sₘ : Type u_5
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
[PROOFSTEP]
rw [IsScalarTower.algebraMap_eq R Rₘ S, ← Polynomial.eval₂_map, hp'₁, Submonoid.smul_def, Algebra.smul_def,
  IsScalarTower.algebraMap_apply R Rₘ S]
[GOAL]
case inr.intro.intro.refine_3.intro.intro.intro
R : Type u_1
inst✝¹¹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
P : Type u_3
inst✝⁸ : CommRing P
Rₘ : Type u_4
Sₘ : Type u_5
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
[PROOFSTEP]
exact Polynomial.scaleRoots_eval₂_eq_zero _ hp₂
[GOAL]
case inr.intro.intro.refine_1
R : Type u_1
inst✝¹¹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
P : Type u_3
inst✝⁸ : CommRing P
Rₘ : Type u_4
Sₘ : Type u_5
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ₘ)
[PROOFSTEP]
rw [hp₁.leadingCoeff]
[GOAL]
case inr.intro.intro.refine_1
R : Type u_1
inst✝¹¹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
P : Type u_3
inst✝⁸ : CommRing P
Rₘ : Type u_4
Sₘ : Type u_5
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ₘ)
[PROOFSTEP]
exact one_mem _
[GOAL]
case inr.intro.intro.refine_2
R : Type u_1
inst✝¹¹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
P : Type u_3
inst✝⁸ : CommRing P
Rₘ : Type u_4
Sₘ : Type u_5
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))))
[PROOFSTEP]
rwa [Polynomial.monic_scaleRoots_iff]
[GOAL]
R : Type u_1
inst✝¹⁶ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁵ : CommRing S
inst✝¹⁴ : Algebra R S
P : Type u_3
inst✝¹³ : CommRing P
A : Type u_4
K : Type u_5
inst✝¹² : CommRing A
inst✝¹¹ : IsDomain A
L : Type u_6
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra A K
inst✝⁷ : Algebra A L
inst✝⁶ : IsFractionRing A K
C : Type u_7
inst✝⁵ : CommRing C
inst✝⁴ : IsDomain C
inst✝³ : Algebra C L
inst✝² : IsIntegralClosure C A L
inst✝¹ : Algebra A C
inst✝ : IsScalarTower A C L
alg : Algebra.IsAlgebraic A L
inj : ∀ (x : A), ↑(algebraMap A L) x = 0 → x = 0
z : L
x : { x // x ∈ integralClosure A L }
y : A
hy : y ≠ 0
hxy : z * ↑(algebraMap A L) y = ↑x
h : ↑(algebraMap A C) y = 0
⊢ ↑(algebraMap A L) y = 0
[PROOFSTEP]
rw [IsScalarTower.algebraMap_apply A C L, h, RingHom.map_zero]
[GOAL]
R : Type u_1
inst✝¹⁶ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁵ : CommRing S
inst✝¹⁴ : Algebra R S
P : Type u_3
inst✝¹³ : CommRing P
A : Type u_4
K : Type u_5
inst✝¹² : CommRing A
inst✝¹¹ : IsDomain A
L : Type u_6
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra A K
inst✝⁷ : Algebra A L
inst✝⁶ : IsFractionRing A K
C : Type u_7
inst✝⁵ : CommRing C
inst✝⁴ : IsDomain C
inst✝³ : Algebra C L
inst✝² : IsIntegralClosure C A L
inst✝¹ : Algebra A C
inst✝ : IsScalarTower A C L
alg : Algebra.IsAlgebraic A L
inj : ∀ (x : A), ↑(algebraMap A L) x = 0 → x = 0
z : L
x : { x // x ∈ integralClosure A L }
y : A
hy : y ≠ 0
hxy : z * ↑(algebraMap A L) y = ↑x
⊢ z *
      ↑(algebraMap C L)
        ↑(mk' C ↑x (_ : ↑x ∈ integralClosure A L),
              { val := ↑(algebraMap A C) y, property := (_ : ↑(algebraMap A C) y ∈ nonZeroDivisors C) }).snd =
    ↑(algebraMap C L)
      (mk' C ↑x (_ : ↑x ∈ integralClosure A L),
          { val := ↑(algebraMap A C) y, property := (_ : ↑(algebraMap A C) y ∈ nonZeroDivisors C) }).fst
[PROOFSTEP]
simp only
[GOAL]
R : Type u_1
inst✝¹⁶ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁵ : CommRing S
inst✝¹⁴ : Algebra R S
P : Type u_3
inst✝¹³ : CommRing P
A : Type u_4
K : Type u_5
inst✝¹² : CommRing A
inst✝¹¹ : IsDomain A
L : Type u_6
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra A K
inst✝⁷ : Algebra A L
inst✝⁶ : IsFractionRing A K
C : Type u_7
inst✝⁵ : CommRing C
inst✝⁴ : IsDomain C
inst✝³ : Algebra C L
inst✝² : IsIntegralClosure C A L
inst✝¹ : Algebra A C
inst✝ : IsScalarTower A C L
alg : Algebra.IsAlgebraic A L
inj : ∀ (x : A), ↑(algebraMap A L) x = 0 → x = 0
z : L
x : { x // x ∈ integralClosure A L }
y : A
hy : y ≠ 0
hxy : z * ↑(algebraMap A L) y = ↑x
⊢ z * ↑(algebraMap C L) (↑(algebraMap A C) y) = ↑(algebraMap C L) (mk' C ↑x (_ : ↑x ∈ integralClosure A L))
[PROOFSTEP]
rw [algebraMap_mk', ← IsScalarTower.algebraMap_apply A C L, hxy]
[GOAL]
R : Type u_1
inst✝¹⁶ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁵ : CommRing S
inst✝¹⁴ : Algebra R S
P : Type u_3
inst✝¹³ : CommRing P
A : Type u_4
K : Type u_5
inst✝¹² : CommRing A
inst✝¹¹ : IsDomain A
L : Type u_6
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra A K
inst✝⁷ : Algebra A L
inst✝⁶ : IsFractionRing A K
C : Type u_7
inst✝⁵ : CommRing C
inst✝⁴ : IsDomain C
inst✝³ : Algebra C L
inst✝² : IsIntegralClosure C A L
inst✝¹ : Algebra A C
inst✝ : IsScalarTower A C L
alg : Algebra.IsAlgebraic A L
inj : ∀ (x : A), ↑(algebraMap A L) x = 0 → x = 0
x y : C
h : ↑(algebraMap C L) x = ↑(algebraMap C L) y
⊢ ↑1 * x = ↑1 * y
[PROOFSTEP]
simpa using algebraMap_injective C A L h
[GOAL]
R : Type u_1
inst✝¹³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
P : Type u_3
inst✝¹⁰ : CommRing P
A : Type u_4
K : Type u_5
inst✝⁹ : CommRing A
inst✝⁸ : IsDomain A
inst✝⁷ : Field K
inst✝⁶ : IsDomain R
inst✝⁵ : IsDomain S
inst✝⁴ : Algebra R K
inst✝³ : Algebra S K
inst✝² : NoZeroSMulDivisors R K
inst✝¹ : IsFractionRing S K
inst✝ : IsScalarTower R S K
⊢ Algebra.IsAlgebraic R S ↔ Algebra.IsAlgebraic R K
[PROOFSTEP]
simp only [Algebra.IsAlgebraic]
[GOAL]
R : Type u_1
inst✝¹³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
P : Type u_3
inst✝¹⁰ : CommRing P
A : Type u_4
K : Type u_5
inst✝⁹ : CommRing A
inst✝⁸ : IsDomain A
inst✝⁷ : Field K
inst✝⁶ : IsDomain R
inst✝⁵ : IsDomain S
inst✝⁴ : Algebra R K
inst✝³ : Algebra S K
inst✝² : NoZeroSMulDivisors R K
inst✝¹ : IsFractionRing S K
inst✝ : IsScalarTower R S K
⊢ (∀ (x : S), IsAlgebraic R x) ↔ ∀ (x : K), IsAlgebraic R x
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u_1
inst✝¹³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
P : Type u_3
inst✝¹⁰ : CommRing P
A : Type u_4
K : Type u_5
inst✝⁹ : CommRing A
inst✝⁸ : IsDomain A
inst✝⁷ : Field K
inst✝⁶ : IsDomain R
inst✝⁵ : IsDomain S
inst✝⁴ : Algebra R K
inst✝³ : Algebra S K
inst✝² : NoZeroSMulDivisors R K
inst✝¹ : IsFractionRing S K
inst✝ : IsScalarTower R S K
⊢ (∀ (x : S), IsAlgebraic R x) → ∀ (x : K), IsAlgebraic R x
[PROOFSTEP]
intro h x
[GOAL]
case mp
R : Type u_1
inst✝¹³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
P : Type u_3
inst✝¹⁰ : CommRing P
A : Type u_4
K : Type u_5
inst✝⁹ : CommRing A
inst✝⁸ : IsDomain A
inst✝⁷ : Field K
inst✝⁶ : IsDomain R
inst✝⁵ : IsDomain S
inst✝⁴ : Algebra R K
inst✝³ : Algebra S K
inst✝² : NoZeroSMulDivisors R K
inst✝¹ : IsFractionRing S K
inst✝ : IsScalarTower R S K
h : ∀ (x : S), IsAlgebraic R x
x : K
⊢ IsAlgebraic R x
[PROOFSTEP]
rw [IsFractionRing.isAlgebraic_iff R (FractionRing R) K, isAlgebraic_iff_isIntegral]
[GOAL]
case mp
R : Type u_1
inst✝¹³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
P : Type u_3
inst✝¹⁰ : CommRing P
A : Type u_4
K : Type u_5
inst✝⁹ : CommRing A
inst✝⁸ : IsDomain A
inst✝⁷ : Field K
inst✝⁶ : IsDomain R
inst✝⁵ : IsDomain S
inst✝⁴ : Algebra R K
inst✝³ : Algebra S K
inst✝² : NoZeroSMulDivisors R K
inst✝¹ : IsFractionRing S K
inst✝ : IsScalarTower R S K
h : ∀ (x : S), IsAlgebraic R x
x : K
⊢ IsIntegral (FractionRing R) x
[PROOFSTEP]
obtain ⟨a : S, b, ha, rfl⟩ := @div_surjective S _ _ _ _ _ _ x
[GOAL]
case mp.intro.intro.intro
R : Type u_1
inst✝¹³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
P : Type u_3
inst✝¹⁰ : CommRing P
A : Type u_4
K : Type u_5
inst✝⁹ : CommRing A
inst✝⁸ : IsDomain A
inst✝⁷ : Field K
inst✝⁶ : IsDomain R
inst✝⁵ : IsDomain S
inst✝⁴ : Algebra R K
inst✝³ : Algebra S K
inst✝² : NoZeroSMulDivisors R K
inst✝¹ : IsFractionRing S K
inst✝ : IsScalarTower R S K
h : ∀ (x : S), IsAlgebraic R x
a b : S
ha : b ∈ nonZeroDivisors S
⊢ IsIntegral (FractionRing R) (↑(algebraMap S K) a / ↑(algebraMap S K) b)
[PROOFSTEP]
obtain ⟨f, hf₁, hf₂⟩ := h b
[GOAL]
case mp.intro.intro.intro.intro.intro
R : Type u_1
inst✝¹³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
P : Type u_3
inst✝¹⁰ : CommRing P
A : Type u_4
K : Type u_5
inst✝⁹ : CommRing A
inst✝⁸ : IsDomain A
inst✝⁷ : Field K
inst✝⁶ : IsDomain R
inst✝⁵ : IsDomain S
inst✝⁴ : Algebra R K
inst✝³ : Algebra S K
inst✝² : NoZeroSMulDivisors R K
inst✝¹ : IsFractionRing S K
inst✝ : IsScalarTower R S K
h : ∀ (x : S), IsAlgebraic R x
a b : S
ha : b ∈ nonZeroDivisors S
f : R[X]
hf₁ : f ≠ 0
hf₂ : ↑(aeval b) f = 0
⊢ IsIntegral (FractionRing R) (↑(algebraMap S K) a / ↑(algebraMap S K) b)
[PROOFSTEP]
rw [div_eq_mul_inv]
[GOAL]
case mp.intro.intro.intro.intro.intro
R : Type u_1
inst✝¹³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
P : Type u_3
inst✝¹⁰ : CommRing P
A : Type u_4
K : Type u_5
inst✝⁹ : CommRing A
inst✝⁸ : IsDomain A
inst✝⁷ : Field K
inst✝⁶ : IsDomain R
inst✝⁵ : IsDomain S
inst✝⁴ : Algebra R K
inst✝³ : Algebra S K
inst✝² : NoZeroSMulDivisors R K
inst✝¹ : IsFractionRing S K
inst✝ : IsScalarTower R S K
h : ∀ (x : S), IsAlgebraic R x
a b : S
ha : b ∈ nonZeroDivisors S
f : R[X]
hf₁ : f ≠ 0
hf₂ : ↑(aeval b) f = 0
⊢ IsIntegral (FractionRing R) (↑(algebraMap S K) a * (↑(algebraMap S K) b)⁻¹)
[PROOFSTEP]
refine' isIntegral_mul _ _
[GOAL]
case mp.intro.intro.intro.intro.intro.refine'_1
R : Type u_1
inst✝¹³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
P : Type u_3
inst✝¹⁰ : CommRing P
A : Type u_4
K : Type u_5
inst✝⁹ : CommRing A
inst✝⁸ : IsDomain A
inst✝⁷ : Field K
inst✝⁶ : IsDomain R
inst✝⁵ : IsDomain S
inst✝⁴ : Algebra R K
inst✝³ : Algebra S K
inst✝² : NoZeroSMulDivisors R K
inst✝¹ : IsFractionRing S K
inst✝ : IsScalarTower R S K
h : ∀ (x : S), IsAlgebraic R x
a b : S
ha : b ∈ nonZeroDivisors S
f : R[X]
hf₁ : f ≠ 0
hf₂ : ↑(aeval b) f = 0
⊢ IsIntegral (FractionRing R) (↑(algebraMap S K) a)
[PROOFSTEP]
rw [← isAlgebraic_iff_isIntegral]
[GOAL]
case mp.intro.intro.intro.intro.intro.refine'_1
R : Type u_1
inst✝¹³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
P : Type u_3
inst✝¹⁰ : CommRing P
A : Type u_4
K : Type u_5
inst✝⁹ : CommRing A
inst✝⁸ : IsDomain A
inst✝⁷ : Field K
inst✝⁶ : IsDomain R
inst✝⁵ : IsDomain S
inst✝⁴ : Algebra R K
inst✝³ : Algebra S K
inst✝² : NoZeroSMulDivisors R K
inst✝¹ : IsFractionRing S K
inst✝ : IsScalarTower R S K
h : ∀ (x : S), IsAlgebraic R x
a b : S
ha : b ∈ nonZeroDivisors S
f : R[X]
hf₁ : f ≠ 0
hf₂ : ↑(aeval b) f = 0
⊢ IsAlgebraic (FractionRing R) (↑(algebraMap S K) a)
[PROOFSTEP]
refine' _root_.isAlgebraic_of_larger_base_of_injective (NoZeroSMulDivisors.algebraMap_injective R (FractionRing R)) _
[GOAL]
case mp.intro.intro.intro.intro.intro.refine'_1
R : Type u_1
inst✝¹³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
P : Type u_3
inst✝¹⁰ : CommRing P
A : Type u_4
K : Type u_5
inst✝⁹ : CommRing A
inst✝⁸ : IsDomain A
inst✝⁷ : Field K
inst✝⁶ : IsDomain R
inst✝⁵ : IsDomain S
inst✝⁴ : Algebra R K
inst✝³ : Algebra S K
inst✝² : NoZeroSMulDivisors R K
inst✝¹ : IsFractionRing S K
inst✝ : IsScalarTower R S K
h : ∀ (x : S), IsAlgebraic R x
a b : S
ha : b ∈ nonZeroDivisors S
f : R[X]
hf₁ : f ≠ 0
hf₂ : ↑(aeval b) f = 0
⊢ IsAlgebraic R (↑(algebraMap S K) a)
[PROOFSTEP]
exact isAlgebraic_algebraMap_of_isAlgebraic (h a)
[GOAL]
case mp.intro.intro.intro.intro.intro.refine'_2
R : Type u_1
inst✝¹³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
P : Type u_3
inst✝¹⁰ : CommRing P
A : Type u_4
K : Type u_5
inst✝⁹ : CommRing A
inst✝⁸ : IsDomain A
inst✝⁷ : Field K
inst✝⁶ : IsDomain R
inst✝⁵ : IsDomain S
inst✝⁴ : Algebra R K
inst✝³ : Algebra S K
inst✝² : NoZeroSMulDivisors R K
inst✝¹ : IsFractionRing S K
inst✝ : IsScalarTower R S K
h : ∀ (x : S), IsAlgebraic R x
a b : S
ha : b ∈ nonZeroDivisors S
f : R[X]
hf₁ : f ≠ 0
hf₂ : ↑(aeval b) f = 0
⊢ IsIntegral (FractionRing R) (↑(algebraMap S K) b)⁻¹
[PROOFSTEP]
rw [← isAlgebraic_iff_isIntegral]
[GOAL]
case mp.intro.intro.intro.intro.intro.refine'_2
R : Type u_1
inst✝¹³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
P : Type u_3
inst✝¹⁰ : CommRing P
A : Type u_4
K : Type u_5
inst✝⁹ : CommRing A
inst✝⁸ : IsDomain A
inst✝⁷ : Field K
inst✝⁶ : IsDomain R
inst✝⁵ : IsDomain S
inst✝⁴ : Algebra R K
inst✝³ : Algebra S K
inst✝² : NoZeroSMulDivisors R K
inst✝¹ : IsFractionRing S K
inst✝ : IsScalarTower R S K
h : ∀ (x : S), IsAlgebraic R x
a b : S
ha : b ∈ nonZeroDivisors S
f : R[X]
hf₁ : f ≠ 0
hf₂ : ↑(aeval b) f = 0
⊢ IsAlgebraic (FractionRing R) (↑(algebraMap S K) b)⁻¹
[PROOFSTEP]
use(f.map (algebraMap R (FractionRing R))).reverse
[GOAL]
case h
R : Type u_1
inst✝¹³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
P : Type u_3
inst✝¹⁰ : CommRing P
A : Type u_4
K : Type u_5
inst✝⁹ : CommRing A
inst✝⁸ : IsDomain A
inst✝⁷ : Field K
inst✝⁶ : IsDomain R
inst✝⁵ : IsDomain S
inst✝⁴ : Algebra R K
inst✝³ : Algebra S K
inst✝² : NoZeroSMulDivisors R K
inst✝¹ : IsFractionRing S K
inst✝ : IsScalarTower R S K
h : ∀ (x : S), IsAlgebraic R x
a b : S
ha : b ∈ nonZeroDivisors S
f : R[X]
hf₁ : f ≠ 0
hf₂ : ↑(aeval b) f = 0
⊢ reverse (Polynomial.map (algebraMap R (FractionRing R)) f) ≠ 0 ∧
    ↑(aeval (↑(algebraMap S K) b)⁻¹) (reverse (Polynomial.map (algebraMap R (FractionRing R)) f)) = 0
[PROOFSTEP]
constructor
[GOAL]
case h.left
R : Type u_1
inst✝¹³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
P : Type u_3
inst✝¹⁰ : CommRing P
A : Type u_4
K : Type u_5
inst✝⁹ : CommRing A
inst✝⁸ : IsDomain A
inst✝⁷ : Field K
inst✝⁶ : IsDomain R
inst✝⁵ : IsDomain S
inst✝⁴ : Algebra R K
inst✝³ : Algebra S K
inst✝² : NoZeroSMulDivisors R K
inst✝¹ : IsFractionRing S K
inst✝ : IsScalarTower R S K
h : ∀ (x : S), IsAlgebraic R x
a b : S
ha : b ∈ nonZeroDivisors S
f : R[X]
hf₁ : f ≠ 0
hf₂ : ↑(aeval b) f = 0
⊢ reverse (Polynomial.map (algebraMap R (FractionRing R)) f) ≠ 0
[PROOFSTEP]
rwa [Ne.def, Polynomial.reverse_eq_zero, ← Polynomial.degree_eq_bot,
  Polynomial.degree_map_eq_of_injective (NoZeroSMulDivisors.algebraMap_injective R (FractionRing R)),
  Polynomial.degree_eq_bot]
[GOAL]
case h.right
R : Type u_1
inst✝¹³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
P : Type u_3
inst✝¹⁰ : CommRing P
A : Type u_4
K : Type u_5
inst✝⁹ : CommRing A
inst✝⁸ : IsDomain A
inst✝⁷ : Field K
inst✝⁶ : IsDomain R
inst✝⁵ : IsDomain S
inst✝⁴ : Algebra R K
inst✝³ : Algebra S K
inst✝² : NoZeroSMulDivisors R K
inst✝¹ : IsFractionRing S K
inst✝ : IsScalarTower R S K
h : ∀ (x : S), IsAlgebraic R x
a b : S
ha : b ∈ nonZeroDivisors S
f : R[X]
hf₁ : f ≠ 0
hf₂ : ↑(aeval b) f = 0
⊢ ↑(aeval (↑(algebraMap S K) b)⁻¹) (reverse (Polynomial.map (algebraMap R (FractionRing R)) f)) = 0
[PROOFSTEP]
have : Invertible (algebraMap S K b) :=
  IsUnit.invertible
    (isUnit_of_mem_nonZeroDivisors
      (mem_nonZeroDivisors_iff_ne_zero.2 fun h =>
        nonZeroDivisors.ne_zero ha
          ((injective_iff_map_eq_zero (algebraMap S K)).1 (NoZeroSMulDivisors.algebraMap_injective _ _) b h)))
[GOAL]
case h.right
R : Type u_1
inst✝¹³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
P : Type u_3
inst✝¹⁰ : CommRing P
A : Type u_4
K : Type u_5
inst✝⁹ : CommRing A
inst✝⁸ : IsDomain A
inst✝⁷ : Field K
inst✝⁶ : IsDomain R
inst✝⁵ : IsDomain S
inst✝⁴ : Algebra R K
inst✝³ : Algebra S K
inst✝² : NoZeroSMulDivisors R K
inst✝¹ : IsFractionRing S K
inst✝ : IsScalarTower R S K
h : ∀ (x : S), IsAlgebraic R x
a b : S
ha : b ∈ nonZeroDivisors S
f : R[X]
hf₁ : f ≠ 0
hf₂ : ↑(aeval b) f = 0
this : Invertible (↑(algebraMap S K) b)
⊢ ↑(aeval (↑(algebraMap S K) b)⁻¹) (reverse (Polynomial.map (algebraMap R (FractionRing R)) f)) = 0
[PROOFSTEP]
rw [Polynomial.aeval_def, ← invOf_eq_inv, Polynomial.eval₂_reverse_eq_zero_iff, Polynomial.eval₂_map, ←
  IsScalarTower.algebraMap_eq, ← Polynomial.aeval_def, Polynomial.aeval_algebraMap_apply, hf₂, RingHom.map_zero]
[GOAL]
case mpr
R : Type u_1
inst✝¹³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
P : Type u_3
inst✝¹⁰ : CommRing P
A : Type u_4
K : Type u_5
inst✝⁹ : CommRing A
inst✝⁸ : IsDomain A
inst✝⁷ : Field K
inst✝⁶ : IsDomain R
inst✝⁵ : IsDomain S
inst✝⁴ : Algebra R K
inst✝³ : Algebra S K
inst✝² : NoZeroSMulDivisors R K
inst✝¹ : IsFractionRing S K
inst✝ : IsScalarTower R S K
⊢ (∀ (x : K), IsAlgebraic R x) → ∀ (x : S), IsAlgebraic R x
[PROOFSTEP]
intro h x
[GOAL]
case mpr
R : Type u_1
inst✝¹³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
P : Type u_3
inst✝¹⁰ : CommRing P
A : Type u_4
K : Type u_5
inst✝⁹ : CommRing A
inst✝⁸ : IsDomain A
inst✝⁷ : Field K
inst✝⁶ : IsDomain R
inst✝⁵ : IsDomain S
inst✝⁴ : Algebra R K
inst✝³ : Algebra S K
inst✝² : NoZeroSMulDivisors R K
inst✝¹ : IsFractionRing S K
inst✝ : IsScalarTower R S K
h : ∀ (x : K), IsAlgebraic R x
x : S
⊢ IsAlgebraic R x
[PROOFSTEP]
obtain ⟨f, hf₁, hf₂⟩ := h (algebraMap S K x)
[GOAL]
case mpr.intro.intro
R : Type u_1
inst✝¹³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
P : Type u_3
inst✝¹⁰ : CommRing P
A : Type u_4
K : Type u_5
inst✝⁹ : CommRing A
inst✝⁸ : IsDomain A
inst✝⁷ : Field K
inst✝⁶ : IsDomain R
inst✝⁵ : IsDomain S
inst✝⁴ : Algebra R K
inst✝³ : Algebra S K
inst✝² : NoZeroSMulDivisors R K
inst✝¹ : IsFractionRing S K
inst✝ : IsScalarTower R S K
h : ∀ (x : K), IsAlgebraic R x
x : S
f : R[X]
hf₁ : f ≠ 0
hf₂ : ↑(aeval (↑(algebraMap S K) x)) f = 0
⊢ IsAlgebraic R x
[PROOFSTEP]
use f, hf₁
[GOAL]
case right
R : Type u_1
inst✝¹³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
P : Type u_3
inst✝¹⁰ : CommRing P
A : Type u_4
K : Type u_5
inst✝⁹ : CommRing A
inst✝⁸ : IsDomain A
inst✝⁷ : Field K
inst✝⁶ : IsDomain R
inst✝⁵ : IsDomain S
inst✝⁴ : Algebra R K
inst✝³ : Algebra S K
inst✝² : NoZeroSMulDivisors R K
inst✝¹ : IsFractionRing S K
inst✝ : IsScalarTower R S K
h : ∀ (x : K), IsAlgebraic R x
x : S
f : R[X]
hf₁ : f ≠ 0
hf₂ : ↑(aeval (↑(algebraMap S K) x)) f = 0
⊢ ↑(aeval x) f = 0
[PROOFSTEP]
rw [Polynomial.aeval_algebraMap_apply] at hf₂ 
[GOAL]
case right
R : Type u_1
inst✝¹³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
P : Type u_3
inst✝¹⁰ : CommRing P
A : Type u_4
K : Type u_5
inst✝⁹ : CommRing A
inst✝⁸ : IsDomain A
inst✝⁷ : Field K
inst✝⁶ : IsDomain R
inst✝⁵ : IsDomain S
inst✝⁴ : Algebra R K
inst✝³ : Algebra S K
inst✝² : NoZeroSMulDivisors R K
inst✝¹ : IsFractionRing S K
inst✝ : IsScalarTower R S K
h : ∀ (x : K), IsAlgebraic R x
x : S
f : R[X]
hf₁ : f ≠ 0
hf₂ : ↑(algebraMap S K) (↑(aeval x) f) = 0
⊢ ↑(aeval x) f = 0
[PROOFSTEP]
exact (injective_iff_map_eq_zero (algebraMap S K)).1 (NoZeroSMulDivisors.algebraMap_injective _ _) _ hf₂
[GOAL]
R : Type u_1
inst✝¹⁷ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁶ : CommRing S
inst✝¹⁵ : Algebra R S
P : Type u_3
inst✝¹⁴ : CommRing P
A : Type u_4
K : Type u_5
inst✝¹³ : CommRing A
inst✝¹² : IsDomain A
L : Type u_6
inst✝¹¹ : IsDomain R
inst✝¹⁰ : IsDomain S
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra R K
inst✝⁶ : Algebra R L
inst✝⁵ : Algebra S L
inst✝⁴ : IsIntegralClosure S R L
inst✝³ : IsFractionRing S L
inst✝² : Algebra K L
inst✝¹ : IsScalarTower R S L
inst✝ : IsScalarTower R K L
a : S
b : Set S
alg : Algebra.IsAlgebraic R L
inj : Function.Injective ↑(algebraMap R L)
h : ↑(Ideal.span {a}) ⊆ ↑(Submodule.span R b)
⊢ ↑(Ideal.span {↑(algebraMap S L) a}) ⊆ ↑(Submodule.span K (↑(algebraMap S L) '' b))
[PROOFSTEP]
intro x hx
[GOAL]
R : Type u_1
inst✝¹⁷ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁶ : CommRing S
inst✝¹⁵ : Algebra R S
P : Type u_3
inst✝¹⁴ : CommRing P
A : Type u_4
K : Type u_5
inst✝¹³ : CommRing A
inst✝¹² : IsDomain A
L : Type u_6
inst✝¹¹ : IsDomain R
inst✝¹⁰ : IsDomain S
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra R K
inst✝⁶ : Algebra R L
inst✝⁵ : Algebra S L
inst✝⁴ : IsIntegralClosure S R L
inst✝³ : IsFractionRing S L
inst✝² : Algebra K L
inst✝¹ : IsScalarTower R S L
inst✝ : IsScalarTower R K L
a : S
b : Set S
alg : Algebra.IsAlgebraic R L
inj : Function.Injective ↑(algebraMap R L)
h : ↑(Ideal.span {a}) ⊆ ↑(Submodule.span R b)
x : L
hx : x ∈ ↑(Ideal.span {↑(algebraMap S L) a})
⊢ x ∈ ↑(Submodule.span K (↑(algebraMap S L) '' b))
[PROOFSTEP]
obtain ⟨x', rfl⟩ := Ideal.mem_span_singleton.mp hx
[GOAL]
case intro
R : Type u_1
inst✝¹⁷ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁶ : CommRing S
inst✝¹⁵ : Algebra R S
P : Type u_3
inst✝¹⁴ : CommRing P
A : Type u_4
K : Type u_5
inst✝¹³ : CommRing A
inst✝¹² : IsDomain A
L : Type u_6
inst✝¹¹ : IsDomain R
inst✝¹⁰ : IsDomain S
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra R K
inst✝⁶ : Algebra R L
inst✝⁵ : Algebra S L
inst✝⁴ : IsIntegralClosure S R L
inst✝³ : IsFractionRing S L
inst✝² : Algebra K L
inst✝¹ : IsScalarTower R S L
inst✝ : IsScalarTower R K L
a : S
b : Set S
alg : Algebra.IsAlgebraic R L
inj : Function.Injective ↑(algebraMap R L)
h : ↑(Ideal.span {a}) ⊆ ↑(Submodule.span R b)
x' : L
hx : ↑(algebraMap S L) a * x' ∈ ↑(Ideal.span {↑(algebraMap S L) a})
⊢ ↑(algebraMap S L) a * x' ∈ ↑(Submodule.span K (↑(algebraMap S L) '' b))
[PROOFSTEP]
obtain ⟨y', z', rfl⟩ := IsLocalization.mk'_surjective S⁰ x'
[GOAL]
case intro.intro.intro
R : Type u_1
inst✝¹⁷ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁶ : CommRing S
inst✝¹⁵ : Algebra R S
P : Type u_3
inst✝¹⁴ : CommRing P
A : Type u_4
K : Type u_5
inst✝¹³ : CommRing A
inst✝¹² : IsDomain A
L : Type u_6
inst✝¹¹ : IsDomain R
inst✝¹⁰ : IsDomain S
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra R K
inst✝⁶ : Algebra R L
inst✝⁵ : Algebra S L
inst✝⁴ : IsIntegralClosure S R L
inst✝³ : IsFractionRing S L
inst✝² : Algebra K L
inst✝¹ : IsScalarTower R S L
inst✝ : IsScalarTower R K L
a : S
b : Set S
alg : Algebra.IsAlgebraic R L
inj : Function.Injective ↑(algebraMap R L)
h : ↑(Ideal.span {a}) ⊆ ↑(Submodule.span R b)
y' : S
z' : { x // x ∈ S⁰ }
hx : ↑(algebraMap S L) a * mk' L y' z' ∈ ↑(Ideal.span {↑(algebraMap S L) a})
⊢ ↑(algebraMap S L) a * mk' L y' z' ∈ ↑(Submodule.span K (↑(algebraMap S L) '' b))
[PROOFSTEP]
obtain ⟨y, z, hz0, yz_eq⟩ := IsIntegralClosure.exists_smul_eq_mul alg inj y' (nonZeroDivisors.coe_ne_zero z')
[GOAL]
case intro.intro.intro.intro.intro.intro
R : Type u_1
inst✝¹⁷ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁶ : CommRing S
inst✝¹⁵ : Algebra R S
P : Type u_3
inst✝¹⁴ : CommRing P
A : Type u_4
K : Type u_5
inst✝¹³ : CommRing A
inst✝¹² : IsDomain A
L : Type u_6
inst✝¹¹ : IsDomain R
inst✝¹⁰ : IsDomain S
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra R K
inst✝⁶ : Algebra R L
inst✝⁵ : Algebra S L
inst✝⁴ : IsIntegralClosure S R L
inst✝³ : IsFractionRing S L
inst✝² : Algebra K L
inst✝¹ : IsScalarTower R S L
inst✝ : IsScalarTower R K L
a : S
b : Set S
alg : Algebra.IsAlgebraic R L
inj : Function.Injective ↑(algebraMap R L)
h : ↑(Ideal.span {a}) ⊆ ↑(Submodule.span R b)
y' : S
z' : { x // x ∈ S⁰ }
hx : ↑(algebraMap S L) a * mk' L y' z' ∈ ↑(Ideal.span {↑(algebraMap S L) a})
y : S
z : R
hz0 : z ≠ 0
yz_eq : z • y' = ↑z' * y
⊢ ↑(algebraMap S L) a * mk' L y' z' ∈ ↑(Submodule.span K (↑(algebraMap S L) '' b))
[PROOFSTEP]
have injRS : Function.Injective (algebraMap R S) :=
  by
  refine' Function.Injective.of_comp (show Function.Injective (algebraMap S L ∘ algebraMap R S) from _)
  rwa [← RingHom.coe_comp, ← IsScalarTower.algebraMap_eq]
[GOAL]
R : Type u_1
inst✝¹⁷ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁶ : CommRing S
inst✝¹⁵ : Algebra R S
P : Type u_3
inst✝¹⁴ : CommRing P
A : Type u_4
K : Type u_5
inst✝¹³ : CommRing A
inst✝¹² : IsDomain A
L : Type u_6
inst✝¹¹ : IsDomain R
inst✝¹⁰ : IsDomain S
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra R K
inst✝⁶ : Algebra R L
inst✝⁵ : Algebra S L
inst✝⁴ : IsIntegralClosure S R L
inst✝³ : IsFractionRing S L
inst✝² : Algebra K L
inst✝¹ : IsScalarTower R S L
inst✝ : IsScalarTower R K L
a : S
b : Set S
alg : Algebra.IsAlgebraic R L
inj : Function.Injective ↑(algebraMap R L)
h : ↑(Ideal.span {a}) ⊆ ↑(Submodule.span R b)
y' : S
z' : { x // x ∈ S⁰ }
hx : ↑(algebraMap S L) a * mk' L y' z' ∈ ↑(Ideal.span {↑(algebraMap S L) a})
y : S
z : R
hz0 : z ≠ 0
yz_eq : z • y' = ↑z' * y
⊢ Function.Injective ↑(algebraMap R S)
[PROOFSTEP]
refine' Function.Injective.of_comp (show Function.Injective (algebraMap S L ∘ algebraMap R S) from _)
[GOAL]
R : Type u_1
inst✝¹⁷ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁶ : CommRing S
inst✝¹⁵ : Algebra R S
P : Type u_3
inst✝¹⁴ : CommRing P
A : Type u_4
K : Type u_5
inst✝¹³ : CommRing A
inst✝¹² : IsDomain A
L : Type u_6
inst✝¹¹ : IsDomain R
inst✝¹⁰ : IsDomain S
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra R K
inst✝⁶ : Algebra R L
inst✝⁵ : Algebra S L
inst✝⁴ : IsIntegralClosure S R L
inst✝³ : IsFractionRing S L
inst✝² : Algebra K L
inst✝¹ : IsScalarTower R S L
inst✝ : IsScalarTower R K L
a : S
b : Set S
alg : Algebra.IsAlgebraic R L
inj : Function.Injective ↑(algebraMap R L)
h : ↑(Ideal.span {a}) ⊆ ↑(Submodule.span R b)
y' : S
z' : { x // x ∈ S⁰ }
hx : ↑(algebraMap S L) a * mk' L y' z' ∈ ↑(Ideal.span {↑(algebraMap S L) a})
y : S
z : R
hz0 : z ≠ 0
yz_eq : z • y' = ↑z' * y
⊢ Function.Injective (↑(algebraMap S L) ∘ ↑(algebraMap R S))
[PROOFSTEP]
rwa [← RingHom.coe_comp, ← IsScalarTower.algebraMap_eq]
[GOAL]
case intro.intro.intro.intro.intro.intro
R : Type u_1
inst✝¹⁷ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁶ : CommRing S
inst✝¹⁵ : Algebra R S
P : Type u_3
inst✝¹⁴ : CommRing P
A : Type u_4
K : Type u_5
inst✝¹³ : CommRing A
inst✝¹² : IsDomain A
L : Type u_6
inst✝¹¹ : IsDomain R
inst✝¹⁰ : IsDomain S
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra R K
inst✝⁶ : Algebra R L
inst✝⁵ : Algebra S L
inst✝⁴ : IsIntegralClosure S R L
inst✝³ : IsFractionRing S L
inst✝² : Algebra K L
inst✝¹ : IsScalarTower R S L
inst✝ : IsScalarTower R K L
a : S
b : Set S
alg : Algebra.IsAlgebraic R L
inj : Function.Injective ↑(algebraMap R L)
h : ↑(Ideal.span {a}) ⊆ ↑(Submodule.span R b)
y' : S
z' : { x // x ∈ S⁰ }
hx : ↑(algebraMap S L) a * mk' L y' z' ∈ ↑(Ideal.span {↑(algebraMap S L) a})
y : S
z : R
hz0 : z ≠ 0
yz_eq : z • y' = ↑z' * y
injRS : Function.Injective ↑(algebraMap R S)
⊢ ↑(algebraMap S L) a * mk' L y' z' ∈ ↑(Submodule.span K (↑(algebraMap S L) '' b))
[PROOFSTEP]
have hz0' : algebraMap R S z ∈ S⁰ := map_mem_nonZeroDivisors (algebraMap R S) injRS (mem_nonZeroDivisors_of_ne_zero hz0)
[GOAL]
case intro.intro.intro.intro.intro.intro
R : Type u_1
inst✝¹⁷ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁶ : CommRing S
inst✝¹⁵ : Algebra R S
P : Type u_3
inst✝¹⁴ : CommRing P
A : Type u_4
K : Type u_5
inst✝¹³ : CommRing A
inst✝¹² : IsDomain A
L : Type u_6
inst✝¹¹ : IsDomain R
inst✝¹⁰ : IsDomain S
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra R K
inst✝⁶ : Algebra R L
inst✝⁵ : Algebra S L
inst✝⁴ : IsIntegralClosure S R L
inst✝³ : IsFractionRing S L
inst✝² : Algebra K L
inst✝¹ : IsScalarTower R S L
inst✝ : IsScalarTower R K L
a : S
b : Set S
alg : Algebra.IsAlgebraic R L
inj : Function.Injective ↑(algebraMap R L)
h : ↑(Ideal.span {a}) ⊆ ↑(Submodule.span R b)
y' : S
z' : { x // x ∈ S⁰ }
hx : ↑(algebraMap S L) a * mk' L y' z' ∈ ↑(Ideal.span {↑(algebraMap S L) a})
y : S
z : R
hz0 : z ≠ 0
yz_eq : z • y' = ↑z' * y
injRS : Function.Injective ↑(algebraMap R S)
hz0' : ↑(algebraMap R S) z ∈ S⁰
⊢ ↑(algebraMap S L) a * mk' L y' z' ∈ ↑(Submodule.span K (↑(algebraMap S L) '' b))
[PROOFSTEP]
have mk_yz_eq : IsLocalization.mk' L y' z' = IsLocalization.mk' L y ⟨_, hz0'⟩ :=
  by
  rw [Algebra.smul_def, mul_comm _ y, mul_comm _ y'] at yz_eq 
  exact IsLocalization.mk'_eq_of_eq (by rw [mul_comm _ y, mul_comm _ y', yz_eq])
[GOAL]
R : Type u_1
inst✝¹⁷ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁶ : CommRing S
inst✝¹⁵ : Algebra R S
P : Type u_3
inst✝¹⁴ : CommRing P
A : Type u_4
K : Type u_5
inst✝¹³ : CommRing A
inst✝¹² : IsDomain A
L : Type u_6
inst✝¹¹ : IsDomain R
inst✝¹⁰ : IsDomain S
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra R K
inst✝⁶ : Algebra R L
inst✝⁵ : Algebra S L
inst✝⁴ : IsIntegralClosure S R L
inst✝³ : IsFractionRing S L
inst✝² : Algebra K L
inst✝¹ : IsScalarTower R S L
inst✝ : IsScalarTower R K L
a : S
b : Set S
alg : Algebra.IsAlgebraic R L
inj : Function.Injective ↑(algebraMap R L)
h : ↑(Ideal.span {a}) ⊆ ↑(Submodule.span R b)
y' : S
z' : { x // x ∈ S⁰ }
hx : ↑(algebraMap S L) a * mk' L y' z' ∈ ↑(Ideal.span {↑(algebraMap S L) a})
y : S
z : R
hz0 : z ≠ 0
yz_eq : z • y' = ↑z' * y
injRS : Function.Injective ↑(algebraMap R S)
hz0' : ↑(algebraMap R S) z ∈ S⁰
⊢ mk' L y' z' = mk' L y { val := ↑(algebraMap R S) z, property := hz0' }
[PROOFSTEP]
rw [Algebra.smul_def, mul_comm _ y, mul_comm _ y'] at yz_eq 
[GOAL]
R : Type u_1
inst✝¹⁷ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁶ : CommRing S
inst✝¹⁵ : Algebra R S
P : Type u_3
inst✝¹⁴ : CommRing P
A : Type u_4
K : Type u_5
inst✝¹³ : CommRing A
inst✝¹² : IsDomain A
L : Type u_6
inst✝¹¹ : IsDomain R
inst✝¹⁰ : IsDomain S
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra R K
inst✝⁶ : Algebra R L
inst✝⁵ : Algebra S L
inst✝⁴ : IsIntegralClosure S R L
inst✝³ : IsFractionRing S L
inst✝² : Algebra K L
inst✝¹ : IsScalarTower R S L
inst✝ : IsScalarTower R K L
a : S
b : Set S
alg : Algebra.IsAlgebraic R L
inj : Function.Injective ↑(algebraMap R L)
h : ↑(Ideal.span {a}) ⊆ ↑(Submodule.span R b)
y' : S
z' : { x // x ∈ S⁰ }
hx : ↑(algebraMap S L) a * mk' L y' z' ∈ ↑(Ideal.span {↑(algebraMap S L) a})
y : S
z : R
hz0 : z ≠ 0
yz_eq : y' * ↑(algebraMap R S) z = y * ↑z'
injRS : Function.Injective ↑(algebraMap R S)
hz0' : ↑(algebraMap R S) z ∈ S⁰
⊢ mk' L y' z' = mk' L y { val := ↑(algebraMap R S) z, property := hz0' }
[PROOFSTEP]
exact IsLocalization.mk'_eq_of_eq (by rw [mul_comm _ y, mul_comm _ y', yz_eq])
[GOAL]
R : Type u_1
inst✝¹⁷ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁶ : CommRing S
inst✝¹⁵ : Algebra R S
P : Type u_3
inst✝¹⁴ : CommRing P
A : Type u_4
K : Type u_5
inst✝¹³ : CommRing A
inst✝¹² : IsDomain A
L : Type u_6
inst✝¹¹ : IsDomain R
inst✝¹⁰ : IsDomain S
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra R K
inst✝⁶ : Algebra R L
inst✝⁵ : Algebra S L
inst✝⁴ : IsIntegralClosure S R L
inst✝³ : IsFractionRing S L
inst✝² : Algebra K L
inst✝¹ : IsScalarTower R S L
inst✝ : IsScalarTower R K L
a : S
b : Set S
alg : Algebra.IsAlgebraic R L
inj : Function.Injective ↑(algebraMap R L)
h : ↑(Ideal.span {a}) ⊆ ↑(Submodule.span R b)
y' : S
z' : { x // x ∈ S⁰ }
hx : ↑(algebraMap S L) a * mk' L y' z' ∈ ↑(Ideal.span {↑(algebraMap S L) a})
y : S
z : R
hz0 : z ≠ 0
yz_eq : y' * ↑(algebraMap R S) z = y * ↑z'
injRS : Function.Injective ↑(algebraMap R S)
hz0' : ↑(algebraMap R S) z ∈ S⁰
⊢ ↑z' * y = ↑{ val := ↑(algebraMap R S) z, property := hz0' } * y'
[PROOFSTEP]
rw [mul_comm _ y, mul_comm _ y', yz_eq]
[GOAL]
case intro.intro.intro.intro.intro.intro
R : Type u_1
inst✝¹⁷ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁶ : CommRing S
inst✝¹⁵ : Algebra R S
P : Type u_3
inst✝¹⁴ : CommRing P
A : Type u_4
K : Type u_5
inst✝¹³ : CommRing A
inst✝¹² : IsDomain A
L : Type u_6
inst✝¹¹ : IsDomain R
inst✝¹⁰ : IsDomain S
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra R K
inst✝⁶ : Algebra R L
inst✝⁵ : Algebra S L
inst✝⁴ : IsIntegralClosure S R L
inst✝³ : IsFractionRing S L
inst✝² : Algebra K L
inst✝¹ : IsScalarTower R S L
inst✝ : IsScalarTower R K L
a : S
b : Set S
alg : Algebra.IsAlgebraic R L
inj : Function.Injective ↑(algebraMap R L)
h : ↑(Ideal.span {a}) ⊆ ↑(Submodule.span R b)
y' : S
z' : { x // x ∈ S⁰ }
hx : ↑(algebraMap S L) a * mk' L y' z' ∈ ↑(Ideal.span {↑(algebraMap S L) a})
y : S
z : R
hz0 : z ≠ 0
yz_eq : z • y' = ↑z' * y
injRS : Function.Injective ↑(algebraMap R S)
hz0' : ↑(algebraMap R S) z ∈ S⁰
mk_yz_eq : mk' L y' z' = mk' L y { val := ↑(algebraMap R S) z, property := hz0' }
⊢ ↑(algebraMap S L) a * mk' L y' z' ∈ ↑(Submodule.span K (↑(algebraMap S L) '' b))
[PROOFSTEP]
suffices hy : algebraMap S L (a * y) ∈ Submodule.span K ((algebraMap S L) '' b)
[GOAL]
case intro.intro.intro.intro.intro.intro
R : Type u_1
inst✝¹⁷ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁶ : CommRing S
inst✝¹⁵ : Algebra R S
P : Type u_3
inst✝¹⁴ : CommRing P
A : Type u_4
K : Type u_5
inst✝¹³ : CommRing A
inst✝¹² : IsDomain A
L : Type u_6
inst✝¹¹ : IsDomain R
inst✝¹⁰ : IsDomain S
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra R K
inst✝⁶ : Algebra R L
inst✝⁵ : Algebra S L
inst✝⁴ : IsIntegralClosure S R L
inst✝³ : IsFractionRing S L
inst✝² : Algebra K L
inst✝¹ : IsScalarTower R S L
inst✝ : IsScalarTower R K L
a : S
b : Set S
alg : Algebra.IsAlgebraic R L
inj : Function.Injective ↑(algebraMap R L)
h : ↑(Ideal.span {a}) ⊆ ↑(Submodule.span R b)
y' : S
z' : { x // x ∈ S⁰ }
hx : ↑(algebraMap S L) a * mk' L y' z' ∈ ↑(Ideal.span {↑(algebraMap S L) a})
y : S
z : R
hz0 : z ≠ 0
yz_eq : z • y' = ↑z' * y
injRS : Function.Injective ↑(algebraMap R S)
hz0' : ↑(algebraMap R S) z ∈ S⁰
mk_yz_eq : mk' L y' z' = mk' L y { val := ↑(algebraMap R S) z, property := hz0' }
hy : ↑(algebraMap S L) (a * y) ∈ Submodule.span K (↑(algebraMap S L) '' b)
⊢ ↑(algebraMap S L) a * mk' L y' z' ∈ ↑(Submodule.span K (↑(algebraMap S L) '' b))
[PROOFSTEP]
rw [mk_yz_eq, IsFractionRing.mk'_eq_div, ← IsScalarTower.algebraMap_apply, IsScalarTower.algebraMap_apply R K L,
  div_eq_mul_inv, ← mul_assoc, mul_comm, ← map_inv₀, ← Algebra.smul_def, ← _root_.map_mul]
[GOAL]
case intro.intro.intro.intro.intro.intro
R : Type u_1
inst✝¹⁷ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁶ : CommRing S
inst✝¹⁵ : Algebra R S
P : Type u_3
inst✝¹⁴ : CommRing P
A : Type u_4
K : Type u_5
inst✝¹³ : CommRing A
inst✝¹² : IsDomain A
L : Type u_6
inst✝¹¹ : IsDomain R
inst✝¹⁰ : IsDomain S
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra R K
inst✝⁶ : Algebra R L
inst✝⁵ : Algebra S L
inst✝⁴ : IsIntegralClosure S R L
inst✝³ : IsFractionRing S L
inst✝² : Algebra K L
inst✝¹ : IsScalarTower R S L
inst✝ : IsScalarTower R K L
a : S
b : Set S
alg : Algebra.IsAlgebraic R L
inj : Function.Injective ↑(algebraMap R L)
h : ↑(Ideal.span {a}) ⊆ ↑(Submodule.span R b)
y' : S
z' : { x // x ∈ S⁰ }
hx : ↑(algebraMap S L) a * mk' L y' z' ∈ ↑(Ideal.span {↑(algebraMap S L) a})
y : S
z : R
hz0 : z ≠ 0
yz_eq : z • y' = ↑z' * y
injRS : Function.Injective ↑(algebraMap R S)
hz0' : ↑(algebraMap R S) z ∈ S⁰
mk_yz_eq : mk' L y' z' = mk' L y { val := ↑(algebraMap R S) z, property := hz0' }
hy : ↑(algebraMap S L) (a * y) ∈ Submodule.span K (↑(algebraMap S L) '' b)
⊢ (↑(algebraMap R K) z)⁻¹ • ↑(algebraMap S L) (a * y) ∈ ↑(Submodule.span K (↑(algebraMap S L) '' b))
[PROOFSTEP]
exact (Submodule.span K _).smul_mem _ hy
[GOAL]
case hy
R : Type u_1
inst✝¹⁷ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁶ : CommRing S
inst✝¹⁵ : Algebra R S
P : Type u_3
inst✝¹⁴ : CommRing P
A : Type u_4
K : Type u_5
inst✝¹³ : CommRing A
inst✝¹² : IsDomain A
L : Type u_6
inst✝¹¹ : IsDomain R
inst✝¹⁰ : IsDomain S
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra R K
inst✝⁶ : Algebra R L
inst✝⁵ : Algebra S L
inst✝⁴ : IsIntegralClosure S R L
inst✝³ : IsFractionRing S L
inst✝² : Algebra K L
inst✝¹ : IsScalarTower R S L
inst✝ : IsScalarTower R K L
a : S
b : Set S
alg : Algebra.IsAlgebraic R L
inj : Function.Injective ↑(algebraMap R L)
h : ↑(Ideal.span {a}) ⊆ ↑(Submodule.span R b)
y' : S
z' : { x // x ∈ S⁰ }
hx : ↑(algebraMap S L) a * mk' L y' z' ∈ ↑(Ideal.span {↑(algebraMap S L) a})
y : S
z : R
hz0 : z ≠ 0
yz_eq : z • y' = ↑z' * y
injRS : Function.Injective ↑(algebraMap R S)
hz0' : ↑(algebraMap R S) z ∈ S⁰
mk_yz_eq : mk' L y' z' = mk' L y { val := ↑(algebraMap R S) z, property := hz0' }
⊢ ↑(algebraMap S L) (a * y) ∈ Submodule.span K (↑(algebraMap S L) '' b)
[PROOFSTEP]
refine' Submodule.span_subset_span R K _ _
[GOAL]
case hy
R : Type u_1
inst✝¹⁷ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁶ : CommRing S
inst✝¹⁵ : Algebra R S
P : Type u_3
inst✝¹⁴ : CommRing P
A : Type u_4
K : Type u_5
inst✝¹³ : CommRing A
inst✝¹² : IsDomain A
L : Type u_6
inst✝¹¹ : IsDomain R
inst✝¹⁰ : IsDomain S
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra R K
inst✝⁶ : Algebra R L
inst✝⁵ : Algebra S L
inst✝⁴ : IsIntegralClosure S R L
inst✝³ : IsFractionRing S L
inst✝² : Algebra K L
inst✝¹ : IsScalarTower R S L
inst✝ : IsScalarTower R K L
a : S
b : Set S
alg : Algebra.IsAlgebraic R L
inj : Function.Injective ↑(algebraMap R L)
h : ↑(Ideal.span {a}) ⊆ ↑(Submodule.span R b)
y' : S
z' : { x // x ∈ S⁰ }
hx : ↑(algebraMap S L) a * mk' L y' z' ∈ ↑(Ideal.span {↑(algebraMap S L) a})
y : S
z : R
hz0 : z ≠ 0
yz_eq : z • y' = ↑z' * y
injRS : Function.Injective ↑(algebraMap R S)
hz0' : ↑(algebraMap R S) z ∈ S⁰
mk_yz_eq : mk' L y' z' = mk' L y { val := ↑(algebraMap R S) z, property := hz0' }
⊢ ↑(algebraMap S L) (a * y) ∈ ↑(Submodule.span R (↑(algebraMap S L) '' b))
[PROOFSTEP]
rw [Submodule.span_algebraMap_image_of_tower]
[GOAL]
case hy
R : Type u_1
inst✝¹⁷ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁶ : CommRing S
inst✝¹⁵ : Algebra R S
P : Type u_3
inst✝¹⁴ : CommRing P
A : Type u_4
K : Type u_5
inst✝¹³ : CommRing A
inst✝¹² : IsDomain A
L : Type u_6
inst✝¹¹ : IsDomain R
inst✝¹⁰ : IsDomain S
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra R K
inst✝⁶ : Algebra R L
inst✝⁵ : Algebra S L
inst✝⁴ : IsIntegralClosure S R L
inst✝³ : IsFractionRing S L
inst✝² : Algebra K L
inst✝¹ : IsScalarTower R S L
inst✝ : IsScalarTower R K L
a : S
b : Set S
alg : Algebra.IsAlgebraic R L
inj : Function.Injective ↑(algebraMap R L)
h : ↑(Ideal.span {a}) ⊆ ↑(Submodule.span R b)
y' : S
z' : { x // x ∈ S⁰ }
hx : ↑(algebraMap S L) a * mk' L y' z' ∈ ↑(Ideal.span {↑(algebraMap S L) a})
y : S
z : R
hz0 : z ≠ 0
yz_eq : z • y' = ↑z' * y
injRS : Function.Injective ↑(algebraMap R S)
hz0' : ↑(algebraMap R S) z ∈ S⁰
mk_yz_eq : mk' L y' z' = mk' L y { val := ↑(algebraMap R S) z, property := hz0' }
⊢ ↑(algebraMap S L) (a * y) ∈ ↑(Submodule.map (↑R (Algebra.linearMap S L)) (Submodule.span R b))
[PROOFSTEP]
exact Submodule.mem_map_of_mem (h (Ideal.mem_span_singleton.mpr ⟨y, rfl⟩))
