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 : 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
⊢ 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
have 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)) sorry)) :
        (a : L) → B ⧸ I)
      pb.gen :
    B ⧸ I)
  ((f : (a : L) → B ⧸ I) pb.gen : B ⧸ I)
Tactic: apply pb.algHom_ext
-- 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
⊢ 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)
have w : HMul.hMul (β := 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)
    ((aeval x : (a : K[X]) → B) (minpoly K pb.gen) : B) ∈
  I * I
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]
-- 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
w :
  HMul.hMul (β := 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)
      ((aeval x : (a : K[X]) → B) (minpoly K pb.gen) : B) ∈
    I * I
⊢ 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)
have w₁ : HPow.hPow (β := ℕ) (HMul.hMul (β := B) u ((aeval x : (a : K[X]) → B) (minpoly K pb.gen) : B)) 2 = 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]
-- 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
⊢ HPow.hPow (β := ℕ) (HMul.hMul (β := B) u ((aeval x : (a : K[X]) → B) (minpoly K pb.gen) : B)) 2 = 0
have w : HPow.hPow (β := ℕ) (HMul.hMul (β := B) u ((aeval x : (a : K[X]) → B) (minpoly K pb.gen) : B)) 2 ∈ HPow.hPow (β := ℕ) I 2
Tactic: rw [← Ideal.mem_bot, ← 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_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
⊢ HPow.hPow (β := ℕ) (HMul.hMul (β := B) u ((aeval x : (a : K[X]) → B) (minpoly K pb.gen) : B)) 2 ∈
    HPow.hPow (β := ℕ) I 2
have w : HMul.hMul (β := B) u ((aeval x : (a : K[X]) → B) (minpoly K pb.gen) : B) ∈ I
Tactic: apply Ideal.pow_mem_pow
-- 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
⊢ HMul.hMul (β := B) u ((aeval x : (a : K[X]) → B) (minpoly K pb.gen) : B) ∈ I
have w : Eq (α := B ⧸ I)
  ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) (HMul.hMul (β := B) u ((aeval x : (a : K[X]) → B) (minpoly K pb.gen) : B)) :
    B ⧸ I)
  (0 : B ⧸ I)
Tactic: rw [← Ideal.Quotient.eq_zero_iff_mem, map_mul, hx', mul_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)
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
w :
  Eq (α := B ⧸ I)
    ((Ideal.Quotient.mk I : (a : B) → B ⧸ I)
        (HMul.hMul (β := B) u ((aeval x : (a : K[X]) → B) (minpoly K pb.gen) : B)) :
      B ⧸ I)
    (0 : B ⧸ I)
⊢ HMul.hMul (β := B) u ((aeval x : (a : K[X]) → B) (minpoly K pb.gen) : B) ∈ I
have w₁ : HMul.hMul (α := B ⧸ I) (β := B ⧸ I) ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) u : B ⧸ I)
    ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) ((aeval x : (a : K[X]) → B) (minpoly K pb.gen)) : B ⧸ I) =
  0
Tactic: rw [← Ideal.Quotient.eq_zero_iff_mem, map_mul, hx', mul_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)
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
w :
  Eq (α := B ⧸ I)
    ((Ideal.Quotient.mk I : (a : B) → B ⧸ I)
        (HMul.hMul (β := B) u ((aeval x : (a : K[X]) → B) (minpoly K pb.gen) : B)) :
      B ⧸ I)
    (0 : B ⧸ I)
w₁ :
  HMul.hMul (α := B ⧸ I) (β := B ⧸ I) ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) u : B ⧸ I)
      ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) ((aeval x : (a : K[X]) → B) (minpoly K pb.gen)) : B ⧸ I) =
    0
