R : Type u_2
inst✝¹³ : CommRing R
M : Submonoid R
S : Type u_3
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
P : Type ?u.599719
inst✝¹⁰ : CommRing P
A : Type ?u.599725
K : Type u_1
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
R : Type u_2
inst✝¹³ : CommRing R
M : Submonoid R
S : Type u_3
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
P : Type ?u.599719
inst✝¹⁰ : CommRing P
A : Type ?u.599725
K : Type u_1
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
simp only [Algebra.IsAlgebraic]
case mp
R : Type u_2
inst✝¹³ : CommRing R
M : Submonoid R
S : Type u_3
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
P : Type ?u.599719
inst✝¹⁰ : CommRing P
A : Type ?u.599725
K : Type u_1
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

case mpr
R : Type u_2
inst✝¹³ : CommRing R
M : Submonoid R
S : Type u_3
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
P : Type ?u.599719
inst✝¹⁰ : CommRing P
A : Type ?u.599725
K : Type u_1
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
R : Type u_2
inst✝¹³ : CommRing R
M : Submonoid R
S : Type u_3
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
P : Type ?u.599719
inst✝¹⁰ : CommRing P
A : Type ?u.599725
K : Type u_1
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
constructor
case mp
R : Type u_2
inst✝¹³ : CommRing R
M : Submonoid R
S : Type u_3
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
P : Type ?u.599719
inst✝¹⁰ : CommRing P
A : Type ?u.599725
K : Type u_1
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
case mp
R : Type u_2
inst✝¹³ : CommRing R
M : Submonoid R
S : Type u_3
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
P : Type ?u.599719
inst✝¹⁰ : CommRing P
A : Type ?u.599725
K : Type u_1
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
intro h x
case mp
R : Type u_2
inst✝¹³ : CommRing R
M : Submonoid R
S : Type u_3
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
P : Type ?u.599719
inst✝¹⁰ : CommRing P
A : Type ?u.599725
K : Type u_1
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
case mp
R : Type u_2
inst✝¹³ : CommRing R
M : Submonoid R
S : Type u_3
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
P : Type ?u.599719
inst✝¹⁰ : CommRing P
A : Type ?u.599725
K : Type u_1
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
rw [IsFractionRing.isAlgebraic_iff R (FractionRing R) K, isAlgebraic_iff_isIntegral]
case mp.intro.intro.intro
R : Type u_2
inst✝¹³ : CommRing R
M : Submonoid R
S : Type u_3
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
P : Type ?u.599719
inst✝¹⁰ : CommRing P
A : Type ?u.599725
K : Type u_1
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)
case mp
R : Type u_2
inst✝¹³ : CommRing R
M : Submonoid R
S : Type u_3
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
P : Type ?u.599719
inst✝¹⁰ : CommRing P
A : Type ?u.599725
K : Type u_1
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
obtain ⟨a : S, b, ha, rfl⟩ := @div_surjective S _ _ _ _ _ _ x
case mp.intro.intro.intro.intro.intro
R : Type u_2
inst✝¹³ : CommRing R
M : Submonoid R
S : Type u_3
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
P : Type ?u.599719
inst✝¹⁰ : CommRing P
A : Type ?u.599725
K : Type u_1
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)
case mp.intro.intro.intro
R : Type u_2
inst✝¹³ : CommRing R
M : Submonoid R
S : Type u_3
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
P : Type ?u.599719
inst✝¹⁰ : CommRing P
A : Type ?u.599725
K : Type u_1
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)
obtain ⟨f, hf₁, hf₂⟩ := h b
case mp.intro.intro.intro.intro.intro
R : Type u_2
inst✝¹³ : CommRing R
M : Submonoid R
S : Type u_3
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
P : Type ?u.599719
inst✝¹⁰ : CommRing P
A : Type ?u.599725
K : Type u_1
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)⁻¹)
case mp.intro.intro.intro.intro.intro
R : Type u_2
inst✝¹³ : CommRing R
M : Submonoid R
S : Type u_3
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
P : Type ?u.599719
inst✝¹⁰ : CommRing P
A : Type ?u.599725
K : Type u_1
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)
rw [div_eq_mul_inv]
case mp.intro.intro.intro.intro.intro.refine'_1
R : Type u_2
inst✝¹³ : CommRing R
M : Submonoid R
S : Type u_3
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
P : Type ?u.599719
inst✝¹⁰ : CommRing P
A : Type ?u.599725
K : Type u_1
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)

