-- 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)}))
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 ⋯ :
            (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)}))
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)})
        (((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)
            ((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)}))
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)})
        ((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 : (a : S) → AdjoinRoot (minpoly R pb.gen))
            ((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)}))
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)})
        ((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 : (a : S) → AdjoinRoot (minpoly R pb.gen))
            ((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)}))
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)})
        ((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)
          ((pb.lift (root (minpoly R pb.gen)) ⋯ : (a : S) → AdjoinRoot (minpoly R pb.gen))
            ((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)}))
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)})
        ((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)
          ((aeval (root (minpoly R pb.gen)) : (a : R[X]) → AdjoinRoot (minpoly R pb.gen)) 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)}))
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)})
        ((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)
          ((AdjoinRoot.mk (minpoly R pb.gen) : (a : R[X]) → AdjoinRoot (minpoly R pb.gen)) 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)}))
  ((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)}))
  ((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]