awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.DedekindDomain.PID
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
S : Type u_2
inst_2 : CommRing S
inst_3 : Algebra R S
inst_4 : Module.IsTorsionFree R S
inst_5 : Module.Finite R S
p : Ideal R
hp0 : p ≠ ⊥
inst_6 : p.IsPrime
Sₚ : Type u_3
inst_7 : CommRing Sₚ
inst_8 : Algebra S Sₚ
inst_9 : IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ
inst_10 : Algebra R Sₚ
inst_11 : IsScalarTower R S Sₚ
inst_12 : IsDedekindDomain Sₚ
inst_13 : IsDomain S
P : Ideal Sₚ
hP : P.IsPrime
hP0 : P ≠ ⊥
non_zero_div : LE.le (α := Submonoid S) (Algebra.algebraMapSubmonoid S p.primeCompl) S⁰
this_1 : Algebra.{u_1, u_3} (Localization.AtPrime p) Sₚ := localizationAlgebra p.primeCompl S
this_2 : IsScalarTower R (Localization.AtPrime p) Sₚ
pid : IsPrincipalIdealRing.{u_1} (Localization.AtPrime p)
p' : Ideal (Localization.AtPrime p)
hpu : ∀ (y : Ideal (Localization.AtPrime p)), (fun (P : Ideal (Localization.AtPrime p)) ↦ P ≠ ⊥ ∧ P.IsPrime) y → y = p'
hp'0 : p' ≠ ⊥
hp'p : p'.IsPrime
this : Ne.{u_1 + 1} (α := Ideal (Localization.AtPrime p)) (IsLocalRing.maximalIdeal (Localization.AtPrime p)) ⊥
⊢ IsPrime (comap (F := RingHom.{u_1, u_3} (Localization.AtPrime p) Sₚ) (algebraMap (Localization.AtPrime p) Sₚ) P)

Tactic:
Ideal.comap_isPrime (algebraMap (Localization.AtPrime p) Sₚ) P

Premises used: Algebra.algebraMap, Localization.AtPrime, Ideal.comap_isPrime
-- Module: Mathlib.RingTheory.DedekindDomain.PID
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
S : Type u_2
inst_2 : CommRing S
inst_3 : Algebra R S
inst_4 : Module.IsTorsionFree R S
inst_5 : Module.Finite R S
p : Ideal R
hp0 : p ≠ ⊥
inst_6 : p.IsPrime
Sₚ : Type u_3
inst_7 : CommRing Sₚ
inst_8 : Algebra S Sₚ
inst_9 : IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ
inst_10 : Algebra R Sₚ
inst_11 : IsScalarTower R S Sₚ
inst_12 : IsDedekindDomain Sₚ
inst_13 : IsDomain S
P : Ideal Sₚ
hP : P.IsPrime
hP0 : P ≠ ⊥
non_zero_div : LE.le (α := Submonoid S) (Algebra.algebraMapSubmonoid S p.primeCompl) S⁰
this_1 : Algebra.{u_1, u_3} (Localization.AtPrime p) Sₚ := localizationAlgebra p.primeCompl S
this_2 : IsScalarTower R (Localization.AtPrime p) Sₚ
pid : IsPrincipalIdealRing.{u_1} (Localization.AtPrime p)
p' : Ideal (Localization.AtPrime p)
hpu : ∀ (y : Ideal (Localization.AtPrime p)), (fun (P : Ideal (Localization.AtPrime p)) ↦ P ≠ ⊥ ∧ P.IsPrime) y → y = p'
hp'0 : p' ≠ ⊥
hp'p : p'.IsPrime
this : Ne.{u_1 + 1} (α := Ideal (Localization.AtPrime p)) (IsLocalRing.maximalIdeal (Localization.AtPrime p)) ⊥
⊢ IsPrime (comap (F := RingHom.{u_1, u_3} (Localization.AtPrime p) Sₚ) (algebraMap (Localization.AtPrime p) Sₚ) P)

Tactic:
exact Ideal.comap_isPrime (algebraMap (Localization.AtPrime p) Sₚ) P