case mp.intro.intro.intro.intro.intro.refine'_2
R : Type u_2
inst✝¹³ : CommRing R
M : Submonoid R
S : Type u_3
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
P : Type ?u.599719
inst✝¹⁰ : CommRing P
A : Type ?u.599725
K : Type u_1
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)⁻¹
case mp.intro.intro.intro.intro.intro
R : Type u_2
inst✝¹³ : CommRing R
M : Submonoid R
S : Type u_3
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
P : Type ?u.599719
inst✝¹⁰ : CommRing P
A : Type ?u.599725
K : Type u_1
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)⁻¹)
refine' isIntegral_mul _ _
case mp.intro.intro.intro.intro.intro.refine'_1
R : Type u_2
inst✝¹³ : CommRing R
M : Submonoid R
S : Type u_3
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
P : Type ?u.599719
inst✝¹⁰ : CommRing P
A : Type ?u.599725
K : Type u_1
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)
case mp.intro.intro.intro.intro.intro.refine'_1
R : Type u_2
inst✝¹³ : CommRing R
M : Submonoid R
S : Type u_3
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
P : Type ?u.599719
inst✝¹⁰ : CommRing P
A : Type ?u.599725
K : Type u_1
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)
rw [← isAlgebraic_iff_isIntegral]
case mp.intro.intro.intro.intro.intro.refine'_1
R : Type u_2
inst✝¹³ : CommRing R
M : Submonoid R
S : Type u_3
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
P : Type ?u.599719
inst✝¹⁰ : CommRing P
A : Type ?u.599725
K : Type u_1
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)
case mp.intro.intro.intro.intro.intro.refine'_1
R : Type u_2
inst✝¹³ : CommRing R
M : Submonoid R
S : Type u_3
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
P : Type ?u.599719
inst✝¹⁰ : CommRing P
A : Type ?u.599725
K : Type u_1
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)
refine'
  _root_.isAlgebraic_of_larger_base_of_injective
    (NoZeroSMulDivisors.algebraMap_injective R (FractionRing R)) _
no goals
case mp.intro.intro.intro.intro.intro.refine'_1
R : Type u_2
inst✝¹³ : CommRing R
M : Submonoid R
S : Type u_3
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
P : Type ?u.599719
inst✝¹⁰ : CommRing P
A : Type ?u.599725
K : Type u_1
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)
exact isAlgebraic_algebraMap_of_isAlgebraic (h a)
case mp.intro.intro.intro.intro.intro.refine'_2
R : Type u_2
inst✝¹³ : CommRing R
M : Submonoid R
S : Type u_3
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
P : Type ?u.599719
inst✝¹⁰ : CommRing P
A : Type ?u.599725
K : Type u_1
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)⁻¹
case mp.intro.intro.intro.intro.intro.refine'_2
R : Type u_2
inst✝¹³ : CommRing R
M : Submonoid R
S : Type u_3
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
P : Type ?u.599719
inst✝¹⁰ : CommRing P
A : Type ?u.599725
K : Type u_1
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)⁻¹
rw [← isAlgebraic_iff_isIntegral]
case mp.intro.intro.intro.intro.intro.refine'_2
R : Type u_2
inst✝¹³ : CommRing R
M : Submonoid R
S : Type u_3
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
P : Type ?u.599719
inst✝¹⁰ : CommRing P
A : Type ?u.599725
K : Type u_1
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
case mp.intro.intro.intro.intro.intro.refine'_2
R : Type u_2
inst✝¹³ : CommRing R
M : Submonoid R
S : Type u_3
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
P : Type ?u.599719
inst✝¹⁰ : CommRing P
A : Type ?u.599725
K : Type u_1
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)⁻¹
use (f.map (algebraMap R (FractionRing R))).reverse
case mp.intro.intro.intro.intro.intro.refine'_2.left
R : Type u_2
inst✝¹³ : CommRing R
M : Submonoid R
S : Type u_3
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
P : Type ?u.599719
inst✝¹⁰ : CommRing P
A : Type ?u.599725
K : Type u_1
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

