-- Mathlib/RingTheory/Localization/Integral.lean
theorem isAlgebraic_iff' [Field K] [IsDomain R] [IsDomain S] [Algebra R K] [Algebra S K]
    [NoZeroSMulDivisors R K] [IsFractionRing S K] [IsScalarTower R S K] :
    Algebra.IsAlgebraic R S ↔ Algebra.IsAlgebraic R K

Proof state:
case h
R : Type u_1
inst✝¹⁰ : CommRing R
S : Type u_2
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
K : Type u_4
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
this✝ : Algebra (FractionRing R) K := FractionRing.liftAlgebra R K
this : IsScalarTower R (FractionRing R) K
a b : S
ha : b ∈ nonZeroDivisors S
f : R[X]
hf₁ : f ≠ 0
hf₂ : (aeval b) f = 0
⊢ (Polynomial.map (algebraMap R (FractionRing R)) f).reverse ≠ 0 ∧
    (aeval ((algebraMap S K) b)⁻¹) (Polynomial.map (algebraMap R (FractionRing R)) f).reverse = 0

Tactic:
constructor

Result:
case h.left
R : Type u_1
inst✝¹⁰ : CommRing R
S : Type u_2
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
K : Type u_4
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
this✝ : Algebra (FractionRing R) K := FractionRing.liftAlgebra R K
this : IsScalarTower R (FractionRing R) K
a b : S
ha : b ∈ nonZeroDivisors S
f : R[X]
hf₁ : f ≠ 0
hf₂ : (aeval b) f = 0
⊢ (Polynomial.map (algebraMap R (FractionRing R)) f).reverse ≠ 0

case h.right
R : Type u_1
inst✝¹⁰ : CommRing R
S : Type u_2
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
K : Type u_4
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
this✝ : Algebra (FractionRing R) K := FractionRing.liftAlgebra R K
this : IsScalarTower R (FractionRing R) K
a b : S
ha : b ∈ nonZeroDivisors S
f : R[X]
hf₁ : f ≠ 0
hf₂ : (aeval b) f = 0
⊢ (aeval ((algebraMap S K) b)⁻¹) (Polynomial.map (algebraMap R (FractionRing R)) f).reverse = 0

Proof state:
case h.right
R : Type u_1
inst✝¹⁰ : CommRing R
S : Type u_2
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
K : Type u_4
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
this✝¹ : Algebra (FractionRing R) K := FractionRing.liftAlgebra R K
this✝ : IsScalarTower R (FractionRing R) K
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)⁻¹) (Polynomial.map (algebraMap R (FractionRing R)) f).reverse = 0

Tactic:
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]

Result:
no goals

Proof state:
case mp.intro.intro.intro.intro.intro.refine_2
R : Type u_1
inst✝¹⁰ : CommRing R
S : Type u_2
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
K : Type u_4
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
this✝ : Algebra (FractionRing R) K := FractionRing.liftAlgebra R K
this : IsScalarTower R (FractionRing R) K
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)⁻¹

Tactic:
use (f.map (algebraMap R (FractionRing R))).reverse

Result:
case h
R : Type u_1
inst✝¹⁰ : CommRing R
S : Type u_2
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
K : Type u_4
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
this✝ : Algebra (FractionRing R) K := FractionRing.liftAlgebra R K
this : IsScalarTower R (FractionRing R) K
a b : S
ha : b ∈ nonZeroDivisors S
f : R[X]
hf₁ : f ≠ 0
hf₂ : (aeval b) f = 0
⊢ (Polynomial.map (algebraMap R (FractionRing R)) f).reverse ≠ 0 ∧
    (aeval ((algebraMap S K) b)⁻¹) (Polynomial.map (algebraMap R (FractionRing R)) f).reverse = 0

Proof state:
R : Type u_1
inst✝¹⁰ : CommRing R
S : Type u_2
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
K : Type u_4
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

Tactic:
constructor

Result:
case mp
R : Type u_1
inst✝¹⁰ : CommRing R
S : Type u_2
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
K : Type u_4
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_1
inst✝¹⁰ : CommRing R
S : Type u_2
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
K : Type u_4
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

Proof state:
case right
R : Type u_1
inst✝¹⁰ : CommRing R
S : Type u_2
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
K : Type u_4
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

Tactic:
rw [Polynomial.aeval_algebraMap_apply] at hf₂

Result:
case right
R : Type u_1
inst✝¹⁰ : CommRing R
S : Type u_2
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
K : Type u_4
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