awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Unramified.Dedekind
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Module.Finite A B
inst_4 : IsDedekindDomain A
inst_5 : IsDomain B
inst_6 : Algebra.FormallyUnramified A B
q : Ideal B
hq : q ≠ ⊥
hqp : q.IsPrime
q' : Ideal (Localization.AtPrime q) := IsLocalRing.maximalIdeal (Localization.AtPrime q)
suffices : Submodule.IsPrincipal q'
⊢ IsDiscreteValuationRing.{u_2} (Localization.AtPrime q)

Tactic:
suffices q'.IsPrincipal from ((IsDiscreteValuationRing.TFAE (Localization.AtPrime q)
      (IsLocalization.AtPrime.not_isField B hq (Localization.AtPrime q))).out 4 0).mp this
-- Module: Mathlib.RingTheory.Unramified.Dedekind
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Module.Finite A B
inst_4 : IsDedekindDomain A
inst_5 : IsDomain B
inst_6 : Algebra.FormallyUnramified A B
q : Ideal B
hq : q ≠ ⊥
hqp : q.IsPrime
q' : Ideal (Localization.AtPrime q) := IsLocalRing.maximalIdeal (Localization.AtPrime q)
p : Ideal A := Ideal.under A q
this : Algebra.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q) :=
  Localization.AtPrime.algebraOfLiesOver p q
⊢ p.IsMaximal

Tactic:
have : p.IsMaximal := (hqp.under A).isMaximal (q.under_ne_bot A hq)
-- Module: Mathlib.RingTheory.Unramified.Dedekind
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Module.Finite A B
inst_4 : IsDedekindDomain A
inst_5 : IsDomain B
inst_6 : Algebra.FormallyUnramified A B
q : Ideal B
hq : q ≠ ⊥
hqp : q.IsPrime
q' : Ideal (Localization.AtPrime q) := IsLocalRing.maximalIdeal (Localization.AtPrime q)
p : Ideal A := Ideal.under A q
this_1 : Algebra.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q) :=
  Localization.AtPrime.algebraOfLiesOver p q
this_2 : p.IsMaximal
this : Field (A ⧸ p) := Ideal.Quotient.field p
⊢ IsArtinianRing.{u_2} (HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p))

Tactic:
have := IsArtinianRing.of_finite (A ⧸ p) (B ⧸ p.map (algebraMap A B))
-- Module: Mathlib.RingTheory.Unramified.Dedekind
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Module.Finite A B
inst_4 : IsDedekindDomain A
inst_5 : IsDomain B
inst_6 : Algebra.FormallyUnramified A B
q : Ideal B
hq : q ≠ ⊥
hqp : q.IsPrime
q' : Ideal (Localization.AtPrime q) := IsLocalRing.maximalIdeal (Localization.AtPrime q)
p : Ideal A := Ideal.under A q
this_1 : Algebra.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q) :=
  Localization.AtPrime.algebraOfLiesOver p q
this_2 : p.IsMaximal
this_3 : Field (A ⧸ p) := Ideal.Quotient.field p
this_4 : IsArtinianRing.{u_2} (HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p))
this :
  q' =
    Ideal.map (R := B) (F := B →+* Localization.AtPrime q) (algebraMap B (Localization.AtPrime q))
      (Ideal.map (F := A →+* B) (algebraMap A B) p)
rw :
  Submodule.IsPrincipal.{u_2, u_2} (R := Localization.AtPrime q)
    (Ideal.map (R := Localization.AtPrime p) (F := RingHom.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q))
      (algebraMap (Localization.AtPrime p) (Localization.AtPrime q))
      (Ideal.map (F := A →+* Localization.AtPrime p) (algebraMap A (Localization.AtPrime p)) p))
⊢ Submodule.IsPrincipal q'

Tactic:
rw [this, Ideal.map_map, ← IsScalarTower.algebraMap_eq,
        IsScalarTower.algebraMap_eq A (Localization.AtPrime p) (Localization.AtPrime q),
        ← Ideal.map_map]

Premises used: Localization.AtPrime, Ideal.map_map, IsScalarTower.algebraMap_eq
-- Module: Mathlib.RingTheory.Unramified.Dedekind
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Module.Finite A B
inst_4 : IsDedekindDomain A
inst_5 : IsDomain B
inst_6 : Algebra.FormallyUnramified A B
q : Ideal B
hq : q ≠ ⊥
hqp : q.IsPrime
q' : Ideal (Localization.AtPrime q) := IsLocalRing.maximalIdeal (Localization.AtPrime q)
p : Ideal A := Ideal.under A q
this_1 : Algebra.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q) :=
  Localization.AtPrime.algebraOfLiesOver p q
