-- 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
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⟯
⊢ IsSeparable F x

Tactic:
have hzero : aeval x g = 0 := by
  simpa only [← hf, ← h, aeval_map_algebraMap] using minpoly.aeval 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
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

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
halg : IsIntegral (↥E') x
⊢ IsSeparable F x

Tactic:
simp only [IsSeparable, ← hf, ← h, separable_map] at 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 : g.Separable
⊢ 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 : g.Separable
⊢ IsSeparable F x

Tactic:
replace hsep := hsep.of_dvd <| minpoly.dvd E' x hzero

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
⊢ 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
⊢ IsSeparable F x

Tactic:
haveI : FiniteDimensional F E' :=
  finiteDimensional_adjoin fun x _ ↦ Algebra.IsSeparable.isIntegral F 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
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'
⊢ 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] := f.toSubring E'.toSubring ⋯
h : Polynomial.map (algebraMap (↥E') E) g = f
⊢ IsSeparable F x

Tactic:
clear_value g

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
⊢ 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
⊢ IsSeparable F x

Tactic:
set f := minpoly E x with hf

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
⊢ 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⟯
⊢ IsSeparable F x

Tactic:
haveI : FiniteDimensional F E'⟮x⟯ := FiniteDimensional.trans 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⟯
⊢ IsSeparable F x