-- Mathlib/RingTheory/Unramified/Field.lean
theorem isSeparable : Algebra.IsSeparable K L

Proof state:
K : Type u_1
L : Type u_3
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FormallyUnramified K L
inst✝ : EssFiniteType K L
this✝¹ : Module.Finite K L
this✝ : FormallyUnramified (↥(separableClosure K L)) L
this : EssFiniteType (↥(separableClosure K L)) L
⊢ separableClosure K L = ⊤

Tactic:
ext

Result:
case h
K : Type u_1
L : Type u_3
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FormallyUnramified K L
inst✝ : EssFiniteType K L
this✝¹ : Module.Finite K L
this✝ : FormallyUnramified (↥(separableClosure K L)) L
this : EssFiniteType (↥(separableClosure K L)) L
x✝ : L
⊢ x✝ ∈ separableClosure K L ↔ x✝ ∈ ⊤

Proof state:
case h
K : Type u_1
L : Type u_3
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FormallyUnramified K L
inst✝ : EssFiniteType K L
this✝¹ : Module.Finite K L
this✝ : FormallyUnramified (↥(separableClosure K L)) L
this : EssFiniteType (↥(separableClosure K L)) L
x✝ : L
⊢ x✝ ∈ separableClosure K L ↔ x✝ ∈ ⊤

Tactic:
rw [← range_eq_top_of_isPurelyInseparable (separableClosure K L) L]

Result:
case h
K : Type u_1
L : Type u_3
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FormallyUnramified K L
inst✝ : EssFiniteType K L
this✝¹ : Module.Finite K L
this✝ : FormallyUnramified (↥(separableClosure K L)) L
this : EssFiniteType (↥(separableClosure K L)) L
x✝ : L
⊢ x✝ ∈ separableClosure K L ↔ x✝ ∈ (algebraMap (↥(separableClosure K L)) L).range

Proof state:
K : Type u_1
L : Type u_3
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FormallyUnramified K L
inst✝ : EssFiniteType K L
this✝ : Module.Finite K L
this : FormallyUnramified (↥(separableClosure K L)) L
⊢ separableClosure K L = ⊤

Tactic:
have := EssFiniteType.of_comp K (separableClosure K L) L

Result:
K : Type u_1
L : Type u_3
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FormallyUnramified K L
inst✝ : EssFiniteType K L
this✝¹ : Module.Finite K L
this✝ : FormallyUnramified (↥(separableClosure K L)) L
this : EssFiniteType (↥(separableClosure K L)) L
⊢ separableClosure K L = ⊤

Proof state:
case h
K : Type u_1
L : Type u_3
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FormallyUnramified K L
inst✝ : EssFiniteType K L
this✝¹ : Module.Finite K L
this✝ : FormallyUnramified (↥(separableClosure K L)) L
this : EssFiniteType (↥(separableClosure K L)) L
x✝ : L
⊢ x✝ ∈ separableClosure K L ↔ x✝ ∈ (algebraMap (↥(separableClosure K L)) L).range

Tactic:
simp

Result:
no goals

Proof state:
K : Type u_1
L : Type u_3
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FormallyUnramified K L
inst✝ : EssFiniteType K L
⊢ Algebra.IsSeparable K L

Tactic:
have := finite_of_free (R := K) (S := L)

Result:
K : Type u_1
L : Type u_3
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FormallyUnramified K L
inst✝ : EssFiniteType K L
this : Module.Finite K L
⊢ Algebra.IsSeparable K L

Proof state:
K : Type u_1
L : Type u_3
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FormallyUnramified K L
inst✝ : EssFiniteType K L
this : Module.Finite K L
⊢ separableClosure K L = ⊤

Tactic:
have := of_comp K (separableClosure K L) L

Result:
K : Type u_1
L : Type u_3
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FormallyUnramified K L
inst✝ : EssFiniteType K L
this✝ : Module.Finite K L
this : FormallyUnramified (↥(separableClosure K L)) L
⊢ separableClosure K L = ⊤

Proof state:
K : Type u_1
L : Type u_3
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FormallyUnramified K L
inst✝ : EssFiniteType K L
this : Module.Finite K L
⊢ Algebra.IsSeparable K L

Tactic:
rw [← separableClosure.eq_top_iff]

Result:
K : Type u_1
L : Type u_3
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FormallyUnramified K L
inst✝ : EssFiniteType K L
this : Module.Finite K L
⊢ separableClosure K L = ⊤