Premises used: Algebra.algebraMap, Localization.AtPrime, Ideal.comap_isPrime
-- Module: Mathlib.RingTheory.DedekindDomain.PID
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
S : Type u_2
inst_2 : CommRing S
inst_3 : Algebra R S
inst_4 : Module.IsTorsionFree R S
inst_5 : Module.Finite R S
p : Ideal R
hp0 : p ≠ ⊥
inst_6 : p.IsPrime
Sₚ : Type u_3
inst_7 : CommRing Sₚ
inst_8 : Algebra S Sₚ
inst_9 : IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ
inst_10 : Algebra R Sₚ
inst_11 : IsScalarTower R S Sₚ
inst_12 : IsDedekindDomain Sₚ
inst_13 : IsDomain S
P : Ideal Sₚ
hP : P.IsPrime
hP0 : P ≠ ⊥
non_zero_div : LE.le (α := Submonoid S) (Algebra.algebraMapSubmonoid S p.primeCompl) S⁰
this_1 : Algebra.{u_1, u_3} (Localization.AtPrime p) Sₚ := localizationAlgebra p.primeCompl S
this_2 : IsScalarTower R (Localization.AtPrime p) Sₚ
pid : IsPrincipalIdealRing.{u_1} (Localization.AtPrime p)
p' : Ideal (Localization.AtPrime p)
hpu : ∀ (y : Ideal (Localization.AtPrime p)), (fun (P : Ideal (Localization.AtPrime p)) ↦ P ≠ ⊥ ∧ P.IsPrime) y → y = p'
hp'0 : p' ≠ ⊥
hp'p : p'.IsPrime
this : Ne.{u_1 + 1} (α := Ideal (Localization.AtPrime p)) (IsLocalRing.maximalIdeal (Localization.AtPrime p)) ⊥
⊢ IsPrime.{u_1} (α := Localization.AtPrime p) (IsLocalRing.maximalIdeal (Localization.AtPrime p))

Tactic:
(IsLocalRing.maximalIdeal.isMaximal _).isPrime

Premises used: Ideal.IsMaximal.isPrime, IsLocalRing.maximalIdeal.isMaximal
-- Module: Mathlib.RingTheory.DedekindDomain.PID
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
S : Type u_2
inst_2 : CommRing S
inst_3 : Algebra R S
inst_4 : Module.IsTorsionFree R S
inst_5 : Module.Finite R S
p : Ideal R
hp0 : p ≠ ⊥
inst_6 : p.IsPrime
Sₚ : Type u_3
inst_7 : CommRing Sₚ
inst_8 : Algebra S Sₚ
inst_9 : IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ
inst_10 : Algebra R Sₚ
inst_11 : IsScalarTower R S Sₚ
inst_12 : IsDedekindDomain Sₚ
inst_13 : IsDomain S
P : Ideal Sₚ
hP : P.IsPrime
hP0 : P ≠ ⊥
non_zero_div : LE.le (α := Submonoid S) (Algebra.algebraMapSubmonoid S p.primeCompl) S⁰
this_1 : Algebra.{u_1, u_3} (Localization.AtPrime p) Sₚ := localizationAlgebra p.primeCompl S
this_2 : IsScalarTower R (Localization.AtPrime p) Sₚ
pid : IsPrincipalIdealRing.{u_1} (Localization.AtPrime p)
p' : Ideal (Localization.AtPrime p)
hpu : ∀ (y : Ideal (Localization.AtPrime p)), (fun (P : Ideal (Localization.AtPrime p)) ↦ P ≠ ⊥ ∧ P.IsPrime) y → y = p'
hp'0 : p' ≠ ⊥
hp'p : p'.IsPrime
this : Ne.{u_1 + 1} (α := Ideal (Localization.AtPrime p)) (IsLocalRing.maximalIdeal (Localization.AtPrime p)) ⊥
⊢ IsPrime.{u_1} (α := Localization.AtPrime p) (IsLocalRing.maximalIdeal (Localization.AtPrime p))

Tactic:
exact (IsLocalRing.maximalIdeal.isMaximal _).isPrime

