awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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_2 : IsArtinianRing 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
hf₁ :
  HSMul.hSMul (α := A) (β := HasQuotient.Quotient A (B := Ideal A) (IsLocalRing.maximalIdeal A))
      ((f : (a : A ⧸ IsLocalRing.maximalIdeal A) → A) 1 : A) 1 =
    1
hf₂ :
  Membership.mem (γ := Ideal A) (IsLocalRing.maximalIdeal A)
    (HSub.hSub (α := A) (β := A) (1 : A) ((f : (a : A ⧸ IsLocalRing.maximalIdeal A) → A) 1 : A))
hf₃ : IsIdempotentElem (HSub.hSub (α := A) (β := A) (1 : A) ((f : (a : A ⧸ IsLocalRing.maximalIdeal A) → A) 1 : A))
n : ℕ
hn : HPow.hPow (α := Ideal A) (IsLocalRing.maximalIdeal A) n = 0
this : HSub.hSub (α := A) (β := A) (1 : A) ((f : (a : A ⧸ IsLocalRing.maximalIdeal A) → A) 1 : A) ^ n = 0
rw : Eq (α := A) (1 : A) ((f : (a : A ⧸ IsLocalRing.maximalIdeal A) → A) 1 : A)
rw₁ : HSub.hSub (α := A) (β := A) (1 : A) ((f : (a : A ⧸ IsLocalRing.maximalIdeal A) → A) 1 : A) = 0
rw₂ : HSub.hSub (α := A) (β := A) (1 : A) ((f : (a : A ⧸ IsLocalRing.maximalIdeal A) → A) 1 : A) ^ (n + 1) = 0
⊢ Eq (α := A) ((f : (a : A ⧸ IsLocalRing.maximalIdeal A) → A) 1 : A) (1 : A)
have rw₃ : HSub.hSub (α := A) (β := A) (1 : A) ((f : (a : A ⧸ IsLocalRing.maximalIdeal A) → A) 1 : A) ^ n *
    HSub.hSub (α := A) (β := A) (1 : A) ((f : (a : A ⧸ IsLocalRing.maximalIdeal A) → A) 1 : A) =
  0
Tactic: rw [eq_comm, ← sub_eq_zero, ← hf₃.pow_succ_eq n, pow_succ, this, zero_mul]
-- 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_2 : IsArtinianRing 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
hf₁ :
  HSMul.hSMul (α := A) (β := HasQuotient.Quotient A (B := Ideal A) (IsLocalRing.maximalIdeal A))
      ((f : (a : A ⧸ IsLocalRing.maximalIdeal A) → A) 1 : A) 1 =
    1
hf₂ :
  Membership.mem (γ := Ideal A) (IsLocalRing.maximalIdeal A)
    (HSub.hSub (α := A) (β := A) (1 : A) ((f : (a : A ⧸ IsLocalRing.maximalIdeal A) → A) 1 : A))
hf₃ : IsIdempotentElem (HSub.hSub (α := A) (β := A) (1 : A) ((f : (a : A ⧸ IsLocalRing.maximalIdeal A) → A) 1 : A))
n : ℕ
hn : HPow.hPow (α := Ideal A) (IsLocalRing.maximalIdeal A) n = 0
this : HSub.hSub (α := A) (β := A) (1 : A) ((f : (a : A ⧸ IsLocalRing.maximalIdeal A) → A) 1 : A) ^ n = 0
rw : Eq (α := A) (1 : A) ((f : (a : A ⧸ IsLocalRing.maximalIdeal A) → A) 1 : A)
rw₁ : HSub.hSub (α := A) (β := A) (1 : A) ((f : (a : A ⧸ IsLocalRing.maximalIdeal A) → A) 1 : A) = 0
rw₂ : HSub.hSub (α := A) (β := A) (1 : A) ((f : (a : A ⧸ IsLocalRing.maximalIdeal A) → A) 1 : A) ^ (n + 1) = 0
rw₃ :
  HSub.hSub (α := A) (β := A) (1 : A) ((f : (a : A ⧸ IsLocalRing.maximalIdeal A) → A) 1 : A) ^ n *
      HSub.hSub (α := A) (β := A) (1 : A) ((f : (a : A ⧸ IsLocalRing.maximalIdeal A) → A) 1 : A) =
    0
