awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
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)
⊢ 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₂ : HAdd.hAdd (α := B ⧸ I) (β := 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) :
      B ⧸ I)
    ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) 1 : B ⧸ I) =
  0
Tactic: rw [← Ideal.Quotient.eq_zero_iff_mem, map_add, map_mul, map_one, hu, mul_neg,
      IsUnit.mul_val_inv, neg_add_cancel]
-- 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)
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)
h₂ :
  HAdd.hAdd (α := B ⧸ I) (β := 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) :
        B ⧸ I)
      ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) 1 : B ⧸ I) =
    0
⊢ 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 ⧸ I) (β := 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)
      ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) u : B ⧸ I) +
    (Ideal.Quotient.mk I : (a : B) → B ⧸ I) 1 =
  0
Tactic: rw [← Ideal.Quotient.eq_zero_iff_mem, map_add, map_mul, map_one, hu, mul_neg,
      IsUnit.mul_val_inv, neg_add_cancel]
-- 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)
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)
h₂ :
  HAdd.hAdd (α := B ⧸ I) (β := 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) :
        B ⧸ I)
      ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) 1 : B ⧸ I) =
    0
h₃ :
  HMul.hMul (α := B ⧸ I) (β := 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)
        ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) u : B ⧸ I) +
      (Ideal.Quotient.mk I : (a : B) → B ⧸ I) 1 =
    0
⊢ 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 ⧸ I) (β := 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)
      ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) u : B ⧸ I) +
    1 =
  0
Tactic: rw [← Ideal.Quotient.eq_zero_iff_mem, map_add, map_mul, map_one, hu, mul_neg,
      IsUnit.mul_val_inv, neg_add_cancel]
-- 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)
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)
h₂ :
  HAdd.hAdd (α := B ⧸ I) (β := 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) :
        B ⧸ I)
      ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) 1 : B ⧸ I) =
    0
h₃ :
  HMul.hMul (α := B ⧸ I) (β := 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)
        ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) u : B ⧸ I) +
      (Ideal.Quotient.mk I : (a : B) → B ⧸ I) 1 =
    0
h₄ :
  HMul.hMul (α := B ⧸ I) (β := 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)
        ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) u : B ⧸ I) +
      1 =
    0
⊢ 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 ⧸ 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)
      (-(↑this.unit⁻¹ : B ⧸ I)) +
    1 =
  0
Tactic: rw [← Ideal.Quotient.eq_zero_iff_mem, map_add, map_mul, map_one, hu, mul_neg,
      IsUnit.mul_val_inv, neg_add_cancel]
-- 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)
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)
h₂ :
  HAdd.hAdd (α := B ⧸ I) (β := 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) :
        B ⧸ I)
      ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) 1 : B ⧸ I) =
    0
h₃ :
  HMul.hMul (α := B ⧸ I) (β := 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)
        ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) u : B ⧸ I) +
      (Ideal.Quotient.mk I : (a : B) → B ⧸ I) 1 =
    0
h₄ :
  HMul.hMul (α := B ⧸ I) (β := 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)
        ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) u : B ⧸ I) +
      1 =
    0
h₅ :
  HMul.hMul (α := 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)
        (-(↑this.unit⁻¹ : B ⧸ I)) +
      1 =
    0
⊢ 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 ⧸ 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)
        (↑this.unit⁻¹ : B ⧸ I) +
    1 =
  0
Tactic: rw [← Ideal.Quotient.eq_zero_iff_mem, map_add, map_mul, map_one, hu, mul_neg,
      IsUnit.mul_val_inv, neg_add_cancel]
-- 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)
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)
h₂ :
  HAdd.hAdd (α := B ⧸ I) (β := 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) :
        B ⧸ I)
      ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) 1 : B ⧸ I) =
    0
h₃ :
  HMul.hMul (α := B ⧸ I) (β := 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)
        ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) u : B ⧸ I) +
      (Ideal.Quotient.mk I : (a : B) → B ⧸ I) 1 =
    0
h₄ :
  HMul.hMul (α := B ⧸ I) (β := 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)
        ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) u : B ⧸ I) +
      1 =
    0
h₅ :
  HMul.hMul (α := 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)
        (-(↑this.unit⁻¹ : B ⧸ I)) +
      1 =
    0
h₆ :
  -HMul.hMul (α := 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)
          (↑this.unit⁻¹ : B ⧸ I) +
      1 =
    0
⊢ 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₇ : HAdd.hAdd (α := B ⧸ I) (-1) 1 = 0
Tactic: rw [← Ideal.Quotient.eq_zero_iff_mem, map_add, map_mul, map_one, hu, mul_neg,
      IsUnit.mul_val_inv, neg_add_cancel]
-- 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)
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)
h₂ :
  HAdd.hAdd (α := B ⧸ I) (β := 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) :
        B ⧸ I)
      ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) 1 : B ⧸ I) =
    0
h₃ :
  HMul.hMul (α := B ⧸ I) (β := 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)
        ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) u : B ⧸ I) +
      (Ideal.Quotient.mk I : (a : B) → B ⧸ I) 1 =
    0
h₄ :
  HMul.hMul (α := B ⧸ I) (β := 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)
        ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) u : B ⧸ I) +
      1 =
    0
h₅ :
  HMul.hMul (α := 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)
        (-(↑this.unit⁻¹ : B ⧸ I)) +
      1 =
    0
h₆ :
  -HMul.hMul (α := 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)
          (↑this.unit⁻¹ : B ⧸ I) +
      1 =
    0
h₇ : HAdd.hAdd (α := B ⧸ I) (-1) 1 = 0
⊢ 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) 0 0
Tactic: rw [← Ideal.Quotient.eq_zero_iff_mem, map_add, map_mul, map_one, hu, mul_neg,
      IsUnit.mul_val_inv, neg_add_cancel]
-- 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)
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)
⊢ ∃ (a : L →ₐ[K] B), AlgHom.comp (Ideal.Quotient.mkₐ K I) a = f
have 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
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]
-- 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)
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
⊢ ∃ (a : L →ₐ[K] B), AlgHom.comp (Ideal.Quotient.mkₐ K I) a = f
have 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)) sorry)) =
  f
Tactic: use pb.liftEquiv.symm ⟨x + u * aeval x (minpoly K pb.gen), ?_⟩
-- 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)
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
⊢ ∃ (a : L →ₐ[K] B), AlgHom.comp (Ideal.Quotient.mkₐ K I) a = f
have 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)
Tactic: use pb.liftEquiv.symm ⟨x + u * aeval x (minpoly K pb.gen), ?_⟩