awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.JacobiSum.Basic
Goal:
F : Type u_1
R : Type u_2
inst : Fintype F
inst_1 : Field F
inst_2 : CommRing R
inst_3 : IsDomain R
χ : MulChar F R
ψ : AddChar F R
hχ : 2 ≤ orderOf χ
hψ : AddChar.IsPrimitive.{u_1, u_2} (R := F) (R' := R) ψ
this :
  gaussSum χ ψ ^ orderOf χ =
    gaussSum χ ψ * (gaussSum (χ ^ (orderOf χ - 1)) ψ * ∏ j ∈ Ico 1 (orderOf χ - 1), jacobiSum χ (χ ^ j))
hχ₁ : χ ≠ 1
rw :
  gaussSum χ ψ * (gaussSum (χ ^ (orderOf χ - 1)) ψ * ∏ j ∈ Ico 1 (orderOf χ - 1), jacobiSum χ (χ ^ j)) =
    HMul.hMul (α := R) (β := R) ((χ : (a : F) → R) (-1) : R) ((↑(Fintype.card F) : R) : R) *
      ∏ i ∈ Ico 1 (orderOf χ - 1), jacobiSum χ (χ ^ i)
rw₁ :
  gaussSum χ ψ * gaussSum (χ ^ (orderOf χ - 1)) ψ * ∏ j ∈ Ico 1 (orderOf χ - 1), jacobiSum χ (χ ^ j) =
    HMul.hMul (α := R) (β := R) ((χ : (a : F) → R) (-1) : R) ((↑(Fintype.card F) : R) : R) *
      ∏ i ∈ Ico 1 (orderOf χ - 1), jacobiSum χ (χ ^ i)
rw₂ rw₃ :
  HMul.hMul (α := R) (β := R) ((χ : (a : F) → R) (-1) : R) ((↑(Fintype.card F) : R) : R) *
      ∏ j ∈ Ico 1 (orderOf χ - 1), jacobiSum χ (χ ^ j) =
    HMul.hMul (α := R) (β := R) ((χ : (a : F) → R) (-1) : R) ((↑(Fintype.card F) : R) : R) *
      ∏ i ∈ Ico 1 (orderOf χ - 1), jacobiSum χ (χ ^ i)
⊢ gaussSum χ ψ ^ orderOf χ =
    HMul.hMul (α := R) (β := R) ((χ : (a : F) → R) (-1) : R) ((↑(Fintype.card F) : R) : R) *
      ∏ i ∈ Ico 1 (orderOf χ - 1), jacobiSum χ (χ ^ i)

Tactic:
rw [this, ← mul_assoc, gaussSum_mul_gaussSum_pow_orderOf_sub_one hχ₁ hψ]

Premises used: mul_assoc, gaussSum_mul_gaussSum_pow_orderOf_sub_one
-- 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
rw rw₁ :
  Eq (α := Ideal (R ⧸ I)[X]) (span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R (adjoin.powerBasis' hx').gen)})
    (span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R (adjoin.powerBasis' hx').gen)})
⊢ Eq (α := Ideal (R ⧸ I)[X]) (span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R (adjoin.powerBasis' hx').gen)})
    (span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)})

Tactic:
rw [Algebra.adjoin.powerBasis'_minpoly_gen hx']

Premises used: Algebra.adjoin.powerBasis'_minpoly_gen
-- 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)}))
    ((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)}))
⊢ Eq.{u_2 + 1} (α := HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I))
    (((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 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:
apply (quotMapEquivQuotQuotMap hx hx').injective

Premises used: RingEquiv.injective, KummerDedekind.quotMapEquivQuotQuotMap
-- 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]
⊢ 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).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))
    ((Ideal.Quotient.mk (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) :
          (a : ↥R[x]) → ↥R[x] ⧸ Ideal.map (algebraMap R ↥R[x]) I)
        ((aeval (adjoin.powerBasis' hx').gen : (a : R[X]) → ↥R[x]) 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:
(adjoin.powerBasis' hx').quotientEquivQuotientMinpolyMap_symm_apply_mk I Q

Premises used: PowerBasis.quotientEquivQuotientMinpolyMap_symm_apply_mk, Algebra.adjoin.powerBasis'
-- 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]
h :
  Eq (α :=
    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 ⋯).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))
    ((Ideal.Quotient.mk (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) :
          (a : ↥R[x]) → ↥R[x] ⧸ Ideal.map (algebraMap R ↥R[x]) I)
        ((aeval (adjoin.powerBasis' hx').gen : (a : R[X]) → ↥R[x]) 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))
⊢ 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 ⋯).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:
convert! (adjoin.powerBasis' hx').quotientEquivQuotientMinpolyMap_symm_apply_mk I Q

Premises used: PowerBasis.quotientEquivQuotientMinpolyMap_symm_apply_mk, Algebra.adjoin.powerBasis'
-- 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]
h :
  Eq (α := HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I))
    ((quotAdjoinEquivQuotMap hx ⋯ : (a : ↥R[x] ⧸ Ideal.map (algebraMap R ↥R[x]) I) → S ⧸ Ideal.map (algebraMap R S) I)
        (((quotAdjoinEquivQuotMap hx ⋯).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 S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I))
    ((quotAdjoinEquivQuotMap hx ⋯ : (a : ↥R[x] ⧸ Ideal.map (algebraMap R ↥R[x]) I) → S ⧸ Ideal.map (algebraMap R S) I)
        ((Ideal.Quotient.mk (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) :
            (a : ↥R[x]) → ↥R[x] ⧸ Ideal.map (algebraMap R ↥R[x]) I)
          ((aeval (adjoin.powerBasis' hx').gen : (a : R[X]) → ↥R[x]) Q)) :
      HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I))
