awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ Function.Bijective.{u_1 + 1, u_2 + 1} (α := K) (β := A) (⇑(algebraMap K A) : (a : K) → A)
have hf₁ : HSMul.hSMul (α := A) (β := HasQuotient.Quotient A (B := Ideal A) (IsLocalRing.maximalIdeal A))
    ((f : (a : A ⧸ IsLocalRing.maximalIdeal A) → A) 1 : A) 1 =
  1
Tactic: have hf₁ : f 1 • (1 : A ⧸ IsLocalRing.maximalIdeal A) = 1 := by
    rw [← algebraMap_eq_smul_one]
    exact LinearMap.congr_fun hf 1
-- 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
⊢ Membership.mem (γ := Ideal A) (IsLocalRing.maximalIdeal A)
    (HSub.hSub (α := A) (β := A) (1 : A) ((f : (a : A ⧸ IsLocalRing.maximalIdeal A) → A) 1 : A))
have rw : Eq (α := HasQuotient.Quotient A (B := Ideal A) (IsLocalRing.maximalIdeal A : Ideal A))
  ((Ideal.Quotient.mk (IsLocalRing.maximalIdeal A) : (a : A) → A ⧸ IsLocalRing.maximalIdeal A)
      (HSub.hSub (α := A) (β := A) (1 : A) ((f : (a : A ⧸ IsLocalRing.maximalIdeal A) → A) 1 : A)) :
    HasQuotient.Quotient A (B := Ideal A) (IsLocalRing.maximalIdeal A : Ideal A))
  (0 : HasQuotient.Quotient A (B := Ideal A) (IsLocalRing.maximalIdeal A : Ideal A))
Tactic: rw [← Ideal.Quotient.eq_zero_iff_mem, map_sub, map_one, ← Ideal.Quotient.algebraMap_eq,
     algebraMap_eq_smul_one, hf₁, sub_self]
-- 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
rw :
  Eq (α := HasQuotient.Quotient A (B := Ideal A) (IsLocalRing.maximalIdeal A : Ideal A))
    ((Ideal.Quotient.mk (IsLocalRing.maximalIdeal A) : (a : A) → A ⧸ IsLocalRing.maximalIdeal A)
        (HSub.hSub (α := A) (β := A) (1 : A) ((f : (a : A ⧸ IsLocalRing.maximalIdeal A) → A) 1 : A)) :
      HasQuotient.Quotient A (B := Ideal A) (IsLocalRing.maximalIdeal A : Ideal A))
    (0 : HasQuotient.Quotient A (B := Ideal A) (IsLocalRing.maximalIdeal A : Ideal A))
⊢ Membership.mem (γ := Ideal A) (IsLocalRing.maximalIdeal A)
    (HSub.hSub (α := A) (β := A) (1 : A) ((f : (a : A ⧸ IsLocalRing.maximalIdeal A) → A) 1 : A))
have rw₁ : HSub.hSub (α := HasQuotient.Quotient A (B := Ideal A) (IsLocalRing.maximalIdeal A : Ideal A))
    ((Ideal.Quotient.mk (IsLocalRing.maximalIdeal A) : (a : A) → A ⧸ IsLocalRing.maximalIdeal A) 1)
    ((Ideal.Quotient.mk (IsLocalRing.maximalIdeal A) : (a : A) → A ⧸ IsLocalRing.maximalIdeal A)
      ((f : (a : A ⧸ IsLocalRing.maximalIdeal A) → A) 1)) =
  0
Tactic: rw [← Ideal.Quotient.eq_zero_iff_mem, map_sub, map_one, ← Ideal.Quotient.algebraMap_eq,
     algebraMap_eq_smul_one, hf₁, sub_self]
-- 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
⊢ Function.Bijective.{u_1 + 1, u_2 + 1} (α := K) (β := A) (⇑(algebraMap K A) : (a : K) → A)
have hf₂ : Membership.mem (γ := Ideal A) (IsLocalRing.maximalIdeal A)
  (HSub.hSub (α := A) (β := A) (1 : A) ((f : (a : A ⧸ IsLocalRing.maximalIdeal A) → A) 1 : A))
