-- Mathlib/FieldTheory/SeparableDegree.lean
theorem IsSeparable.of_algebra_isSeparable_of_isSeparable [Algebra E K] [IsScalarTower F E K]
    [Algebra.IsSeparable F E] {x : K} (hsep : IsSeparable E x) : IsSeparable F x

Proof state:
F : Type u
E : Type v
inst✝⁷ : Field F
inst✝⁶ : Field E
inst✝⁵ : Algebra F E
K : Type w
inst✝⁴ : Field K
inst✝³ : Algebra F K
inst✝² : Algebra E K
inst✝¹ : IsScalarTower F E K
inst✝ : Algebra.IsSeparable F E
x : K
f : E[X] := minpoly E x
hf : f = minpoly E x
E' : IntermediateField F E := adjoin F ↑f.coeffs
this✝⁵ : FiniteDimensional F ↥E'
g : (↥E')[X]
h : Polynomial.map (algebraMap (↥E') E) g = f
hx : x ∈ restrictScalars F (↥E')⟮x⟯
hzero : (aeval x) g = 0
halg : IsIntegral (↥E') x
hsep : (minpoly (↥E') x).Separable
this✝⁴ : Algebra.IsSeparable F ↥E'
this✝³ : Algebra.IsSeparable ↥E' ↥(↥E')⟮x⟯
this✝² : FiniteDimensional ↥E' ↥(↥E')⟮x⟯
this✝¹ : FiniteDimensional F ↥(↥E')⟮x⟯
this✝ : Algebra.IsAlgebraic ↥E' ↥(↥E')⟮x⟯
this : Algebra.IsSeparable F ↥(↥E')⟮x⟯
⊢ IsSeparable F x

Tactic:
change Algebra.IsSeparable F (restrictScalars F E'⟮x⟯) at this

Result:
F : Type u
E : Type v
inst✝⁷ : Field F
inst✝⁶ : Field E
inst✝⁵ : Algebra F E
K : Type w
inst✝⁴ : Field K
inst✝³ : Algebra F K
inst✝² : Algebra E K
inst✝¹ : IsScalarTower F E K
inst✝ : Algebra.IsSeparable F E
x : K
f : E[X] := minpoly E x
hf : f = minpoly E x
E' : IntermediateField F E := adjoin F ↑f.coeffs
this✝⁵ : FiniteDimensional F ↥E'
g : (↥E')[X]
h : Polynomial.map (algebraMap (↥E') E) g = f
hx : x ∈ restrictScalars F (↥E')⟮x⟯
hzero : (aeval x) g = 0
halg : IsIntegral (↥E') x
hsep : (minpoly (↥E') x).Separable
this✝⁴ : Algebra.IsSeparable F ↥E'
this✝³ : Algebra.IsSeparable ↥E' ↥(↥E')⟮x⟯
this✝² : FiniteDimensional ↥E' ↥(↥E')⟮x⟯
this✝¹ : FiniteDimensional F ↥(↥E')⟮x⟯
this✝ : Algebra.IsAlgebraic ↥E' ↥(↥E')⟮x⟯
this : Algebra.IsSeparable F ↥(restrictScalars F (↥E')⟮x⟯)
⊢ IsSeparable F x

Proof state:
F : Type u
E : Type v
inst✝⁷ : Field F
inst✝⁶ : Field E
inst✝⁵ : Algebra F E
K : Type w
inst✝⁴ : Field K
inst✝³ : Algebra F K
inst✝² : Algebra E K
inst✝¹ : IsScalarTower F E K
inst✝ : Algebra.IsSeparable F E
x : K
hsep : IsSeparable E x
f : E[X] := minpoly E x
hf : f = minpoly E x
E' : IntermediateField F E := adjoin F ↑f.coeffs
this : FiniteDimensional F ↥E'
g : (↥E')[X]
h : Polynomial.map (algebraMap (↥E') E) g = f
hx : x ∈ restrictScalars F (↥E')⟮x⟯
hzero : (aeval x) g = 0
⊢ IsSeparable F x

Tactic:
have halg : IsIntegral E' x :=
  isIntegral_trans (R := F) (A := E) _ (IsSeparable.isIntegral hsep) |>.tower_top

Result:
F : Type u
E : Type v
inst✝⁷ : Field F
inst✝⁶ : Field E
inst✝⁵ : Algebra F E
K : Type w
inst✝⁴ : Field K
inst✝³ : Algebra F K
inst✝² : Algebra E K
inst✝¹ : IsScalarTower F E K
inst✝ : Algebra.IsSeparable F E
x : K
hsep : IsSeparable E x
f : E[X] := minpoly E x
hf : f = minpoly E x
E' : IntermediateField F E := adjoin F ↑f.coeffs
this : FiniteDimensional F ↥E'
g : (↥E')[X]
h : Polynomial.map (algebraMap (↥E') E) g = f
hx : x ∈ restrictScalars F (↥E')⟮x⟯
hzero : (aeval x) g = 0
halg : IsIntegral (↥E') x
⊢ IsSeparable F x

Proof state:
F : Type u
E : Type v
inst✝⁷ : Field F
inst✝⁶ : Field E
inst✝⁵ : Algebra F E
K : Type w
inst✝⁴ : Field K
inst✝³ : Algebra F K
inst✝² : Algebra E K
inst✝¹ : IsScalarTower F E K
inst✝ : Algebra.IsSeparable F E
x : K
f : E[X] := minpoly E x
hf : f = minpoly E x
E' : IntermediateField F E := adjoin F ↑f.coeffs
this✝⁴ : FiniteDimensional F ↥E'
g : (↥E')[X]
h : Polynomial.map (algebraMap (↥E') E) g = f
hx : x ∈ restrictScalars F (↥E')⟮x⟯
hzero : (aeval x) g = 0
halg : IsIntegral (↥E') x
hsep : (minpoly (↥E') x).Separable
this✝³ : Algebra.IsSeparable F ↥E'
this✝² : Algebra.IsSeparable ↥E' ↥(↥E')⟮x⟯
this✝¹ : FiniteDimensional ↥E' ↥(↥E')⟮x⟯
this✝ : FiniteDimensional F ↥(↥E')⟮x⟯
this : Algebra.IsAlgebraic ↥E' ↥(↥E')⟮x⟯
⊢ IsSeparable F x

Tactic:
have := finSepDegree_mul_finSepDegree_of_isAlgebraic F E' E'⟮x⟯

Result:
F : Type u
E : Type v
inst✝⁷ : Field F
inst✝⁶ : Field E
inst✝⁵ : Algebra F E
K : Type w
inst✝⁴ : Field K
inst✝³ : Algebra F K
inst✝² : Algebra E K
inst✝¹ : IsScalarTower F E K
inst✝ : Algebra.IsSeparable F E
x : K
f : E[X] := minpoly E x
hf : f = minpoly E x
E' : IntermediateField F E := adjoin F ↑f.coeffs
this✝⁵ : FiniteDimensional F ↥E'
g : (↥E')[X]
h : Polynomial.map (algebraMap (↥E') E) g = f
hx : x ∈ restrictScalars F (↥E')⟮x⟯
hzero : (aeval x) g = 0
halg : IsIntegral (↥E') x
hsep : (minpoly (↥E') x).Separable
this✝⁴ : Algebra.IsSeparable F ↥E'
this✝³ : Algebra.IsSeparable ↥E' ↥(↥E')⟮x⟯
this✝² : FiniteDimensional ↥E' ↥(↥E')⟮x⟯
this✝¹ : FiniteDimensional F ↥(↥E')⟮x⟯
this✝ : Algebra.IsAlgebraic ↥E' ↥(↥E')⟮x⟯
this : finSepDegree F ↥E' * finSepDegree ↥E' ↥(↥E')⟮x⟯ = finSepDegree F ↥(↥E')⟮x⟯
⊢ IsSeparable F x

Proof state:
F : Type u
E : Type v
inst✝⁷ : Field F
inst✝⁶ : Field E
inst✝⁵ : Algebra F E
K : Type w
inst✝⁴ : Field K
inst✝³ : Algebra F K
inst✝² : Algebra E K
inst✝¹ : IsScalarTower F E K
inst✝ : Algebra.IsSeparable F E
x : K
f : E[X] := minpoly E x
hf : f = minpoly E x
E' : IntermediateField F E := adjoin F ↑f.coeffs
this✝ : FiniteDimensional F ↥E'
g : (↥E')[X]
h : Polynomial.map (algebraMap (↥E') E) g = f
hx : x ∈ restrictScalars F (↥E')⟮x⟯
hzero : (aeval x) g = 0
halg : IsIntegral (↥E') x
hsep : (minpoly (↥E') x).Separable
this : Algebra.IsSeparable F ↥E'
⊢ IsSeparable F x

Tactic:
haveI := (isSeparable_adjoin_simple_iff_isSeparable _ _).2 hsep

Result:
F : Type u
E : Type v
inst✝⁷ : Field F
inst✝⁶ : Field E
inst✝⁵ : Algebra F E
K : Type w
inst✝⁴ : Field K
inst✝³ : Algebra F K
inst✝² : Algebra E K
inst✝¹ : IsScalarTower F E K
inst✝ : Algebra.IsSeparable F E
x : K
f : E[X] := minpoly E x
hf : f = minpoly E x
E' : IntermediateField F E := adjoin F ↑f.coeffs
this✝¹ : FiniteDimensional F ↥E'
g : (↥E')[X]
h : Polynomial.map (algebraMap (↥E') E) g = f
hx : x ∈ restrictScalars F (↥E')⟮x⟯
hzero : (aeval x) g = 0
halg : IsIntegral (↥E') x
hsep : (minpoly (↥E') x).Separable
this✝ : Algebra.IsSeparable F ↥E'
this : Algebra.IsSeparable ↥E' ↥(↥E')⟮x⟯
⊢ IsSeparable F x

Proof state:
F : Type u
E : Type v
inst✝⁷ : Field F
inst✝⁶ : Field E
inst✝⁵ : Algebra F E
K : Type w
inst✝⁴ : Field K
inst✝³ : Algebra F K
inst✝² : Algebra E K
inst✝¹ : IsScalarTower F E K
inst✝ : Algebra.IsSeparable F E
x : K
f : E[X] := minpoly E x
hf : f = minpoly E x
E' : IntermediateField F E := adjoin F ↑f.coeffs
this✝³ : FiniteDimensional F ↥E'
g : (↥E')[X]
h : Polynomial.map (algebraMap (↥E') E) g = f
hx : x ∈ restrictScalars F (↥E')⟮x⟯
hzero : (aeval x) g = 0
halg : IsIntegral (↥E') x
hsep : (minpoly (↥E') x).Separable
this✝² : Algebra.IsSeparable F ↥E'
this✝¹ : Algebra.IsSeparable ↥E' ↥(↥E')⟮x⟯
this✝ : FiniteDimensional ↥E' ↥(↥E')⟮x⟯
this : FiniteDimensional F ↥(↥E')⟮x⟯
⊢ IsSeparable F x

Tactic:
have : Algebra.IsAlgebraic E' E'⟮x⟯ := Algebra.IsSeparable.isAlgebraic _ _

Result:
F : Type u
E : Type v
inst✝⁷ : Field F
inst✝⁶ : Field E
inst✝⁵ : Algebra F E
K : Type w
inst✝⁴ : Field K
inst✝³ : Algebra F K
inst✝² : Algebra E K
inst✝¹ : IsScalarTower F E K
inst✝ : Algebra.IsSeparable F E
x : K
f : E[X] := minpoly E x
hf : f = minpoly E x
E' : IntermediateField F E := adjoin F ↑f.coeffs
this✝⁴ : FiniteDimensional F ↥E'
g : (↥E')[X]
h : Polynomial.map (algebraMap (↥E') E) g = f
hx : x ∈ restrictScalars F (↥E')⟮x⟯
hzero : (aeval x) g = 0
halg : IsIntegral (↥E') x
hsep : (minpoly (↥E') x).Separable
this✝³ : Algebra.IsSeparable F ↥E'
this✝² : Algebra.IsSeparable ↥E' ↥(↥E')⟮x⟯
this✝¹ : FiniteDimensional ↥E' ↥(↥E')⟮x⟯
this✝ : FiniteDimensional F ↥(↥E')⟮x⟯
this : Algebra.IsAlgebraic ↥E' ↥(↥E')⟮x⟯
⊢ IsSeparable F x