-- 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
hI : I.IsMaximal
hI' : I ≠ ⊥
hx : comap (F := R →+* S) (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
hf : Irreducible (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))
mem_norm_factors :
  Membership.mem (α := (R ⧸ I)[X]) (normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)))
    ((normalize : (a : (R ⧸ I)[X]) → (R ⧸ I)[X]) (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)) : (R ⧸ I)[X])
⊢ ∃ (a : (↑{d : (R ⧸ I)[X] | d ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))} : Type u_1)),
    (normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))).attach = {a} ∧
      Eq.{u_2 + 1} (α := Ideal S)
        (↑(((Equiv.symm (normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx') :
                  Equiv.{u_1 + 1, u_2 + 1}
                    (↑{d : (R ⧸ I)[X] | d ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))} :
                      Type u_1)
                    (↑{J : Ideal S |
                          Membership.mem (γ := Multiset (Ideal S))
                            (normalizedFactors (Ideal.map (F := R →+* S) (algebraMap R S) I)) J} :
                      Type u_2)) :
                (a :
                    (↑{d : (R ⧸ I)[X] | d ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))} :
                      Type u_1)) →
                  (↑{J : Ideal S | J ∈ normalizedFactors (Ideal.map (algebraMap R S) I)} : Type u_2))
              a) :
          Ideal S)
        (↑(((Equiv.symm (normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx') :
                  Equiv.{u_1 + 1, u_2 + 1}
                    (↑{d : (R ⧸ I)[X] | d ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))} :
                      Type u_1)
                    (↑{J : Ideal S |
                          Membership.mem (γ := Multiset (Ideal S))
                            (normalizedFactors (Ideal.map (F := R →+* S) (algebraMap R S) I)) J} :
                      Type u_2)) :
                (a :
                    (↑{d : (R ⧸ I)[X] | d ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))} :
                      Type u_1)) →
                  (↑{J : Ideal S | J ∈ normalizedFactors (Ideal.map (algebraMap R S) I)} : Type u_2))
              (Subtype.mk (p := fun (x_1 : (R ⧸ I)[X]) ↦
                Membership.mem (γ := Set (R ⧸ I)[X])
                  {d : (R ⧸ I)[X] | d ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))} x_1)
                ((normalize : (a : (R ⧸ I)[X]) → (R ⧸ I)[X]) (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)))
                mem_norm_factors)) :
          Ideal S)
have h : (normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))).attach =
    singleton (α :=
      (↑{d : (R ⧸ I)[X] | d ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))} : Type u_1))
      (Subtype.mk (p := fun (x_1 : (R ⧸ I)[X]) ↦
          Membership.mem (γ := Set (R ⧸ I)[X])
            {d : (R ⧸ I)[X] | d ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))} x_1)
          ((normalize : (a : (R ⧸ I)[X]) → (R ⧸ I)[X]) (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)))
          mem_norm_factors :
        { x_1 : (R ⧸ I)[X] //
          Membership.mem (γ := Set (R ⧸ I)[X])
            {d : (R ⧸ I)[X] | d ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))} x_1 }) ∧
  Eq.{u_2 + 1} (α := Ideal S)
    (↑(((Equiv.symm (normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx') :
              Equiv.{u_1 + 1, u_2 + 1}
                (↑{d : (R ⧸ I)[X] | d ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))} :
                  Type u_1)
                (↑{J : Ideal S |
                      Membership.mem (γ := Multiset (Ideal S))
                        (normalizedFactors (Ideal.map (F := R →+* S) (algebraMap R S) I)) J} :
                  Type u_2)) :
            (a :
                (↑{d : (R ⧸ I)[X] | d ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))} :
                  Type u_1)) →
              (↑{J : Ideal S | J ∈ normalizedFactors (Ideal.map (algebraMap R S) I)} : Type u_2))
          (Subtype.mk (p := fun (x_1 : (R ⧸ I)[X]) ↦
            Membership.mem (γ := Set (R ⧸ I)[X])
              {d : (R ⧸ I)[X] | d ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))} x_1)
            ((normalize : (a : (R ⧸ I)[X]) → (R ⧸ I)[X]) (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)))
            mem_norm_factors)) :
      Ideal S)
    (↑(((Equiv.symm (normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx') :
              Equiv.{u_1 + 1, u_2 + 1}
                (↑{d : (R ⧸ I)[X] | d ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))} :
                  Type u_1)
                (↑{J : Ideal S |
                      Membership.mem (γ := Multiset (Ideal S))
                        (normalizedFactors (Ideal.map (F := R →+* S) (algebraMap R S) I)) J} :
                  Type u_2)) :
            (a :
                (↑{d : (R ⧸ I)[X] | d ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))} :
                  Type u_1)) →
              (↑{J : Ideal S | J ∈ normalizedFactors (Ideal.map (algebraMap R S) I)} : Type u_2))
          (Subtype.mk (p := fun (x_1 : (R ⧸ I)[X]) ↦
            Membership.mem (γ := Set (R ⧸ I)[X])
              {d : (R ⧸ I)[X] | d ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))} x_1)
            ((normalize : (a : (R ⧸ I)[X]) → (R ⧸ I)[X]) (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)))
            mem_norm_factors)) :
      Ideal S)
Tactic: use ⟨normalize (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)), mem_norm_factors⟩