-- Mathlib/RingTheory/Norm/Basic.lean
theorem isIntegral_norm [Algebra R L] [Algebra R K] [IsScalarTower R K L] [Algebra.IsSeparable K L]
    [FiniteDimensional K L] {x : L} (hx : IsIntegral R x) : IsIntegral R (norm K x)

Proof state:
R : Type u_1
inst✝⁸ : CommRing R
K : Type u_4
L : Type u_5
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra R L
inst✝³ : Algebra R K
inst✝² : IsScalarTower R K L
inst✝¹ : Algebra.IsSeparable K L
inst✝ : FiniteDimensional K L
x : L
hx : IsIntegral R x
hx' : IsIntegral K x
⊢ IsIntegral R ((norm K) x)

Tactic:
rw [← isIntegral_algebraMap_iff (algebraMap K (AlgebraicClosure L)).injective, norm_eq_prod_roots]

Result:
R : Type u_1
inst✝⁸ : CommRing R
K : Type u_4
L : Type u_5
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra R L
inst✝³ : Algebra R K
inst✝² : IsScalarTower R K L
inst✝¹ : Algebra.IsSeparable K L
inst✝ : FiniteDimensional K L
x : L
hx : IsIntegral R x
hx' : IsIntegral K x
⊢ IsIntegral R (((minpoly K x).aroots (AlgebraicClosure L)).prod ^ finrank (↥K⟮x⟯) L)

case hF
R : Type u_1
inst✝⁸ : CommRing R
K : Type u_4
L : Type u_5
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra R L
inst✝³ : Algebra R K
inst✝² : IsScalarTower R K L
inst✝¹ : Algebra.IsSeparable K L
inst✝ : FiniteDimensional K L
x : L
hx : IsIntegral R x
hx' : IsIntegral K x
⊢ Splits (algebraMap K (AlgebraicClosure L)) (minpoly K x)

Proof state:
R : Type u_1
inst✝⁸ : CommRing R
K : Type u_4
L : Type u_5
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra R L
inst✝³ : Algebra R K
inst✝² : IsScalarTower R K L
inst✝¹ : Algebra.IsSeparable K L
inst✝ : FiniteDimensional K L
x : L
hx : IsIntegral R x
hx' : IsIntegral K x
⊢ IsIntegral R (((minpoly K x).aroots (AlgebraicClosure L)).prod ^ finrank (↥K⟮x⟯) L)

Tactic:
refine (IsIntegral.multiset_prod fun y hy => ?_).pow _

Result:
R : Type u_1
inst✝⁸ : CommRing R
K : Type u_4
L : Type u_5
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra R L
inst✝³ : Algebra R K
inst✝² : IsScalarTower R K L
inst✝¹ : Algebra.IsSeparable K L
inst✝ : FiniteDimensional K L
x : L
hx : IsIntegral R x
hx' : IsIntegral K x
y : AlgebraicClosure L
hy : y ∈ (minpoly K x).aroots (AlgebraicClosure L)
⊢ IsIntegral R y

Proof state:
case right
R : Type u_1
inst✝⁸ : CommRing R
K : Type u_4
L : Type u_5
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra R L
inst✝³ : Algebra R K
inst✝² : IsScalarTower R K L
inst✝¹ : Algebra.IsSeparable K L
inst✝ : FiniteDimensional K L
x : L
hx : IsIntegral R x
hx' : IsIntegral K x
y : AlgebraicClosure L
hy : (aeval y) (minpoly K x) = 0
⊢ (aeval y) (minpoly R x) = 0

Tactic:
exact minpoly.aeval_of_isScalarTower R x y hy

Result:
no goals

Proof state:
case right
R : Type u_1
inst✝⁸ : CommRing R
K : Type u_4
L : Type u_5
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra R L
inst✝³ : Algebra R K
inst✝² : IsScalarTower R K L
inst✝¹ : Algebra.IsSeparable K L
inst✝ : FiniteDimensional K L
x : L
hx : IsIntegral R x
hx' : IsIntegral K x
y : AlgebraicClosure L
hy : eval₂ (algebraMap K (AlgebraicClosure L)) y (minpoly K x) = 0
⊢ eval₂ (algebraMap R (AlgebraicClosure L)) y (minpoly R x) = 0

Tactic:
rw [← aeval_def] at hy ⊢

