-- Lean 4 proof step from Mathlib.NumberTheory.KummerDedekind (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
I : Ideal R
inst_3 : IsDomain R
inst_4 : IsIntegrallyClosed R
inst_5 : IsDedekindDomain S
inst_6 : Module.IsTorsionFree R S
hx : comap (F := R →+* S) (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
Q : R[X]
⊢ Eq.{u_1 + 1} (α :=
    HasQuotient.Quotient (R ⧸ I)[X] (B := Ideal (R ⧸ I)[X]) (span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)}))
    ((quotMapEquivQuotQuotMap hx hx' :
          (a : S ⧸ Ideal.map (algebraMap R S) I) →
            (R ⧸ I)[X] ⧸ span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)})
        (((quotMapEquivQuotQuotMap hx hx').symm :
            (a : (R ⧸ I)[X] ⧸ span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)}) →
              S ⧸ Ideal.map (algebraMap R S) I)
          ((Ideal.Quotient.mk (span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)}) :
              (a : (R ⧸ I)[X]) → (R ⧸ I)[X] ⧸ span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)})
            (Polynomial.map (Ideal.Quotient.mk I) Q))) :
      HasQuotient.Quotient (R ⧸ I)[X] (B := Ideal (R ⧸ I)[X])
        (span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)}))
    ((quotMapEquivQuotQuotMap hx hx' :
          (a : S ⧸ Ideal.map (algebraMap R S) I) →
            (R ⧸ I)[X] ⧸ span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)})
        ((Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) I) : (a : S) → S ⧸ Ideal.map (algebraMap R S) I)
          ((aeval x : (a : R[X]) → S) Q)) :
      HasQuotient.Quotient (R ⧸ I)[X] (B := Ideal (R ⧸ I)[X])
        (span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)}))
have a : Eq.{u_1 + 1} (α :=
  HasQuotient.Quotient (R ⧸ I)[X] (B := Ideal (R ⧸ I)[X]) (span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)}))
  (((((adjoin.powerBasis' hx').quotientEquivQuotientMinpolyMap I).toRingEquiv.trans (quotEquivOfEq sorry) :
          RingEquiv.{u_2, u_1}
            (HasQuotient.Quotient ↥R[x] (B := Ideal ↥R[x])
              (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I))
            (HasQuotient.Quotient (R ⧸ I)[X] (B := Ideal (R ⧸ I)[X])
              (span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)}))) :
        (a : ↥R[x] ⧸ Ideal.map (algebraMap R ↥R[x]) I) →
          (R ⧸ I)[X] ⧸ span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)})
      ((((adjoin.powerBasis' hx').quotientEquivQuotientMinpolyMap I).toRingEquiv.symm :
          (a : (R ⧸ I)[X] ⧸ span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R (adjoin.powerBasis' hx').gen)}) →
            ↥R[x] ⧸ Ideal.map (algebraMap R ↥R[x]) I)
        ((Ideal.Quotient.mk (span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R (adjoin.powerBasis' hx').gen)}) :
            (a : (R ⧸ I)[X]) →
              (R ⧸ I)[X] ⧸ span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R (adjoin.powerBasis' hx').gen)})
          (Polynomial.map (Ideal.Quotient.mk I) Q))) :
    HasQuotient.Quotient (R ⧸ I)[X] (B := Ideal (R ⧸ I)[X]) (span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)}))
  (Function.comp (α := HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I)) (β :=
      HasQuotient.Quotient ↥R[x] (B := Ideal ↥R[x])
        (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I))
      (⇑(((adjoin.powerBasis' hx').quotientEquivQuotientMinpolyMap I).toRingEquiv.trans (quotEquivOfEq sorry)) :
        (a : ↥R[x] ⧸ Ideal.map (algebraMap R ↥R[x]) I) →
          (R ⧸ I)[X] ⧸ span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)})
      ((⇑(quotAdjoinEquivQuotMap hx sorry).symm :
          (a : HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I)) →
            HasQuotient.Quotient ↥R[x] (B := Ideal ↥R[x])
              (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I)) :
        (a : HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I)) →
          HasQuotient.Quotient ↥R[x] (B := Ideal ↥R[x])
            (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I))
      ((Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) I) : (a : S) → S ⧸ Ideal.map (algebraMap R S) I)
          ((aeval x : (a : R[X]) → S) Q) :
        HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I)) :
    HasQuotient.Quotient (R ⧸ I)[X] (B := Ideal (R ⧸ I)[X]) (span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)}))
Tactic: rw [quotMapEquivQuotQuotMap, RingEquiv.symm_trans_apply,
    RingEquiv.symm_symm, RingEquiv.coe_trans, Function.comp_apply, RingEquiv.symm_apply_apply,
    RingEquiv.symm_trans_apply, quotEquivOfEq_symm, quotEquivOfEq_mk]