awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Etale.Descent
Goal:
R S T : Type u_1
x : CommRing R
x_1 : CommRing S
x_2 : CommRing T
x_3 : Algebra R S
x_4 : Algebra R T
h : FaithfullyFlat (algebraMap R S)
h' : Algebra.FormallyUnramified S (S ⊗[R] T)
h₁ : Module.FaithfullyFlat R S
⊢ Algebra.FormallyUnramified S (S ⊗[R] T)

Tactic:
rw [faithfullyFlat_algebraMap_iff] at h

Premises used: RingHom.faithfullyFlat_algebraMap_iff
-- Module: Mathlib.RingTheory.Etale.Descent
Goal:
R S T : Type u_1
x : CommRing R
x_1 : CommRing S
x_2 : CommRing T
x_3 : Algebra R S
x_4 : Algebra R T
h : Module.FaithfullyFlat R S
h' : Algebra.FormallyUnramified S (S ⊗[R] T)
⊢ Algebra.FormallyUnramified R T

Tactic:
.of_formallyUnramified_tensorProduct_of_faithfullyFlat S

Premises used: Algebra.FormallyUnramified.of_formallyUnramified_tensorProduct_of_faithfullyFlat
-- Module: Mathlib.RingTheory.Etale.Descent
Goal:
R S T : Type u_1
x : CommRing R
x_1 : CommRing S
x_2 : CommRing T
x_3 : Algebra R S
x_4 : Algebra R T
h : Module.FaithfullyFlat R S
h' : Algebra.FormallyUnramified S (S ⊗[R] T)
⊢ Algebra.FormallyUnramified R T

Tactic:
exact .of_formallyUnramified_tensorProduct_of_faithfullyFlat S
-- Module: Mathlib.RingTheory.Etale.Descent
Goal:
⊢ CodescendsAlong.{u_1} (fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ Etale)
    fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ FaithfullyFlat

Tactic:
.mk _ Etale.respectsIso fun R S T _ _ _ _ _ h h' ↦ ?_