this_2 : p.IsMaximal
this_3 : Field (A ⧸ p) := Ideal.Quotient.field p
this_4 : IsArtinianRing.{u_2} (HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p))
this :
  q' =
    Ideal.map (R := B) (F := B →+* Localization.AtPrime q) (algebraMap B (Localization.AtPrime q))
      (Ideal.map (F := A →+* B) (algebraMap A B) p)
⊢ Submodule.IsPrincipal.{u_2, u_2} (R := Localization.AtPrime q)
    (Ideal.map (R := Localization.AtPrime p) (F := RingHom.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q))
      (algebraMap (Localization.AtPrime p) (Localization.AtPrime q))
      (Ideal.map (F := A →+* Localization.AtPrime p) (algebraMap A (Localization.AtPrime p)) p))

Tactic:
infer_instance
-- Module: Mathlib.RingTheory.Unramified.Dedekind
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Module.Finite A B
inst_4 : IsDedekindDomain A
inst_5 : IsDomain B
inst_6 : Algebra.FormallyUnramified A B
q : Ideal B
hq : q ≠ ⊥
hqp : q.IsPrime
q' : Ideal (Localization.AtPrime q) := IsLocalRing.maximalIdeal (Localization.AtPrime q)
p : Ideal A := Ideal.under A q
this_1 : Algebra.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q) :=
  Localization.AtPrime.algebraOfLiesOver p q
this_2 : p.IsMaximal
this_3 : Field (A ⧸ p) := Ideal.Quotient.field p
this : IsArtinianRing.{u_2} (HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p))
suffices :
  q' =
    Ideal.map (R := B) (F := B →+* Localization.AtPrime q) (algebraMap B (Localization.AtPrime q))
      (Ideal.map (F := A →+* B) (algebraMap A B) p)
⊢ Submodule.IsPrincipal q'

Tactic:
suffices q' = (p.map (algebraMap A B)).map (algebraMap B (Localization.AtPrime q)) by
      rw [this, Ideal.map_map, ← IsScalarTower.algebraMap_eq,
        IsScalarTower.algebraMap_eq A (Localization.AtPrime p) (Localization.AtPrime q),
        ← Ideal.map_map]
      infer_instance
-- Module: Mathlib.RingTheory.Unramified.Dedekind
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Module.Finite A B
inst_4 : IsDedekindDomain A
inst_5 : IsDomain B
inst_6 : Algebra.FormallyUnramified A B
q : Ideal B
hq : q ≠ ⊥
hqp : q.IsPrime
q' : Ideal (Localization.AtPrime q) := IsLocalRing.maximalIdeal (Localization.AtPrime q)
p : Ideal A := Ideal.under A q
this_1 : Algebra.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q) :=
  Localization.AtPrime.algebraOfLiesOver p q
this_2 : p.IsMaximal
this_3 : Field (A ⧸ p) := Ideal.Quotient.field p
this : IsArtinianRing.{u_2} (HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p))
hIq : Membership.mem (γ := Set (Ideal B)) (Ideal.minimalPrimes (Ideal.map (F := A →+* B) (algebraMap A B) p)) q
⊢ q' =
    Ideal.map (R := B) (F := B →+* Localization.AtPrime q) (algebraMap B (Localization.AtPrime q))
      (Ideal.map (F := A →+* B) (algebraMap A B) p)

Tactic:
rw [← (Algebra.FormallyUnramified.isRadical_map_isMaximal A B p).radical,
      IsLocalization.map_radical q.primeCompl,
      IsLocalization.AtPrime.radical_map_of_mem_minimalPrimes (Localization.AtPrime q) q,
      Localization.AtPrime.map_eq_maximalIdeal]

