-- Module: Mathlib.RingTheory.Unramified.LocalStructure
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))
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))
⊢ 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))))

Tactic:
ext a