awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ Ne.{u_2 + 1} (α := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I) ⊥
have refine_1 : ¬Eq.{u_2 + 1} (α := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I) ⊥
Tactic: rwa [Ne, map_eq_bot_iff_of_injective (FaithfulSMul.algebraMap_injective R S), ← Ne]
-- 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
refine_1 : ¬Eq.{u_2 + 1} (α := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I) ⊥
⊢ Ne.{u_2 + 1} (α := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I) ⊥
have refine_1₁ : ¬I = ⊥
Tactic: rwa [Ne, map_eq_bot_iff_of_injective (FaithfulSMul.algebraMap_injective R S), ← Ne]
-- 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
⊢ (↑{M : Ideal (R ⧸ I)[X] |
          Membership.mem (γ := Multiset (Ideal (R ⧸ I)[X]))
            (normalizedFactors (span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)})) M} :
      Type u_1) ≃
    (↑{d : (R ⧸ I)[X] | d ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))} : Type u_1)
have refine_3 : Polynomial.map (Ideal.Quotient.mk I) (minpoly R x) ≠ 0
Tactic: refine (Ideal.normalizedFactorsEquivSpanNormalizedFactors ?_).symm
-- Lean 4 proof step from Mathlib.NumberTheory.KummerDedekind (hypothesis)
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))
⊢ Irreducible.{u_2} (M := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I)
have 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])
Tactic: have mem_norm_factors : normalize (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)) ∈
      normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)) := by
    simp [normalizedFactors_irreducible hf]
-- 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])
this :
  ∃ (y : Ideal S), Eq (α := Multiset (Ideal S)) (normalizedFactors (Ideal.map (F := R →+* S) (algebraMap R S) I)) {y}
⊢ Irreducible.{u_2} (M := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I)
have obtain : ∀ (y : Ideal S)
  (hy : Eq (α := Multiset (Ideal S)) (normalizedFactors (Ideal.map (F := R →+* S) (algebraMap R S) I)) {y}),
  Irreducible.{u_2} (M := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I)
Tactic: obtain ⟨y, hy⟩ := this
Cleared hypotheses: this
-- 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])
y : Ideal S
hy : Eq (α := Multiset (Ideal S)) (normalizedFactors (Ideal.map (F := R →+* S) (algebraMap R S) I)) {y}
⊢ Ne.{u_2 + 1} (α := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I) 0
have rwa : Ne.{u_2 + 1} (α := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I) ⊥
Tactic: rwa [← bot_eq_zero, Ne,
            map_eq_bot_iff_of_injective (FaithfulSMul.algebraMap_injective R S)]
-- 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])
y : Ideal S
hy : Eq (α := Multiset (Ideal S)) (normalizedFactors (Ideal.map (F := R →+* S) (algebraMap R S) I)) {y}
rwa : Ne.{u_2 + 1} (α := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I) ⊥
⊢ Ne.{u_2 + 1} (α := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I) 0
have rwa₁ : ¬Eq.{u_2 + 1} (α := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I) ⊥
Tactic: rwa [← bot_eq_zero, Ne,
            map_eq_bot_iff_of_injective (FaithfulSMul.algebraMap_injective R S)]
-- 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])
y : Ideal S
hy : Eq (α := Multiset (Ideal S)) (normalizedFactors (Ideal.map (F := R →+* S) (algebraMap R S) I)) {y}
rwa : Ne.{u_2 + 1} (α := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I) ⊥
rwa₁ : ¬Eq.{u_2 + 1} (α := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I) ⊥
⊢ Ne.{u_2 + 1} (α := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I) 0
have rwa₂ : ¬I = ⊥
Tactic: rwa [← bot_eq_zero, Ne,
            map_eq_bot_iff_of_injective (FaithfulSMul.algebraMap_injective R S)]
-- Lean 4 proof step from Mathlib.NumberTheory.KummerDedekind (hypothesis)
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])
y : Ideal S
hy : Eq (α := Multiset (Ideal S)) (normalizedFactors (Ideal.map (F := R →+* S) (algebraMap R S) I)) {y}
⊢ Irreducible.{u_2} (M := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I)
have h : Associated.{u_2} (M := Ideal S) (Multiset.prod (normalizedFactors (Ideal.map (F := R →+* S) (algebraMap R S) I)))
  (Ideal.map (F := R →+* S) (algebraMap R S) I)
Tactic: have h := prod_normalizedFactors (show I.map (algebraMap R S) ≠ 0 by
          rwa [← bot_eq_zero, Ne,
            map_eq_bot_iff_of_injective (FaithfulSMul.algebraMap_injective R S)])
-- Lean 4 proof step from Mathlib.NumberTheory.KummerDedekind (hypothesis)
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])
y : Ideal S
hy : Eq (α := Multiset (Ideal S)) (normalizedFactors (Ideal.map (F := R →+* S) (algebraMap R S) I)) {y}
h :
  Associated.{u_2} (M := Ideal S) (Multiset.prod (normalizedFactors (Ideal.map (F := R →+* S) (algebraMap R S) I)))
    (Ideal.map (F := R →+* S) (algebraMap R S) I)