⊢ Eq (α := A) ((f : (a : A ⧸ IsLocalRing.maximalIdeal A) → A) 1 : A) (1 : A)
have rw₄ : 0 * HSub.hSub (α := A) (β := A) (1 : A) ((f : (a : A ⧸ IsLocalRing.maximalIdeal A) → A) 1 : A) = 0
Tactic: rw [eq_comm, ← sub_eq_zero, ← hf₃.pow_succ_eq n, pow_succ, this, zero_mul]
-- 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))
hf :
  AlgHom.toLinearMap (ofId A (HasQuotient.Quotient A (B := Ideal A) (IsLocalRing.maximalIdeal A))) ∘ₗ f = LinearMap.id
hf₁ :
  HSMul.hSMul (α := A) (β := HasQuotient.Quotient A (B := Ideal A) (IsLocalRing.maximalIdeal A))
      ((f : (a : A ⧸ IsLocalRing.maximalIdeal A) → A) 1 : A) 1 =
    1
hf₂ :
  Membership.mem (γ := Ideal A) (IsLocalRing.maximalIdeal A)
    (HSub.hSub (α := A) (β := A) (1 : A) ((f : (a : A ⧸ IsLocalRing.maximalIdeal A) → A) 1 : A))
hf₃ : IsIdempotentElem (HSub.hSub (α := A) (β := A) (1 : A) ((f : (a : A ⧸ IsLocalRing.maximalIdeal A) → A) 1 : A))
⊢ Function.Bijective.{u_1 + 1, u_2 + 1} (α := K) (β := A) (⇑(algebraMap K A) : (a : K) → A)
have hf₄ : Eq (α := A) ((f : (a : A ⧸ IsLocalRing.maximalIdeal A) → A) 1 : A) (1 : A)
Tactic: have hf₄ : f 1 = 1 := by
    obtain ⟨n, hn⟩ := hA
    have : (1 - f 1) ^ n = 0 := by
      rw [← Ideal.mem_bot, ← Ideal.zero_eq_bot, ← hn]
      exact Ideal.pow_mem_pow hf₂ n
    rw [eq_comm, ← sub_eq_zero, ← hf₃.pow_succ_eq n, pow_succ, this, zero_mul]
-- 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
hf₁ :
  HSMul.hSMul (α := A) (β := HasQuotient.Quotient A (B := Ideal A) (IsLocalRing.maximalIdeal A))
      ((f : (a : A ⧸ IsLocalRing.maximalIdeal A) → A) 1 : A) 1 =
    1
hf₂ :
  Membership.mem (γ := Ideal A) (IsLocalRing.maximalIdeal A)
    (HSub.hSub (α := A) (β := A) (1 : A) ((f : (a : A ⧸ IsLocalRing.maximalIdeal A) → A) 1 : A))
hf₃ : IsIdempotentElem (HSub.hSub (α := A) (β := A) (1 : A) ((f : (a : A ⧸ IsLocalRing.maximalIdeal A) → A) 1 : A))
hf₄ : Eq (α := A) ((f : (a : A ⧸ IsLocalRing.maximalIdeal A) → A) 1 : A) (1 : A)
⊢ Function.Bijective.{u_1 + 1, u_2 + 1} (α := K) (β := A) (⇑(algebraMap K A) : (a : K) → A)
have refine : ∀ (x : A),
  (algebraMap K A : (a : K) → A)
      (Function.comp (β := HasQuotient.Quotient A (B := Ideal A) (IsLocalRing.maximalIdeal A))
        (⇑e.symm : (a : A ⧸ IsLocalRing.maximalIdeal A) → K)
        (⇑(algebraMap A (HasQuotient.Quotient A (B := Ideal A) (IsLocalRing.maximalIdeal A))) :
          (a : A) → A ⧸ IsLocalRing.maximalIdeal A)
        x) =
    x
