-- Mathlib/RingTheory/Etale/Field.lean
theorem of_isSeparable_aux [Algebra.IsSeparable K L] [EssFiniteType K L] :
    FormallyEtale K L

Proof state:
case comp_bijective.intro
K L : Type u
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : Algebra.IsSeparable K L
inst✝² : EssFiniteType K L
this✝ : FormallyUnramified K L
this : Module.Finite K L
B : Type u
inst✝¹ : CommRing B
inst✝ : Algebra K B
I : Ideal B
h : I ^ 2 = ⊥
f : L →ₐ[K] B ⧸ I
pb : PowerBasis K L := Field.powerBasisOfFiniteOfSeparable K L
x : B
hx : (Ideal.Quotient.mk I) x = f pb.gen
helper : ∀ (x : B), (IsScalarTower.toAlgHom K B (B ⧸ I)) x = (Ideal.Quotient.mk I) x
⊢ ∃ a, (Ideal.Quotient.mkₐ K I).comp a = f

Tactic:
have hx' : Ideal.Quotient.mk I (aeval x (minpoly K pb.gen)) = 0 := by
  rw [← helper, ← aeval_algHom_apply, helper, hx, aeval_algHom_apply, minpoly.aeval, map_zero]

Result:
case comp_bijective.intro
K L : Type u
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : Algebra.IsSeparable K L
inst✝² : EssFiniteType K L
this✝ : FormallyUnramified K L
this : Module.Finite K L
B : Type u
inst✝¹ : CommRing B
inst✝ : Algebra K B
I : Ideal B
h : I ^ 2 = ⊥
f : L →ₐ[K] B ⧸ I
pb : PowerBasis K L := Field.powerBasisOfFiniteOfSeparable K L
x : B
hx : (Ideal.Quotient.mk I) x = f pb.gen
helper : ∀ (x : B), (IsScalarTower.toAlgHom K B (B ⧸ I)) x = (Ideal.Quotient.mk I) x
hx' : (Ideal.Quotient.mk I) ((aeval x) (minpoly K pb.gen)) = 0
⊢ ∃ a, (Ideal.Quotient.mkₐ K I).comp a = f

Proof state:
case comp_bijective
K L : Type u
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : Algebra.IsSeparable K L
inst✝² : EssFiniteType K L
this✝ : FormallyUnramified K L
this : Module.Finite K L
B : Type u
inst✝¹ : CommRing B
inst✝ : Algebra K B
I : Ideal B
h : I ^ 2 = ⊥
⊢ Function.Bijective (Ideal.Quotient.mkₐ K I).comp

Tactic:
refine ⟨FormallyUnramified.iff_comp_injective.mp (FormallyUnramified.of_isSeparable K L) I h, ?_⟩

Result:
case comp_bijective
K L : Type u
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : Algebra.IsSeparable K L
inst✝² : EssFiniteType K L
this✝ : FormallyUnramified K L
this : Module.Finite K L
B : Type u
inst✝¹ : CommRing B
inst✝ : Algebra K B
I : Ideal B
h : I ^ 2 = ⊥
⊢ Function.Surjective (Ideal.Quotient.mkₐ K I).comp

Proof state:
K L : Type u
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : Algebra.IsSeparable K L
inst✝² : EssFiniteType K L
this✝¹ : FormallyUnramified K L
this✝ : Module.Finite K L
B : Type u
inst✝¹ : CommRing B
inst✝ : Algebra K B
I : Ideal B
h : I ^ 2 = ⊥
f : L →ₐ[K] B ⧸ I
pb : PowerBasis K L := Field.powerBasisOfFiniteOfSeparable K L
x : B
hx : (Ideal.Quotient.mk I) x = f pb.gen
helper : ∀ (x : B), (IsScalarTower.toAlgHom K B (B ⧸ I)) x = (Ideal.Quotient.mk I) x
hx' : (Ideal.Quotient.mk I) ((aeval x) (minpoly K pb.gen)) = 0
this : IsUnit (f ((aeval pb.gen) (derivative (minpoly K pb.gen))))
⊢ ∃ u, (aeval x) (derivative (minpoly K pb.gen)) * u + 1 ∈ I

Tactic:
rw [← aeval_algHom_apply, ← hx, ← helper, aeval_algHom_apply, helper] at this

Result:
K L : Type u
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : Algebra.IsSeparable K L
inst✝² : EssFiniteType K L
this✝¹ : FormallyUnramified K L
this✝ : Module.Finite K L
B : Type u
inst✝¹ : CommRing B
inst✝ : Algebra K B
I : Ideal B
h : I ^ 2 = ⊥
f : L →ₐ[K] B ⧸ I
pb : PowerBasis K L := Field.powerBasisOfFiniteOfSeparable K L
x : B
hx : (Ideal.Quotient.mk I) x = f pb.gen
helper : ∀ (x : B), (IsScalarTower.toAlgHom K B (B ⧸ I)) x = (Ideal.Quotient.mk I) x
hx' : (Ideal.Quotient.mk I) ((aeval x) (minpoly K pb.gen)) = 0
this : IsUnit ((Ideal.Quotient.mk I) ((aeval x) (derivative (minpoly K pb.gen))))
⊢ ∃ u, (aeval x) (derivative (minpoly K pb.gen)) * u + 1 ∈ I