Premises used: Ideal.IsMaximal.isPrime, IsLocalRing.maximalIdeal.isMaximal
-- Module: Mathlib.RingTheory.DedekindDomain.PID
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
S : Type u_2
inst_2 : CommRing S
inst_3 : Algebra R S
inst_4 : Module.IsTorsionFree R S
inst_5 : Module.Finite R S
p : Ideal R
hp0 : p ≠ ⊥
inst_6 : p.IsPrime
Sₚ : Type u_3
inst_7 : CommRing Sₚ
inst_8 : Algebra S Sₚ
inst_9 : IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ
inst_10 : Algebra R Sₚ
inst_11 : IsScalarTower R S Sₚ
inst_12 : IsDedekindDomain Sₚ
inst_13 : IsDomain S
P : Ideal Sₚ
hP : P.IsPrime
hP0 : P ≠ ⊥
non_zero_div : LE.le (α := Submonoid S) (Algebra.algebraMapSubmonoid S p.primeCompl) S⁰
this_1 : Algebra.{u_1, u_3} (Localization.AtPrime p) Sₚ := localizationAlgebra p.primeCompl S
this_2 : IsScalarTower R (Localization.AtPrime p) Sₚ
pid : IsPrincipalIdealRing.{u_1} (Localization.AtPrime p)
p' : Ideal (Localization.AtPrime p)
hpu : ∀ (y : Ideal (Localization.AtPrime p)), (fun (P : Ideal (Localization.AtPrime p)) ↦ P ≠ ⊥ ∧ P.IsPrime) y → y = p'
hp'0 : p' ≠ ⊥
hp'p : p'.IsPrime
this : Ne.{u_1 + 1} (α := Ideal (Localization.AtPrime p)) (IsLocalRing.maximalIdeal (Localization.AtPrime p)) ⊥
rw : ¬p = ⊥
rw₁ : Function.Injective.{u_1 + 1, u_3 + 1} (α := R) (β := Sₚ) (⇑(algebraMap R Sₚ) : (a : R) → Sₚ)
⊢ Ne.{u_3 + 1} (α := Ideal Sₚ) (Ideal.map (F := R →+* Sₚ) (algebraMap R Sₚ) p) 0

Tactic:
rw [Ne, zero_eq_bot, Ideal.map_eq_bot_iff_of_injective]

Premises used: Ideal.map_eq_bot_iff_of_injective, Ne, Ideal.zero_eq_bot
-- Module: Mathlib.RingTheory.DedekindDomain.PID
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
S : Type u_2
inst_2 : CommRing S
inst_3 : Algebra R S
inst_4 : Module.IsTorsionFree R S
inst_5 : Module.Finite R S
p : Ideal R
hp0 : p ≠ ⊥
inst_6 : p.IsPrime
Sₚ : Type u_3
inst_7 : CommRing Sₚ
inst_8 : Algebra S Sₚ
inst_9 : IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ
inst_10 : Algebra R Sₚ
inst_11 : IsScalarTower R S Sₚ
inst_12 : IsDedekindDomain Sₚ
inst_13 : IsDomain S
P : Ideal Sₚ
hP : P.IsPrime
hP0 : P ≠ ⊥
non_zero_div : LE.le (α := Submonoid S) (Algebra.algebraMapSubmonoid S p.primeCompl) S⁰
this_1 : Algebra.{u_1, u_3} (Localization.AtPrime p) Sₚ := localizationAlgebra p.primeCompl S
this_2 : IsScalarTower R (Localization.AtPrime p) Sₚ
pid : IsPrincipalIdealRing.{u_1} (Localization.AtPrime p)
p' : Ideal (Localization.AtPrime p)
hpu : ∀ (y : Ideal (Localization.AtPrime p)), (fun (P : Ideal (Localization.AtPrime p)) ↦ P ≠ ⊥ ∧ P.IsPrime) y → y = p'
hp'0 : p' ≠ ⊥
hp'p : p'.IsPrime
this : Ne.{u_1 + 1} (α := Ideal (Localization.AtPrime p)) (IsLocalRing.maximalIdeal (Localization.AtPrime p)) ⊥
⊢ ¬p = ⊥

