-- Mathlib/RingTheory/DedekindDomain/PID.lean
theorem IsLocalization.OverPrime.mem_normalizedFactors_of_isPrime [IsDomain S]
    {P : Ideal Sₚ} (hP : IsPrime P) (hP0 : P ≠ ⊥) :
    P ∈ normalizedFactors (Ideal.map (algebraMap R Sₚ) p)

Proof state:
case intro.intro.intro.intro
R : Type u_1
inst✝¹³ : CommRing R
inst✝¹² : IsDedekindDomain R
S : Type u_2
inst✝¹¹ : CommRing S
inst✝¹⁰ : Algebra R S
inst✝⁹ : NoZeroSMulDivisors R S
inst✝⁸ : Module.Finite R S
p : Ideal R
hp0 : p ≠ ⊥
inst✝⁷ : p.IsPrime
Sₚ : Type u_3
inst✝⁶ : CommRing Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝³ : Algebra R Sₚ
inst✝² : IsScalarTower R S Sₚ
inst✝¹ : IsDedekindDomain Sₚ
inst✝ : IsDomain S
P : Ideal Sₚ
hP : P.IsPrime
hP0 : P ≠ ⊥
non_zero_div : Algebra.algebraMapSubmonoid S p.primeCompl ≤ S⁰
this✝¹ : Algebra (Localization.AtPrime p) Sₚ := localizationAlgebra p.primeCompl S
this✝ : IsScalarTower R (Localization.AtPrime p) Sₚ
pid : IsPrincipalIdealRing (Localization.AtPrime p)
p' : Ideal (Localization.AtPrime p)
hpu : ∀ (y : Ideal (Localization.AtPrime p)), (fun P => P ≠ ⊥ ∧ P.IsPrime) y → y = p'
hp'0 : p' ≠ ⊥
hp'p : p'.IsPrime
this : IsLocalRing.maximalIdeal (Localization.AtPrime p) ≠ ⊥
⊢ P ∈ normalizedFactors (Ideal.map (algebraMap R 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 _ _) ⟨_, _⟩]

Result:
R : Type u_1
inst✝¹³ : CommRing R
inst✝¹² : IsDedekindDomain R
S : Type u_2
inst✝¹¹ : CommRing S
inst✝¹⁰ : Algebra R S
inst✝⁹ : NoZeroSMulDivisors R S
inst✝⁸ : Module.Finite R S
p : Ideal R
hp0 : p ≠ ⊥
inst✝⁷ : p.IsPrime
Sₚ : Type u_3
inst✝⁶ : CommRing Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝³ : Algebra R Sₚ
inst✝² : IsScalarTower R S Sₚ
inst✝¹ : IsDedekindDomain Sₚ
inst✝ : IsDomain S
P : Ideal Sₚ
hP : P.IsPrime
hP0 : P ≠ ⊥
non_zero_div : Algebra.algebraMapSubmonoid S p.primeCompl ≤ S⁰
this✝¹ : Algebra (Localization.AtPrime p) Sₚ := localizationAlgebra p.primeCompl S
this✝ : IsScalarTower R (Localization.AtPrime p) Sₚ
pid : IsPrincipalIdealRing (Localization.AtPrime p)
p' : Ideal (Localization.AtPrime p)
hpu : ∀ (y : Ideal (Localization.AtPrime p)), (fun P => P ≠ ⊥ ∧ P.IsPrime) y → y = p'
hp'0 : p' ≠ ⊥
hp'p : p'.IsPrime
this : IsLocalRing.maximalIdeal (Localization.AtPrime p) ≠ ⊥
⊢ comap (algebraMap (Localization.AtPrime p) Sₚ) P ≠ ⊥

R : Type u_1
inst✝¹³ : CommRing R
inst✝¹² : IsDedekindDomain R
S : Type u_2
inst✝¹¹ : CommRing S
inst✝¹⁰ : Algebra R S
inst✝⁹ : NoZeroSMulDivisors R S
inst✝⁸ : Module.Finite R S
p : Ideal R
hp0 : p ≠ ⊥
inst✝⁷ : p.IsPrime
Sₚ : Type u_3
inst✝⁶ : CommRing Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝³ : Algebra R Sₚ
inst✝² : IsScalarTower R S Sₚ
inst✝¹ : IsDedekindDomain Sₚ
inst✝ : IsDomain S
P : Ideal Sₚ
hP : P.IsPrime
hP0 : P ≠ ⊥
non_zero_div : Algebra.algebraMapSubmonoid S p.primeCompl ≤ S⁰
this✝¹ : Algebra (Localization.AtPrime p) Sₚ := localizationAlgebra p.primeCompl S
this✝ : IsScalarTower R (Localization.AtPrime p) Sₚ
pid : IsPrincipalIdealRing (Localization.AtPrime p)
p' : Ideal (Localization.AtPrime p)
hpu : ∀ (y : Ideal (Localization.AtPrime p)), (fun P => P ≠ ⊥ ∧ P.IsPrime) y → y = p'
hp'0 : p' ≠ ⊥
hp'p : p'.IsPrime
this : IsLocalRing.maximalIdeal (Localization.AtPrime p) ≠ ⊥
⊢ (comap (algebraMap (Localization.AtPrime p) Sₚ) P).IsPrime