Premises used: RingHom.CodescendsAlong.mk, RingHom.Etale.respectsIso
-- Module: Mathlib.RingTheory.Etale.Descent
Goal:
refine :
  ∀ (R S T : Type u_1) (x : CommRing R) (x_1 : CommRing S) (x_2 : CommRing T) (x_3 : Algebra R S) (x_4 : Algebra R T)
    (h : FaithfullyFlat (algebraMap R S)) (h' : Etale (S := S ⊗[R] T) (algebraMap S (S ⊗[R] T))), Etale (algebraMap R T)
⊢ CodescendsAlong.{u_1} (fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ Etale)
    fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ FaithfullyFlat

Tactic:
refine .mk _ Etale.respectsIso fun R S T _ _ _ _ _ h h' ↦ ?_
-- Module: Mathlib.RingTheory.Etale.Descent
Goal:
R S T : Type u_1
x : CommRing R
x_1 : CommRing S
x_2 : CommRing T
x_3 : Algebra R S
x_4 : Algebra R T
h : FaithfullyFlat (algebraMap R S)
h' : Etale (S := S ⊗[R] T) (algebraMap S (S ⊗[R] T))
rw : ∀ (h' : Algebra.Etale S (S ⊗[R] T)), Algebra.Etale R T
⊢ Etale (algebraMap R T)

Tactic:
rw [etale_algebraMap] at h' ⊢

Premises used: RingHom.etale_algebraMap
-- Module: Mathlib.RingTheory.Etale.Descent
Goal:
R S T : Type u_1
x : CommRing R
x_1 : CommRing S
x_2 : CommRing T
x_3 : Algebra R S
x_4 : Algebra R T
h : FaithfullyFlat (algebraMap R S)
h' : Algebra.Etale S (S ⊗[R] T)
⊢ Module.FaithfullyFlat R S

Tactic:
rw [faithfullyFlat_algebraMap_iff] at h

Premises used: RingHom.faithfullyFlat_algebraMap_iff
-- Module: Mathlib.RingTheory.Etale.Descent
Goal:
R S T : Type u_1
x : CommRing R
x_1 : CommRing S
x_2 : CommRing T
x_3 : Algebra R S
x_4 : Algebra R T
h : FaithfullyFlat (algebraMap R S)
h' : Algebra.Etale S (S ⊗[R] T)
h₁ : Module.FaithfullyFlat R S
⊢ Algebra.Etale S (S ⊗[R] T)

Tactic:
rw [faithfullyFlat_algebraMap_iff] at h

Premises used: RingHom.faithfullyFlat_algebraMap_iff
-- Module: Mathlib.RingTheory.Etale.Descent
Goal:
R S T : Type u_1
x : CommRing R
x_1 : CommRing S
x_2 : CommRing T
x_3 : Algebra R S
x_4 : Algebra R T
h : Module.FaithfullyFlat R S
h' : Algebra.Etale S (S ⊗[R] T)
⊢ Algebra.Etale R T

Tactic:
.of_etale_tensorProduct_of_faithfullyFlat S

Premises used: Algebra.Etale.of_etale_tensorProduct_of_faithfullyFlat
-- Module: Mathlib.RingTheory.Etale.Descent
Goal:
R S T : Type u_1
x : CommRing R
x_1 : CommRing S
x_2 : CommRing T
x_3 : Algebra R S
x_4 : Algebra R T
h : Module.FaithfullyFlat R S
h' : Algebra.Etale S (S ⊗[R] T)
⊢ Algebra.Etale R T

Tactic:
exact .of_etale_tensorProduct_of_faithfullyFlat S
-- Module: Mathlib.RingTheory.Etale.Field
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsSeparable K L
inst_4 : EssFiniteType K L
⊢ FormallyUnramified K L

Tactic:
have := FormallyUnramified.of_isSeparable K L
-- Module: Mathlib.RingTheory.Etale.Field
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsSeparable K L
inst_4 : EssFiniteType K L
this : FormallyUnramified K L
⊢ Module.Finite K L

Tactic:
have := FormallyUnramified.finite_of_free (R := K) (S := L)
-- Module: Mathlib.RingTheory.Etale.Field
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsSeparable K L
inst_4 : EssFiniteType K L
this_1 : FormallyUnramified K L
this : Module.Finite K L
⊢ FormallyEtale K L

Tactic:
FormallyEtale.iff_comp_bijective.mpr fun B _ _ I h ↦ ?_

Premises used: Iff.mpr, Algebra.FormallyEtale.iff_comp_bijective
-- Module: Mathlib.RingTheory.Etale.Field
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsSeparable K L
inst_4 : EssFiniteType K L
this_1 : FormallyUnramified K L
this : Module.Finite K L
refine :
  ∀ (B : Type (max u_1 u_2)) (x : CommRing B) (x_1 : Algebra K B) (I : Ideal B) (h : HPow.hPow (β := ℕ) I 2 = ⊥),
    Function.Bijective (α := L →ₐ[K] B) (β := L →ₐ[K] B ⧸ I) (AlgHom.comp (Ideal.Quotient.mkₐ K I))
⊢ FormallyEtale K L

Tactic:
refine FormallyEtale.iff_comp_bijective.mpr fun B _ _ I h ↦ ?_

Premises used: Iff.mpr, Algebra.FormallyEtale.iff_comp_bijective
-- Module: Mathlib.RingTheory.Etale.Field
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsSeparable K L
inst_4 : EssFiniteType K L
this_1 : FormallyUnramified K L
this : Module.Finite K L
B : Type (max u_1 u_2)
x : CommRing B
x_1 : Algebra K B
I : Ideal B
h : HPow.hPow (β := ℕ) I 2 = ⊥
⊢ Function.Bijective (α := L →ₐ[K] B) (β := L →ₐ[K] B ⧸ I) (AlgHom.comp (Ideal.Quotient.mkₐ K I))

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

Premises used: Algebra.FormallyUnramified.of_isSeparable, And.intro, Iff.mp, Function.Bijective, Algebra.FormallyUnramified.iff_comp_injective_of_small
-- Module: Mathlib.RingTheory.Etale.Field
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsSeparable K L
inst_4 : EssFiniteType K L
this_1 : FormallyUnramified K L
this : Module.Finite K L
B : Type (max u_1 u_2)
x : CommRing B
x_1 : Algebra K B
I : Ideal B
h : HPow.hPow (β := ℕ) I 2 = ⊥
refine : Function.Surjective (α := L →ₐ[K] B) (β := L →ₐ[K] B ⧸ I) (AlgHom.comp (Ideal.Quotient.mkₐ K I))
⊢ Function.Bijective (α := L →ₐ[K] B) (β := L →ₐ[K] B ⧸ I) (AlgHom.comp (Ideal.Quotient.mkₐ K I))

Tactic:
refine ⟨FormallyUnramified.iff_comp_injective_of_small.mp
    (FormallyUnramified.of_isSeparable K L) I h, ?_⟩
-- Module: Mathlib.RingTheory.Etale.Field
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsSeparable K L
inst_4 : EssFiniteType K L
this_1 : FormallyUnramified K L
this : Module.Finite K L
B : Type (max u_1 u_2)
x : CommRing B
x_1 : Algebra K B
I : Ideal B
h : HPow.hPow (β := ℕ) I 2 = ⊥
f : L →ₐ[K] B ⧸ I
pb : PowerBasis K L := Field.powerBasisOfFiniteOfSeparable K L
obtain :
  ∀ (x_2 : B)
    (hx : Eq (α := B ⧸ I) ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) x_2 : B ⧸ I) ((f : (a : L) → B ⧸ I) pb.gen : B ⧸ I)),
    ∃ (a : L →ₐ[K] B), AlgHom.comp (Ideal.Quotient.mkₐ K I) a = f
