-- Mathlib/RingTheory/DedekindDomain/Ideal.lean
theorem count_span_normalizedFactors_eq {r X : R} (hr : r ≠ 0) (hX : Prime X) :
    Multiset.count (Ideal.span {X} : Ideal R) (normalizedFactors (Ideal.span {r}))  =
        Multiset.count (normalize X) (normalizedFactors r)

Proof state:
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
inst✝² : NormalizationMonoid R
inst✝¹ : DecidableEq R
inst✝ : DecidableEq (Ideal R)
r X : R
hr : r ≠ 0
hX : Prime X
this : emultiplicity (span {X}) (span {r}) = ↑(Multiset.count (normalize X) (normalizedFactors r))
⊢ Prime (span {X})

Tactic:
simpa only [prime_span_singleton_iff]

Result:
no goals

Proof state:
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
inst✝² : NormalizationMonoid R
inst✝¹ : DecidableEq R
inst✝ : DecidableEq (Ideal R)
r X : R
hr : r ≠ 0
hX : Prime X
⊢ Multiset.count (span {X}) (normalizedFactors (span {r})) = Multiset.count (normalize X) (normalizedFactors r)

Tactic:
have := emultiplicity_eq_emultiplicity_span (R := R) (a := X) (b := r)

Result:
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
inst✝² : NormalizationMonoid R
inst✝¹ : DecidableEq R
inst✝ : DecidableEq (Ideal R)
r X : R
hr : r ≠ 0
hX : Prime X
this : emultiplicity (span {X}) (span {r}) = emultiplicity X r
⊢ Multiset.count (span {X}) (normalizedFactors (span {r})) = Multiset.count (normalize X) (normalizedFactors r)

Proof state:
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
inst✝² : NormalizationMonoid R
inst✝¹ : DecidableEq R
inst✝ : DecidableEq (Ideal R)
r X : R
hr : r ≠ 0
hX : Prime X
this : Multiset.count (span {X}) (normalizedFactors (span {r})) = Multiset.count (normalize X) (normalizedFactors r)
⊢ Multiset.count (span {X}) (normalizedFactors (span {r})) = Multiset.count (normalize X) (normalizedFactors r)

Tactic:
simp only [normalize_apply, this]

Result:
no goals

Proof state:
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
inst✝² : NormalizationMonoid R
inst✝¹ : DecidableEq R
inst✝ : DecidableEq (Ideal R)
r X : R
hr : r ≠ 0
hX : Prime X
this : emultiplicity (span {X}) (span {r}) = emultiplicity X r
⊢ Multiset.count (span {X}) (normalizedFactors (span {r})) = Multiset.count (normalize X) (normalizedFactors r)

Tactic:
rw [emultiplicity_eq_count_normalizedFactors (Prime.irreducible hX) hr,
  emultiplicity_eq_count_normalizedFactors (Prime.irreducible ?_), normalize_apply,
  normUnit_eq_one, Units.val_one, one_eq_top, mul_top, Nat.cast_inj] at this

Result:
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
inst✝² : NormalizationMonoid R
inst✝¹ : DecidableEq R
inst✝ : DecidableEq (Ideal R)
r X : R
hr : r ≠ 0
hX : Prime X
this : Multiset.count (span {X}) (normalizedFactors (span {r})) = Multiset.count (normalize X) (normalizedFactors r)
⊢ Multiset.count (span {X}) (normalizedFactors (span {r})) = Multiset.count (normalize X) (normalizedFactors r)

R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
inst✝² : NormalizationMonoid R
inst✝¹ : DecidableEq R
inst✝ : DecidableEq (Ideal R)
r X : R
hr : r ≠ 0
hX : Prime X
this : emultiplicity (span {X}) (span {r}) = ↑(Multiset.count (normalize X) (normalizedFactors r))
⊢ span {r} ≠ 0

R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
inst✝² : NormalizationMonoid R
inst✝¹ : DecidableEq R
inst✝ : DecidableEq (Ideal R)
r X : R
hr : r ≠ 0
hX : Prime X
this : emultiplicity (span {X}) (span {r}) = ↑(Multiset.count (normalize X) (normalizedFactors r))
⊢ Prime (span {X})

Proof state:
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
inst✝² : NormalizationMonoid R
inst✝¹ : DecidableEq R
inst✝ : DecidableEq (Ideal R)
r X : R
hr : r ≠ 0
hX : Prime X
this : emultiplicity (span {X}) (span {r}) = ↑(Multiset.count (normalize X) (normalizedFactors r))
⊢ span {r} ≠ 0

Tactic:
simp only [Submodule.zero_eq_bot, ne_eq, span_singleton_eq_bot, hr, not_false_eq_true]

Result:
no goals