-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
pb : PowerBasis R S
I : Ideal R
x : R
rw :
  Eq.{u_1 + 1} (α :=
    HasQuotient.Quotient (AdjoinRoot (minpoly R pb.gen)) (B := Ideal (AdjoinRoot (minpoly R pb.gen)))
      (Ideal.map (F := R →+* AdjoinRoot (minpoly R pb.gen)) (of (minpoly R pb.gen)) I))
    (((quotientEquiv (Ideal.map (F := R →+* S) (algebraMap R S) I)
              (Ideal.map (F := R →+* AdjoinRoot (minpoly R pb.gen)) (of (minpoly R pb.gen)) I)
              (equiv' (minpoly R pb.gen) pb ⋯ ⋯).symm.toRingEquiv ⋯ :
            RingEquiv.{u_2, u_1} (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I))
              (HasQuotient.Quotient (AdjoinRoot (minpoly R pb.gen)) (B := Ideal (AdjoinRoot (minpoly R pb.gen)))
                (Ideal.map (F := R →+* AdjoinRoot (minpoly R pb.gen)) (of (minpoly R pb.gen)) I))) :
          (a : S ⧸ Ideal.map (algebraMap R S) I) → AdjoinRoot (minpoly R pb.gen) ⧸ Ideal.map (of (minpoly R pb.gen)) I)
        ((Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) I) : (a : S) → S ⧸ Ideal.map (algebraMap R S) I)
          ((algebraMap R S : (a : R) → S) x)) :
      HasQuotient.Quotient (AdjoinRoot (minpoly R pb.gen)) (B := Ideal (AdjoinRoot (minpoly R pb.gen)))
        (Ideal.map (F := R →+* AdjoinRoot (minpoly R pb.gen)) (of (minpoly R pb.gen)) I))
    ((algebraMap R
            (HasQuotient.Quotient (AdjoinRoot (minpoly R pb.gen)) (B := Ideal (AdjoinRoot (minpoly R pb.gen)))
              (Ideal.map (F := R →+* AdjoinRoot (minpoly R pb.gen)) (of (minpoly R pb.gen)) I)) :
          (a : R) → AdjoinRoot (minpoly R pb.gen) ⧸ Ideal.map (of (minpoly R pb.gen)) I)
        x :
      HasQuotient.Quotient (AdjoinRoot (minpoly R pb.gen)) (B := Ideal (AdjoinRoot (minpoly R pb.gen)))
        (Ideal.map (F := R →+* AdjoinRoot (minpoly R pb.gen)) (of (minpoly R pb.gen)) I))
⊢ Eq.{u_1 + 1} (α :=
    HasQuotient.Quotient (AdjoinRoot (minpoly R pb.gen)) (B := Ideal (AdjoinRoot (minpoly R pb.gen)))
      (Ideal.map (F := R →+* AdjoinRoot (minpoly R pb.gen)) (of (minpoly R pb.gen)) I))
    (((quotientEquiv (Ideal.map (F := R →+* S) (algebraMap R S) I)
              (Ideal.map (F := R →+* AdjoinRoot (minpoly R pb.gen)) (of (minpoly R pb.gen)) I)
              (equiv' (minpoly R pb.gen) pb ⋯ ⋯).symm.toRingEquiv ⋯ :
            RingEquiv.{u_2, u_1} (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I))
              (HasQuotient.Quotient (AdjoinRoot (minpoly R pb.gen)) (B := Ideal (AdjoinRoot (minpoly R pb.gen)))
                (Ideal.map (F := R →+* AdjoinRoot (minpoly R pb.gen)) (of (minpoly R pb.gen)) I))) :
          (a : S ⧸ Ideal.map (algebraMap R S) I) → AdjoinRoot (minpoly R pb.gen) ⧸ Ideal.map (of (minpoly R pb.gen)) I)
        ((algebraMap R (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I)) :
            (a : R) → S ⧸ Ideal.map (algebraMap R S) I)
          x) :
      HasQuotient.Quotient (AdjoinRoot (minpoly R pb.gen)) (B := Ideal (AdjoinRoot (minpoly R pb.gen)))
        (Ideal.map (F := R →+* AdjoinRoot (minpoly R pb.gen)) (of (minpoly R pb.gen)) I))
    ((algebraMap R
            (HasQuotient.Quotient (AdjoinRoot (minpoly R pb.gen)) (B := Ideal (AdjoinRoot (minpoly R pb.gen)))
              (Ideal.map (F := R →+* AdjoinRoot (minpoly R pb.gen)) (of (minpoly R pb.gen)) I)) :
          (a : R) → AdjoinRoot (minpoly R pb.gen) ⧸ Ideal.map (of (minpoly R pb.gen)) I)
        x :
      HasQuotient.Quotient (AdjoinRoot (minpoly R pb.gen)) (B := Ideal (AdjoinRoot (minpoly R pb.gen)))
        (Ideal.map (F := R →+* AdjoinRoot (minpoly R pb.gen)) (of (minpoly R pb.gen)) I))
have rw₁ : OneHom.toFun
    (↑(↑(quotientMap (Ideal.map (F := R →+* AdjoinRoot (minpoly R pb.gen)) (of (minpoly R pb.gen)) I)
              (↑(equiv' (minpoly R pb.gen) pb sorry sorry).symm.toRingEquiv : S →+* AdjoinRoot (minpoly R pb.gen)) sorry) :
          S ⧸ Ideal.map (algebraMap R S) I →* AdjoinRoot (minpoly R pb.gen) ⧸ Ideal.map (of (minpoly R pb.gen)) I) :
      OneHom (S ⧸ Ideal.map (algebraMap R S) I) (AdjoinRoot (minpoly R pb.gen) ⧸ Ideal.map (of (minpoly R pb.gen)) I))
    ((Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) I) : (a : S) → S ⧸ Ideal.map (algebraMap R S) I)
      ((algebraMap R S : (a : R) → S) x)) =
  (algebraMap R
        (HasQuotient.Quotient (AdjoinRoot (minpoly R pb.gen)) (B := Ideal (AdjoinRoot (minpoly R pb.gen)))
          (Ideal.map (F := R →+* AdjoinRoot (minpoly R pb.gen)) (of (minpoly R pb.gen)) I)) :
      (a : R) → AdjoinRoot (minpoly R pb.gen) ⧸ Ideal.map (of (minpoly R pb.gen)) I)
    x
Tactic: rw [← Ideal.Quotient.mk_algebraMap, Ideal.quotientEquiv_apply,
                    RingHom.toFun_eq_coe, Ideal.quotientMap_mk,
                    RingEquiv.coe_toRingHom, AlgEquiv.coe_ringEquiv, AlgEquiv.commutes,
                    Quotient.mk_algebraMap]