case mp.intro.intro.intro.intro.intro.refine'_2.right
R : Type u_2
inst✝¹³ : CommRing R
M : Submonoid R
S : Type u_3
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
P : Type ?u.599719
inst✝¹⁰ : CommRing P
A : Type ?u.599725
K : Type u_1
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
case mp.intro.intro.intro.intro.intro.refine'_2
R : Type u_2
inst✝¹³ : CommRing R
M : Submonoid R
S : Type u_3
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
P : Type ?u.599719
inst✝¹⁰ : CommRing P
A : Type ?u.599725
K : Type u_1
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
constructor
no goals
case mp.intro.intro.intro.intro.intro.refine'_2.left
R : Type u_2
inst✝¹³ : CommRing R
M : Submonoid R
S : Type u_3
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
P : Type ?u.599719
inst✝¹⁰ : CommRing P
A : Type ?u.599725
K : Type u_1
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
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]
case mp.intro.intro.intro.intro.intro.refine'_2.right
R : Type u_2
inst✝¹³ : CommRing R
M : Submonoid R
S : Type u_3
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
P : Type ?u.599719
inst✝¹⁰ : CommRing P
A : Type ?u.599725
K : Type u_1
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
case mp.intro.intro.intro.intro.intro.refine'_2.right
R : Type u_2
inst✝¹³ : CommRing R
M : Submonoid R
S : Type u_3
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
P : Type ?u.599719
inst✝¹⁰ : CommRing P
A : Type ?u.599725
K : Type u_1
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
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)))
no goals
case mp.intro.intro.intro.intro.intro.refine'_2.right
R : Type u_2
inst✝¹³ : CommRing R
M : Submonoid R
S : Type u_3
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
P : Type ?u.599719
inst✝¹⁰ : CommRing P
A : Type ?u.599725
K : Type u_1
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
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]
case mpr
R : Type u_2
inst✝¹³ : CommRing R
M : Submonoid R
S : Type u_3
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
P : Type ?u.599719
inst✝¹⁰ : CommRing P
A : Type ?u.599725
K : Type u_1
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
case mpr
R : Type u_2
inst✝¹³ : CommRing R
M : Submonoid R
S : Type u_3
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
P : Type ?u.599719
inst✝¹⁰ : CommRing P
A : Type ?u.599725
K : Type u_1
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
intro h x
case mpr.intro.intro
R : Type u_2
inst✝¹³ : CommRing R
M : Submonoid R
S : Type u_3
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
P : Type ?u.599719
inst✝¹⁰ : CommRing P
A : Type ?u.599725
K : Type u_1
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
case mpr
R : Type u_2
inst✝¹³ : CommRing R
M : Submonoid R
S : Type u_3
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
P : Type ?u.599719
inst✝¹⁰ : CommRing P
A : Type ?u.599725
K : Type u_1
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
obtain ⟨f, hf₁, hf₂⟩ := h (algebraMap S K x)
case mpr.intro.intro
R : Type u_2
inst✝¹³ : CommRing R
M : Submonoid R
S : Type u_3
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
P : Type ?u.599719
inst✝¹⁰ : CommRing P
A : Type ?u.599725
K : Type u_1
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
case mpr.intro.intro
R : Type u_2
inst✝¹³ : CommRing R
M : Submonoid R
S : Type u_3
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
P : Type ?u.599719
inst✝¹⁰ : CommRing P
A : Type ?u.599725
K : Type u_1
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
use f, hf₁
case mpr.intro.intro
R : Type u_2
inst✝¹³ : CommRing R
M : Submonoid R
S : Type u_3
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
P : Type ?u.599719
inst✝¹⁰ : CommRing P
A : Type ?u.599725
K : Type u_1
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
case mpr.intro.intro
R : Type u_2
inst✝¹³ : CommRing R
M : Submonoid R
S : Type u_3
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
P : Type ?u.599719
inst✝¹⁰ : CommRing P
A : Type ?u.599725
K : Type u_1
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
rw [Polynomial.aeval_algebraMap_apply] at hf₂
no goals
case mpr.intro.intro
R : Type u_2
inst✝¹³ : CommRing R
M : Submonoid R
S : Type u_3
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
P : Type ?u.599719
inst✝¹⁰ : CommRing P
A : Type ?u.599725
K : Type u_1
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
exact
  (injective_iff_map_eq_zero (algebraMap S K)).1 (NoZeroSMulDivisors.algebraMap_injective _ _) _
    hf₂