-- 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
h :
  ∀ (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))
⊢ e.toRingEquiv.toRingHom.comp (AlgHom.toRingHom (aeval (1 ⊗ₜ[R] x))) =
    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))))
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))
  ((e.toRingEquiv.toRingHom.comp (AlgHom.toRingHom (aeval (1 ⊗ₜ[R] x))) :
        (a : P.ResidueField[X]) → P.ResidueField[X] ⧸ Ideal.map (mapRingHom (algebraMap R P.ResidueField)) I)
      X :
    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) (AlgHom.toRingHom (aeval x)))) :
        (a : P.ResidueField[X]) → P.ResidueField[X] ⧸ Ideal.map (mapRingHom (algebraMap R P.ResidueField)) I)
      X :
    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: ext a