-- 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.{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))
have h : 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))
  ((algebraMap 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)) :
        (a : P.ResidueField) → P.ResidueField[X] ⧸ Ideal.map (mapRingHom (algebraMap R P.ResidueField)) I)
      ((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: rw [aeval_C, AlgEquiv.commutes]