awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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
w₁ : HPow.hPow (β := ℕ) (HMul.hMul (β := B) u ((aeval x : (a : K[X]) → B) (minpoly K pb.gen) : B)) 2 = 0
⊢ 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:
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]

Premises used: Ideal.mem_bot, add_mul, Polynomial.eval, pow_two, mul_assoc, add_comm, Polynomial.eval_map_algebraMap, Polynomial.eval_add_of_sq_eq_zero, Polynomial.derivative_map, one_mul
-- 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
⊢ 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:
Ideal.mul_mem_mul hu (Ideal.Quotient.eq_zero_iff_mem.mp hx')

Premises used: Set.Mem, Ideal.mul_mem_mul, Ideal.Quotient.eq_zero_iff_mem, Iff.mp
-- 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
⊢ 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:
exact Ideal.mul_mem_mul hu (Ideal.Quotient.eq_zero_iff_mem.mp hx')

Premises used: Ideal.mul_mem_mul, Ideal.Quotient.eq_zero_iff_mem, Iff.mp
-- 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
w :
  HPow.hPow (β := ℕ) (HMul.hMul (β := B) u ((aeval x : (a : K[X]) → B) (minpoly K pb.gen) : B)) 2 ∈
    HPow.hPow (β := ℕ) I 2
⊢ HPow.hPow (β := ℕ) (HMul.hMul (β := B) u ((aeval x : (a : K[X]) → B) (minpoly K pb.gen) : B)) 2 = 0

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

Premises used: Ideal.mem_bot
-- 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
w : HMul.hMul (β := B) u ((aeval x : (a : K[X]) → B) (minpoly K pb.gen) : B) ∈ I
⊢ HPow.hPow (β := ℕ) (HMul.hMul (β := B) u ((aeval x : (a : K[X]) → B) (minpoly K pb.gen) : B)) 2 ∈
    HPow.hPow (β := ℕ) I 2

Tactic:
apply Ideal.pow_mem_pow

Premises used: Ideal.pow_mem_pow
-- 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
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
w₃ w₄ : Eq (α := B ⧸ I) 0 0
⊢ HMul.hMul (β := B) u ((aeval x : (a : K[X]) → B) (minpoly K pb.gen) : B) ∈ I

Tactic:
rw [← Ideal.Quotient.eq_zero_iff_mem, map_mul, hx', mul_zero]

Premises used: Ideal.Quotient.eq_zero_iff_mem, MulZeroClass.mul_zero, map_mul
-- 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 : EssFiniteType K L
⊢ FormallyEtale K L ↔ Algebra.IsSeparable K L

Tactic:
⟨fun _ ↦ FormallyUnramified.isSeparable K L, fun _ ↦ of_isSeparable K L⟩

Premises used: Algebra.FormallyUnramified.isSeparable, Iff.intro, Algebra.FormallyEtale.of_isSeparable
-- Module: Mathlib.RingTheory.Etale.Field
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
⊢ IsReduced A

Tactic:
have := FormallyUnramified.isReduced_of_field K A
-- Module: Mathlib.RingTheory.Etale.Field
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
⊢ IsArtinianRing A

Tactic:
have : IsArtinianRing A := .of_finite K A
-- Module: Mathlib.RingTheory.Etale.Field
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
rw : FormallyUnramified.{u, u_1} K (A ⧸ I.asIdeal)
⊢ FormallyEtale.{u_1, u} K (A ⧸ I.asIdeal)

Tactic:
rw [FormallyEtale.iff_isSeparable, ← FormallyUnramified.iff_isSeparable]

Premises used: Algebra.FormallyUnramified.iff_isSeparable, Algebra.FormallyEtale.iff_isSeparable
-- Module: Mathlib.RingTheory.Etale.Field
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
⊢ FormallyUnramified.{u, u_1} K (A ⧸ I.asIdeal)

Tactic:
infer_instance
-- Module: Mathlib.RingTheory.Etale.Field
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)

Tactic:
have (I : MaximalSpectrum A) : FormallyEtale K (A ⧸ I.asIdeal) := by
    rw [FormallyEtale.iff_isSeparable, ← FormallyUnramified.iff_isSeparable]
    infer_instance
-- Module: Mathlib.RingTheory.Etale.Field
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_2 : IsArtinianRing A
this : ∀ (I : MaximalSpectrum A), FormallyEtale.{u_1, u} K (A ⧸ I.asIdeal)
⊢ FormallyEtale K A

Tactic:
.of_equiv ((IsArtinianRing.equivPi A).restrictScalars K).symm

Premises used: AlgEquiv.symm, AlgEquiv.restrictScalars, IsArtinianRing.equivPi, Algebra.FormallyEtale.of_equiv
-- Module: Mathlib.RingTheory.Etale.Field
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_2 : IsArtinianRing A
this : ∀ (I : MaximalSpectrum A), FormallyEtale.{u_1, u} K (A ⧸ I.asIdeal)
⊢ FormallyEtale K A

Tactic:
exact .of_equiv ((IsArtinianRing.equivPi A).restrictScalars K).symm
-- Module: Mathlib.RingTheory.Etale.Field
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 ↔ FormallyUnramified K A

Tactic:
⟨fun _ ↦ inferInstance, fun _ ↦ .of_formallyUnramified_of_field K A⟩

Premises used: inferInstance, Iff.intro, Algebra.FormallyEtale.of_formallyUnramified_of_field
-- Module: Mathlib.RingTheory.Etale.Field
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)
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
⊢ 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
-- Module: Mathlib.RingTheory.Etale.Field
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
⊢ Module.Finite K A

Tactic:
have := FormallyUnramified.finite_of_free K A
-- Module: Mathlib.RingTheory.Etale.Field
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
⊢ IsReduced A

Tactic:
have := FormallyUnramified.isReduced_of_field K A
-- Module: Mathlib.RingTheory.Etale.Field
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
⊢ IsArtinianRing A

Tactic:
have : IsArtinianRing A := isArtinian_of_tower K inferInstance
-- Module: Mathlib.RingTheory.Etale.Field
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 : 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

Premises used: AlgEquiv.restrictScalars, Algebra.FormallyEtale.pi_iff, IsArtinianRing.equivPi, Algebra.FormallyEtale.iff_of_equiv
-- Module: Mathlib.RingTheory.Etale.Field
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)
H₁ : ∀ (i : MaximalSpectrum A), FormallyEtale.{u_1, u} K (A ⧸ i.asIdeal)
⊢ Module.Finite K A

