-- 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
⊢ 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 : 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 sorry sorry).symm.toRingEquiv sorry :
          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))
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]