Tactic: refine Equiv.bijective ⟨algebraMap K A, ⇑e.symm ∘ ⇑(algebraMap A _), fun x ↦ by simp, fun x ↦ ?_⟩
-- 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
hf₁ :
  HSMul.hSMul (α := A) (β := HasQuotient.Quotient A (B := Ideal A) (IsLocalRing.maximalIdeal A))
      ((f : (a : A ⧸ IsLocalRing.maximalIdeal A) → A) 1 : A) 1 =
    1
hf₂ :
  Membership.mem (γ := Ideal A) (IsLocalRing.maximalIdeal A)
    (HSub.hSub (α := A) (β := A) (1 : A) ((f : (a : A ⧸ IsLocalRing.maximalIdeal A) → A) 1 : A))
hf₃ : IsIdempotentElem (HSub.hSub (α := A) (β := A) (1 : A) ((f : (a : A ⧸ IsLocalRing.maximalIdeal A) → A) 1 : A))
hf₄ : Eq (α := A) ((f : (a : A ⧸ IsLocalRing.maximalIdeal A) → A) 1 : A) (1 : A)
x : A
⊢ Eq (α := (a : K) → A) (⇑(algebraMap K A) : (a : K) → A)
    (Function.comp (β := HasQuotient.Quotient A (B := Ideal A) (IsLocalRing.maximalIdeal A))
      (⇑f : (a : A ⧸ IsLocalRing.maximalIdeal A) → A) (⇑e : (a : K) → A ⧸ IsLocalRing.maximalIdeal A))
have h : ∀ (k : K),
  Eq (α := A) ((algebraMap K A : (a : K) → A) k : A)
    (Function.comp (β := HasQuotient.Quotient A (B := Ideal A) (IsLocalRing.maximalIdeal A))
        (⇑f : (a : A ⧸ IsLocalRing.maximalIdeal A) → A) (⇑e : (a : K) → A ⧸ IsLocalRing.maximalIdeal A) k :
      A)
Tactic: ext k
-- 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
hf₁ :
  HSMul.hSMul (α := A) (β := HasQuotient.Quotient A (B := Ideal A) (IsLocalRing.maximalIdeal A))
      ((f : (a : A ⧸ IsLocalRing.maximalIdeal A) → A) 1 : A) 1 =
    1
hf₂ :
  Membership.mem (γ := Ideal A) (IsLocalRing.maximalIdeal A)
    (HSub.hSub (α := A) (β := A) (1 : A) ((f : (a : A ⧸ IsLocalRing.maximalIdeal A) → A) 1 : A))
hf₃ : IsIdempotentElem (HSub.hSub (α := A) (β := A) (1 : A) ((f : (a : A ⧸ IsLocalRing.maximalIdeal A) → A) 1 : A))
hf₄ : Eq (α := A) ((f : (a : A ⧸ IsLocalRing.maximalIdeal A) → A) 1 : A) (1 : A)
x : A
k : K
| (Function.comp (β := HasQuotient.Quotient A (B := Ideal A) (IsLocalRing.maximalIdeal A))
      (⇑f : (a : A ⧸ IsLocalRing.maximalIdeal A) → A) (⇑e : (a : K) → A ⧸ IsLocalRing.maximalIdeal A) k :
    A)
have rw : ((algebraMap K A : (a : K) → A) k : A)
Tactic: rw [← mul_one k, ← smul_eq_mul, Function.comp_apply, map_smul,
      LinearMap.map_smul_of_tower, map_one, hf₄, ← algebraMap_eq_smul_one]
-- 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
hf₁ :
  HSMul.hSMul (α := A) (β := HasQuotient.Quotient A (B := Ideal A) (IsLocalRing.maximalIdeal A))
      ((f : (a : A ⧸ IsLocalRing.maximalIdeal A) → A) 1 : A) 1 =
    1