Result:
case right
R : Type u_1
inst✝⁸ : CommRing R
K : Type u_4
L : Type u_5
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra R L
inst✝³ : Algebra R K
inst✝² : IsScalarTower R K L
inst✝¹ : Algebra.IsSeparable K L
inst✝ : FiniteDimensional K L
x : L
hx : IsIntegral R x
hx' : IsIntegral K x
y : AlgebraicClosure L
hy : (aeval y) (minpoly K x) = 0
⊢ (aeval y) (minpoly R x) = 0

Proof state:
R : Type u_1
inst✝⁸ : CommRing R
K : Type u_4
L : Type u_5
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra R L
inst✝³ : Algebra R K
inst✝² : IsScalarTower R K L
inst✝¹ : Algebra.IsSeparable K L
inst✝ : FiniteDimensional K L
x : L
hx : IsIntegral R x
hx' : IsIntegral K x
y : AlgebraicClosure L
hy : eval₂ (algebraMap K (AlgebraicClosure L)) y (minpoly K x) = 0
⊢ IsIntegral R y

Tactic:
use minpoly R x, minpoly.monic hx

Result:
case right
R : Type u_1
inst✝⁸ : CommRing R
K : Type u_4
L : Type u_5
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra R L
inst✝³ : Algebra R K
inst✝² : IsScalarTower R K L
inst✝¹ : Algebra.IsSeparable K L
inst✝ : FiniteDimensional K L
x : L
hx : IsIntegral R x
hx' : IsIntegral K x
y : AlgebraicClosure L
hy : eval₂ (algebraMap K (AlgebraicClosure L)) y (minpoly K x) = 0
⊢ eval₂ (algebraMap R (AlgebraicClosure L)) y (minpoly R x) = 0

Proof state:
R : Type u_1
inst✝⁸ : CommRing R
K : Type u_4
L : Type u_5
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra R L
inst✝³ : Algebra R K
inst✝² : IsScalarTower R K L
inst✝¹ : Algebra.IsSeparable K L
inst✝ : FiniteDimensional K L
x : L
hx : IsIntegral R x
⊢ IsIntegral R ((norm K) x)

Tactic:
have hx' : IsIntegral K x := hx.tower_top

Result:
R : Type u_1
inst✝⁸ : CommRing R
K : Type u_4
L : Type u_5
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra R L
inst✝³ : Algebra R K
inst✝² : IsScalarTower R K L
inst✝¹ : Algebra.IsSeparable K L
inst✝ : FiniteDimensional K L
x : L
hx : IsIntegral R x
hx' : IsIntegral K x
⊢ IsIntegral R ((norm K) x)

Proof state:
case hF
R : Type u_1
inst✝⁸ : CommRing R
K : Type u_4
L : Type u_5
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra R L
inst✝³ : Algebra R K
inst✝² : IsScalarTower R K L
inst✝¹ : Algebra.IsSeparable K L
inst✝ : FiniteDimensional K L
x : L
hx : IsIntegral R x
hx' : IsIntegral K x
⊢ Splits (algebraMap K (AlgebraicClosure L)) (minpoly K x)

Tactic:
apply IsAlgClosed.splits_codomain

Result:
no goals

Proof state:
R : Type u_1
inst✝⁸ : CommRing R
K : Type u_4
L : Type u_5
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra R L
inst✝³ : Algebra R K
inst✝² : IsScalarTower R K L
inst✝¹ : Algebra.IsSeparable K L
inst✝ : FiniteDimensional K L
x : L
hx : IsIntegral R x
hx' : IsIntegral K x
y : AlgebraicClosure L
hy : y ∈ (minpoly K x).aroots (AlgebraicClosure L)
⊢ IsIntegral R y

Tactic:
rw [mem_roots_map (minpoly.ne_zero hx')] at hy

Result:
R : Type u_1
inst✝⁸ : CommRing R
K : Type u_4
L : Type u_5
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra R L
inst✝³ : Algebra R K
inst✝² : IsScalarTower R K L
inst✝¹ : Algebra.IsSeparable K L
inst✝ : FiniteDimensional K L
x : L
hx : IsIntegral R x
hx' : IsIntegral K x
y : AlgebraicClosure L
hy : eval₂ (algebraMap K (AlgebraicClosure L)) y (minpoly K x) = 0
⊢ IsIntegral R y