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

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
⊢ ∃ u, (aeval x) (derivative (minpoly K pb.gen)) * u + 1 ∈ I

Tactic:
have := (isUnit_iff_ne_zero.mpr ((Algebra.IsSeparable.isSeparable K
  pb.gen).aeval_derivative_ne_zero (minpoly.aeval K _))).map f

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 (f ((aeval pb.gen) (derivative (minpoly K pb.gen))))
⊢ ∃ u, (aeval x) (derivative (minpoly K pb.gen)) * u + 1 ∈ I

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 ((Ideal.Quotient.mk I) ((aeval x) (derivative (minpoly K pb.gen))))
⊢ ∃ u, (aeval x) (derivative (minpoly K pb.gen)) * u + 1 ∈ I

Tactic:
obtain ⟨u, hu⟩ := Ideal.Quotient.mk_surjective (-this.unit⁻¹ : B ⧸ I)

Result:
case 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
this : IsUnit ((Ideal.Quotient.mk I) ((aeval x) (derivative (minpoly K pb.gen))))
u : B
hu : (Ideal.Quotient.mk I) u = -↑this.unit⁻¹
⊢ ∃ u, (aeval x) (derivative (minpoly K pb.gen)) * u + 1 ∈ I

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
⊢ (Ideal.Quotient.mk I) ((aeval x) (minpoly K pb.gen)) = 0

Tactic:
rw [← helper, ← aeval_algHom_apply, helper, hx, aeval_algHom_apply, minpoly.aeval, map_zero]

Result:
no goals

Proof state:
case w.hy
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
⊢ (u * (aeval x) (minpoly K pb.gen)) ^ 2 ∈ I ^ 2

Tactic:
apply Ideal.pow_mem_pow

Result:
case w.hy.hx
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
⊢ u * (aeval x) (minpoly K pb.gen) ∈ I

Proof state:
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

Tactic:
rw [← eval_map_algebraMap, Polynomial.eval_add_of_sq_eq_zero, derivative_map,
  ← one_mul (eval x _), eval_map_algebraMap, eval_map_algebraMap, ← mul_assoc, ← add_mul,
  ← Ideal.mem_bot, ← h, pow_two, add_comm]

Result:
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) (derivative (minpoly K pb.gen)) * u + 1) * (aeval x) (minpoly K pb.gen) ∈ I * I

case w.hy
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
⊢ (u * (aeval x) (minpoly K pb.gen)) ^ 2 = 0