awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.DedekindDomain.PID
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
h : Set.Finite.{u_1} (α := Ideal R) {I : Ideal R | I.IsMaximal}
I : Ideal R
hI : I ≠ ⊥
⊢ IsUnit (M := FractionalIdeal (R := R) R⁰ (FractionRing R)) (↑I : FractionalIdeal R⁰ (FractionRing R))

Tactic:
.of_mul_eq_one _ (FractionalIdeal.coe_ideal_mul_inv I hI)

Premises used: IsUnit.of_mul_eq_one, FractionalIdeal.coe_ideal_mul_inv
-- Module: Mathlib.RingTheory.DedekindDomain.PID
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
h : Set.Finite.{u_1} (α := Ideal R) {I : Ideal R | I.IsMaximal}
I : Ideal R
hI : I ≠ ⊥
⊢ IsUnit (M := FractionalIdeal (R := R) R⁰ (FractionRing R)) (↑I : FractionalIdeal R⁰ (FractionRing R))

Tactic:
exact .of_mul_eq_one _ (FractionalIdeal.coe_ideal_mul_inv I hI)
-- Module: Mathlib.RingTheory.DedekindDomain.PID
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
h : Set.Finite.{u_1} (α := Ideal R) {I : Ideal R | I.IsPrime}
⊢ IsPrincipalIdealRing R

Tactic:
IsPrincipalIdealRing.of_finite_maximals <| h.subset fun _ hi ↦ hi.isPrime

Premises used: Set.Finite.subset, Ideal.IsMaximal.isPrime, IsPrincipalIdealRing.of_finite_maximals
-- 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 ≠ ⊥
⊢ LE.le (α := Submonoid S) (Algebra.algebraMapSubmonoid S p.primeCompl) S⁰

Tactic:
have non_zero_div : Algebra.algebraMapSubmonoid S p.primeCompl ≤ S⁰ :=
    map_le_nonZeroDivisors_of_injective _ (FaithfulSMul.algebraMap_injective _ _)
      p.primeCompl_le_nonZeroDivisors
-- 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 : Algebra.{u_1, u_3} (Localization.AtPrime p) Sₚ := localizationAlgebra p.primeCompl S
x : R
rw :
  Eq.{u_3 + 1} (α := Sₚ) ((algebraMap S Sₚ : (a : S) → Sₚ) ((algebraMap R S : (a : R) → S) x : S) : Sₚ)
    ((algebraMap (Localization.AtPrime p) Sₚ : (a : Localization.AtPrime p) → Sₚ)
        ((algebraMap R (Localization.AtPrime p) : (a : R) → Localization.AtPrime p) x : Localization.AtPrime p) :
      Sₚ)
⊢ Eq.{u_3 + 1} (α := Sₚ) ((algebraMap R Sₚ : (a : R) → Sₚ) x : Sₚ)
    ((algebraMap (Localization.AtPrime p) Sₚ : (a : Localization.AtPrime p) → Sₚ)
        ((algebraMap R (Localization.AtPrime p) : (a : R) → Localization.AtPrime p) x : Localization.AtPrime p) :
      Sₚ)

Tactic:
rw [IsScalarTower.algebraMap_apply R S]

Premises used: IsScalarTower.algebraMap_apply
-- 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 : Algebra.{u_1, u_3} (Localization.AtPrime p) Sₚ := localizationAlgebra p.primeCompl S
x : R
⊢ Eq.{u_3 + 1} (α := Sₚ) ((algebraMap S Sₚ : (a : S) → Sₚ) ((algebraMap R S : (a : R) → S) x : S) : Sₚ)
    ((algebraMap (Localization.AtPrime p) Sₚ : (a : Localization.AtPrime p) → Sₚ)
        ((algebraMap R (Localization.AtPrime p) : (a : R) → Localization.AtPrime p) x : Localization.AtPrime p) :
      Sₚ)