Premises used: IsLocalization.map_radical, Localization.AtPrime, Algebra.FormallyUnramified.isRadical_map_isMaximal, Ideal.primeCompl, Ideal.IsRadical.radical, Localization.AtPrime.map_eq_maximalIdeal, IsLocalization.AtPrime.radical_map_of_mem_minimalPrimes
-- Module: Mathlib.RingTheory.Unramified.Dedekind
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Module.Finite A B
inst_4 : IsDedekindDomain A
inst_5 : IsDomain B
inst_6 : Algebra.FormallyUnramified A B
q : Ideal B
hq : q ≠ ⊥
hqp : q.IsPrime
q' : Ideal (Localization.AtPrime q) := IsLocalRing.maximalIdeal (Localization.AtPrime q)
p : Ideal A := Ideal.under A q
this_1 : Algebra.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q) :=
  Localization.AtPrime.algebraOfLiesOver p q
this_2 : p.IsMaximal
this_3 : Field (A ⧸ p) := Ideal.Quotient.field p
this : IsArtinianRing.{u_2} (HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p))
hIq :
  Membership.mem (γ := Set (Ideal B))
    (Set.image (α := Ideal (HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p)))
      (Ideal.comap (F := B →+* HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p))
        (Ideal.Quotient.mk (Ideal.map (F := A →+* B) (algebraMap A B) p)))
      (minimalPrimes (HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p))))
    q
⊢ Membership.mem (γ := Set (Ideal B)) (Ideal.minimalPrimes (Ideal.map (F := A →+* B) (algebraMap A B) p)) q

Tactic:
rw [Ideal.minimalPrimes_eq_comap]

Premises used: Ideal.minimalPrimes_eq_comap
-- Module: Mathlib.RingTheory.Unramified.Dedekind
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Module.Finite A B
inst_4 : IsDedekindDomain A
inst_5 : IsDomain B
inst_6 : Algebra.FormallyUnramified A B
q : Ideal B
hq : q ≠ ⊥
hqp : q.IsPrime
q' : Ideal (Localization.AtPrime q) := IsLocalRing.maximalIdeal (Localization.AtPrime q)
p : Ideal A := Ideal.under A q
this_1 : Algebra.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q) :=
  Localization.AtPrime.algebraOfLiesOver p q
this_2 : p.IsMaximal
this_3 : Field (A ⧸ p) := Ideal.Quotient.field p
this : IsArtinianRing.{u_2} (HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p))
⊢ Membership.mem (γ := Set (Ideal B))
    (Set.image (α := Ideal (HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p)))
      (Ideal.comap (F := B →+* HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p))
        (Ideal.Quotient.mk (Ideal.map (F := A →+* B) (algebraMap A B) p)))
      (minimalPrimes (HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p))))
    q

Tactic:
⟨q.map (Ideal.Quotient.mk (p.map (algebraMap A B))),
      IsArtinianRing.mem_minimalPrimes bot_le, Ideal.comap_map_mk Ideal.map_comap_le⟩

Premises used: Algebra.algebraMap, Set.Mem, Ideal.Quotient.mk, setOf, Ideal.map, Ideal.comap_map_mk, IsArtinianRing.mem_minimalPrimes, And.intro, Exists.intro, Set.image, Ideal.map_comap_le, bot_le
-- Module: Mathlib.RingTheory.Unramified.Dedekind
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Module.Finite A B
inst_4 : IsDedekindDomain A
inst_5 : IsDomain B
inst_6 : Algebra.FormallyUnramified A B
q : Ideal B
hq : q ≠ ⊥
hqp : q.IsPrime
q' : Ideal (Localization.AtPrime q) := IsLocalRing.maximalIdeal (Localization.AtPrime q)
p : Ideal A := Ideal.under A q
this_1 : Algebra.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q) :=
  Localization.AtPrime.algebraOfLiesOver p q
this_2 : p.IsMaximal
this_3 : Field (A ⧸ p) := Ideal.Quotient.field p
this : IsArtinianRing.{u_2} (HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p))
⊢ Membership.mem (γ := Set (Ideal B))
    (Set.image (α := Ideal (HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p)))
      (Ideal.comap (F := B →+* HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p))
        (Ideal.Quotient.mk (Ideal.map (F := A →+* B) (algebraMap A B) p)))
      (minimalPrimes (HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p))))
    q

Tactic:
exact ⟨q.map (Ideal.Quotient.mk (p.map (algebraMap A B))),
      IsArtinianRing.mem_minimalPrimes bot_le, Ideal.comap_map_mk Ideal.map_comap_le⟩
-- Module: Mathlib.RingTheory.Unramified.Dedekind
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Module.Finite A B
inst_4 : IsDedekindDomain A
inst_5 : IsDomain B
inst_6 : Algebra.FormallyUnramified A B
⊢ IsDedekindDomain B

