-- Mathlib/FieldTheory/PurelyInseparable/Basic.lean
theorem separableClosure_le_iff [Algebra.IsAlgebraic F E] (L : IntermediateField F E) :
    separableClosure F E ≤ L ↔ IsPurelyInseparable L E

Proof state:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsAlgebraic F E
L : IntermediateField F E
⊢ separableClosure F E ≤ L ↔ IsPurelyInseparable (↥L) E

Tactic:
refine ⟨fun h ↦ ?_, fun _ ↦ separableClosure_le F E L⟩

Result:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsAlgebraic F E
L : IntermediateField F E
h : separableClosure F E ≤ L
⊢ IsPurelyInseparable (↥L) E

Proof state:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsAlgebraic F E
L : IntermediateField F E
h : separableClosure F E ≤ L
this : IsPurelyInseparable (↥(separableClosure F E)) E
⊢ IsPurelyInseparable (↥L) E

Tactic:
letI := (inclusion h).toAlgebra

Result:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsAlgebraic F E
L : IntermediateField F E
h : separableClosure F E ≤ L
this✝ : IsPurelyInseparable (↥(separableClosure F E)) E
this : Algebra ↥(separableClosure F E) ↥L := (inclusion h).toAlgebra
⊢ IsPurelyInseparable (↥L) E

Proof state:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsAlgebraic F E
L : IntermediateField F E
h : separableClosure F E ≤ L
this✝¹ : IsPurelyInseparable (↥(separableClosure F E)) E
this✝ : Algebra ↥(separableClosure F E) ↥L := (inclusion h).toAlgebra
this : SMul ↥(separableClosure F E) ↥L := Algebra.toSMul
⊢ IsPurelyInseparable (↥L) E

Tactic:
haveI : IsScalarTower (separableClosure F E) L E := IsScalarTower.of_algebraMap_eq (congrFun rfl)

Result:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsAlgebraic F E
L : IntermediateField F E
h : separableClosure F E ≤ L
this✝² : IsPurelyInseparable (↥(separableClosure F E)) E
this✝¹ : Algebra ↥(separableClosure F E) ↥L := (inclusion h).toAlgebra
this✝ : SMul ↥(separableClosure F E) ↥L := Algebra.toSMul
this : IsScalarTower (↥(separableClosure F E)) (↥L) E
⊢ IsPurelyInseparable (↥L) E

Proof state:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsAlgebraic F E
L : IntermediateField F E
h : separableClosure F E ≤ L
this✝² : IsPurelyInseparable (↥(separableClosure F E)) E
this✝¹ : Algebra ↥(separableClosure F E) ↥L := (inclusion h).toAlgebra
this✝ : SMul ↥(separableClosure F E) ↥L := Algebra.toSMul
this : IsScalarTower (↥(separableClosure F E)) (↥L) E
⊢ IsPurelyInseparable (↥L) E

Tactic:
exact IsPurelyInseparable.tower_top (separableClosure F E) L E

Result:
no goals

Proof state:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsAlgebraic F E
L : IntermediateField F E
h : separableClosure F E ≤ L
⊢ IsPurelyInseparable (↥L) E

Tactic:
have := separableClosure.isPurelyInseparable F E

Result:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsAlgebraic F E
L : IntermediateField F E
h : separableClosure F E ≤ L
this : IsPurelyInseparable (↥(separableClosure F E)) E
⊢ IsPurelyInseparable (↥L) E

Proof state:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsAlgebraic F E
L : IntermediateField F E
h : separableClosure F E ≤ L
this✝ : IsPurelyInseparable (↥(separableClosure F E)) E
this : Algebra ↥(separableClosure F E) ↥L := (inclusion h).toAlgebra
⊢ IsPurelyInseparable (↥L) E

Tactic:
letI : SMul (separableClosure F E) L := Algebra.toSMul

Result:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsAlgebraic F E
L : IntermediateField F E
h : separableClosure F E ≤ L
this✝¹ : IsPurelyInseparable (↥(separableClosure F E)) E
this✝ : Algebra ↥(separableClosure F E) ↥L := (inclusion h).toAlgebra
this : SMul ↥(separableClosure F E) ↥L := Algebra.toSMul
⊢ IsPurelyInseparable (↥L) E