⊢ ∃ (a : L →ₐ[K] B), AlgHom.comp (Ideal.Quotient.mkₐ K I) a = f

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

Premises used: PowerBasis.gen, Ideal.Quotient.mk_surjective, DFunLike.coe
-- Module: Mathlib.RingTheory.Etale.Field
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsSeparable K L
inst_4 : EssFiniteType K L
this_1 : FormallyUnramified K L
this : Module.Finite K L
B : Type (max u_1 u_2)
x_1 : CommRing B
x_2 : Algebra K B
I : Ideal B
h : HPow.hPow (β := ℕ) I 2 = ⊥
f : L →ₐ[K] B ⧸ I
pb : PowerBasis K L := Field.powerBasisOfFiniteOfSeparable K L
x : B
hx : Eq (α := B ⧸ I) ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) x : B ⧸ I) ((f : (a : L) → B ⧸ I) pb.gen : B ⧸ I)
⊢ ∀ (x : B),
    Eq (α := B ⧸ I) ((IsScalarTower.toAlgHom K B (B ⧸ I) : (a : B) → B ⧸ I) x : B ⧸ I)
      ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) x : B ⧸ I)

Tactic:
have helper : ∀ x, IsScalarTower.toAlgHom K B (B ⧸ I) x = Ideal.Quotient.mk I x := fun _ ↦ rfl
-- Module: Mathlib.RingTheory.Etale.Field
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsSeparable K L
inst_4 : EssFiniteType K L
this_1 : FormallyUnramified K L
this : Module.Finite K L
B : Type (max u_1 u_2)
x_1 : CommRing B
x_2 : Algebra K B
I : Ideal B
h : HPow.hPow (β := ℕ) I 2 = ⊥
f : L →ₐ[K] B ⧸ I
pb : PowerBasis K L := Field.powerBasisOfFiniteOfSeparable K L
x : B
hx : Eq (α := B ⧸ I) ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) x : B ⧸ I) ((f : (a : L) → B ⧸ I) pb.gen : B ⧸ I)
helper :
  ∀ (x : B),
    Eq (α := B ⧸ I) ((IsScalarTower.toAlgHom K B (B ⧸ I) : (a : B) → B ⧸ I) x : B ⧸ I)
      ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) x : B ⧸ I)