Tactic:
have := isDedekindDomainDvr.of_formallyUnramified A B
  inferInstance

Premises used: inferInstance, isDedekindDomainDvr.of_formallyUnramified
-- Module: Mathlib.RingTheory.Unramified.Field
Goal:
K : Type u_1
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsSeparable K L
rw :
  ∀ ⦃B : Type u_3⦄ [inst_4 : CommRing B] [inst_5 : Algebra K B] (I : Ideal B),
    HPow.hPow (β := ℕ) I 2 = ⊥ →
      Function.Injective (α := L →ₐ[K] B) (β := L →ₐ[K] B ⧸ I) (AlgHom.comp (Ideal.Quotient.mkₐ K I))
⊢ FormallyUnramified K L

Tactic:
rw [iff_comp_injective]

Premises used: Algebra.FormallyUnramified.iff_comp_injective
-- Module: Mathlib.RingTheory.Unramified.Field
Goal:
K : Type u_1
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsSeparable K L
B : Type u_3
_ :
  ∀ [inst_4 : CommRing B] [inst_5 : Algebra K B] (I : Ideal B),
    HPow.hPow (β := ℕ) I 2 = ⊥ →
      Function.Injective (α := L →ₐ[K] B) (β := L →ₐ[K] B ⧸ I) (AlgHom.comp (Ideal.Quotient.mkₐ K I))
⊢ ∀ [inst_4 : CommRing B] [inst_5 : Algebra K B] (I : Ideal B),
    HPow.hPow (β := ℕ) I 2 = ⊥ →
      Function.Injective (α := L →ₐ[K] B) (β := L →ₐ[K] B ⧸ I) (AlgHom.comp (Ideal.Quotient.mkₐ K I))

Tactic:
_
-- Module: Mathlib.RingTheory.Unramified.Field
Goal:
K : Type u_1
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsSeparable K L
B : Type u_3
inst_4 : CommRing B
_ :
  ∀ [inst_5 : Algebra K B] (I : Ideal B),
    HPow.hPow (β := ℕ) I 2 = ⊥ →
      Function.Injective (α := L →ₐ[K] B) (β := L →ₐ[K] B ⧸ I) (AlgHom.comp (Ideal.Quotient.mkₐ K I))
⊢ ∀ [inst_5 : Algebra K B] (I : Ideal B),
    HPow.hPow (β := ℕ) I 2 = ⊥ →
      Function.Injective (α := L →ₐ[K] B) (β := L →ₐ[K] B ⧸ I) (AlgHom.comp (Ideal.Quotient.mkₐ K I))

Tactic:
_
-- Module: Mathlib.RingTheory.Unramified.Field
Goal:
K : Type u_1
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsSeparable K L
B : Type u_3
inst_4 : CommRing B
inst_5 : Algebra K B
I : Ideal B
hI : HPow.hPow (β := ℕ) I 2 = ⊥
f₁ f₂ : L →ₐ[K] B
e : Eq (α := L →ₐ[K] B ⧸ I) (AlgHom.comp (Ideal.Quotient.mkₐ K I) f₁) (AlgHom.comp (Ideal.Quotient.mkₐ K I) f₂)
H : ∀ (x : L), Eq (α := B) ((f₁ : (a : L) → B) x : B) ((f₂ : (a : L) → B) x : B)
⊢ f₁ = f₂

Tactic:
ext x
-- Module: Mathlib.RingTheory.Unramified.Field
Goal:
K : Type u_1
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsSeparable K L
B : Type u_3
inst_4 : CommRing B
inst_5 : Algebra K B
I : Ideal B
hI : HPow.hPow (β := ℕ) I 2 = ⊥
f₁ f₂ : L →ₐ[K] B
e : Eq (α := L →ₐ[K] B ⧸ I) (AlgHom.comp (Ideal.Quotient.mkₐ K I) f₁) (AlgHom.comp (Ideal.Quotient.mkₐ K I) f₂)
x : L
⊢ HSub.hSub (α := B) (β := B) ((f₁ : (a : L) → B) x : B) ((f₂ : (a : L) → B) x : B) ∈ I

Tactic:
simpa [Ideal.Quotient.mk_eq_mk_iff_sub_mem] using AlgHom.congr_fun e x

