-- 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))
⊢ Eq (α :=
    A ⊗[K] HasQuotient.Quotient A (B := Ideal A) (IsLocalRing.maximalIdeal A) →ₗ[A]
      HasQuotient.Quotient A (B := Ideal A) (IsLocalRing.maximalIdeal A))
    (AlgHom.toLinearMap (ofId A (HasQuotient.Quotient A (B := Ideal A) (IsLocalRing.maximalIdeal A))) ∘ₗ e'.toLinearMap)
    (TensorProduct.AlgebraTensorModule.lift
      (LinearMap.flip
        ((↑K :
            {S M M₂ : Type u_2} →
              [inst : Semiring K] →
                [inst_7 : Semiring S] →
                  [inst_8 : AddCommMonoid M] →
                    [inst_9 : AddCommMonoid M₂] →
                      [inst_10 : Module K M] →
                        [inst_11 : Module K M₂] →
                          [inst_12 : Module S M] →
                            [inst_13 : Module S M₂] →
                              [LinearMap.CompatibleSMul M M₂ K S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[K] M₂)
          (LinearMap.flip
              (AlgHom.toLinearMap (lsmul A A (HasQuotient.Quotient A (B := Ideal A) (IsLocalRing.maximalIdeal A))) :
                A →ₗ[A] End A (HasQuotient.Quotient A (B := Ideal A) (IsLocalRing.maximalIdeal A))) :
            HasQuotient.Quotient A (B := Ideal A) (IsLocalRing.maximalIdeal A) →ₗ[A]
              A →ₗ[A] HasQuotient.Quotient A (B := Ideal A) (IsLocalRing.maximalIdeal A)))))
have e_f : Eq (α :=
  A ⊗[K] HasQuotient.Quotient A (B := Ideal A) (IsLocalRing.maximalIdeal A) →ₗ[K]
    HasQuotient.Quotient A (B := Ideal A) (IsLocalRing.maximalIdeal A))
  ((↑K :
      {S M M₂ : Type u_2} →
        [inst : Semiring K] →
          [inst_7 : Semiring S] →
            [inst_8 : AddCommMonoid M] →
              [inst_9 : AddCommMonoid M₂] →
                [inst_10 : Module K M] →
                  [inst_11 : Module K M₂] →
                    [inst_12 : Module S M] →
                      [inst_13 : Module S M₂] → [LinearMap.CompatibleSMul M M₂ K S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[K] M₂)
    (AlgHom.toLinearMap (ofId A (HasQuotient.Quotient A (B := Ideal A) (IsLocalRing.maximalIdeal A))) ∘ₗ
      e'.toLinearMap))
  ((↑K :
      {S M M₂ : Type u_2} →
        [inst : Semiring K] →
          [inst_7 : Semiring S] →
            [inst_8 : AddCommMonoid M] →
              [inst_9 : AddCommMonoid M₂] →
                [inst_10 : Module K M] →
                  [inst_11 : Module K M₂] →
                    [inst_12 : Module S M] →
                      [inst_13 : Module S M₂] → [LinearMap.CompatibleSMul M M₂ K S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[K] M₂)
    (TensorProduct.AlgebraTensorModule.lift
        (LinearMap.flip
          ((↑K :
              {S M M₂ : Type u_2} →
                [inst : Semiring K] →
                  [inst_7 : Semiring S] →
                    [inst_8 : AddCommMonoid M] →
                      [inst_9 : AddCommMonoid M₂] →
                        [inst_10 : Module K M] →
                          [inst_11 : Module K M₂] →
                            [inst_12 : Module S M] →
                              [inst_13 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ K S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[K] M₂)
            (LinearMap.flip
                (AlgHom.toLinearMap (lsmul A A (HasQuotient.Quotient A (B := Ideal A) (IsLocalRing.maximalIdeal A))) :
                  A →ₗ[A] End A (HasQuotient.Quotient A (B := Ideal A) (IsLocalRing.maximalIdeal A))) :
              HasQuotient.Quotient A (B := Ideal A) (IsLocalRing.maximalIdeal A) →ₗ[A]
                A →ₗ[A] HasQuotient.Quotient A (B := Ideal A) (IsLocalRing.maximalIdeal A)))) :
      A ⊗[K] HasQuotient.Quotient A (B := Ideal A) (IsLocalRing.maximalIdeal A) →ₗ[A]
        HasQuotient.Quotient A (B := Ideal A) (IsLocalRing.maximalIdeal A)))
Tactic: apply LinearMap.restrictScalars_injective K