-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
pb : PowerBasis R S
I : Ideal R
g : R[X]
rw :
  Eq.{u_1 + 1} (α :=
    HasQuotient.Quotient (R ⧸ I)[X] (B := Ideal (R ⧸ I)[X])
      (span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R pb.gen)}))
    (((ofRingEquiv ⋯).trans (quotEquivQuotMap (minpoly R pb.gen) I) :
          (a : S ⧸ Ideal.map (algebraMap R S) I) →
            (R ⧸ I)[X] ⧸ span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R pb.gen)})
        ((Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) I) : (a : S) → S ⧸ Ideal.map (algebraMap R S) I)
          ((aeval pb.gen : (a : R[X]) → S) g)) :
      HasQuotient.Quotient (R ⧸ I)[X] (B := Ideal (R ⧸ I)[X])
        (span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R pb.gen)}))
    ((Ideal.Quotient.mk (span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R pb.gen)}) :
          (a : (R ⧸ I)[X]) → (R ⧸ I)[X] ⧸ span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R pb.gen)})
        (Polynomial.map (Ideal.Quotient.mk I) g) :
      HasQuotient.Quotient (R ⧸ I)[X] (B := Ideal (R ⧸ I)[X])
        (span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R pb.gen)}))
⊢ Eq.{u_1 + 1} (α :=
    HasQuotient.Quotient (R ⧸ I)[X] (B := Ideal (R ⧸ I)[X])
      (span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R pb.gen)}))
    ((pb.quotientEquivQuotientMinpolyMap I :
          (a : S ⧸ Ideal.map (algebraMap R S) I) →
            (R ⧸ I)[X] ⧸ span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R pb.gen)})
        ((Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) I) : (a : S) → S ⧸ Ideal.map (algebraMap R S) I)
          ((aeval pb.gen : (a : R[X]) → S) g)) :
      HasQuotient.Quotient (R ⧸ I)[X] (B := Ideal (R ⧸ I)[X])
        (span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R pb.gen)}))
    ((Ideal.Quotient.mk (span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R pb.gen)}) :
          (a : (R ⧸ I)[X]) → (R ⧸ I)[X] ⧸ span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R pb.gen)})
        (Polynomial.map (Ideal.Quotient.mk I) g) :
      HasQuotient.Quotient (R ⧸ I)[X] (B := Ideal (R ⧸ I)[X])
        (span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R pb.gen)}))
have rw₁ : Eq (α :=
  HasQuotient.Quotient (R ⧸ I)[X] (B := Ideal (R ⧸ I)[X])
    (span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R pb.gen)}))
  ((quotEquivQuotMap (minpoly R pb.gen) I :
        (a : AdjoinRoot (minpoly R pb.gen) ⧸ Ideal.map (of (minpoly R pb.gen)) I) →
          (R ⧸ I)[X] ⧸ span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R pb.gen)})
      ((ofRingEquiv sorry :
          (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)
          ((aeval pb.gen : (a : R[X]) → S) g))) :
    HasQuotient.Quotient (R ⧸ I)[X] (B := Ideal (R ⧸ I)[X])
      (span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R pb.gen)}))
  ((Ideal.Quotient.mk (span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R pb.gen)}) :
        (a : (R ⧸ I)[X]) → (R ⧸ I)[X] ⧸ span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R pb.gen)})
      (Polynomial.map (Ideal.Quotient.mk I) g) :
    HasQuotient.Quotient (R ⧸ I)[X] (B := Ideal (R ⧸ I)[X])
      (span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R pb.gen)}))
Tactic: rw [PowerBasis.quotientEquivQuotientMinpolyMap, AlgEquiv.trans_apply, AlgEquiv.ofRingEquiv_apply,
    quotientEquiv_mk, AlgEquiv.coe_ringEquiv', AdjoinRoot.equiv'_symm_apply, PowerBasis.lift_aeval,
    AdjoinRoot.aeval_eq, AdjoinRoot.quotEquivQuotMap_apply_mk]