-- 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))
r : A
s : K
⊢ Eq (α := 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) :
          (a : A ⊗[K] (A ⧸ IsLocalRing.maximalIdeal A)) → A ⧸ IsLocalRing.maximalIdeal A)
        (r ⊗ₜ[K] (e : (a : K) → A ⧸ IsLocalRing.maximalIdeal A) s) :
      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₂)
            (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)) :
          (a : A ⊗[K] (A ⧸ IsLocalRing.maximalIdeal A)) → A ⧸ IsLocalRing.maximalIdeal A)
        (r ⊗ₜ[K] (e : (a : K) → A ⧸ IsLocalRing.maximalIdeal A) s) :
      HasQuotient.Quotient A (B := Ideal A) (IsLocalRing.maximalIdeal A))
have e_f : HSMul.hSMul (β := HasQuotient.Quotient A (B := Ideal A) (IsLocalRing.maximalIdeal A : Ideal A)) s
    ((Ideal.Quotient.mk (IsLocalRing.maximalIdeal A) : (a : A) → A ⧸ IsLocalRing.maximalIdeal A) r :
      HasQuotient.Quotient A (B := Ideal A) (IsLocalRing.maximalIdeal A : Ideal A)) =
  HSMul.hSMul (β := HasQuotient.Quotient A (B := Ideal A) (IsLocalRing.maximalIdeal A)) r
    ((e : (a : K) → A ⧸ IsLocalRing.maximalIdeal A) s :
      HasQuotient.Quotient A (B := Ideal A) (IsLocalRing.maximalIdeal A))
Tactic: suffices s • (Ideal.Quotient.mk (IsLocalRing.maximalIdeal A)) r = r • e s by
      simpa [ofId, e']