Premises used: Ideal.Quotient.mk_eq_mk_iff_sub_mem, AlgHom.congr_fun
-- Module: Mathlib.RingTheory.Unramified.Field
Goal:
K : Type u_1
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsSeparable K L
B : Type u_3
inst_4 : CommRing B
inst_5 : Algebra K B
I : Ideal B
hI : HPow.hPow (β := ℕ) I 2 = ⊥
f₁ f₂ : L →ₐ[K] B
e : Eq (α := L →ₐ[K] B ⧸ I) (AlgHom.comp (Ideal.Quotient.mkₐ K I) f₁) (AlgHom.comp (Ideal.Quotient.mkₐ K I) f₂)
x : L
⊢ HSub.hSub (α := B) (β := B) ((f₁ : (a : L) → B) x : B) ((f₂ : (a : L) → B) x : B) ∈ I

Tactic:
have : f₁ x - f₂ x ∈ I := by
    simpa [Ideal.Quotient.mk_eq_mk_iff_sub_mem] using AlgHom.congr_fun e x
-- Module: Mathlib.RingTheory.Unramified.Field
Goal:
K : Type u_1
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsSeparable K L
B : Type u_3
inst_4 : CommRing B
inst_5 : Algebra K B
I : Ideal B
hI : HPow.hPow (β := ℕ) I 2 = ⊥
f₁ f₂ : L →ₐ[K] B
e : Eq (α := L →ₐ[K] B ⧸ I) (AlgHom.comp (Ideal.Quotient.mkₐ K I) f₁) (AlgHom.comp (Ideal.Quotient.mkₐ K I) f₂)
x : L
this : HSub.hSub (α := B) (β := B) ((f₁ : (a : L) → B) x : B) ((f₂ : (a : L) → B) x : B) ∈ I
⊢ eval
      (HAdd.hAdd (α := B) ((f₂ : (a : L) → B) x : B)
        (HSub.hSub (α := B) (β := B) ((f₁ : (a : L) → B) x : B) ((f₂ : (a : L) → B) x : B)))
      (map (algebraMap K B) (minpoly K x)) =
    HAdd.hAdd (α := B) (eval ((f₂ : (a : L) → B) x) (map (algebraMap K B) (minpoly K x)) : B)
      (HMul.hMul (α := B)
        (eval ((f₂ : (a : L) → B) x) ((derivative : (a : B[X]) → B[X]) (map (algebraMap K B) (minpoly K x))) : B)
        (HSub.hSub (α := B) (β := B) ((f₁ : (a : L) → B) x : B) ((f₂ : (a : L) → B) x : B)))

Tactic:
have := Polynomial.eval_add_of_sq_eq_zero ((minpoly K x).map (algebraMap K B)) (f₂ x)
    (f₁ x - f₂ x) (show (f₁ x - f₂ x) ^ 2 ∈ ⊥ from hI ▸ Ideal.pow_mem_pow this 2)
-- Module: Mathlib.RingTheory.Unramified.Field
Goal:
K : Type u_1
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsSeparable K L
B : Type u_3
inst_4 : CommRing B
inst_5 : Algebra K B
I : Ideal B
hI : HPow.hPow (β := ℕ) I 2 = ⊥
f₁ f₂ : L →ₐ[K] B
e : Eq (α := L →ₐ[K] B ⧸ I) (AlgHom.comp (Ideal.Quotient.mkₐ K I) f₁) (AlgHom.comp (Ideal.Quotient.mkₐ K I) f₂)
x : L
this_1 : HSub.hSub (α := B) (β := B) ((f₁ : (a : L) → B) x : B) ((f₂ : (a : L) → B) x : B) ∈ I
this :
  eval
      (HAdd.hAdd (α := B) ((f₂ : (a : L) → B) x : B)
        (HSub.hSub (α := B) (β := B) ((f₁ : (a : L) → B) x : B) ((f₂ : (a : L) → B) x : B)))
      (map (algebraMap K B) (minpoly K x)) =
    HAdd.hAdd (α := B) (eval ((f₂ : (a : L) → B) x) (map (algebraMap K B) (minpoly K x)) : B)
      (HMul.hMul (α := B)
        (eval ((f₂ : (a : L) → B) x) ((derivative : (a : B[X]) → B[X]) (map (algebraMap K B) (minpoly K x))) : B)
        (HSub.hSub (α := B) (β := B) ((f₁ : (a : L) → B) x : B) ((f₂ : (a : L) → B) x : B)))