R : Type u_1
inst✝¹³ : CommRing R
inst✝¹² : IsDedekindDomain R
S : Type u_2
inst✝¹¹ : CommRing S
inst✝¹⁰ : Algebra R S
inst✝⁹ : NoZeroSMulDivisors R S
inst✝⁸ : Module.Finite R S
p : Ideal R
hp0 : p ≠ ⊥
inst✝⁷ : p.IsPrime
Sₚ : Type u_3
inst✝⁶ : CommRing Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝³ : Algebra R Sₚ
inst✝² : IsScalarTower R S Sₚ
inst✝¹ : IsDedekindDomain Sₚ
inst✝ : IsDomain S
P : Ideal Sₚ
hP : P.IsPrime
hP0 : P ≠ ⊥
non_zero_div : Algebra.algebraMapSubmonoid S p.primeCompl ≤ S⁰
this✝¹ : Algebra (Localization.AtPrime p) Sₚ := localizationAlgebra p.primeCompl S
this✝ : IsScalarTower R (Localization.AtPrime p) Sₚ
pid : IsPrincipalIdealRing (Localization.AtPrime p)
p' : Ideal (Localization.AtPrime p)
hpu : ∀ (y : Ideal (Localization.AtPrime p)), (fun P => P ≠ ⊥ ∧ P.IsPrime) y → y = p'
hp'0 : p' ≠ ⊥
hp'p : p'.IsPrime
this : IsLocalRing.maximalIdeal (Localization.AtPrime p) ≠ ⊥
⊢ (IsLocalRing.maximalIdeal (Localization.AtPrime p)).IsPrime

case intro.intro.intro.intro
R : Type u_1
inst✝¹³ : CommRing R
inst✝¹² : IsDedekindDomain R
S : Type u_2
inst✝¹¹ : CommRing S
inst✝¹⁰ : Algebra R S
inst✝⁹ : NoZeroSMulDivisors R S
inst✝⁸ : Module.Finite R S
p : Ideal R
hp0 : p ≠ ⊥
inst✝⁷ : p.IsPrime
Sₚ : Type u_3
inst✝⁶ : CommRing Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝³ : Algebra R Sₚ
inst✝² : IsScalarTower R S Sₚ
inst✝¹ : IsDedekindDomain Sₚ
inst✝ : IsDomain S
P : Ideal Sₚ
hP : P.IsPrime
hP0 : P ≠ ⊥
non_zero_div : Algebra.algebraMapSubmonoid S p.primeCompl ≤ S⁰
this✝¹ : Algebra (Localization.AtPrime p) Sₚ := localizationAlgebra p.primeCompl S
this✝ : IsScalarTower R (Localization.AtPrime p) Sₚ
pid : IsPrincipalIdealRing (Localization.AtPrime p)
p' : Ideal (Localization.AtPrime p)
hpu : ∀ (y : Ideal (Localization.AtPrime p)), (fun P => P ≠ ⊥ ∧ P.IsPrime) y → y = p'
hp'0 : p' ≠ ⊥
hp'p : p'.IsPrime
this : IsLocalRing.maximalIdeal (Localization.AtPrime p) ≠ ⊥
⊢ Ideal.map (algebraMap R Sₚ) p ≠ 0

Proof state:
R : Type u_1
inst✝¹³ : CommRing R
inst✝¹² : IsDedekindDomain R
S : Type u_2
inst✝¹¹ : CommRing S
inst✝¹⁰ : Algebra R S
inst✝⁹ : NoZeroSMulDivisors R S
inst✝⁸ : Module.Finite R S
p : Ideal R
hp0 : p ≠ ⊥
inst✝⁷ : p.IsPrime
Sₚ : Type u_3
inst✝⁶ : CommRing Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝³ : Algebra R Sₚ
inst✝² : IsScalarTower R S Sₚ
inst✝¹ : IsDedekindDomain Sₚ
inst✝ : IsDomain S
P : Ideal Sₚ
hP : P.IsPrime
hP0 : P ≠ ⊥
non_zero_div : Algebra.algebraMapSubmonoid S p.primeCompl ≤ S⁰
this : Algebra (Localization.AtPrime p) Sₚ := localizationAlgebra p.primeCompl S
x : R
⊢ (algebraMap S Sₚ) ((algebraMap R S) x) =
    (algebraMap (Localization.AtPrime p) Sₚ) ((algebraMap R (Localization.AtPrime p)) x)

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

Result:
no goals