Proof state:
case comp_bijective.intro.intro
K L : Type u
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : Algebra.IsSeparable K L
inst✝² : EssFiniteType K L
this✝ : FormallyUnramified K L
this : Module.Finite K L
B : Type u
inst✝¹ : CommRing B
inst✝ : Algebra K B
I : Ideal B
h : I ^ 2 = ⊥
f : L →ₐ[K] B ⧸ I
pb : PowerBasis K L := Field.powerBasisOfFiniteOfSeparable K L
x : B
hx : (Ideal.Quotient.mk I) x = f pb.gen
helper : ∀ (x : B), (IsScalarTower.toAlgHom K B (B ⧸ I)) x = (Ideal.Quotient.mk I) x
hx' : (Ideal.Quotient.mk I) ((aeval x) (minpoly K pb.gen)) = 0
u : B
hu : (aeval x) (derivative (minpoly K pb.gen)) * u + 1 ∈ I
⊢ ∃ a, (Ideal.Quotient.mkₐ K I).comp a = f

Tactic:
use pb.liftEquiv.symm ⟨x + u * aeval x (minpoly K pb.gen), ?_⟩

Result:
case h
K L : Type u
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : Algebra.IsSeparable K L
inst✝² : EssFiniteType K L
this✝ : FormallyUnramified K L
this : Module.Finite K L
B : Type u
inst✝¹ : CommRing B
inst✝ : Algebra K B
I : Ideal B
h : I ^ 2 = ⊥
f : L →ₐ[K] B ⧸ I
pb : PowerBasis K L := Field.powerBasisOfFiniteOfSeparable K L
x : B
hx : (Ideal.Quotient.mk I) x = f pb.gen
helper : ∀ (x : B), (IsScalarTower.toAlgHom K B (B ⧸ I)) x = (Ideal.Quotient.mk I) x
hx' : (Ideal.Quotient.mk I) ((aeval x) (minpoly K pb.gen)) = 0
u : B
hu : (aeval x) (derivative (minpoly K pb.gen)) * u + 1 ∈ I
⊢ (Ideal.Quotient.mkₐ K I).comp (pb.liftEquiv.symm ⟨x + u * (aeval x) (minpoly K pb.gen), ?w⟩) = f

case w
K L : Type u
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : Algebra.IsSeparable K L
inst✝² : EssFiniteType K L
this✝ : FormallyUnramified K L
this : Module.Finite K L
B : Type u
inst✝¹ : CommRing B
inst✝ : Algebra K B
I : Ideal B
h : I ^ 2 = ⊥
f : L →ₐ[K] B ⧸ I
pb : PowerBasis K L := Field.powerBasisOfFiniteOfSeparable K L
x : B
hx : (Ideal.Quotient.mk I) x = f pb.gen
helper : ∀ (x : B), (IsScalarTower.toAlgHom K B (B ⧸ I)) x = (Ideal.Quotient.mk I) x
hx' : (Ideal.Quotient.mk I) ((aeval x) (minpoly K pb.gen)) = 0
u : B
hu : (aeval x) (derivative (minpoly K pb.gen)) * u + 1 ∈ I
⊢ (aeval (x + u * (aeval x) (minpoly K pb.gen))) (minpoly K pb.gen) = 0

Proof state:
case h
K L : Type u
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : Algebra.IsSeparable K L
inst✝² : EssFiniteType K L
this✝ : FormallyUnramified K L
this : Module.Finite K L
B : Type u
inst✝¹ : CommRing B
inst✝ : Algebra K B
I : Ideal B
h : I ^ 2 = ⊥
f : L →ₐ[K] B ⧸ I
pb : PowerBasis K L := Field.powerBasisOfFiniteOfSeparable K L
x : B
hx : (Ideal.Quotient.mk I) x = f pb.gen
helper : ∀ (x : B), (IsScalarTower.toAlgHom K B (B ⧸ I)) x = (Ideal.Quotient.mk I) x
hx' : (Ideal.Quotient.mk I) ((aeval x) (minpoly K pb.gen)) = 0
u : B
hu : (aeval x) (derivative (minpoly K pb.gen)) * u + 1 ∈ I
⊢ (Ideal.Quotient.mkₐ K I).comp (pb.liftEquiv.symm ⟨x + u * (aeval x) (minpoly K pb.gen), ?w⟩) = f

Tactic:
apply pb.algHom_ext

Result:
case h.h
K L : Type u
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : Algebra.IsSeparable K L
inst✝² : EssFiniteType K L
this✝ : FormallyUnramified K L
this : Module.Finite K L
B : Type u
inst✝¹ : CommRing B
inst✝ : Algebra K B
I : Ideal B
h : I ^ 2 = ⊥
f : L →ₐ[K] B ⧸ I
pb : PowerBasis K L := Field.powerBasisOfFiniteOfSeparable K L
x : B
hx : (Ideal.Quotient.mk I) x = f pb.gen
helper : ∀ (x : B), (IsScalarTower.toAlgHom K B (B ⧸ I)) x = (Ideal.Quotient.mk I) x
hx' : (Ideal.Quotient.mk I) ((aeval x) (minpoly K pb.gen)) = 0
u : B
hu : (aeval x) (derivative (minpoly K pb.gen)) * u + 1 ∈ I
⊢ ((Ideal.Quotient.mkₐ K I).comp (pb.liftEquiv.symm ⟨x + u * (aeval x) (minpoly K pb.gen), ?w⟩)) pb.gen = f pb.gen

Proof state:
K L : Type u
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Algebra.IsSeparable K L
inst✝ : EssFiniteType K L
this : FormallyUnramified K L
⊢ FormallyEtale K L

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

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