Tactic:
rw [FormallyEtale.iff_of_equiv ((IsArtinianRing.equivPi A).restrictScalars K),
      FormallyEtale.pi_iff] at H

Premises used: AlgEquiv.restrictScalars, Algebra.FormallyEtale.pi_iff, IsArtinianRing.equivPi, Algebra.FormallyEtale.iff_of_equiv
-- Module: Mathlib.RingTheory.Etale.Field
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)
H₁ : ∀ (i : MaximalSpectrum A), FormallyEtale.{u_1, u} K (A ⧸ i.asIdeal)
this₁ : Module.Finite K A
⊢ IsReduced A

Tactic:
rw [FormallyEtale.iff_of_equiv ((IsArtinianRing.equivPi A).restrictScalars K),
      FormallyEtale.pi_iff] at H

Premises used: AlgEquiv.restrictScalars, Algebra.FormallyEtale.pi_iff, IsArtinianRing.equivPi, Algebra.FormallyEtale.iff_of_equiv
-- Module: Mathlib.RingTheory.Etale.Field
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)
H₁ : ∀ (i : MaximalSpectrum A), FormallyEtale.{u_1, u} K (A ⧸ i.asIdeal)
this₁ : Module.Finite K A
this₂ : IsReduced A
⊢ IsArtinianRing A

Tactic:
rw [FormallyEtale.iff_of_equiv ((IsArtinianRing.equivPi A).restrictScalars K),
      FormallyEtale.pi_iff] at H

Premises used: AlgEquiv.restrictScalars, Algebra.FormallyEtale.pi_iff, IsArtinianRing.equivPi, Algebra.FormallyEtale.iff_of_equiv
-- Module: Mathlib.RingTheory.Etale.Field
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 : ∀ (i : MaximalSpectrum A), FormallyEtale.{u_1, u} K (A ⧸ i.asIdeal)
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)

Tactic:
⟨_, inferInstance, _, _, _, (IsArtinianRing.equivPi A).restrictScalars K,
      fun I ↦ (iff_isSeparable _ _).mp inferInstance⟩

Premises used: MaximalSpectrum.asIdeal, Algebra.FormallyEtale.iff_isSeparable, inferInstance, AlgEquiv.restrictScalars, HasQuotient.Quotient, IsArtinianRing.equivPi, Exists.intro, Iff.mp
-- Module: Mathlib.RingTheory.Etale.Field
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 : ∀ (i : MaximalSpectrum A), FormallyEtale.{u_1, u} K (A ⧸ i.asIdeal)
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)

Tactic:
exact ⟨_, inferInstance, _, _, _, (IsArtinianRing.equivPi A).restrictScalars K,
      fun I ↦ (iff_isSeparable _ _).mp inferInstance⟩
-- Module: Mathlib.RingTheory.Etale.Field
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)
mpr : ∀ (i : I), FormallyEtale.{u_1, u} K (Ai i)
⊢ FormallyEtale K A

Tactic:
rw [FormallyEtale.iff_of_equiv e, FormallyEtale.pi_iff]

Premises used: Algebra.FormallyEtale.pi_iff, Algebra.FormallyEtale.iff_of_equiv
-- Module: Mathlib.RingTheory.Etale.Field
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)
⊢ ∀ (i : I), FormallyEtale.{u_1, u} K (Ai i)

Tactic:
fun I ↦ of_isSeparable K (Ai I)

Premises used: Algebra.FormallyEtale.of_isSeparable
-- Module: Mathlib.RingTheory.Etale.Field
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)
⊢ ∀ (i : I), FormallyEtale.{u_1, u} K (Ai i)

Tactic:
exact fun I ↦ of_isSeparable K (Ai I)

Premises used: Algebra.FormallyEtale.of_isSeparable
-- Module: Mathlib.RingTheory.Etale.Field
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)
mpr 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
⊢ 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)

Premises used: Algebra.FormallyEtale.pi_iff
-- Module: Mathlib.RingTheory.Etale.Field
Goal:
K : Type u_1
A : Type u
inst : Field K
inst_1 : CommRing A
inst_2 : Algebra K A
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)
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), Module.Finite.{u_1, u} K (Ai i) ∧ Algebra.IsSeparable.{u_1, u} K (Ai i)) →
    Etale 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)

Tactic:
constructor