Tactic:
(IsLocalization.map_eq (T := Algebra.algebraMapSubmonoid S (primeCompl p))
        (Submonoid.le_comap_map _) x).symm

Premises used: Submonoid.le_comap_map, IsLocalization.map_eq, Eq.symm
-- 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 : Algebra.{u_1, u_3} (Localization.AtPrime p) Sₚ := localizationAlgebra p.primeCompl S
x : R
⊢ Eq.{u_3 + 1} (α := Sₚ) ((algebraMap S Sₚ : (a : S) → Sₚ) ((algebraMap R S : (a : R) → S) x : S) : Sₚ)
    ((algebraMap (Localization.AtPrime p) Sₚ : (a : Localization.AtPrime p) → Sₚ)
        ((algebraMap R (Localization.AtPrime p) : (a : R) → Localization.AtPrime p) x : Localization.AtPrime p) :
      Sₚ)

Tactic:
exact (IsLocalization.map_eq (T := Algebra.algebraMapSubmonoid S (primeCompl p))
        (Submonoid.le_comap_map _) x).symm

Premises used: Submonoid.le_comap_map, IsLocalization.map_eq, Eq.symm
-- 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 : Algebra.{u_1, u_3} (Localization.AtPrime p) Sₚ := localizationAlgebra p.primeCompl S
⊢ IsScalarTower R (Localization.AtPrime p) Sₚ

Tactic:
haveI : IsScalarTower R (Localization.AtPrime p) Sₚ :=
    IsScalarTower.of_algebraMap_eq fun x => by
      rw [IsScalarTower.algebraMap_apply R S]
      exact (IsLocalization.map_eq (T := Algebra.algebraMapSubmonoid S (primeCompl p))
        (Submonoid.le_comap_map _) x).symm
-- 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 : IsScalarTower R (Localization.AtPrime p) Sₚ
obtain :
  ∀ (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),
    Membership.mem (γ := Multiset (Ideal Sₚ)) (normalizedFactors (Ideal.map (F := R →+* Sₚ) (algebraMap R Sₚ) p)) P
⊢ Membership.mem (γ := Multiset (Ideal Sₚ)) (normalizedFactors (Ideal.map (F := R →+* Sₚ) (algebraMap R Sₚ) p)) P

Tactic:
obtain ⟨pid, p', ⟨hp'0, hp'p⟩, hpu⟩ :=
    (IsDiscreteValuationRing.iff_pid_with_one_nonzero_prime (Localization.AtPrime p)).mp
      (IsLocalization.AtPrime.isDiscreteValuationRing_of_dedekind_domain R hp0 _)

Premises used: Localization.AtPrime, IsLocalization.AtPrime.isDiscreteValuationRing_of_dedekind_domain, Iff.mp, IsDiscreteValuationRing.iff_pid_with_one_nonzero_prime
-- 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 : 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
rw :
  ∀ (hp0 : ∃ x ∈ p, x ≠ 0) [inst_14 : p.IsPrime] {Sₚ : Type u_3} [inst_15 : CommRing Sₚ] [inst_16 : Algebra S Sₚ]
    [inst_17 : IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ] [inst_18 : Algebra R Sₚ]
    [IsScalarTower R S Sₚ] [IsDedekindDomain Sₚ] [IsDomain S] {P : Ideal Sₚ} (hP : P.IsPrime) (hP0 : P ≠ ⊥)
    (non_zero_div : LE.le (α := Submonoid S) (Algebra.algebraMapSubmonoid S p.primeCompl) S⁰),
    let this : Algebra.{u_1, u_3} (Localization.AtPrime p) Sₚ := localizationAlgebra p.primeCompl S;
    ∀ (this : 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),
      ∃ (x : Localization.AtPrime p),
        Membership.mem (γ := Submodule (Localization.AtPrime p) (Localization.AtPrime p))
            (IsLocalRing.maximalIdeal (Localization.AtPrime p)) x ∧
          x ≠ 0