⊢ Eq (α :=
    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 ⋯).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))
    ((Ideal.Quotient.mk (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) :
          (a : ↥R[x]) → ↥R[x] ⧸ Ideal.map (algebraMap R ↥R[x]) I)
        ((aeval (adjoin.powerBasis' hx').gen : (a : R[X]) → ↥R[x]) 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:
apply (quotAdjoinEquivQuotMap hx
    (FaithfulSMul.algebraMap_injective ((adjoin R {x})) S)).injective

Premises used: Algebra.adjoin, Membership.mem, RingEquiv.injective, Subtype, FaithfulSMul.algebraMap_injective, quotAdjoinEquivQuotMap, Singleton.singleton
-- 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]
⊢ Eq (α := HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I))
    ((quotAdjoinEquivQuotMap hx ⋯ : (a : ↥R[x] ⧸ Ideal.map (algebraMap R ↥R[x]) I) → S ⧸ Ideal.map (algebraMap R S) I)
        (((quotAdjoinEquivQuotMap hx ⋯).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 S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I))
    ((quotAdjoinEquivQuotMap hx ⋯ : (a : ↥R[x] ⧸ Ideal.map (algebraMap R ↥R[x]) I) → S ⧸ Ideal.map (algebraMap R S) I)
        ((Ideal.Quotient.mk (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) :
            (a : ↥R[x]) → ↥R[x] ⧸ Ideal.map (algebraMap R ↥R[x]) I)
          ((aeval (adjoin.powerBasis' hx').gen : (a : R[X]) → ↥R[x]) Q)) :
      HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I))

Tactic:
simp only [RingEquiv.apply_symm_apply, adjoin.powerBasis'_gen, quotAdjoinEquivQuotMap_apply_mk,
    coe_aeval_mk_apply]

Premises used: RingEquiv.apply_symm_apply, quotAdjoinEquivQuotMap_apply_mk, Polynomial.coe_aeval_mk_apply, Algebra.adjoin.powerBasis'_gen
-- 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
refine_1 : Ne.{u_2 + 1} (α := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I) ⊥
refine_2 : Ne (α := Ideal (R ⧸ I)[X]) (span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)}) ⊥
refine_3 :
  (↑{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)
⊢ Equiv.{u_2 + 1, u_1 + 1}
    (↑{J : Ideal S |
          Membership.mem (γ := Multiset (Ideal S)) (normalizedFactors (Ideal.map (F := R →+* S) (algebraMap R S) I))
            J} :
      Type u_2)
    (↑{d : (R ⧸ I)[X] | d ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))} : Type u_1)

Tactic:
refine (IsDedekindDomain.normalizedFactorsEquivOfQuotEquiv (quotMapEquivQuotQuotMap hx hx')
    ?_ ?_).trans ?_

Premises used: IsDedekindDomain.normalizedFactorsEquivOfQuotEquiv, Equiv.trans, KummerDedekind.quotMapEquivQuotQuotMap
-- 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
refine_1 : ¬Eq.{u_2 + 1} (α := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I) ⊥
refine_1₁ : ¬I = ⊥
refine_1₂ refine_1₃ refine_1₄ refine_1₅ : I ≠ ⊥
⊢ Ne.{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]

Premises used: Ideal.map_eq_bot_iff_of_injective, Ne, FaithfulSMul.algebraMap_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
refine_2 : ∀ (h : Eq (α := Ideal (R ⧸ I)[X]) (span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)}) ⊥), False
⊢ Ne (α := Ideal (R ⧸ I)[X]) (span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)}) ⊥

Tactic:
by_contra 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
h : Eq (α := Ideal (R ⧸ I)[X]) (span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)}) ⊥
⊢ False

Tactic:
(show Polynomial.map (Ideal.Quotient.mk I) (minpoly R x) ≠ 0 from
      Polynomial.map_monic_ne_zero (minpoly.monic hx')) (span_singleton_eq_bot.mp h)

Premises used: minpoly.monic, Ideal.span_singleton_eq_bot, Polynomial.map_monic_ne_zero, Iff.mp
-- 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
h : Eq (α := Ideal (R ⧸ I)[X]) (span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)}) ⊥
⊢ False

Tactic:
exact (show Polynomial.map (Ideal.Quotient.mk I) (minpoly R x) ≠ 0 from
      Polynomial.map_monic_ne_zero (minpoly.monic hx')) (span_singleton_eq_bot.mp h)

Premises used: minpoly.monic, Ideal.span_singleton_eq_bot, Polynomial.map_monic_ne_zero, Iff.mp
-- 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
refine_3 : Polynomial.map (Ideal.Quotient.mk I) (minpoly R x) ≠ 0
⊢ (↑{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)

Tactic:
refine (Ideal.normalizedFactorsEquivSpanNormalizedFactors ?_).symm

Premises used: Equiv.symm, Ideal.normalizedFactorsEquivSpanNormalizedFactors
-- 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
⊢ Polynomial.map (Ideal.Quotient.mk I) (minpoly R x) ≠ 0

Tactic:
Polynomial.map_monic_ne_zero (minpoly.monic hx')

Premises used: minpoly.monic, Polynomial.map_monic_ne_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
⊢ Polynomial.map (Ideal.Quotient.mk I) (minpoly R x) ≠ 0

Tactic:
exact Polynomial.map_monic_ne_zero (minpoly.monic hx')

Premises used: minpoly.monic, Polynomial.map_monic_ne_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))
⊢ 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:
simp [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))
⊢ 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]
-- 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])
this :
  ∃ (y : Ideal S), Eq (α := Multiset (Ideal S)) (normalizedFactors (Ideal.map (F := R →+* S) (algebraMap R S) I)) {y}
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)
⊢ Irreducible.{u_2} (M := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I)

Tactic:
obtain ⟨y, hy⟩ := this