Tactic:
assumption
-- Module: Mathlib.RingTheory.DedekindDomain.PID
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
S : Type u_2
inst_2 : CommRing S
inst_3 : Algebra R S
inst_4 : Module.IsTorsionFree R S
inst_5 : Module.Finite R S
p : Ideal R
hp0 : p ≠ ⊥
inst_6 : p.IsPrime
Sₚ : Type u_3
inst_7 : CommRing Sₚ
inst_8 : Algebra S Sₚ
inst_9 : IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ
inst_10 : Algebra R Sₚ
inst_11 : IsScalarTower R S Sₚ
inst_12 : IsDedekindDomain Sₚ
inst_13 : IsDomain S
P : Ideal Sₚ
hP : P.IsPrime
hP0 : P ≠ ⊥
non_zero_div : LE.le (α := Submonoid S) (Algebra.algebraMapSubmonoid S p.primeCompl) S⁰
this_1 : Algebra.{u_1, u_3} (Localization.AtPrime p) Sₚ := localizationAlgebra p.primeCompl S
this_2 : IsScalarTower R (Localization.AtPrime p) Sₚ
pid : IsPrincipalIdealRing.{u_1} (Localization.AtPrime p)
p' : Ideal (Localization.AtPrime p)
hpu : ∀ (y : Ideal (Localization.AtPrime p)), (fun (P : Ideal (Localization.AtPrime p)) ↦ P ≠ ⊥ ∧ P.IsPrime) y → y = p'
hp'0 : p' ≠ ⊥
hp'p : p'.IsPrime
this : Ne.{u_1 + 1} (α := Ideal (Localization.AtPrime p)) (IsLocalRing.maximalIdeal (Localization.AtPrime p)) ⊥
rw :
  Function.Injective.{u_1 + 1, u_3 + 1} (α := R) (β := Sₚ)
    (⇑(@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S Sₚ) (algebraMap R S)) : (a : R) → Sₚ)
⊢ Function.Injective.{u_1 + 1, u_3 + 1} (α := R) (β := Sₚ) (⇑(algebraMap R Sₚ) : (a : R) → Sₚ)

Tactic:
rw [IsScalarTower.algebraMap_eq R S Sₚ]

Premises used: IsScalarTower.algebraMap_eq
-- Module: Mathlib.RingTheory.DedekindDomain.PID
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
S : Type u_2
inst_2 : CommRing S
inst_3 : Algebra R S
inst_4 : Module.IsTorsionFree R S
inst_5 : Module.Finite R S
p : Ideal R
hp0 : p ≠ ⊥
inst_6 : p.IsPrime
Sₚ : Type u_3
inst_7 : CommRing Sₚ
inst_8 : Algebra S Sₚ
inst_9 : IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ
inst_10 : Algebra R Sₚ
inst_11 : IsScalarTower R S Sₚ
inst_12 : IsDedekindDomain Sₚ
inst_13 : IsDomain S
P : Ideal Sₚ
hP : P.IsPrime
hP0 : P ≠ ⊥
non_zero_div : LE.le (α := Submonoid S) (Algebra.algebraMapSubmonoid S p.primeCompl) S⁰
this_1 : Algebra.{u_1, u_3} (Localization.AtPrime p) Sₚ := localizationAlgebra p.primeCompl S
this_2 : IsScalarTower R (Localization.AtPrime p) Sₚ
pid : IsPrincipalIdealRing.{u_1} (Localization.AtPrime p)
p' : Ideal (Localization.AtPrime p)
hpu : ∀ (y : Ideal (Localization.AtPrime p)), (fun (P : Ideal (Localization.AtPrime p)) ↦ P ≠ ⊥ ∧ P.IsPrime) y → y = p'
hp'0 : p' ≠ ⊥
hp'p : p'.IsPrime
this : Ne.{u_1 + 1} (α := Ideal (Localization.AtPrime p)) (IsLocalRing.maximalIdeal (Localization.AtPrime p)) ⊥
⊢ Function.Injective.{u_1 + 1, u_3 + 1} (α := R) (β := Sₚ)
    (⇑(@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S Sₚ) (algebraMap R S)) : (a : R) → Sₚ)

Tactic:
(IsLocalization.injective Sₚ non_zero_div).comp (FaithfulSMul.algebraMap_injective _ _)

Premises used: IsLocalization.injective, Function.Injective.comp, FaithfulSMul.algebraMap_injective
-- Module: Mathlib.RingTheory.DedekindDomain.PID
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
S : Type u_2
inst_2 : CommRing S
inst_3 : Algebra R S
inst_4 : Module.IsTorsionFree R S
inst_5 : Module.Finite R S
p : Ideal R
hp0 : p ≠ ⊥
inst_6 : p.IsPrime
Sₚ : Type u_3
inst_7 : CommRing Sₚ
inst_8 : Algebra S Sₚ
inst_9 : IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ
inst_10 : Algebra R Sₚ
inst_11 : IsScalarTower R S Sₚ
inst_12 : IsDedekindDomain Sₚ
inst_13 : IsDomain S
P : Ideal Sₚ
hP : P.IsPrime
hP0 : P ≠ ⊥
non_zero_div : LE.le (α := Submonoid S) (Algebra.algebraMapSubmonoid S p.primeCompl) S⁰
this_1 : Algebra.{u_1, u_3} (Localization.AtPrime p) Sₚ := localizationAlgebra p.primeCompl S
this_2 : IsScalarTower R (Localization.AtPrime p) Sₚ
pid : IsPrincipalIdealRing.{u_1} (Localization.AtPrime p)
p' : Ideal (Localization.AtPrime p)
hpu : ∀ (y : Ideal (Localization.AtPrime p)), (fun (P : Ideal (Localization.AtPrime p)) ↦ P ≠ ⊥ ∧ P.IsPrime) y → y = p'
hp'0 : p' ≠ ⊥
hp'p : p'.IsPrime
this : Ne.{u_1 + 1} (α := Ideal (Localization.AtPrime p)) (IsLocalRing.maximalIdeal (Localization.AtPrime p)) ⊥
⊢ Function.Injective.{u_1 + 1, u_3 + 1} (α := R) (β := Sₚ)
    (⇑(@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S Sₚ) (algebraMap R S)) : (a : R) → Sₚ)

