awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.PID (hypothesis)
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 ≠ ⊥
⊢ Membership.mem (γ := Multiset (Ideal Sₚ)) (normalizedFactors (Ideal.map (F := R →+* Sₚ) (algebraMap R Sₚ) p)) P
have non_zero_div : 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
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.PID (goal)
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 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ₚ)
have 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ₚ)
Tactic: rw [IsScalarTower.algebraMap_apply R S]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.PID (hypothesis)
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
⊢ Membership.mem (γ := Multiset (Ideal Sₚ)) (normalizedFactors (Ideal.map (F := R →+* Sₚ) (algebraMap R Sₚ) p)) P
have this₁ : 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
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.PID (goal)
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ₚ
⊢ Membership.mem (γ := Multiset (Ideal Sₚ)) (normalizedFactors (Ideal.map (F := R →+* Sₚ) (algebraMap R Sₚ) p)) P
have 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
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 _)
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.PID (goal)
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)) ⊥
have 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
Tactic: rw [Submodule.ne_bot_iff] at hp0 ⊢
Cleared hypotheses: hp0, inst_6, Sₚ, inst_7, inst_8, inst_9, inst_10, inst_11, inst_12, inst_13, P, hP, hP0, non_zero_div, this_1, this, pid, p', hpu, hp'0, hp'p
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.PID (goal)
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
⊢ ∃ (x : Localization.AtPrime p),
    Membership.mem (γ := Submodule (Localization.AtPrime p) (Localization.AtPrime p))
        (IsLocalRing.maximalIdeal (Localization.AtPrime p)) x ∧
      x ≠ 0
have 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
Tactic: obtain ⟨x, x_mem, x_ne⟩ := hp0
Cleared hypotheses: hp0
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.PID (hypothesis)
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
⊢ Membership.mem (γ := Multiset (Ideal Sₚ)) (normalizedFactors (Ideal.map (F := R →+* Sₚ) (algebraMap R Sₚ) p)) P
have this₁ : 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)⟩
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.PID (goal)
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)) ⊥
⊢ Membership.mem (γ := Multiset (Ideal Sₚ)) (normalizedFactors (Ideal.map (F := R →+* Sₚ) (algebraMap R Sₚ) p)) P
have rw : Ne (α := Ideal (Localization.AtPrime p))
  (comap (F := RingHom.{u_1, u_3} (Localization.AtPrime p) Sₚ) (algebraMap (Localization.AtPrime p) Sₚ) 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 _ _) ⟨_, _⟩]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.PID (goal)
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) ⊥
⊢ Membership.mem (γ := Multiset (Ideal Sₚ)) (normalizedFactors (Ideal.map (F := R →+* Sₚ) (algebraMap R Sₚ) p)) P
have rw₁ : IsPrime (comap (F := RingHom.{u_1, u_3} (Localization.AtPrime p) Sₚ) (algebraMap (Localization.AtPrime p) Sₚ) 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 _ _) ⟨_, _⟩]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.PID (goal)
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)
⊢ Membership.mem (γ := Multiset (Ideal Sₚ)) (normalizedFactors (Ideal.map (F := R →+* Sₚ) (algebraMap R Sₚ) p)) P
have rw₂ : IsPrime.{u_1} (α := Localization.AtPrime p) (IsLocalRing.maximalIdeal (Localization.AtPrime 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 _ _) ⟨_, _⟩]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.PID (goal)
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))
⊢ Membership.mem (γ := Multiset (Ideal Sₚ)) (normalizedFactors (Ideal.map (F := R →+* Sₚ) (algebraMap R Sₚ) p)) P
have rw₃ : Ne.{u_3 + 1} (α := Ideal Sₚ) (Ideal.map (F := R →+* Sₚ) (algebraMap R Sₚ) p) 0
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 _ _) ⟨_, _⟩]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.PID (hypothesis)
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)) ⊥
⊢ Ne (α := Ideal (Localization.AtPrime p))
    (comap (F := RingHom.{u_1, u_3} (Localization.AtPrime p) Sₚ) (algebraMap (Localization.AtPrime p) Sₚ) P) ⊥
have this₁ : Algebra.IsIntegral.{u_1, u_3} (Localization.AtPrime p) Sₚ
Tactic: have : Algebra.IsIntegral (Localization.AtPrime p) Sₚ := ⟨isIntegral_localization⟩
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.PID (goal)
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)) ⊥
⊢ Ne.{u_3 + 1} (α := Ideal Sₚ) (Ideal.map (F := R →+* Sₚ) (algebraMap R Sₚ) p) 0
have rw : ¬p = ⊥
Tactic: rw [Ne, zero_eq_bot, Ideal.map_eq_bot_iff_of_injective]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.PID (goal)
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 = ⊥
⊢ Ne.{u_3 + 1} (α := Ideal Sₚ) (Ideal.map (F := R →+* Sₚ) (algebraMap R Sₚ) p) 0
have rw₁ : Function.Injective.{u_1 + 1, u_3 + 1} (α := R) (β := Sₚ) (⇑(algebraMap R Sₚ) : (a : R) → Sₚ)
Tactic: rw [Ne, zero_eq_bot, Ideal.map_eq_bot_iff_of_injective]