awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Dedekind (hypothesis)
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
⊢ Submodule.IsPrincipal q'
have this₁ : 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))
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Dedekind (goal)
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 q'
have 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))
Tactic: rw [this, Ideal.map_map, ← IsScalarTower.algebraMap_eq,
        IsScalarTower.algebraMap_eq A (Localization.AtPrime p) (Localization.AtPrime q),
        ← Ideal.map_map]
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Dedekind (goal)
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))
⊢ Submodule.IsPrincipal q'
have 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)
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
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Dedekind (goal)
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))
⊢ q' =
    Ideal.map (R := B) (F := B →+* Localization.AtPrime q) (algebraMap B (Localization.AtPrime q))
      (Ideal.map (F := A →+* B) (algebraMap A B) p)
have hIq : Membership.mem (γ := Set (Ideal B)) (Ideal.minimalPrimes (Ideal.map (F := A →+* B) (algebraMap A B) p)) q
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]
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Dedekind (goal)
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)) (Ideal.minimalPrimes (Ideal.map (F := A →+* B) (algebraMap A B) p)) q
have 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
Tactic: rw [Ideal.minimalPrimes_eq_comap]
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Field (goal)
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
⊢ FormallyUnramified K L
have 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))
Tactic: rw [iff_comp_injective]
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Field (goal)
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₂)
⊢ f₁ = f₂
have H : ∀ (x : L), Eq (α := B) ((f₁ : (a : L) → B) x : B) ((f₂ : (a : L) → B) x : B)
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Field (hypothesis)
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
⊢ Eq (α := B) ((f₁ : (a : L) → B) x : B) ((f₂ : (a : L) → B) x : B)
have this : 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
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Field (hypothesis)
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
⊢ Eq (α := B) ((f₁ : (a : L) → B) x : B) ((f₂ : (a : L) → B) x : B)
have 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)))
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)
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Field (hypothesis)
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)))
⊢ Eq (α := B) ((f₁ : (a : L) → B) x : B) ((f₂ : (a : L) → B) x : B)
have 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))
Tactic: simp only [add_sub_cancel, eval_map_algebraMap, aeval_algHom_apply, minpoly.aeval, map_zero,
    derivative_map, zero_add] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Field (goal)
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))
⊢ Eq (α := B) ((f₁ : (a : L) → B) x : B) ((f₂ : (a : L) → B) x : B)
have 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)
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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Field (goal)
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)
⊢ Eq (α := B) ((f₁ : (a : L) → B) x : B) ((f₂ : (a : L) → B) x : B)
have 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)
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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Field (goal)
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)
⊢ Eq (α := B) ((f₁ : (a : L) → B) x : B) ((f₂ : (a : L) → B) x : B)
have 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)
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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Field (hypothesis)
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
⊢ Function.Bijective.{u_1 + 1, u_2 + 1} (α := K) (β := A) (⇑(algebraMap K A) : (a : K) → A)
have this : Module.Finite K A
Tactic: have := finite_of_free (R := K) (S := A)
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Field (hypothesis)
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
⊢ Function.Bijective.{u_1 + 1, u_2 + 1} (α := K) (β := A) (⇑(algebraMap K A) : (a : K) → A)
have this₁ : IsArtinianRing A
Tactic: have : IsArtinianRing A := isArtinian_of_tower K inferInstance
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Field (goal)
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)
have rw : IsNilpotent.{u_2} (R := Ideal A) (Ideal.jacobson ⊥)
Tactic: rw [← IsLocalRing.jacobson_eq_maximalIdeal ⊥]
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Field (goal)
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 ⊥)
⊢ IsNilpotent (R := Ideal A) (IsLocalRing.maximalIdeal A)
have rw₁ : Ne.{u_2 + 1} (α := Ideal A) ⊥ ⊤
Tactic: rw [← IsLocalRing.jacobson_eq_maximalIdeal ⊥]
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Field (hypothesis)
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
⊢ Function.Bijective.{u_1 + 1, u_2 + 1} (α := K) (β := A) (⇑(algebraMap K A) : (a : K) → A)
have hA : 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
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Field (hypothesis)
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
hA : IsNilpotent (R := Ideal A) (IsLocalRing.maximalIdeal A)
e : AlgEquiv.{u_1, u_1, u_2} K K (HasQuotient.Quotient A (B := Ideal A) (IsLocalRing.maximalIdeal A)) :=
  let __spread.0 : AlgHom.{u_1, u_1, u_2} K K (HasQuotient.Quotient A (B := Ideal A) (IsLocalRing.maximalIdeal A)) :=
    ofId K (HasQuotient.Quotient A (B := Ideal A) (IsLocalRing.maximalIdeal A));
  let __spread.1 : Equiv.{u_1 + 1, u_2 + 1} K (HasQuotient.Quotient A (B := Ideal A) (IsLocalRing.maximalIdeal A)) :=
    Equiv.ofBijective
      (⇑(algebraMap K (HasQuotient.Quotient A (B := Ideal A) (IsLocalRing.maximalIdeal A))) :
        (a : K) → A ⧸ IsLocalRing.maximalIdeal A)
      ⋯;
  {
    toFun :=
      (↑(↑__spread.0.toRingHom : K →* A ⧸ IsLocalRing.maximalIdeal A) :
          OneHom K (A ⧸ IsLocalRing.maximalIdeal A)).toFun,
    invFun := __spread.1.invFun, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
e' : A ⊗[K] HasQuotient.Quotient A (B := Ideal A) (IsLocalRing.maximalIdeal A) ≃ₐ[A] A :=
  AlgEquiv.trans (A₂ := A ⊗[K] K)
    (TensorProduct.congr AlgEquiv.refl e.symm :
      A ⊗[K] HasQuotient.Quotient A (B := Ideal A) (IsLocalRing.maximalIdeal A) ≃ₐ[A] A ⊗[K] K)
    (TensorProduct.rid K A A : A ⊗[K] K ≃ₐ[A] A)
f : HasQuotient.Quotient A (B := Ideal A) (IsLocalRing.maximalIdeal A) →ₗ[A] A :=
  e'.toLinearMap ∘ₗ sec K A (HasQuotient.Quotient A (B := Ideal A) (IsLocalRing.maximalIdeal A))
⊢ Function.Bijective.{u_1 + 1, u_2 + 1} (α := K) (β := A) (⇑(algebraMap K A) : (a : K) → A)
have hf : AlgHom.toLinearMap (ofId A (HasQuotient.Quotient A (B := Ideal A) (IsLocalRing.maximalIdeal A))) ∘ₗ f = LinearMap.id
Tactic: have hf : (Algebra.ofId _ _).toLinearMap ∘ₗ f = LinearMap.id := by
    dsimp [f]
    rw [← LinearMap.comp_assoc, ← comp_sec K A]
    congr 1
    apply LinearMap.restrictScalars_injective K
    apply _root_.TensorProduct.ext'
    intro r s
    obtain ⟨s, rfl⟩ := e.surjective s
    suffices s • (Ideal.Quotient.mk (IsLocalRing.maximalIdeal A)) r = r • e s by
      simpa [ofId, e']
    simp [Algebra.smul_def, e, ofId, mul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Field (goal)
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
hA : IsNilpotent (R := Ideal A) (IsLocalRing.maximalIdeal A)
e : AlgEquiv.{u_1, u_1, u_2} K K (HasQuotient.Quotient A (B := Ideal A) (IsLocalRing.maximalIdeal A)) :=
  let __spread.0 : AlgHom.{u_1, u_1, u_2} K K (HasQuotient.Quotient A (B := Ideal A) (IsLocalRing.maximalIdeal A)) :=
    ofId K (HasQuotient.Quotient A (B := Ideal A) (IsLocalRing.maximalIdeal A));
  let __spread.1 : Equiv.{u_1 + 1, u_2 + 1} K (HasQuotient.Quotient A (B := Ideal A) (IsLocalRing.maximalIdeal A)) :=
    Equiv.ofBijective
      (⇑(algebraMap K (HasQuotient.Quotient A (B := Ideal A) (IsLocalRing.maximalIdeal A))) :
        (a : K) → A ⧸ IsLocalRing.maximalIdeal A)
      ⋯;
  {
    toFun :=
      (↑(↑__spread.0.toRingHom : K →* A ⧸ IsLocalRing.maximalIdeal A) :
          OneHom K (A ⧸ IsLocalRing.maximalIdeal A)).toFun,
    invFun := __spread.1.invFun, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
e' : A ⊗[K] HasQuotient.Quotient A (B := Ideal A) (IsLocalRing.maximalIdeal A) ≃ₐ[A] A :=
  AlgEquiv.trans (A₂ := A ⊗[K] K)
    (TensorProduct.congr AlgEquiv.refl e.symm :
      A ⊗[K] HasQuotient.Quotient A (B := Ideal A) (IsLocalRing.maximalIdeal A) ≃ₐ[A] A ⊗[K] K)
    (TensorProduct.rid K A A : A ⊗[K] K ≃ₐ[A] A)
f : HasQuotient.Quotient A (B := Ideal A) (IsLocalRing.maximalIdeal A) →ₗ[A] A :=
  e'.toLinearMap ∘ₗ sec K A (HasQuotient.Quotient A (B := Ideal A) (IsLocalRing.maximalIdeal A))
hf :
  AlgHom.toLinearMap (ofId A (HasQuotient.Quotient A (B := Ideal A) (IsLocalRing.maximalIdeal A))) ∘ₗ f = LinearMap.id
⊢ HSMul.hSMul (α := A) (β := HasQuotient.Quotient A (B := Ideal A) (IsLocalRing.maximalIdeal A))
      ((f : (a : A ⧸ IsLocalRing.maximalIdeal A) → A) 1 : A) 1 =
    1
have rw : Eq (α := HasQuotient.Quotient A (B := Ideal A) (IsLocalRing.maximalIdeal A))
  ((algebraMap A (HasQuotient.Quotient A (B := Ideal A) (IsLocalRing.maximalIdeal A)) :
      (a : A) → A ⧸ IsLocalRing.maximalIdeal A)
    ((f : (a : A ⧸ IsLocalRing.maximalIdeal A) → A) 1))
  1
Tactic: rw [← algebraMap_eq_smul_one]