rw :
  Eq (α := B ⧸ I)
    ((IsScalarTower.toAlgHom K B (B ⧸ I) : (a : B) → B ⧸ I) ((aeval x : (a : K[X]) → B) (minpoly K pb.gen)) : B ⧸ I)
    (0 : B ⧸ I)
rw₁ :
  Eq (α := B ⧸ I)
    (((aeval ((IsScalarTower.toAlgHom K B (B ⧸ I) : (a : B) → B ⧸ I) x) : K[X] →ₐ[K] B ⧸ I) : (a : K[X]) → B ⧸ I)
        (minpoly K pb.gen) :
      B ⧸ I)
    (0 : B ⧸ I)
rw₂ :
  Eq (α := B ⧸ I)
    (((aeval ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) x) : K[X] →ₐ[K] B ⧸ I) : (a : K[X]) → B ⧸ I) (minpoly K pb.gen) :
      B ⧸ I)
    (0 : B ⧸ I)
rw₃ :
  Eq (α := B ⧸ I)
    (((aeval ((f : (a : L) → B ⧸ I) pb.gen) : K[X] →ₐ[K] B ⧸ I) : (a : K[X]) → B ⧸ I) (minpoly K pb.gen) : B ⧸ I)
    (0 : B ⧸ I)
rw₄ : Eq (α := B ⧸ I) ((f : (a : L) → B ⧸ I) ((aeval pb.gen : (a : K[X]) → L) (minpoly K pb.gen)) : B ⧸ I) (0 : B ⧸ I)
rw₅ : Eq (α := B ⧸ I) ((f : (a : L) → B ⧸ I) 0) 0
rw₆ rw₇ : Eq (α := B ⧸ I) 0 0
⊢ Eq (α := B ⧸ I) ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) ((aeval x : (a : K[X]) → B) (minpoly K pb.gen)) : B ⧸ I)
    (0 : B ⧸ I)

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

Premises used: map_zero, minpoly.aeval, Polynomial.aeval_algHom_apply
-- Module: Mathlib.RingTheory.Etale.Field
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsSeparable K L
inst_4 : EssFiniteType K L
this_1 : FormallyUnramified K L
this : Module.Finite K L
B : Type (max u_1 u_2)
x_1 : CommRing B
x_2 : Algebra K B
I : Ideal B
h : HPow.hPow (β := ℕ) I 2 = ⊥
f : L →ₐ[K] B ⧸ I
pb : PowerBasis K L := Field.powerBasisOfFiniteOfSeparable K L
x : B
hx : Eq (α := B ⧸ I) ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) x : B ⧸ I) ((f : (a : L) → B ⧸ I) pb.gen : B ⧸ I)
helper :
  ∀ (x : B),
    Eq (α := B ⧸ I) ((IsScalarTower.toAlgHom K B (B ⧸ I) : (a : B) → B ⧸ I) x : B ⧸ I)
      ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) x : B ⧸ I)
⊢ Eq (α := B ⧸ I) ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) ((aeval x : (a : K[X]) → B) (minpoly K pb.gen)) : B ⧸ I)
    (0 : B ⧸ I)

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]
-- Module: Mathlib.RingTheory.Etale.Field
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsSeparable K L
inst_4 : EssFiniteType K L
this_1 : FormallyUnramified K L
this : Module.Finite K L
B : Type (max u_1 u_2)
x_1 : CommRing B
x_2 : Algebra K B
I : Ideal B
h : HPow.hPow (β := ℕ) I 2 = ⊥
f : L →ₐ[K] B ⧸ I
pb : PowerBasis K L := Field.powerBasisOfFiniteOfSeparable K L
x : B
hx : Eq (α := B ⧸ I) ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) x : B ⧸ I) ((f : (a : L) → B ⧸ I) pb.gen : B ⧸ I)
helper :
  ∀ (x : B),
    Eq (α := B ⧸ I) ((IsScalarTower.toAlgHom K B (B ⧸ I) : (a : B) → B ⧸ I) x : B ⧸ I)
      ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) x : B ⧸ I)