Tactic:
exact
      (IsLocalization.injective Sₚ non_zero_div).comp (FaithfulSMul.algebraMap_injective _ _)

Premises used: IsLocalization.injective, Function.Injective.comp, FaithfulSMul.algebraMap_injective
-- Module: Mathlib.RingTheory.DedekindDomain.PID
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
S : Type u_2
inst_2 : CommRing S
inst_3 : Algebra R S
inst_4 : Module.IsTorsionFree R S
inst_5 : Module.Finite R S
p : Ideal R
hp0 : p ≠ ⊥
inst_6 : p.IsPrime
Sₚ : Type u_3
inst_7 : CommRing Sₚ
inst_8 : Algebra S Sₚ
inst_9 : IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ
inst_10 : Algebra R Sₚ
inst_11 : IsScalarTower R S Sₚ
inst_12 : IsDedekindDomain Sₚ
inst_13 : IsDomain S
this_1 : DecidableEq (Ideal Sₚ) := Classical.decEq (Ideal Sₚ)
this : DecidablePred fun (P : Ideal Sₚ) ↦ P.IsPrime := Classical.decPred fun (P : Ideal Sₚ) ↦ P.IsPrime
⊢ IsPrincipalIdealRing Sₚ

Tactic:
IsPrincipalIdealRing.of_finite_primes
      (Set.Finite.ofFinset
        {P ∈ {⊥} ∪ (normalizedFactors (Ideal.map (algebraMap R Sₚ) p)).toFinset | P.IsPrime}
        fun P => ?_)

Premises used: UniqueFactorizationMonoid.normalizedFactors, Multiset.toFinset, Algebra.algebraMap, Ideal.map, Bot.bot, Ideal.IsPrime, Set.Finite.ofFinset, Union.union, Singleton.singleton, Finset.filter, IsPrincipalIdealRing.of_finite_primes
-- Module: Mathlib.RingTheory.DedekindDomain.PID
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
S : Type u_2
inst_2 : CommRing S
inst_3 : Algebra R S
inst_4 : Module.IsTorsionFree R S
inst_5 : Module.Finite R S
p : Ideal R
hp0 : p ≠ ⊥
inst_6 : p.IsPrime
Sₚ : Type u_3
inst_7 : CommRing Sₚ
inst_8 : Algebra S Sₚ
inst_9 : IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ
inst_10 : Algebra R Sₚ
inst_11 : IsScalarTower R S Sₚ
inst_12 : IsDedekindDomain Sₚ
inst_13 : IsDomain S
this_1 : DecidableEq (Ideal Sₚ) := Classical.decEq (Ideal Sₚ)
this : DecidablePred fun (P : Ideal Sₚ) ↦ P.IsPrime := Classical.decPred fun (P : Ideal Sₚ) ↦ P.IsPrime
R₁ :
  ∀ (P : Ideal Sₚ),
    Membership.mem (γ := Finset (Ideal Sₚ))
        ({P ∈ {⊥} ∪ Multiset.toFinset (normalizedFactors (map (F := R →+* Sₚ) (algebraMap R Sₚ) p)) | P.IsPrime}) P ↔
      Membership.mem (γ := Set (Ideal Sₚ)) {I : Ideal Sₚ | I.IsPrime} P
⊢ IsPrincipalIdealRing Sₚ

Tactic:
refine
    IsPrincipalIdealRing.of_finite_primes
      (Set.Finite.ofFinset
        {P ∈ {⊥} ∪ (normalizedFactors (Ideal.map (algebraMap R Sₚ) p)).toFinset | P.IsPrime}
        fun P => ?_)