⊢ Irreducible.{u_2} (M := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I)
have h₁ : y = Ideal.map (F := R →+* S) (algebraMap R S) I
Tactic: rw [associated_iff_eq, hy, Multiset.prod_singleton] at h
Cleared hypotheses: h
-- 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])
y : Ideal S
hy : Eq (α := Multiset (Ideal S)) (normalizedFactors (Ideal.map (F := R →+* S) (algebraMap R S) I)) {y}
h : y = Ideal.map (F := R →+* S) (algebraMap R S) I
⊢ Irreducible.{u_2} (M := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I)
have rw : Irreducible y
Tactic: rw [← h]
-- 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])
⊢ Irreducible.{u_2} (M := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I)
have suffices : ∃ (y : Ideal S), Eq (α := Multiset (Ideal S)) (normalizedFactors (Ideal.map (F := R →+* S) (algebraMap R S) I)) {y}
Tactic: suffices ∃ y, normalizedFactors (I.map (algebraMap R S)) = {y} by
    obtain ⟨y, hy⟩ := this
    have h := prod_normalizedFactors (show I.map (algebraMap R S) ≠ 0 by
          rwa [← bot_eq_zero, Ne,
            map_eq_bot_iff_of_injective (FaithfulSMul.algebraMap_injective R S)])
    rw [associated_iff_eq, hy, Multiset.prod_singleton] at h
    rw [← h]
    exact
      irreducible_of_normalized_factor y
        (show y ∈ normalizedFactors (I.map (algebraMap R S)) by simp [hy])
-- 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])
⊢ ∃ (y : Ideal S), Eq (α := Multiset (Ideal S)) (normalizedFactors (Ideal.map (F := R →+* S) (algebraMap R S) I)) {y}
have rw : ∃ (y : Ideal S),
  Eq (α := Multiset (Ideal S))
    (Multiset.map
      (fun
          (f :
            (↑{d : (R ⧸ I)[X] | d ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))} :
              Type u_1)) ↦
        (↑(((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))
              f) :
          Ideal S))
      (normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))).attach)
    {y}
Tactic: rw [normalizedFactors_ideal_map_eq_normalizedFactors_min_poly_mk_map hI hI' hx hx']
-- 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])
⊢ (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 })
have h : Eq (α := Multiset (R ⧸ I)[X])
  (Multiset.map
    (fun (a : { x_1 : (R ⧸ I)[X] // x_1 ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)) }) ↦
      (↑a : (R ⧸ I)[X]))
    (normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))).attach)
  (Multiset.map
    (fun (a : { x_1 : (R ⧸ I)[X] // x_1 ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)) }) ↦
      (↑a : (R ⧸ I)[X]))
    (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 })))
Tactic: apply Multiset.map_injective Subtype.coe_injective
-- 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])
⊢ Eq (α := Multiset (R ⧸ I)[X])
    (Multiset.map
      (fun (a : { x_1 : (R ⧸ I)[X] // x_1 ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)) }) ↦
        (↑a : (R ⧸ I)[X]))
      (normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))).attach)
    (Multiset.map
      (fun (a : { x_1 : (R ⧸ I)[X] // x_1 ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)) }) ↦
        (↑a : (R ⧸ I)[X]))
      (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 })))
have h : normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)) =
  singleton (α := (R ⧸ I)[X])
    ((normalize : (a : (R ⧸ I)[X]) → (R ⧸ I)[X]) (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)) : (R ⧸ I)[X])
Tactic: rw [Multiset.attach_map_val, Multiset.map_singleton, Subtype.coe_mk]
-- 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))
⊢ Irreducible.{u_2} (M := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I)
have have : 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])
Tactic: classical
  have mem_norm_factors : normalize (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)) ∈
      normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)) := by
    simp [normalizedFactors_irreducible hf]
  suffices ∃ y, normalizedFactors (I.map (algebraMap R S)) = {y} by
    obtain ⟨y, hy⟩ := this
    have h := prod_normalizedFactors (show I.map (algebraMap R S) ≠ 0 by
          rwa [← bot_eq_zero, Ne,
            map_eq_bot_iff_of_injective (FaithfulSMul.algebraMap_injective R S)])
    rw [associated_iff_eq, hy, Multiset.prod_singleton] at h
    rw [← h]
    exact
      irreducible_of_normalized_factor y
        (show y ∈ normalizedFactors (I.map (algebraMap R S)) by simp [hy])
  rw [normalizedFactors_ideal_map_eq_normalizedFactors_min_poly_mk_map hI hI' hx hx']
  use ((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx').symm
        ⟨normalize (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)), mem_norm_factors⟩ :
      Ideal S)
  rw [Multiset.map_eq_singleton]
  use ⟨normalize (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)), mem_norm_factors⟩
  refine ⟨?_, rfl⟩
  apply Multiset.map_injective Subtype.coe_injective
  rw [Multiset.attach_map_val, Multiset.map_singleton, Subtype.coe_mk]
  exact normalizedFactors_irreducible hf