Tactic: have hf₂ : 1 - f 1 ∈ IsLocalRing.maximalIdeal A := by
    rw [← Ideal.Quotient.eq_zero_iff_mem, map_sub, map_one, ← Ideal.Quotient.algebraMap_eq,
     algebraMap_eq_smul_one, hf₁, sub_self]
-- 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))
⊢ IsIdempotentElem (HSub.hSub (α := A) (β := A) (1 : A) ((f : (a : A ⧸ IsLocalRing.maximalIdeal A) → A) 1 : A))
have h : IsIdempotentElem (M := A) ((f : (a : A ⧸ IsLocalRing.maximalIdeal A) → A) 1 : A)
Tactic: apply IsIdempotentElem.one_sub
-- 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))
⊢ IsIdempotentElem (M := A) ((f : (a : A ⧸ IsLocalRing.maximalIdeal A) → A) 1 : A)
have h : HMul.hMul (α := A) (β := A) ((f : (a : A ⧸ IsLocalRing.maximalIdeal A) → A) 1 : A)
    ((f : (a : A ⧸ IsLocalRing.maximalIdeal A) → A) 1 : A) =
  (f : (a : A ⧸ IsLocalRing.maximalIdeal A) → A) 1
Tactic: rw [IsIdempotentElem, ← smul_eq_mul, ← map_smul, hf₁]
-- 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))
h :
  HMul.hMul (α := A) (β := A) ((f : (a : A ⧸ IsLocalRing.maximalIdeal A) → A) 1 : A)
      ((f : (a : A ⧸ IsLocalRing.maximalIdeal A) → A) 1 : A) =
    (f : (a : A ⧸ IsLocalRing.maximalIdeal A) → A) 1
⊢ IsIdempotentElem (M := A) ((f : (a : A ⧸ IsLocalRing.maximalIdeal A) → A) 1 : A)
have h₁ : HSMul.hSMul (α := A) (β := A) ((f : (a : A ⧸ IsLocalRing.maximalIdeal A) → A) 1 : A)
    ((f : (a : A ⧸ IsLocalRing.maximalIdeal A) → A) 1 : A) =
  (f : (a : A ⧸ IsLocalRing.maximalIdeal A) → A) 1
Tactic: rw [IsIdempotentElem, ← smul_eq_mul, ← map_smul, hf₁]
-- 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))
h :
  HMul.hMul (α := A) (β := A) ((f : (a : A ⧸ IsLocalRing.maximalIdeal A) → A) 1 : A)
      ((f : (a : A ⧸ IsLocalRing.maximalIdeal A) → A) 1 : A) =
    (f : (a : A ⧸ IsLocalRing.maximalIdeal A) → A) 1
h₁ :
  HSMul.hSMul (α := A) (β := A) ((f : (a : A ⧸ IsLocalRing.maximalIdeal A) → A) 1 : A)
      ((f : (a : A ⧸ IsLocalRing.maximalIdeal A) → A) 1 : A) =
    (f : (a : A ⧸ IsLocalRing.maximalIdeal A) → A) 1
⊢ IsIdempotentElem (M := A) ((f : (a : A ⧸ IsLocalRing.maximalIdeal A) → A) 1 : A)
have h₂ : Eq (α := A)
  ((f : (a : A ⧸ IsLocalRing.maximalIdeal A) → A)
      (HSMul.hSMul (α := A) (β := HasQuotient.Quotient A (B := Ideal A) (IsLocalRing.maximalIdeal A))
        ((f : (a : A ⧸ IsLocalRing.maximalIdeal A) → A) 1 : A) 1) :
    A)
  ((f : (a : A ⧸ IsLocalRing.maximalIdeal A) → A) 1 : A)
Tactic: rw [IsIdempotentElem, ← smul_eq_mul, ← map_smul, hf₁]