Premises used: UniqueFactorizationMonoid.normalizedFactors, Multiset.toFinset, Algebra.algebraMap, Ideal.map, Bot.bot, Ideal.IsPrime, Set.Finite.ofFinset, Union.union, Singleton.singleton, Finset.filter, IsPrincipalIdealRing.of_finite_primes
-- Module: Mathlib.RingTheory.DedekindDomain.PID
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
S : Type u_2
inst_2 : CommRing S
inst_3 : Algebra R S
inst_4 : Module.IsTorsionFree R S
inst_5 : Module.Finite R S
p : Ideal R
hp0 : p ≠ ⊥
inst_6 : p.IsPrime
Sₚ : Type u_3
inst_7 : CommRing Sₚ
inst_8 : Algebra S Sₚ
inst_9 : IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ
inst_10 : Algebra R Sₚ
inst_11 : IsScalarTower R S Sₚ
inst_12 : IsDedekindDomain Sₚ
inst_13 : IsDomain S
this_1 : DecidableEq (Ideal Sₚ) := Classical.decEq (Ideal Sₚ)
this : DecidablePred fun (P : Ideal Sₚ) ↦ P.IsPrime := Classical.decPred fun (P : Ideal Sₚ) ↦ P.IsPrime
P : Ideal Sₚ
rw :
  (P = ⊥ ∨ Membership.mem (γ := Multiset (Ideal Sₚ)) (normalizedFactors (map (F := R →+* Sₚ) (algebraMap R Sₚ) p)) P) ∧
      P.IsPrime ↔
    P.IsPrime
⊢ Membership.mem (γ := Finset (Ideal Sₚ))
      ({P ∈ {⊥} ∪ Multiset.toFinset (normalizedFactors (map (F := R →+* Sₚ) (algebraMap R Sₚ) p)) | P.IsPrime}) P ↔
    Membership.mem (γ := Set (Ideal Sₚ)) {I : Ideal Sₚ | I.IsPrime} P

Tactic:
rw [Finset.mem_filter, Finset.mem_union, Finset.mem_singleton, Set.mem_setOf,
    Multiset.mem_toFinset]

Premises used: Finset.mem_singleton, Set.mem_setOf, Finset.mem_filter, Finset.mem_union, Multiset.mem_toFinset
-- Module: Mathlib.RingTheory.DedekindDomain.PID
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
S : Type u_2
inst_2 : CommRing S
inst_3 : Algebra R S
inst_4 : Module.IsTorsionFree R S
inst_5 : Module.Finite R S
p : Ideal R
hp0 : p ≠ ⊥
inst_6 : p.IsPrime
Sₚ : Type u_3
inst_7 : CommRing Sₚ
inst_8 : Algebra S Sₚ
inst_9 : IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ
inst_10 : Algebra R Sₚ
inst_11 : IsScalarTower R S Sₚ
inst_12 : IsDedekindDomain Sₚ
inst_13 : IsDomain S
this_1 : DecidableEq (Ideal Sₚ) := Classical.decEq (Ideal Sₚ)
this : DecidablePred fun (P : Ideal Sₚ) ↦ P.IsPrime := Classical.decPred fun (P : Ideal Sₚ) ↦ P.IsPrime
P : Ideal Sₚ
⊢ (P = ⊥ ∨ Membership.mem (γ := Multiset (Ideal Sₚ)) (normalizedFactors (map (F := R →+* Sₚ) (algebraMap R Sₚ) p)) P) ∧
      P.IsPrime ↔
    P.IsPrime

Tactic:
and_iff_right_of_imp fun hP =>
      or_iff_not_imp_left.mpr (IsLocalization.OverPrime.mem_normalizedFactors_of_isPrime S p hp0 hP)

