awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Descent (goal)
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))
⊢ Etale (algebraMap R T)
have rw : ∀ (h' : Algebra.Etale S (S ⊗[R] T)), Algebra.Etale R T
Tactic: rw [etale_algebraMap] at h' ⊢
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Descent (hypothesis)
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)
⊢ Algebra.Etale R T
have h₁ : Module.FaithfullyFlat R S
Tactic: rw [faithfullyFlat_algebraMap_iff] at h
Cleared hypotheses: h, h'
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Field (hypothesis)
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
⊢ FormallyEtale K L
have this : FormallyUnramified K L
Tactic: have := FormallyUnramified.of_isSeparable K L
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Field (hypothesis)
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
⊢ FormallyEtale K L
have this₁ : Module.Finite K L
Tactic: have := FormallyUnramified.finite_of_free (R := K) (S := L)
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Field (goal)
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
have 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))
Tactic: refine FormallyEtale.iff_comp_bijective.mpr fun B _ _ I h ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Field (goal)
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))
have refine : Function.Surjective (α := 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, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Field (goal)
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
⊢ ∃ (a : L →ₐ[K] B), AlgHom.comp (Ideal.Quotient.mkₐ K I) a = f
have 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
Tactic: obtain ⟨x, hx⟩ := Ideal.Quotient.mk_surjective (f pb.gen)
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Field (hypothesis)
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)
⊢ ∃ (a : L →ₐ[K] B), AlgHom.comp (Ideal.Quotient.mkₐ K I) a = f
have 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)
Tactic: have helper : ∀ x, IsScalarTower.toAlgHom K B (B ⧸ I) x = Ideal.Quotient.mk I x := fun _ ↦ rfl
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Field (goal)
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)
have 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)
Tactic: rw [← helper, ← aeval_algHom_apply, helper, hx, aeval_algHom_apply, minpoly.aeval, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Field (goal)
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)
⊢ 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)
have 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)
Tactic: rw [← helper, ← aeval_algHom_apply, helper, hx, aeval_algHom_apply, minpoly.aeval, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Field (goal)
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)
⊢ 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)
have 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)
Tactic: rw [← helper, ← aeval_algHom_apply, helper, hx, aeval_algHom_apply, minpoly.aeval, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Field (goal)
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)
⊢ 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)
have 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)
Tactic: rw [← helper, ← aeval_algHom_apply, helper, hx, aeval_algHom_apply, minpoly.aeval, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Field (goal)
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)
⊢ 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)
have 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)
Tactic: rw [← helper, ← aeval_algHom_apply, helper, hx, aeval_algHom_apply, minpoly.aeval, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Field (goal)
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)
⊢ 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)
have rw₅ : Eq (α := B ⧸ I) ((f : (a : L) → B ⧸ I) 0) 0
Tactic: rw [← helper, ← aeval_algHom_apply, helper, hx, aeval_algHom_apply, minpoly.aeval, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Field (goal)
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
⊢ 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)
have rw₆ : Eq (α := B ⧸ I) 0 0
Tactic: rw [← helper, ← aeval_algHom_apply, helper, hx, aeval_algHom_apply, minpoly.aeval, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Field (hypothesis)
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)
⊢ ∃ (a : L →ₐ[K] B), AlgHom.comp (Ideal.Quotient.mkₐ K I) a = f
have 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)
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]
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Field (hypothesis)
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),
    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
have 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)
Tactic: have := (isUnit_iff_ne_zero.mpr ((Algebra.IsSeparable.isSeparable K
      pb.gen).aeval_derivative_ne_zero (minpoly.aeval K _))).map f
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Field (hypothesis)
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)
⊢ ∃ (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
have 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)
Tactic: rw [← aeval_algHom_apply, ← hx, ← helper, aeval_algHom_apply, helper] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Field (goal)
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),
    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
have 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
Tactic: obtain ⟨u, hu⟩ := Ideal.Quotient.mk_surjective (-this.unit⁻¹ : B ⧸ I)
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Field (goal)
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)
⊢ ∃ (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
have 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
Tactic: use u
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Field (goal)
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)
⊢ 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
have h₁ : Eq (α := B ⧸ I)
  ((Ideal.Quotient.mk I : (a : B) → B ⧸ I)
      (HMul.hMul (α := B) ((aeval x : (a : K[X]) → B) ((derivative : (a : K[X]) → K[X]) (minpoly K pb.gen) : K[X]) : B)
          u +
        1) :
    B ⧸ I)
  (0 : B ⧸ 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]