-- Module: Mathlib.RingTheory.Unramified.Field
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))
e_f :
  ∀ (x : A) (y : HasQuotient.Quotient A (B := Ideal A) (IsLocalRing.maximalIdeal A)),
    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)
          (x ⊗ₜ[K] y) :
        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)
          (x ⊗ₜ[K] y) :
        HasQuotient.Quotient A (B := Ideal A) (IsLocalRing.maximalIdeal A))
⊢ 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 _root_.TensorProduct.ext'

Premises used: TensorProduct.ext'