Premises used: Iff.mpr, IsLocalization.OverPrime.mem_normalizedFactors_of_isPrime, Classical.or_iff_not_imp_left, and_iff_right_of_imp
-- Module: Mathlib.RingTheory.DedekindDomain.PID
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
S : Type u_2
inst_2 : CommRing S
inst_3 : Algebra R S
inst_4 : Module.IsTorsionFree R S
inst_5 : Module.Finite R S
p : Ideal R
hp0 : p ≠ ⊥
inst_6 : p.IsPrime
Sₚ : Type u_3
inst_7 : CommRing Sₚ
inst_8 : Algebra S Sₚ
inst_9 : IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ
inst_10 : Algebra R Sₚ
inst_11 : IsScalarTower R S Sₚ
inst_12 : IsDedekindDomain Sₚ
inst_13 : IsDomain S
this_1 : DecidableEq (Ideal Sₚ) := Classical.decEq (Ideal Sₚ)
this : DecidablePred fun (P : Ideal Sₚ) ↦ P.IsPrime := Classical.decPred fun (P : Ideal Sₚ) ↦ P.IsPrime
P : Ideal Sₚ
⊢ (P = ⊥ ∨ Membership.mem (γ := Multiset (Ideal Sₚ)) (normalizedFactors (map (F := R →+* Sₚ) (algebraMap R Sₚ) p)) P) ∧
      P.IsPrime ↔
    P.IsPrime

Tactic:
exact
    and_iff_right_of_imp fun hP =>
      or_iff_not_imp_left.mpr (IsLocalization.OverPrime.mem_normalizedFactors_of_isPrime S p hp0 hP)

Premises used: Iff.mpr, IsLocalization.OverPrime.mem_normalizedFactors_of_isPrime, Classical.or_iff_not_imp_left, and_iff_right_of_imp
-- Module: Mathlib.RingTheory.DedekindDomain.PID
Goal:
R : Type u_2
inst : CommRing R
inst_1 : IsDedekindDomain R
inst_2 : UniqueFactorizationMonoid R
⊢ IsPrincipalIdealRing R

Tactic:
.of_prime_ne_bot fun P hp hp₀ ↦ ?_

Premises used: IsPrincipalIdealRing.of_prime_ne_bot
-- Module: Mathlib.RingTheory.DedekindDomain.PID
Goal:
R : Type u_2
inst : CommRing R
inst_1 : IsDedekindDomain R
inst_2 : UniqueFactorizationMonoid R
refine : ∀ (P : Ideal R) (hp : P.IsPrime) (hp₀ : P ≠ ⊥), Submodule.IsPrincipal P
⊢ IsPrincipalIdealRing R

Tactic:
refine .of_prime_ne_bot fun P hp hp₀ ↦ ?_
-- Module: Mathlib.RingTheory.DedekindDomain.PID
Goal:
R : Type u_2
inst : CommRing R
inst_1 : IsDedekindDomain R
inst_2 : UniqueFactorizationMonoid R
P : Ideal R
hp : P.IsPrime
hp₀ : P ≠ ⊥
obtain : ∀ (x : R) (hx₁ : x ∈ P) (hx₂ : Prime x), Submodule.IsPrincipal P
⊢ Submodule.IsPrincipal P

Tactic:
obtain ⟨x, hx₁, hx₂⟩ := hp.exists_mem_prime_of_ne_bot hp₀

Premises used: Ideal.IsPrime.exists_mem_prime_of_ne_bot
-- Module: Mathlib.RingTheory.DedekindDomain.PID
Goal:
R : Type u_2
inst : CommRing R
inst_1 : IsDedekindDomain R
inst_2 : UniqueFactorizationMonoid R
P : Ideal R
hp : P.IsPrime
hp₀ : P ≠ ⊥
x : R
hx₁ : x ∈ P
hx₂ : Prime x
suffices : span {x} = P
⊢ Submodule.IsPrincipal P

Tactic:
suffices Ideal.span {x} = P from this ▸ inferInstance
-- Module: Mathlib.RingTheory.DedekindDomain.PID
Goal:
R : Type u_2
inst : CommRing R
inst_1 : IsDedekindDomain R
inst_2 : UniqueFactorizationMonoid R
P : Ideal R
hp : P.IsPrime
hp₀ : P ≠ ⊥
x : R
hx₁ : x ∈ P
hx₂ : Prime x
⊢ IsPrime (α := R) (span {x})

Tactic:
have := (Ideal.span_singleton_prime hx₂.ne_zero).mpr hx₂
-- Module: Mathlib.RingTheory.DedekindDomain.PID
Goal:
R : Type u_2
inst : CommRing R
inst_1 : IsDedekindDomain R
inst_2 : UniqueFactorizationMonoid R
P : Ideal R
hp : P.IsPrime
hp₀ : P ≠ ⊥
x : R
hx₁ : x ∈ P
hx₂ : Prime x
this : IsPrime (α := R) (span {x})
⊢ Ne (α := Ideal R) (span {x}) ⊥