hf₂ :
  Membership.mem (γ := Ideal A) (IsLocalRing.maximalIdeal A)
    (HSub.hSub (α := A) (β := A) (1 : A) ((f : (a : A ⧸ IsLocalRing.maximalIdeal A) → A) 1 : A))
hf₃ : IsIdempotentElem (HSub.hSub (α := A) (β := A) (1 : A) ((f : (a : A ⧸ IsLocalRing.maximalIdeal A) → A) 1 : A))
hf₄ : Eq (α := A) ((f : (a : A ⧸ IsLocalRing.maximalIdeal A) → A) 1 : A) (1 : A)
x : A
k : K
⊢ Eq (α := A) ((algebraMap K A : (a : K) → A) k : A)
    (Function.comp (β := HasQuotient.Quotient A (B := Ideal A) (IsLocalRing.maximalIdeal A))
        (⇑f : (a : A ⧸ IsLocalRing.maximalIdeal A) → A) (⇑e : (a : K) → A ⧸ IsLocalRing.maximalIdeal A) k :
      A)
have conv_rhs : Eq (α := A) ((algebraMap K A : (a : K) → A) k : A)
  (Function.comp (β := HasQuotient.Quotient A (B := Ideal A) (IsLocalRing.maximalIdeal A))
      (⇑f : (a : A ⧸ IsLocalRing.maximalIdeal A) → A) (⇑e : (a : K) → A ⧸ IsLocalRing.maximalIdeal A) k :
    A)
Tactic: conv_rhs => rw [← mul_one k, ← smul_eq_mul, Function.comp_apply, map_smul,
      LinearMap.map_smul_of_tower, map_one, hf₄, ← algebraMap_eq_smul_one]
-- 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
⊢ IsField A
have rw : LE.le (α := Ideal A) (IsLocalRing.maximalIdeal A) ⊥
Tactic: rw [IsLocalRing.isField_iff_maximalIdeal_eq, eq_bot_iff]
-- 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
x : A
hx : Membership.mem (γ := Submodule A A) (IsLocalRing.maximalIdeal A) x
⊢ Membership.mem (γ := Submodule A A) ⊥ x
have obtain : ∀ (x : K)
  (hx :
    Membership.mem (α := A) (γ := Submodule A A) (IsLocalRing.maximalIdeal A) ((algebraMap K A : (a : K) → A) x : A)),
  Membership.mem.{u_2, u_2} (α := A) (γ := Submodule A A) ⊥ ((algebraMap K A : (a : K) → A) x : A)
Tactic: obtain ⟨x, rfl⟩ := (bijective_of_isAlgClosed_of_isLocalRing K A).surjective x
Cleared hypotheses: x, hx
-- 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
x : K
hx : Membership.mem (α := A) (γ := Submodule A A) (IsLocalRing.maximalIdeal A) ((algebraMap K A : (a : K) → A) x : A)
⊢ Eq.{u_2 + 1} (α := A) ((algebraMap K A : (a : K) → A) x : A) (0 : A)
have rw : Eq.{u_2 + 1} (α := A) ((algebraMap K A : (a : K) → A) x : A) ((algebraMap K A : (a : K) → A) 0 : A)
Tactic: rw [← (algebraMap K A).map_zero]
-- 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
x : K
hx : Membership.mem (α := A) (γ := Submodule A A) (IsLocalRing.maximalIdeal A) ((algebraMap K A : (a : K) → A) x : A)
⊢ Eq.{u_2 + 1} (α := A) ((algebraMap K A : (a : K) → A) x : A) ((algebraMap K A : (a : K) → A) 0 : A)
have by_contra : ∀ (hx' : ¬Eq.{u_2 + 1} (α := A) ((algebraMap K A : (a : K) → A) x : A) ((algebraMap K A : (a : K) → A) 0 : A)), False
Tactic: by_contra hx'
-- 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
⊢ IsReduced A
have eq_zero : ∀ (x : A), IsNilpotent x → x = 0
Tactic: constructor