⊢ 0 =
    HMul.hMul (α := B)
      ((f₂ : (a : L) → B) ((aeval x : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K x) : K[X]) : L) : B)
      (HSub.hSub (α := B) (β := B) ((f₁ : (a : L) → B) x : B) ((f₂ : (a : L) → B) x : B))

Tactic:
simp only [add_sub_cancel, eval_map_algebraMap, aeval_algHom_apply, minpoly.aeval, map_zero,
    derivative_map, zero_add] at this

Premises used: map_zero, minpoly.aeval, zero_add, add_sub_cancel, Polynomial.eval_map_algebraMap, Polynomial.derivative_map, Polynomial.aeval_algHom_apply
-- Module: Mathlib.RingTheory.Unramified.Field
Goal:
K : Type u_1
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsSeparable K L
B : Type u_3
inst_4 : CommRing B
inst_5 : Algebra K B
I : Ideal B
hI : HPow.hPow (β := ℕ) I 2 = ⊥
f₁ f₂ : L →ₐ[K] B
e : Eq (α := L →ₐ[K] B ⧸ I) (AlgHom.comp (Ideal.Quotient.mkₐ K I) f₁) (AlgHom.comp (Ideal.Quotient.mkₐ K I) f₂)
x : L
this_1 : HSub.hSub (α := B) (β := B) ((f₁ : (a : L) → B) x : B) ((f₂ : (a : L) → B) x : B) ∈ I
this :
  0 =
    HMul.hMul (α := B)
      ((f₂ : (a : L) → B) ((aeval x : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K x) : K[X]) : L) : B)
      (HSub.hSub (α := B) (β := B) ((f₁ : (a : L) → B) x : B) ((f₂ : (a : L) → B) x : B))
H :
  ∀
    (this :
      HMul.hMul (α := B)
          ((f₂ : (a : L) → B) ((aeval x : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K x) : K[X]) : L) :
            B)
          (HSub.hSub (α := B) (β := B) ((f₁ : (a : L) → B) x : B) ((f₂ : (a : L) → B) x : B)) =
        0),
    Eq (α := B) ((f₁ : (a : L) → B) x : B) ((f₂ : (a : L) → B) x : B)
H₁ :
  ∀ (this : HSub.hSub (α := B) (β := B) ((f₁ : (a : L) → B) x : B) ((f₂ : (a : L) → B) x : B) = 0),
    Eq (α := B) ((f₁ : (a : L) → B) x : B) ((f₂ : (a : L) → B) x : B)
H₂ H₃ H₄ H₅ :
  ∀ (this : Eq (α := B) ((f₁ : (a : L) → B) x : B) ((f₂ : (a : L) → B) x : B)),
    Eq (α := B) ((f₁ : (a : L) → B) x : B) ((f₂ : (a : L) → B) x : B)
⊢ Eq (α := B) ((f₁ : (a : L) → B) x : B) ((f₂ : (a : L) → B) x : B)

Tactic:
rwa [eq_comm, ((isUnit_iff_ne_zero.mpr
    ((Algebra.IsSeparable.isSeparable K x).aeval_derivative_ne_zero
      (minpoly.aeval K x))).map f₂).mul_right_eq_zero, sub_eq_zero] at this

Premises used: Iff.mpr, Algebra.IsSeparable.isSeparable, sub_eq_zero, IsUnit.mul_right_eq_zero, isUnit_iff_ne_zero, minpoly.aeval, eq_comm, Polynomial.Separable.aeval_derivative_ne_zero, IsUnit.map
-- Module: Mathlib.RingTheory.Unramified.Field
Goal:
K : Type u_1
A : Type u_2
inst : Field K
inst_1 : CommRing A
inst_2 : Algebra K A
inst_3 : FormallyUnramified K A
inst_4 : EssFiniteType K A
inst_5 : IsAlgClosed K
inst_6 : IsLocalRing A
⊢ Module.Finite K A

Tactic:
have := finite_of_free (R := K) (S := A)
-- Module: Mathlib.RingTheory.Unramified.Field
Goal:
K : Type u_1
A : Type u_2
inst : Field K
inst_1 : CommRing A
inst_2 : Algebra K A
inst_3 : FormallyUnramified K A
inst_4 : EssFiniteType K A
inst_5 : IsAlgClosed K
inst_6 : IsLocalRing A
this : Module.Finite K A
⊢ IsArtinianRing A