Tactic:
aesop
-- Module: Mathlib.RingTheory.DedekindDomain.PID
Goal:
R : Type u_2
inst : CommRing R
inst_1 : IsDedekindDomain R
inst_2 : UniqueFactorizationMonoid R
P : Ideal R
hp : P.IsPrime
hp₀ : P ≠ ⊥
x : R
hx₁ : x ∈ P
hx₂ : Prime x
this : IsPrime (α := R) (span {x})
⊢ span {x} = P

Tactic:
exact (Ring.DimensionLeOne.prime_le_prime_iff_eq (by aesop)).mp <|
    P.span_singleton_le_iff_mem.mpr hx₁

Premises used: Iff.mpr, Ring.DimensionLeOne.prime_le_prime_iff_eq, Ideal.span_singleton_le_iff_mem, Iff.mp
-- Module: Mathlib.RingTheory.DedekindDomain.SInteger
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDedekindDomain R
S : Set (HeightOneSpectrum R)
K : Type v
inst_2 : Field K
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
x : K
⊢ Membership.mem (γ := Set K)
      {x : K |
        ∀ v ∉ S,
          LE.le (α := WithZero (Multiplicative ℤ))
            (((HeightOneSpectrum.valuation K v : Valuation K (WithZero (Multiplicative ℤ))) :
                  (a : K) → WithZero (Multiplicative ℤ))
                x :
              WithZero (Multiplicative ℤ))
            (1 : WithZero (Multiplicative ℤ))}
      x ↔
    x ∈
      (↑(⨅ (v : HeightOneSpectrum R),
            ⨅ (_ : v ∉ S), ValuationSubring.toSubring (Valuation.valuationSubring (HeightOneSpectrum.valuation K v))) :
        Set K)

Tactic:
simp [SetLike.mem_coe]

Premises used: SetLike.mem_coe
-- Module: Mathlib.RingTheory.DedekindDomain.SInteger
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDedekindDomain R
S : Set (HeightOneSpectrum R)
K : Type v
inst_2 : Field K
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
h :
  ∀ (x : K),
    x ∈ (↑(Subalgebra.toSubring (S.integer K)) : Set K) ↔
      x ∈
        (↑(⨅ (v : HeightOneSpectrum R),
              ⨅ (_ : v ∉ S),
                ValuationSubring.toSubring (Valuation.valuationSubring (HeightOneSpectrum.valuation K v))) :
          Set K)
⊢ (↑(Subalgebra.toSubring (S.integer K)) : Set K) =
    (↑(⨅ (v : HeightOneSpectrum R),
          ⨅ (_ : v ∉ S), ValuationSubring.toSubring (Valuation.valuationSubring (HeightOneSpectrum.valuation K v))) :
      Set K)

Tactic:
ext
-- Module: Mathlib.RingTheory.DedekindDomain.SInteger
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDedekindDomain R
S : Set (HeightOneSpectrum R)
K : Type v
inst_2 : Field K
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
x : K
⊢ x ∈ (↑(Subalgebra.toSubring (S.integer K)) : Set K) ↔
    x ∈
      (↑(⨅ (v : HeightOneSpectrum R),
            ⨅ (_ : v ∉ S), ValuationSubring.toSubring (Valuation.valuationSubring (HeightOneSpectrum.valuation K v))) :
        Set K)

Tactic:
simp
-- Module: Mathlib.RingTheory.DedekindDomain.SInteger
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDedekindDomain R
S : Set (HeightOneSpectrum R)
K : Type v
inst_2 : Field K
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
x : ↥(S.integer K)
v : HeightOneSpectrum R
hv : v ∉ S
⊢ LE.le (α := WithZero (Multiplicative ℤ))
    (((HeightOneSpectrum.valuation K v : Valuation K (WithZero (Multiplicative ℤ))) :
          (a : K) → WithZero (Multiplicative ℤ))
        (↑x : K) :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))

Tactic:
x.property v hv

Premises used: Subtype.property
-- Module: Mathlib.RingTheory.DedekindDomain.SInteger
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDedekindDomain R
K : Type v
inst_2 : Field K
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
h :
  ∀ (x : K), Membership.mem (γ := Subalgebra R K) (Set.integer Set.univ K) x ↔ Membership.mem (γ := Subalgebra R K) ⊤ x
⊢ Eq (α := Subalgebra R K) (Set.integer Set.univ K) ⊤

Tactic:
ext