⊢ Ne.{u_1 + 1} (α := Ideal (Localization.AtPrime p)) (IsLocalRing.maximalIdeal (Localization.AtPrime p)) ⊥

Tactic:
rw [Submodule.ne_bot_iff] at hp0 ⊢

Premises used: Submodule.ne_bot_iff
-- 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 : ∃ x ∈ p, x ≠ 0
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 : 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
obtain :
  ∀ (x : R) (x_mem : x ∈ p) (x_ne : x ≠ 0),
    ∃ (x : Localization.AtPrime p),
      Membership.mem (γ := Submodule (Localization.AtPrime p) (Localization.AtPrime p))
          (IsLocalRing.maximalIdeal (Localization.AtPrime p)) x ∧
        x ≠ 0
⊢ ∃ (x : Localization.AtPrime p),
    Membership.mem (γ := Submodule (Localization.AtPrime p) (Localization.AtPrime p))
        (IsLocalRing.maximalIdeal (Localization.AtPrime p)) x ∧
      x ≠ 0

Tactic:
obtain ⟨x, x_mem, x_ne⟩ := hp0
-- 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
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 : 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
x : R
x_mem : x ∈ p
x_ne : x ≠ 0
⊢ ∃ (x : Localization.AtPrime p),
    Membership.mem (γ := Submodule (Localization.AtPrime p) (Localization.AtPrime p))
        (IsLocalRing.maximalIdeal (Localization.AtPrime p)) x ∧
      x ≠ 0

Tactic:
⟨algebraMap _ _ x, (IsLocalization.AtPrime.to_map_mem_maximal_iff _ _ _).mpr x_mem,
        IsLocalization.to_map_ne_zero_of_mem_nonZeroDivisors _ p.primeCompl_le_nonZeroDivisors
          (mem_nonZeroDivisors_of_ne_zero x_ne)⟩

Premises used: Iff.mpr, Algebra.algebraMap, IsLocalization.AtPrime.to_map_mem_maximal_iff, And.intro, IsLocalization.AtPrime.isLocalRing, Exists.intro, mem_nonZeroDivisors_of_ne_zero, Ideal.primeCompl_le_nonZeroDivisors, IsLocalization.to_map_ne_zero_of_mem_nonZeroDivisors, DFunLike.coe
-- 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
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 : 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
x : R
x_mem : x ∈ p
x_ne : x ≠ 0
⊢ ∃ (x : Localization.AtPrime p),
    Membership.mem (γ := Submodule (Localization.AtPrime p) (Localization.AtPrime p))
        (IsLocalRing.maximalIdeal (Localization.AtPrime p)) x ∧
      x ≠ 0

Tactic:
exact
      ⟨algebraMap _ _ x, (IsLocalization.AtPrime.to_map_mem_maximal_iff _ _ _).mpr x_mem,
        IsLocalization.to_map_ne_zero_of_mem_nonZeroDivisors _ p.primeCompl_le_nonZeroDivisors
          (mem_nonZeroDivisors_of_ne_zero x_ne)⟩
-- 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 : 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
⊢ Ne.{u_1 + 1} (α := Ideal (Localization.AtPrime p)) (IsLocalRing.maximalIdeal (Localization.AtPrime p)) ⊥

Tactic:
have : IsLocalRing.maximalIdeal (Localization.AtPrime p) ≠ ⊥ := by
    rw [Submodule.ne_bot_iff] at hp0 ⊢
    obtain ⟨x, x_mem, x_ne⟩ := hp0
    exact
      ⟨algebraMap _ _ x, (IsLocalization.AtPrime.to_map_mem_maximal_iff _ _ _).mpr x_mem,
        IsLocalization.to_map_ne_zero_of_mem_nonZeroDivisors _ p.primeCompl_le_nonZeroDivisors
          (mem_nonZeroDivisors_of_ne_zero x_ne)⟩
