-- Lean 4 proof step from Mathlib.RingTheory.Unramified.LocalStructure (goal)
Goal:
R : Type u_1
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Ideal R
inst_3 : P.IsPrime
x : S
hx : Eq (α := Subalgebra R S) R[x] ⊤
hx' : Function.Surjective.{u_1 + 1, u_3 + 1} (α := R[X]) (β := S) (⇑(aeval x) : (a : R[X]) → S)
I : Ideal R[X] := RingHom.ker (F := RingHom.{u_1, u_3} R[X] S) (AlgHom.toRingHom (aeval x))
e : P.Fiber S ≃ₐ[P.ResidueField]
  HasQuotient.Quotient P.ResidueField[X] (B := Ideal P.ResidueField[X])
    (Ideal.map (F := R[X] →+* P.ResidueField[X]) (mapRingHom (algebraMap R P.ResidueField)) I) :=
  fiberEquivQuotient (aeval x) hx' P
a : R
⊢ Eq (α :=
    HasQuotient.Quotient P.ResidueField[X] (B := Ideal P.ResidueField[X])
      (Ideal.map (F := R[X] →+* P.ResidueField[X]) (mapRingHom (algebraMap R P.ResidueField)) I))
    ((@RingHom.comp _ P.ResidueField _ _ Semiring.toNonAssocSemiring _
            (RingHom.comp (e.toRingEquiv.toRingHom.comp (AlgHom.toRingHom (aeval (1 ⊗ₜ[R] x)))) C)
            (algebraMap R P.ResidueField) :
          (a : R) → P.ResidueField[X] ⧸ Ideal.map (mapRingHom (algebraMap R P.ResidueField)) I)
        a :
      HasQuotient.Quotient P.ResidueField[X] (B := Ideal P.ResidueField[X])
        (Ideal.map (F := R[X] →+* P.ResidueField[X]) (mapRingHom (algebraMap R P.ResidueField)) I))
    ((@RingHom.comp _ P.ResidueField _ _ Semiring.toNonAssocSemiring _
            (RingHom.comp
              (Ideal.Quotient.mk
                (Ideal.map (F := R[X] →+* P.ResidueField[X]) (mapRingHom (algebraMap R P.ResidueField))
                  (RingHom.ker (F := RingHom.{u_1, u_3} R[X] S) (AlgHom.toRingHom (aeval x)))))
              C)
            (algebraMap R P.ResidueField) :
          (a : R) → P.ResidueField[X] ⧸ Ideal.map (mapRingHom (algebraMap R P.ResidueField)) I)
        a :
      HasQuotient.Quotient P.ResidueField[X] (B := Ideal P.ResidueField[X])
        (Ideal.map (F := R[X] →+* P.ResidueField[X]) (mapRingHom (algebraMap R P.ResidueField)) I))
have h : Eq.{u_1 + 1} (α :=
  HasQuotient.Quotient P.ResidueField[X] (B := Ideal P.ResidueField[X])
    (Ideal.map (F := R[X] →+* P.ResidueField[X]) (mapRingHom (algebraMap R P.ResidueField)) I))
  ((e : (a : P.Fiber S) → P.ResidueField[X] ⧸ Ideal.map (mapRingHom (algebraMap R P.ResidueField)) I)
      ((aeval (1 ⊗ₜ[R] x) : (a : P.ResidueField[X]) → P.ResidueField ⊗[R] S)
        ((C : (a : P.ResidueField) → P.ResidueField[X]) ((algebraMap R P.ResidueField : (a : R) → P.ResidueField) a))) :
    HasQuotient.Quotient P.ResidueField[X] (B := Ideal P.ResidueField[X])
      (Ideal.map (F := R[X] →+* P.ResidueField[X]) (mapRingHom (algebraMap R P.ResidueField)) I))
  ((Ideal.Quotient.mk
          (Ideal.map (F := R[X] →+* P.ResidueField[X]) (mapRingHom (algebraMap R P.ResidueField))
            (RingHom.ker (F := RingHom.{u_1, u_3} R[X] S) (↑(aeval x) : R[X] →+* S))) :
        (a : P.ResidueField[X]) → P.ResidueField[X] ⧸ Ideal.map (mapRingHom (algebraMap R P.ResidueField)) I)
      ((C : (a : P.ResidueField) → P.ResidueField[X]) ((algebraMap R P.ResidueField : (a : R) → P.ResidueField) a)) :
    HasQuotient.Quotient P.ResidueField[X] (B := Ideal P.ResidueField[X])
      (Ideal.map (F := R[X] →+* P.ResidueField[X]) (mapRingHom (algebraMap R P.ResidueField)) I))
Tactic: dsimp [-TensorProduct.algebraMap_apply]