hx' :
  Eq (α := B ⧸ I) ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) ((aeval x : (a : K[X]) → B) (minpoly K pb.gen)) : B ⧸ I)
    (0 : B ⧸ I)
⊢ IsUnit (M := B ⧸ I)
    ((f : (a : L) → B ⧸ I)
        ((aeval pb.gen : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K pb.gen) : K[X])) :
      B ⧸ I)

Tactic:
have := (isUnit_iff_ne_zero.mpr ((Algebra.IsSeparable.isSeparable K
      pb.gen).aeval_derivative_ne_zero (minpoly.aeval K _))).map f
-- Module: Mathlib.RingTheory.Etale.Field
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsSeparable K L
inst_4 : EssFiniteType K L
this_1 : FormallyUnramified K L
this_2 : Module.Finite K L
B : Type (max u_1 u_2)
x_1 : CommRing B
x_2 : Algebra K B
I : Ideal B
h : HPow.hPow (β := ℕ) I 2 = ⊥
f : L →ₐ[K] B ⧸ I
pb : PowerBasis K L := Field.powerBasisOfFiniteOfSeparable K L
x : B
hx : Eq (α := B ⧸ I) ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) x : B ⧸ I) ((f : (a : L) → B ⧸ I) pb.gen : B ⧸ I)
helper :
  ∀ (x : B),
    Eq (α := B ⧸ I) ((IsScalarTower.toAlgHom K B (B ⧸ I) : (a : B) → B ⧸ I) x : B ⧸ I)
      ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) x : B ⧸ I)
hx' :
  Eq (α := B ⧸ I) ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) ((aeval x : (a : K[X]) → B) (minpoly K pb.gen)) : B ⧸ I)
    (0 : B ⧸ I)
this :
  IsUnit (M := B ⧸ I)
    ((f : (a : L) → B ⧸ I)
        ((aeval pb.gen : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K pb.gen) : K[X])) :
      B ⧸ I)
⊢ IsUnit (M := B ⧸ I)
    ((Ideal.Quotient.mk I : (a : B) → B ⧸ I)
        ((aeval x : (a : K[X]) → B) ((derivative : (a : K[X]) → K[X]) (minpoly K pb.gen) : K[X])) :
      B ⧸ I)

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

Premises used: Polynomial.aeval_algHom_apply
-- Module: Mathlib.RingTheory.Etale.Field
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsSeparable K L
inst_4 : EssFiniteType K L
this_1 : FormallyUnramified K L
this_2 : Module.Finite K L
B : Type (max u_1 u_2)
x_1 : CommRing B
x_2 : Algebra K B
I : Ideal B
h : HPow.hPow (β := ℕ) I 2 = ⊥
f : L →ₐ[K] B ⧸ I
pb : PowerBasis K L := Field.powerBasisOfFiniteOfSeparable K L
x : B
hx : Eq (α := B ⧸ I) ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) x : B ⧸ I) ((f : (a : L) → B ⧸ I) pb.gen : B ⧸ I)
helper :
  ∀ (x : B),
    Eq (α := B ⧸ I) ((IsScalarTower.toAlgHom K B (B ⧸ I) : (a : B) → B ⧸ I) x : B ⧸ I)
      ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) x : B ⧸ I)
hx' :
  Eq (α := B ⧸ I) ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) ((aeval x : (a : K[X]) → B) (minpoly K pb.gen)) : B ⧸ I)
    (0 : B ⧸ I)
this :
  IsUnit (M := B ⧸ I)
    ((Ideal.Quotient.mk I : (a : B) → B ⧸ I)
        ((aeval x : (a : K[X]) → B) ((derivative : (a : K[X]) → K[X]) (minpoly K pb.gen) : K[X])) :
      B ⧸ I)
obtain :
  ∀ (u : B) (hu : (Ideal.Quotient.mk I : (a : B) → B ⧸ I) u = -(↑this.unit⁻¹ : B ⧸ I)),
    ∃ (u : B),
      HMul.hMul (α := B) ((aeval x : (a : K[X]) → B) ((derivative : (a : K[X]) → K[X]) (minpoly K pb.gen) : K[X]) : B)
            u +
          1 ∈
        I