-- 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 :
  Ne (α := Ideal (Localization.AtPrime p))
    (comap (F := RingHom.{u_1, u_3} (Localization.AtPrime p) Sₚ) (algebraMap (Localization.AtPrime p) Sₚ) P) ⊥
rw₁ : IsPrime (comap (F := RingHom.{u_1, u_3} (Localization.AtPrime p) Sₚ) (algebraMap (Localization.AtPrime p) Sₚ) P)
rw₂ : IsPrime.{u_1} (α := Localization.AtPrime p) (IsLocalRing.maximalIdeal (Localization.AtPrime p))
rw₃ : Ne.{u_3 + 1} (α := Ideal Sₚ) (Ideal.map (F := R →+* Sₚ) (algebraMap R Sₚ) p) 0
⊢ Membership.mem (γ := Multiset (Ideal Sₚ)) (normalizedFactors (Ideal.map (F := R →+* Sₚ) (algebraMap R Sₚ) p)) P

Tactic:
rw [← Multiset.singleton_le, ← normalize_eq P, ←
    normalizedFactors_irreducible (Ideal.prime_of_isPrime hP0 hP).irreducible, ←
    dvd_iff_normalizedFactors_le_normalizedFactors hP0, dvd_iff_le,
    IsScalarTower.algebraMap_eq R (Localization.AtPrime p) Sₚ, ← Ideal.map_map,
    Localization.AtPrime.map_eq_maximalIdeal, Ideal.map_le_iff_le_comap,
    hpu (IsLocalRing.maximalIdeal _) ⟨this, _⟩, hpu (comap _ _) ⟨_, _⟩]

Premises used: Prime.irreducible, Ideal.dvd_iff_le, Localization.AtPrime, IsLocalRing.maximalIdeal, Ideal.map_le_iff_le_comap, UniqueFactorizationMonoid.normalizedFactors_irreducible, Ideal.map_map, And.intro, IsScalarTower.algebraMap_eq, Ideal.comap, UniqueFactorizationMonoid.dvd_iff_normalizedFactors_le_normalizedFactors, Multiset.singleton_le, Ideal.prime_of_isPrime, Localization.AtPrime.map_eq_maximalIdeal, normalize_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)) ⊥
⊢ Algebra.IsIntegral.{u_1, u_3} (Localization.AtPrime p) Sₚ

Tactic:
have : Algebra.IsIntegral (Localization.AtPrime p) Sₚ := ⟨isIntegral_localization⟩
-- 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_3 : Ne.{u_1 + 1} (α := Ideal (Localization.AtPrime p)) (IsLocalRing.maximalIdeal (Localization.AtPrime p)) ⊥
this : Algebra.IsIntegral.{u_1, u_3} (Localization.AtPrime p) Sₚ
⊢ Ne (α := Ideal (Localization.AtPrime p))
    (comap (F := RingHom.{u_1, u_3} (Localization.AtPrime p) Sₚ) (algebraMap (Localization.AtPrime p) Sₚ) P) ⊥

Tactic:
mt (Ideal.eq_bot_of_comap_eq_bot) hP0

Premises used: Ideal.eq_bot_of_comap_eq_bot, mt
-- 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_3 : Ne.{u_1 + 1} (α := Ideal (Localization.AtPrime p)) (IsLocalRing.maximalIdeal (Localization.AtPrime p)) ⊥
this : Algebra.IsIntegral.{u_1, u_3} (Localization.AtPrime p) Sₚ
⊢ Ne (α := Ideal (Localization.AtPrime p))
    (comap (F := RingHom.{u_1, u_3} (Localization.AtPrime p) Sₚ) (algebraMap (Localization.AtPrime p) Sₚ) P) ⊥

Tactic:
exact mt (Ideal.eq_bot_of_comap_eq_bot) hP0

Premises used: Ideal.eq_bot_of_comap_eq_bot, mt