awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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) ⊥
rwa₂ rwa₃ rwa₄ rwa₅ : ¬I = ⊥
⊢ Ne.{u_2 + 1} (α := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I) 0

Tactic:
rwa [← bot_eq_zero, Ne,
            map_eq_bot_iff_of_injective (FaithfulSMul.algebraMap_injective R S)]

Premises used: Ideal.map_eq_bot_iff_of_injective, Ne, FaithfulSMul.algebraMap_injective, bot_eq_zero
-- 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
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}
⊢ 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)])
-- 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
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)
⊢ y = Ideal.map (F := R →+* S) (algebraMap R S) I

Tactic:
rw [associated_iff_eq, hy, Multiset.prod_singleton] at h

Premises used: Multiset.prod_singleton, associated_iff_eq
-- 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
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
rw : Irreducible y
⊢ Irreducible.{u_2} (M := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I)

Tactic:
rw [← h]
-- 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
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
⊢ Membership.mem (γ := Multiset (Ideal S)) (normalizedFactors (Ideal.map (F := R →+* S) (algebraMap R S) I)) y

Tactic:
simp [hy]
-- 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
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 y

Tactic:
exact
      irreducible_of_normalized_factor y
        (show y ∈ normalizedFactors (I.map (algebraMap R S)) by simp [hy])

Premises used: UniqueFactorizationMonoid.irreducible_of_normalized_factor
-- 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
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])
suffices :
  ∃ (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)

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])
-- 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
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])
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}
⊢ ∃ (y : Ideal S), Eq (α := Multiset (Ideal S)) (normalizedFactors (Ideal.map (F := R →+* S) (algebraMap R S) I)) {y}

Tactic:
rw [normalizedFactors_ideal_map_eq_normalizedFactors_min_poly_mk_map hI hI' hx hx']

Premises used: KummerDedekind.normalizedFactors_ideal_map_eq_normalizedFactors_min_poly_mk_map
-- 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
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])
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 })))
⊢ (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 })

Tactic:
apply Multiset.map_injective Subtype.coe_injective

Premises used: Subtype.coe_injective, Multiset.map_injective
-- 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
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])
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])
⊢ 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:
rw [Multiset.attach_map_val, Multiset.map_singleton, Subtype.coe_mk]

Premises used: Subtype.coe_mk, Multiset.map_singleton, Multiset.attach_map_val
-- 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
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)) =
    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:
normalizedFactors_irreducible hf

Premises used: UniqueFactorizationMonoid.normalizedFactors_irreducible
-- 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
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)) =
    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:
exact normalizedFactors_irreducible hf

Premises used: UniqueFactorizationMonoid.normalizedFactors_irreducible
-- 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
hI : I.IsMaximal
Q : R[X]
hQ : Polynomial.map (Ideal.Quotient.mk I) Q ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))
hI' : I ≠ ⊥
hx : comap (F := R →+* S) (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
simp :
  Eq (α := Ideal S)
    (comap (F := S →+* HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I))
      (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) I))
      (span
        (singleton (α := HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) 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)))))
    (span
      ((↑(Ideal.map (F := R →+* S) (algebraMap R S) I) : Set S) ∪
        singleton (α := S) ((aeval x : (a : R[X]) → S) Q : S)))
⊢ Eq (α := Ideal S)
    (comap (F := S →+* HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I))
      (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) I))
      (Ideal.map (R :=
        HasQuotient.Quotient (R ⧸ I)[X] (B := Ideal (R ⧸ I)[X])
          (span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)}))
        (F :=
        RingHom.{u_1, u_2}
          (HasQuotient.Quotient (R ⧸ I)[X] (B := Ideal (R ⧸ I)[X])
            (span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)}))
          (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I)))
        (↑(quotMapEquivQuotQuotMap hx hx').symm :
          (R ⧸ I)[X] ⧸ span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)} →+* S ⧸ Ideal.map (algebraMap R S) I)
        (Ideal.map (R := (R ⧸ I)[X]) (F :=
          (R ⧸ I)[X] →+*
            HasQuotient.Quotient (R ⧸ I)[X] (B := Ideal (R ⧸ I)[X])
              (span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)}))
          (Ideal.Quotient.mk (span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)}))
          (span {Polynomial.map (Ideal.Quotient.mk I) Q}))))
    (span
      ((↑(Ideal.map (F := R →+* S) (algebraMap R S) I) : Set S) ∪
        singleton (α := S) ((aeval x : (a : R[X]) → S) Q : S)))

Tactic:
simp only [map_span, image_singleton, coe_coe, quotMapEquivQuotQuotMap_symm_apply hx hx' Q]

Premises used: Set.image_singleton, RingHom.coe_coe, Ideal.map_span, KummerDedekind.quotMapEquivQuotQuotMap_symm_apply
-- 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
hI : I.IsMaximal
Q : R[X]
hQ : Polynomial.map (Ideal.Quotient.mk I) Q ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))
hI' : I ≠ ⊥
hx : comap (F := R →+* S) (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
⊢ LE.le (α := Ideal (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I)))
    (Ideal.map (R := S) (F := S →+* HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I))
      (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) I)) (Ideal.map (F := R →+* S) (algebraMap R S) I))
    (span
      (singleton (α := HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) 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))))

Tactic:
simp
-- 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
hI : I.IsMaximal
Q : R[X]
hQ : Polynomial.map (Ideal.Quotient.mk I) Q ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))
hI' : I ≠ ⊥
hx : comap (F := R →+* S) (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
⊢ singleton (α := S) ((aeval x : (a : R[X]) → S) Q : S) ⊆
    (↑(comap (F := S →+* HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I))
          (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) I))
          (span
            (singleton (α := HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) 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))))) :
      Set S)

Tactic:
simp