⊢ ∃ (u : B),
    HMul.hMul (α := B) ((aeval x : (a : K[X]) → B) ((derivative : (a : K[X]) → K[X]) (minpoly K pb.gen) : K[X]) : B) u +
        1 ∈
      I

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

Premises used: Units.val, Ideal.Quotient.mk_surjective, Inv.inv, IsUnit.unit, Neg.neg
-- Module: Mathlib.RingTheory.Etale.Field
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsSeparable K L
inst_4 : EssFiniteType K L
this_1 : FormallyUnramified K L
this_2 : Module.Finite K L
B : Type (max u_1 u_2)
x_1 : CommRing B
x_2 : Algebra K B
I : Ideal B
h : HPow.hPow (β := ℕ) I 2 = ⊥
f : L →ₐ[K] B ⧸ I
pb : PowerBasis K L := Field.powerBasisOfFiniteOfSeparable K L
x : B
hx : Eq (α := B ⧸ I) ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) x : B ⧸ I) ((f : (a : L) → B ⧸ I) pb.gen : B ⧸ I)
helper :
  ∀ (x : B),
    Eq (α := B ⧸ I) ((IsScalarTower.toAlgHom K B (B ⧸ I) : (a : B) → B ⧸ I) x : B ⧸ I)
      ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) x : B ⧸ I)
hx' :
  Eq (α := B ⧸ I) ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) ((aeval x : (a : K[X]) → B) (minpoly K pb.gen)) : B ⧸ I)
    (0 : B ⧸ I)
this :
  IsUnit (M := B ⧸ I)
    ((Ideal.Quotient.mk I : (a : B) → B ⧸ I)
        ((aeval x : (a : K[X]) → B) ((derivative : (a : K[X]) → K[X]) (minpoly K pb.gen) : K[X])) :
      B ⧸ I)
u : B
hu : (Ideal.Quotient.mk I : (a : B) → B ⧸ I) u = -(↑this.unit⁻¹ : B ⧸ I)
h₁ :
  HMul.hMul (α := B) ((aeval x : (a : K[X]) → B) ((derivative : (a : K[X]) → K[X]) (minpoly K pb.gen) : K[X]) : B) u +
      1 ∈
    I
⊢ ∃ (u : B),
    HMul.hMul (α := B) ((aeval x : (a : K[X]) → B) ((derivative : (a : K[X]) → K[X]) (minpoly K pb.gen) : K[X]) : B) u +
        1 ∈
      I

Tactic:
use u
-- Module: Mathlib.RingTheory.Etale.Field
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsSeparable K L
inst_4 : EssFiniteType K L
this_1 : FormallyUnramified K L
this : Module.Finite K L
B : Type (max u_1 u_2)
x_1 : CommRing B
x_2 : Algebra K B
I : Ideal B
h : HPow.hPow (β := ℕ) I 2 = ⊥
f : L →ₐ[K] B ⧸ I
pb : PowerBasis K L := Field.powerBasisOfFiniteOfSeparable K L
x : B
hx : Eq (α := B ⧸ I) ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) x : B ⧸ I) ((f : (a : L) → B ⧸ I) pb.gen : B ⧸ I)
helper :
  ∀ (x : B),
    Eq (α := B ⧸ I) ((IsScalarTower.toAlgHom K B (B ⧸ I) : (a : B) → B ⧸ I) x : B ⧸ I)
      ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) x : B ⧸ I)
hx' :
  Eq (α := B ⧸ I) ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) ((aeval x : (a : K[X]) → B) (minpoly K pb.gen)) : B ⧸ I)
    (0 : B ⧸ I)
obtain :
  ∀ (u : B)
    (hu :
      HMul.hMul (α := B) ((aeval x : (a : K[X]) → B) ((derivative : (a : K[X]) → K[X]) (minpoly K pb.gen) : K[X]) : B)
            u +
          1 ∈
        I),
    ∃ (a : L →ₐ[K] B), AlgHom.comp (Ideal.Quotient.mkₐ K I) a = f
