-- Module: Mathlib.NumberTheory.KummerDedekind
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]
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 ⋯) :
            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)}))
⊢ 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)}))

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]

Premises used: Ideal.quotEquivOfEq_mk, RingEquiv.symm_apply_apply, KummerDedekind.quotMapEquivQuotQuotMap, RingEquiv.symm_trans_apply, Ideal.quotEquivOfEq_symm, RingEquiv.symm_symm, Function.comp_apply, RingEquiv.coe_trans