-- 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
⊢ (∀ (x : S), IsAlgebraic R x) → ∀ (x : K), IsAlgebraic R x

Tactic:
intro h x

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
⊢ IsAlgebraic R x

Proof state:
case mp.intro.intro.intro.intro.intro.refine_1
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
⊢ IsIntegral (FractionRing R) ((algebraMap S K) a)

Tactic:
rw [← isAlgebraic_iff_isIntegral]

Result:
case mp.intro.intro.intro.intro.intro.refine_1
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) a)

Proof state:
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)

Tactic:
obtain ⟨f, hf₁, hf₂⟩ := h b

Result:
case mp.intro.intro.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
f : R[X]
hf₁ : f ≠ 0
hf₂ : (aeval b) f = 0
⊢ IsIntegral (FractionRing R) ((algebraMap S K) a / (algebraMap S K) b)

Proof state:
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

Tactic:
intro h x

Result:
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
h : ∀ (x : K), IsAlgebraic R x
x : S
⊢ IsAlgebraic R x

Proof state:
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
h : ∀ (x : K), IsAlgebraic R x
x : S
⊢ IsAlgebraic R x

Tactic:
obtain ⟨f, hf₁, hf₂⟩ := h (algebraMap S K x)

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

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
⊢ IsAlgebraic R x

Tactic:
letI := FractionRing.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
⊢ IsAlgebraic R x

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
⊢ IsIntegral (FractionRing R) ((algebraMap S K) b)⁻¹

Tactic:
rw [← isAlgebraic_iff_isIntegral]

Result:
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)⁻¹