⊢ HMul.hMul (β := B) u ((aeval x : (a : K[X]) → B) (minpoly K pb.gen) : B) ∈ I
have w₂ : HMul.hMul (α := B ⧸ I) (β := B ⧸ I) ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) u : B ⧸ I) (0 : B ⧸ I) = 0
Tactic: rw [← Ideal.Quotient.eq_zero_iff_mem, map_mul, hx', mul_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)
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
w :
  Eq (α := B ⧸ I)
    ((Ideal.Quotient.mk I : (a : B) → B ⧸ I)
        (HMul.hMul (β := B) u ((aeval x : (a : K[X]) → B) (minpoly K pb.gen) : B)) :
      B ⧸ I)
    (0 : B ⧸ I)
w₁ :
  HMul.hMul (α := B ⧸ I) (β := B ⧸ I) ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) u : B ⧸ I)
      ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) ((aeval x : (a : K[X]) → B) (minpoly K pb.gen)) : B ⧸ I) =
    0
w₂ : HMul.hMul (α := B ⧸ I) (β := B ⧸ I) ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) u : B ⧸ I) (0 : B ⧸ I) = 0
⊢ HMul.hMul (β := B) u ((aeval x : (a : K[X]) → B) (minpoly K pb.gen) : B) ∈ I
have w₃ : Eq (α := B ⧸ I) 0 0
Tactic: rw [← Ideal.Quotient.eq_zero_iff_mem, map_mul, hx', mul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Field (hypothesis)
Goal:
K : Type u_1
A : Type u
inst : Field K
inst_1 : CommRing A
inst_2 : Algebra K A
inst_3 : EssFiniteType K A
inst_4 : FormallyUnramified K A
⊢ FormallyEtale K A
have this : IsReduced A
Tactic: have := FormallyUnramified.isReduced_of_field K A
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Field (hypothesis)
Goal:
K : Type u_1
A : Type u
inst : Field K
inst_1 : CommRing A
inst_2 : Algebra K A
inst_3 : EssFiniteType K A
inst_4 : FormallyUnramified K A
this : IsReduced A
⊢ FormallyEtale K A
have this₁ : IsArtinianRing A
Tactic: have : IsArtinianRing A := .of_finite K A
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Field (goal)
Goal:
K : Type u_1
A : Type u
inst : Field K
inst_1 : CommRing A
inst_2 : Algebra K A
inst_3 : EssFiniteType K A
inst_4 : FormallyUnramified K A
this_1 : IsReduced A
this : IsArtinianRing A
I : MaximalSpectrum A
⊢ FormallyEtale.{u_1, u} K (A ⧸ I.asIdeal)
have rw : FormallyUnramified.{u, u_1} K (A ⧸ I.asIdeal)
Tactic: rw [FormallyEtale.iff_isSeparable, ← FormallyUnramified.iff_isSeparable]
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Field (hypothesis)
Goal:
K : Type u_1
A : Type u
inst : Field K
inst_1 : CommRing A
inst_2 : Algebra K A
inst_3 : EssFiniteType K A
inst_4 : FormallyUnramified K A
this_1 : IsReduced A
this : IsArtinianRing A
⊢ FormallyEtale K A
have this₁ : ∀ (I : MaximalSpectrum A), FormallyEtale.{u_1, u} K (A ⧸ I.asIdeal)
Tactic: have (I : MaximalSpectrum A) : FormallyEtale K (A ⧸ I.asIdeal) := by
    rw [FormallyEtale.iff_isSeparable, ← FormallyUnramified.iff_isSeparable]
    infer_instance
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Field (goal)
Goal:
K : Type u_1
A : Type u
inst : Field K
inst_1 : CommRing A
inst_2 : Algebra K A
inst_3 : EssFiniteType K A
⊢ FormallyEtale K A ↔
    ∃ (I : Type u) (_ : Finite I) (Ai : I → Type u) (x : (i : I) → Field (Ai i)) (x_1 :
      (i : I) → Algebra.{u_1, u} K (Ai i)) (x_2 : A ≃ₐ[K] (i : I) → Ai i),
      ∀ (i : I), Algebra.IsSeparable.{u_1, u} K (Ai i)
have mp : FormallyEtale K A →
  ∃ (I : Type u) (_ : Finite I) (Ai : I → Type u) (x : (i : I) → Field (Ai i)) (x_1 :
    (i : I) → Algebra.{u_1, u} K (Ai i)) (x_2 : A ≃ₐ[K] (i : I) → Ai i),
    ∀ (i : I), Algebra.IsSeparable.{u_1, u} K (Ai i)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Field (goal)
Goal:
K : Type u_1
A : Type u
inst : Field K
inst_1 : CommRing A
inst_2 : Algebra K A
inst_3 : EssFiniteType K A
mp :
  FormallyEtale K A →
    ∃ (I : Type u) (_ : Finite I) (Ai : I → Type u) (x : (i : I) → Field (Ai i)) (x_1 :
      (i : I) → Algebra.{u_1, u} K (Ai i)) (x_2 : A ≃ₐ[K] (i : I) → Ai i),
      ∀ (i : I), Algebra.IsSeparable.{u_1, u} K (Ai i)
⊢ FormallyEtale K A ↔
    ∃ (I : Type u) (_ : Finite I) (Ai : I → Type u) (x : (i : I) → Field (Ai i)) (x_1 :
      (i : I) → Algebra.{u_1, u} K (Ai i)) (x_2 : A ≃ₐ[K] (i : I) → Ai i),
      ∀ (i : I), Algebra.IsSeparable.{u_1, u} K (Ai i)
have mpr : (∃ (I : Type u) (_ : Finite I) (Ai : I → Type u) (x : (i : I) → Field (Ai i)) (x_1 :
    (i : I) → Algebra.{u_1, u} K (Ai i)) (x_2 : A ≃ₐ[K] (i : I) → Ai i),
    ∀ (i : I), Algebra.IsSeparable.{u_1, u} K (Ai i)) →
  FormallyEtale K A
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Field (hypothesis)
Goal:
K : Type u_1
A : Type u
inst : Field K
inst_1 : CommRing A
inst_2 : Algebra K A
inst_3 : EssFiniteType K A
H : FormallyEtale K A
⊢ ∃ (I : Type u) (_ : Finite I) (Ai : I → Type u) (x : (i : I) → Field (Ai i)) (x_1 :
    (i : I) → Algebra.{u_1, u} K (Ai i)) (x_2 : A ≃ₐ[K] (i : I) → Ai i),
    ∀ (i : I), Algebra.IsSeparable.{u_1, u} K (Ai i)
have this : Module.Finite K A
Tactic: have := FormallyUnramified.finite_of_free K A
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Field (hypothesis)
Goal:
K : Type u_1
A : Type u
inst : Field K
inst_1 : CommRing A
inst_2 : Algebra K A
inst_3 : EssFiniteType K A
H : FormallyEtale K A
this : Module.Finite K A
⊢ ∃ (I : Type u) (_ : Finite I) (Ai : I → Type u) (x : (i : I) → Field (Ai i)) (x_1 :
    (i : I) → Algebra.{u_1, u} K (Ai i)) (x_2 : A ≃ₐ[K] (i : I) → Ai i),
    ∀ (i : I), Algebra.IsSeparable.{u_1, u} K (Ai i)
have this₁ : IsReduced A
Tactic: have := FormallyUnramified.isReduced_of_field K A
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Field (hypothesis)
Goal:
K : Type u_1
A : Type u
inst : Field K
inst_1 : CommRing A
inst_2 : Algebra K A
inst_3 : EssFiniteType K A
H : FormallyEtale K A
this_1 : Module.Finite K A
this : IsReduced A
⊢ ∃ (I : Type u) (_ : Finite I) (Ai : I → Type u) (x : (i : I) → Field (Ai i)) (x_1 :
    (i : I) → Algebra.{u_1, u} K (Ai i)) (x_2 : A ≃ₐ[K] (i : I) → Ai i),
    ∀ (i : I), Algebra.IsSeparable.{u_1, u} K (Ai i)
have this₁ : IsArtinianRing A
Tactic: have : IsArtinianRing A := isArtinian_of_tower K inferInstance
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Field (hypothesis)
Goal:
K : Type u_1
A : Type u
inst : Field K
inst_1 : CommRing A
inst_2 : Algebra K A
inst_3 : EssFiniteType K A
H : FormallyEtale K A
this_1 : Module.Finite K A
this_2 : IsReduced A
this : IsArtinianRing A
v : (i : MaximalSpectrum A) → A :=
  fun (i : MaximalSpectrum A) ↦
    (AlgEquiv.symm (IsArtinianRing.equivPi A) : (a : (I : MaximalSpectrum A) → A ⧸ I.asIdeal) → A)
      (Pi.single (M := fun (I : MaximalSpectrum A) ↦ A ⧸ I.asIdeal) i 1)
⊢ ∃ (I : Type u) (_ : Finite I) (Ai : I → Type u) (x : (i : I) → Field (Ai i)) (x_1 :
    (i : I) → Algebra.{u_1, u} K (Ai i)) (x_2 : A ≃ₐ[K] (i : I) → Ai i),
    ∀ (i : I), Algebra.IsSeparable.{u_1, u} K (Ai i)
have H₁ : ∀ (i : MaximalSpectrum A), FormallyEtale.{u_1, u} K (A ⧸ i.asIdeal)
Tactic: rw [FormallyEtale.iff_of_equiv ((IsArtinianRing.equivPi A).restrictScalars K),
      FormallyEtale.pi_iff] at H
Cleared hypotheses: H, this_1, this_2, this, v
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Field (goal)
Goal:
K : Type u_1
A : Type u
inst : Field K
inst_1 : CommRing A
inst_2 : Algebra K A
inst_3 : EssFiniteType K A
I : Type u
w : Finite I
Ai : I → Type u
w_1 : (i : I) → Field (Ai i)
w_2 : (i : I) → Algebra.{u_1, u} K (Ai i)
e : A ≃ₐ[K] (i : I) → Ai i
h : ∀ (i : I), Algebra.IsSeparable.{u_1, u} K (Ai i)
⊢ FormallyEtale K A
have mpr : ∀ (i : I), FormallyEtale.{u_1, u} K (Ai i)
Tactic: rw [FormallyEtale.iff_of_equiv e, FormallyEtale.pi_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Field (goal)
Goal:
K : Type u_1
A : Type u
inst : Field K
inst_1 : CommRing A
inst_2 : Algebra K A
inst_3 : EssFiniteType K A
⊢ FormallyEtale K A ↔
    ∃ (I : Type u) (_ : Finite I) (Ai : I → Type u) (x : (i : I) → Field (Ai i)) (x_1 :
      (i : I) → Algebra.{u_1, u} K (Ai i)) (x_2 : A ≃ₐ[K] (i : I) → Ai i),
      ∀ (i : I), Algebra.IsSeparable.{u_1, u} K (Ai i)
have mp : FormallyEtale K A →
  ∃ (I : Type u) (_ : Finite I) (Ai : I → Type u) (x : (i : I) → Field (Ai i)) (x_1 :
    (i : I) → Algebra.{u_1, u} K (Ai i)) (x_2 : A ≃ₐ[K] (i : I) → Ai i),
    ∀ (i : I), Algebra.IsSeparable.{u_1, u} K (Ai i)
Tactic: classical
  constructor
  · intro H
    have := FormallyUnramified.finite_of_free K A
    have := FormallyUnramified.isReduced_of_field K A
    have : IsArtinianRing A := isArtinian_of_tower K inferInstance
    let v (i : MaximalSpectrum A) : A := (IsArtinianRing.equivPi A).symm (Pi.single i 1)
    rw [FormallyEtale.iff_of_equiv ((IsArtinianRing.equivPi A).restrictScalars K),
      FormallyEtale.pi_iff] at H
    exact ⟨_, inferInstance, _, _, _, (IsArtinianRing.equivPi A).restrictScalars K,
      fun I ↦ (iff_isSeparable _ _).mp inferInstance⟩
  · intro ⟨I, _, Ai, _, _, e, _⟩
    rw [FormallyEtale.iff_of_equiv e, FormallyEtale.pi_iff]
    exact fun I ↦ of_isSeparable K (Ai I)
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Field (goal)
Goal:
K : Type u_1
A : Type u
inst : Field K
inst_1 : CommRing A
inst_2 : Algebra K A
inst_3 : EssFiniteType K A
mp :
  FormallyEtale K A →
    ∃ (I : Type u) (_ : Finite I) (Ai : I → Type u) (x : (i : I) → Field (Ai i)) (x_1 :
      (i : I) → Algebra.{u_1, u} K (Ai i)) (x_2 : A ≃ₐ[K] (i : I) → Ai i),
      ∀ (i : I), Algebra.IsSeparable.{u_1, u} K (Ai i)
⊢ FormallyEtale K A ↔
    ∃ (I : Type u) (_ : Finite I) (Ai : I → Type u) (x : (i : I) → Field (Ai i)) (x_1 :
      (i : I) → Algebra.{u_1, u} K (Ai i)) (x_2 : A ≃ₐ[K] (i : I) → Ai i),
      ∀ (i : I), Algebra.IsSeparable.{u_1, u} K (Ai i)
have mpr : (∃ (I : Type u) (_ : Finite I) (Ai : I → Type u) (x : (i : I) → Field (Ai i)) (x_1 :
    (i : I) → Algebra.{u_1, u} K (Ai i)) (x_2 : A ≃ₐ[K] (i : I) → Ai i),
    ∀ (i : I), Algebra.IsSeparable.{u_1, u} K (Ai i)) →
  FormallyEtale K A
Tactic: classical
  constructor
  · intro H
    have := FormallyUnramified.finite_of_free K A
    have := FormallyUnramified.isReduced_of_field K A
    have : IsArtinianRing A := isArtinian_of_tower K inferInstance
    let v (i : MaximalSpectrum A) : A := (IsArtinianRing.equivPi A).symm (Pi.single i 1)
    rw [FormallyEtale.iff_of_equiv ((IsArtinianRing.equivPi A).restrictScalars K),
      FormallyEtale.pi_iff] at H
    exact ⟨_, inferInstance, _, _, _, (IsArtinianRing.equivPi A).restrictScalars K,
      fun I ↦ (iff_isSeparable _ _).mp inferInstance⟩
  · intro ⟨I, _, Ai, _, _, e, _⟩
    rw [FormallyEtale.iff_of_equiv e, FormallyEtale.pi_iff]
    exact fun I ↦ of_isSeparable K (Ai I)
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Field (goal)
Goal:
K : Type u_1
A : Type u
inst : Field K
inst_1 : CommRing A
inst_2 : Algebra K A
⊢ Etale K A ↔
    ∃ (I : Type u) (_ : Finite I) (Ai : I → Type u) (x : (i : I) → Field (Ai i)) (x_1 :
      (i : I) → Algebra.{u_1, u} K (Ai i)) (x_2 : A ≃ₐ[K] (i : I) → Ai i),
      ∀ (i : I), Module.Finite.{u_1, u} K (Ai i) ∧ Algebra.IsSeparable.{u_1, u} K (Ai i)
have mp : Etale K A →
  ∃ (I : Type u) (_ : Finite I) (Ai : I → Type u) (x : (i : I) → Field (Ai i)) (x_1 :
    (i : I) → Algebra.{u_1, u} K (Ai i)) (x_2 : A ≃ₐ[K] (i : I) → Ai i),
    ∀ (i : I), Module.Finite.{u_1, u} K (Ai i) ∧ Algebra.IsSeparable.{u_1, u} K (Ai i)
Tactic: constructor