-- 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
hx' : (Ideal.Quotient.mk I) ((aeval x) (minpoly K pb.gen)) = 0
⊢ ∃ a, (Ideal.Quotient.mkₐ K I).comp a = f

Tactic:
obtain ⟨u, hu⟩ : ∃ u, (aeval x) (derivative (minpoly K pb.gen)) * u + 1 ∈ I := by
  have := (isUnit_iff_ne_zero.mpr ((Algebra.IsSeparable.isSeparable K
    pb.gen).aeval_derivative_ne_zero (minpoly.aeval K _))).map f
  rw [← aeval_algHom_apply, ← hx, ← helper, aeval_algHom_apply, helper] at this
  obtain ⟨u, hu⟩ := Ideal.Quotient.mk_surjective (-this.unit⁻¹ : B ⧸ I)
  use u
  rw [← Ideal.Quotient.eq_zero_iff_mem, map_add, map_mul, map_one, hu, mul_neg,
    IsUnit.mul_val_inv, neg_add_cancel]

Result:
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

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

Tactic:
exact Ideal.mul_mem_mul hu (Ideal.Quotient.eq_zero_iff_mem.mp hx')

Result:
no goals

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
⊢ ∃ a, (Ideal.Quotient.mkₐ K I).comp a = f

Tactic:
have helper : ∀ x, IsScalarTower.toAlgHom K B (B ⧸ I) x = Ideal.Quotient.mk I x := fun _ ↦ rfl

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
⊢ ∃ 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 = ⊥
f : L →ₐ[K] B ⧸ I
pb : PowerBasis K L := Field.powerBasisOfFiniteOfSeparable K L
⊢ ∃ a, (Ideal.Quotient.mkₐ K I).comp a = f

Tactic:
obtain ⟨x, hx⟩ := Ideal.Quotient.mk_surjective (f pb.gen)

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
⊢ ∃ a, (Ideal.Quotient.mkₐ K I).comp a = f

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

Tactic:
rw [← Ideal.Quotient.eq_zero_iff_mem, map_add, map_mul, map_one, hu, mul_neg,
  IsUnit.mul_val_inv, neg_add_cancel]

Result:
no goals

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.Surjective (Ideal.Quotient.mkₐ K I).comp

Tactic:
intro f

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 = ⊥
f : L →ₐ[K] B ⧸ I
⊢ ∃ a, (Ideal.Quotient.mkₐ K I).comp a = f

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 = 0

Tactic:
rw [← Ideal.mem_bot, ← h]

Result:
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