-- 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)}))
    (((((adjoin.powerBasis' hx').quotientEquivQuotientMinpolyMap I).toRingEquiv.trans (quotEquivOfEq ⋯) :
            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 ⋯)) :
          (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 ⋯).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)}))
have a : Eq.{u_2 + 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))
  ((((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[x] (B := Ideal ↥R[x]) (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I))
  (((quotAdjoinEquivQuotMap hx sorry).symm :
        (a : S ⧸ Ideal.map (algebraMap R S) I) → ↥R[x] ⧸ Ideal.map (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 ↥R[x] (B := Ideal ↥R[x]) (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I))
Tactic: congr