-- 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))
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 ⋯ ⋯).symm.toRingEquiv : S →+* AdjoinRoot (minpoly R pb.gen)) ⋯) :
            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
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))
    (((quotientMap (Ideal.map (F := R →+* AdjoinRoot (minpoly R pb.gen)) (of (minpoly R pb.gen)) I)
              (↑(equiv' (minpoly R pb.gen) pb ⋯ ⋯).symm.toRingEquiv : S →+* AdjoinRoot (minpoly R pb.gen)) ⋯ :
            RingHom.{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))
rw₃ :
  Eq (α :=
    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))
    ((Ideal.Quotient.mk (Ideal.map (F := R →+* AdjoinRoot (minpoly R pb.gen)) (of (minpoly R pb.gen)) I) :
          (a : AdjoinRoot (minpoly R pb.gen)) → AdjoinRoot (minpoly R pb.gen) ⧸ Ideal.map (of (minpoly R pb.gen)) I)
        ((((↑(equiv' (minpoly R pb.gen) pb ⋯ ⋯).symm.toRingEquiv :
                RingHom.{u_2, u_1} S (AdjoinRoot (minpoly R pb.gen))) :
              RingHom.{u_2, u_1} S (AdjoinRoot (minpoly R pb.gen))) :
            (a : S) → AdjoinRoot (minpoly R pb.gen))
          ((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₄ : Eq (α :=
  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))
  ((Ideal.Quotient.mk (Ideal.map (F := R →+* AdjoinRoot (minpoly R pb.gen)) (of (minpoly R pb.gen)) I) :
        (a : AdjoinRoot (minpoly R pb.gen)) → AdjoinRoot (minpoly R pb.gen) ⧸ Ideal.map (of (minpoly R pb.gen)) I)
      (((equiv' (minpoly R pb.gen) pb sorry sorry).symm.toRingEquiv : (a : S) → AdjoinRoot (minpoly R pb.gen))
        ((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]