⊢ ∃ (a : L →ₐ[K] B), AlgHom.comp (Ideal.Quotient.mkₐ K I) 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]

Premises used: Polynomial.derivative, PowerBasis.gen, minpoly, Polynomial.aeval, DFunLike.coe
-- Module: Mathlib.RingTheory.Etale.Field
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsSeparable K L
inst_4 : EssFiniteType K L
this_1 : FormallyUnramified K L
this : Module.Finite K L
B : Type (max u_1 u_2)
x_1 : CommRing B
x_2 : Algebra K B
I : Ideal B
h : HPow.hPow (β := ℕ) I 2 = ⊥
f : L →ₐ[K] B ⧸ I
pb : PowerBasis K L := Field.powerBasisOfFiniteOfSeparable K L
x : B
hx : Eq (α := B ⧸ I) ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) x : B ⧸ I) ((f : (a : L) → B ⧸ I) pb.gen : B ⧸ I)
helper :
  ∀ (x : B),
    Eq (α := B ⧸ I) ((IsScalarTower.toAlgHom K B (B ⧸ I) : (a : B) → B ⧸ I) x : B ⧸ I)
      ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) x : B ⧸ I)
hx' :
  Eq (α := B ⧸ I) ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) ((aeval x : (a : K[X]) → B) (minpoly K pb.gen)) : B ⧸ I)
    (0 : B ⧸ I)
u : B
hu :
  HMul.hMul (α := B) ((aeval x : (a : K[X]) → B) ((derivative : (a : K[X]) → K[X]) (minpoly K pb.gen) : K[X]) : B) u +
      1 ∈
    I
h₁ :
  AlgHom.comp (Ideal.Quotient.mkₐ K I)
      ((Equiv.symm pb.liftEquiv : (a : { y : B // (aeval y : (a : K[X]) → B) (minpoly K pb.gen) = 0 }) → L →ₐ[K] B)
        (Subtype.mk (p := fun (y : B) ↦ Eq (α := B) ((aeval y : (a : K[X]) → B) (minpoly K pb.gen) : B) (0 : B))
          (x + HMul.hMul (β := B) u ((aeval x : (a : K[X]) → B) (minpoly K pb.gen) : B)) ⋯)) =
    f
w :
  Eq (α := B)
    ((aeval (x + HMul.hMul (β := B) u ((aeval x : (a : K[X]) → B) (minpoly K pb.gen) : B)) : (a : K[X]) → B)
        (minpoly K pb.gen) :
      B)
    (0 : B)
⊢ ∃ (a : L →ₐ[K] B), AlgHom.comp (Ideal.Quotient.mkₐ K I) a = f

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

Premises used: HMul.hMul, PowerBasis.gen, minpoly, Subtype.mk, HAdd.hAdd, PowerBasis.liftEquiv, Polynomial.aeval, Equiv.symm, DFunLike.coe
-- Module: Mathlib.RingTheory.Etale.Field
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsSeparable K L
inst_4 : EssFiniteType K L
this_1 : FormallyUnramified K L
this : Module.Finite K L
B : Type (max u_1 u_2)
x_1 : CommRing B
x_2 : Algebra K B
I : Ideal B
h : HPow.hPow (β := ℕ) I 2 = ⊥
f : L →ₐ[K] B ⧸ I
pb : PowerBasis K L := Field.powerBasisOfFiniteOfSeparable K L
x : B
hx : Eq (α := B ⧸ I) ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) x : B ⧸ I) ((f : (a : L) → B ⧸ I) pb.gen : B ⧸ I)
helper :
  ∀ (x : B),
    Eq (α := B ⧸ I) ((IsScalarTower.toAlgHom K B (B ⧸ I) : (a : B) → B ⧸ I) x : B ⧸ I)
      ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) x : B ⧸ I)
hx' :
  Eq (α := B ⧸ I) ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) ((aeval x : (a : K[X]) → B) (minpoly K pb.gen)) : B ⧸ I)
    (0 : B ⧸ I)
