-- 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))
⊢ AlgHom.toLinearMap (ofId A (HasQuotient.Quotient A (B := Ideal A) (IsLocalRing.maximalIdeal A))) ∘ₗ
      e'.toLinearMap ∘ₗ sec K A (HasQuotient.Quotient A (B := Ideal A) (IsLocalRing.maximalIdeal A)) =
    LinearMap.id
have rw : Eq (α :=
  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) ∘ₗ
    sec K A (HasQuotient.Quotient A (B := Ideal A) (IsLocalRing.maximalIdeal A)))
  ((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)) ∘ₗ
    (sec K A (HasQuotient.Quotient A (B := Ideal A) (IsLocalRing.maximalIdeal A)) :
      HasQuotient.Quotient A (B := Ideal A) (IsLocalRing.maximalIdeal A) →ₗ[A]
        A ⊗[K] HasQuotient.Quotient A (B := Ideal A) (IsLocalRing.maximalIdeal A)))
Tactic: rw [← LinearMap.comp_assoc, ← comp_sec K A]