-- 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 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
h : ∀ (x : S), IsAlgebraic R x
x : K
this✝ : Algebra (FractionRing R) K := FractionRing.liftAlgebra R K
this : IsScalarTower R (FractionRing R) K
⊢ IsIntegral (FractionRing R) x

Tactic:
obtain ⟨a : S, b, ha, rfl⟩ := div_surjective (A := S) x

Result:
case mp.intro.intro.intro
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
⊢ IsIntegral (FractionRing R) ((algebraMap S K) a / (algebraMap S K) b)

Proof state:
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
h : ∀ (x : S), IsAlgebraic R x
x : K
this : Algebra (FractionRing R) K := FractionRing.liftAlgebra R K
⊢ IsAlgebraic R x

Tactic:
have := FractionRing.isScalarTower_liftAlgebra R K

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
h : ∀ (x : S), IsAlgebraic R x
x : K
this✝ : Algebra (FractionRing R) K := FractionRing.liftAlgebra R K
this : IsScalarTower R (FractionRing R) K
⊢ IsAlgebraic R x

Proof state:
case mpr.intro.intro
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
⊢ IsAlgebraic R x

Tactic:
use f, 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₂ : (aeval ((algebraMap S K) x)) f = 0
⊢ (aeval x) f = 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
⊢ Algebra.IsAlgebraic R S ↔ Algebra.IsAlgebraic R K

Tactic:
simp only [Algebra.isAlgebraic_def]

Result:
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

Proof state:
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
h : ∀ (x : S), IsAlgebraic R x
x : K
this✝ : Algebra (FractionRing R) K := FractionRing.liftAlgebra R K
this : IsScalarTower R (FractionRing R) K
⊢ IsAlgebraic R x

Tactic:
rw [IsFractionRing.isAlgebraic_iff R (FractionRing R) K, isAlgebraic_iff_isIntegral]

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
h : ∀ (x : S), IsAlgebraic R x
x : K
this✝ : Algebra (FractionRing R) K := FractionRing.liftAlgebra R K
this : IsScalarTower R (FractionRing R) K
⊢ IsIntegral (FractionRing 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₂ : (algebraMap S K) ((aeval x) f) = 0
⊢ (aeval x) f = 0

Tactic:
exact
  (injective_iff_map_eq_zero (algebraMap S K)).1 (FaithfulSMul.algebraMap_injective _ _) _
    hf₂

Result:
no goals

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
⊢ (aeval ((algebraMap S K) b)⁻¹) (Polynomial.map (algebraMap R (FractionRing R)) f).reverse = 0

Tactic:
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
            (FaithfulSMul.algebraMap_injective _ _) b h)))

Result:
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