Tactic:
have : IsArtinianRing A := isArtinian_of_tower K inferInstance
-- Module: Mathlib.RingTheory.Unramified.Field
Goal:
K : Type u_1
A : Type u_2
inst : Field K
inst_1 : CommRing A
inst_2 : Algebra K A
inst_3 : FormallyUnramified K A
inst_4 : EssFiniteType K A
inst_5 : IsAlgClosed K
inst_6 : IsLocalRing A
this_1 : Module.Finite K A
this : IsArtinianRing A
rw : IsNilpotent.{u_2} (R := Ideal A) (Ideal.jacobson ⊥)
rw₁ : Ne.{u_2 + 1} (α := Ideal A) ⊥ ⊤
⊢ IsNilpotent (R := Ideal A) (IsLocalRing.maximalIdeal A)

Tactic:
rw [← IsLocalRing.jacobson_eq_maximalIdeal ⊥]

Premises used: Bot.bot, IsLocalRing.jacobson_eq_maximalIdeal
-- Module: Mathlib.RingTheory.Unramified.Field
Goal:
K : Type u_1
A : Type u_2
inst : Field K
inst_1 : CommRing A
inst_2 : Algebra K A
inst_3 : FormallyUnramified K A
inst_4 : EssFiniteType K A
inst_5 : IsAlgClosed K
inst_6 : IsLocalRing A
this_1 : Module.Finite K A
this : IsArtinianRing A
⊢ IsNilpotent.{u_2} (R := Ideal A) (Ideal.jacobson ⊥)

Tactic:
IsArtinianRing.isNilpotent_jacobson_bot

Premises used: IsArtinianRing.isNilpotent_jacobson_bot
-- Module: Mathlib.RingTheory.Unramified.Field
Goal:
K : Type u_1
A : Type u_2
inst : Field K
inst_1 : CommRing A
inst_2 : Algebra K A
inst_3 : FormallyUnramified K A
inst_4 : EssFiniteType K A
inst_5 : IsAlgClosed K
inst_6 : IsLocalRing A
this_1 : Module.Finite K A
this : IsArtinianRing A
⊢ IsNilpotent.{u_2} (R := Ideal A) (Ideal.jacobson ⊥)

Tactic:
exact IsArtinianRing.isNilpotent_jacobson_bot

Premises used: IsArtinianRing.isNilpotent_jacobson_bot
-- Module: Mathlib.RingTheory.Unramified.Field
Goal:
K : Type u_1
A : Type u_2
inst : Field K
inst_1 : CommRing A
inst_2 : Algebra K A
inst_3 : FormallyUnramified K A
inst_4 : EssFiniteType K A
inst_5 : IsAlgClosed K
inst_6 : IsLocalRing A
this_1 : Module.Finite K A
this : IsArtinianRing A
⊢ Ne.{u_2 + 1} (α := Ideal A) ⊥ ⊤

Tactic:
bot_ne_top

Premises used: bot_ne_top
-- Module: Mathlib.RingTheory.Unramified.Field
Goal:
K : Type u_1
A : Type u_2
inst : Field K
inst_1 : CommRing A
inst_2 : Algebra K A
inst_3 : FormallyUnramified K A
inst_4 : EssFiniteType K A
inst_5 : IsAlgClosed K
inst_6 : IsLocalRing A
this_1 : Module.Finite K A
this : IsArtinianRing A
⊢ Ne.{u_2 + 1} (α := Ideal A) ⊥ ⊤

Tactic:
exact bot_ne_top

Premises used: bot_ne_top
-- Module: Mathlib.RingTheory.Unramified.Field
Goal:
K : Type u_1
A : Type u_2
inst : Field K
inst_1 : CommRing A
inst_2 : Algebra K A
inst_3 : FormallyUnramified K A
inst_4 : EssFiniteType K A
inst_5 : IsAlgClosed K
inst_6 : IsLocalRing A
this_1 : Module.Finite K A
this : IsArtinianRing A
⊢ IsNilpotent (R := Ideal A) (IsLocalRing.maximalIdeal A)

Tactic:
have hA : IsNilpotent (IsLocalRing.maximalIdeal A) := by
    rw [← IsLocalRing.jacobson_eq_maximalIdeal ⊥]
    · exact IsArtinianRing.isNilpotent_jacobson_bot
    · exact bot_ne_top