u : B
hu :
  HMul.hMul (α := B) ((aeval x : (a : K[X]) → B) ((derivative : (a : K[X]) → K[X]) (minpoly K pb.gen) : K[X]) : B) u +
      1 ∈
    I
h₁ :
  Eq (α := B ⧸ I)
    ((AlgHom.comp (Ideal.Quotient.mkₐ K I)
            ((Equiv.symm pb.liftEquiv :
                (a : { y : B // (aeval y : (a : K[X]) → B) (minpoly K pb.gen) = 0 }) → L →ₐ[K] B)
              (Subtype.mk (p := fun (y : B) ↦ Eq (α := B) ((aeval y : (a : K[X]) → B) (minpoly K pb.gen) : B) (0 : B))
                (x + HMul.hMul (β := B) u ((aeval x : (a : K[X]) → B) (minpoly K pb.gen) : B)) ⋯)) :
          (a : L) → B ⧸ I)
        pb.gen :
      B ⧸ I)
    ((f : (a : L) → B ⧸ I) pb.gen : B ⧸ I)
⊢ AlgHom.comp (Ideal.Quotient.mkₐ K I)
      ((Equiv.symm pb.liftEquiv : (a : { y : B // (aeval y : (a : K[X]) → B) (minpoly K pb.gen) = 0 }) → L →ₐ[K] B)
        (Subtype.mk (p := fun (y : B) ↦ Eq (α := B) ((aeval y : (a : K[X]) → B) (minpoly K pb.gen) : B) (0 : B))
          (x + HMul.hMul (β := B) u ((aeval x : (a : K[X]) → B) (minpoly K pb.gen) : B)) ⋯)) =
    f

Tactic:
apply pb.algHom_ext

Premises used: PowerBasis.algHom_ext
-- Module: Mathlib.RingTheory.Etale.Field
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsSeparable K L
inst_4 : EssFiniteType K L
this_1 : FormallyUnramified K L
this : Module.Finite K L
B : Type (max u_1 u_2)
x_1 : CommRing B
x_2 : Algebra K B
I : Ideal B
h : HPow.hPow (β := ℕ) I 2 = ⊥
f : L →ₐ[K] B ⧸ I
pb : PowerBasis K L := Field.powerBasisOfFiniteOfSeparable K L
x : B
hx : Eq (α := B ⧸ I) ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) x : B ⧸ I) ((f : (a : L) → B ⧸ I) pb.gen : B ⧸ I)
helper :
  ∀ (x : B),
    Eq (α := B ⧸ I) ((IsScalarTower.toAlgHom K B (B ⧸ I) : (a : B) → B ⧸ I) x : B ⧸ I)
      ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) x : B ⧸ I)
hx' :
  Eq (α := B ⧸ I) ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) ((aeval x : (a : K[X]) → B) (minpoly K pb.gen)) : B ⧸ I)
    (0 : B ⧸ I)
u : B
hu :
  HMul.hMul (α := B) ((aeval x : (a : K[X]) → B) ((derivative : (a : K[X]) → K[X]) (minpoly K pb.gen) : K[X]) : B) u +
      1 ∈
    I
⊢ Eq (α := B ⧸ I)
    ((AlgHom.comp (Ideal.Quotient.mkₐ K I)
            ((Equiv.symm pb.liftEquiv :
                (a : { y : B // (aeval y : (a : K[X]) → B) (minpoly K pb.gen) = 0 }) → L →ₐ[K] B)
              (Subtype.mk (p := fun (y : B) ↦ Eq (α := B) ((aeval y : (a : K[X]) → B) (minpoly K pb.gen) : B) (0 : B))
                (x + HMul.hMul (β := B) u ((aeval x : (a : K[X]) → B) (minpoly K pb.gen) : B)) ⋯)) :
          (a : L) → B ⧸ I)
        pb.gen :
      B ⧸ I)
    ((f : (a : L) → B ⧸ I) pb.gen : B ⧸ I)

Tactic:
simp [hx, hx']