-- Mathlib/RingTheory/DedekindDomain/PID.lean
theorem Ideal.eq_span_singleton_of_mem_of_not_mem_sq_of_not_mem_prime_ne {P : Ideal R}
    (hP : P.IsPrime) [IsDedekindDomain R] {x : R} (x_mem : x ∈ P) (hxP2 : x ∉ P ^ 2)
    (hxQ : ∀ Q : Ideal R, IsPrime Q → Q ≠ P → x ∉ Q) : P = Ideal.span {x}

Proof state:
R : Type u_1
inst✝¹ : CommRing R
P : Ideal R
hP : P.IsPrime
inst✝ : IsDedekindDomain R
x : R
x_mem : x ∈ P
hxP2 : x ∉ P ^ 2
hxQ : ∀ (Q : Ideal R), Q.IsPrime → Q ≠ P → x ∉ Q
this : DecidableEq (Ideal R) := Classical.decEq (Ideal R)
⊢ x ≠ 0

Tactic:
rintro rfl

Result:
R : Type u_1
inst✝¹ : CommRing R
P : Ideal R
hP : P.IsPrime
inst✝ : IsDedekindDomain R
this : DecidableEq (Ideal R) := Classical.decEq (Ideal R)
x_mem : 0 ∈ P
hxP2 : 0 ∉ P ^ 2
hxQ : ∀ (Q : Ideal R), Q.IsPrime → Q ≠ P → 0 ∉ Q
⊢ False

Proof state:
case neg
R : Type u_1
inst✝¹ : CommRing R
P : Ideal R
hP : P.IsPrime
inst✝ : IsDedekindDomain R
x : R
x_mem : x ∈ P
hxP2 : x ∉ P ^ 2
hxQ : ∀ (Q : Ideal R), Q.IsPrime → Q ≠ P → x ∉ Q
this : DecidableEq (Ideal R) := Classical.decEq (Ideal R)
hx0 : x ≠ 0
hP0 : ¬P = ⊥
hspan0 : span {x} ≠ ⊥
span_le : span {x} ≤ P
Q : Ideal R
hQ : ¬Q = P
⊢ Multiset.count Q (normalizedFactors (span {x})) ≤ 0

Tactic:
by_cases hQp : IsPrime Q

Result:
case pos
R : Type u_1
inst✝¹ : CommRing R
P : Ideal R
hP : P.IsPrime
inst✝ : IsDedekindDomain R
x : R
x_mem : x ∈ P
hxP2 : x ∉ P ^ 2
hxQ : ∀ (Q : Ideal R), Q.IsPrime → Q ≠ P → x ∉ Q
this : DecidableEq (Ideal R) := Classical.decEq (Ideal R)
hx0 : x ≠ 0
hP0 : ¬P = ⊥
hspan0 : span {x} ≠ ⊥
span_le : span {x} ≤ P
Q : Ideal R
hQ : ¬Q = P
hQp : Q.IsPrime
⊢ Multiset.count Q (normalizedFactors (span {x})) ≤ 0

case neg
R : Type u_1
inst✝¹ : CommRing R
P : Ideal R
hP : P.IsPrime
inst✝ : IsDedekindDomain R
x : R
x_mem : x ∈ P
hxP2 : x ∉ P ^ 2
hxQ : ∀ (Q : Ideal R), Q.IsPrime → Q ≠ P → x ∉ Q
this : DecidableEq (Ideal R) := Classical.decEq (Ideal R)
hx0 : x ≠ 0
hP0 : ¬P = ⊥
hspan0 : span {x} ≠ ⊥
span_le : span {x} ≤ P
Q : Ideal R
hQ : ¬Q = P
hQp : ¬Q.IsPrime
⊢ Multiset.count Q (normalizedFactors (span {x})) ≤ 0

Proof state:
case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
x : R
this : DecidableEq (Ideal R) := Classical.decEq (Ideal R)
hx0 : x ≠ 0
hP : ⊥.IsPrime
x_mem : x ∈ ⊥
hxP2 : x ∉ ⊥ ^ 2
hxQ : ∀ (Q : Ideal R), Q.IsPrime → Q ≠ ⊥ → x ∉ Q
⊢ ⊥ = span {x}

Tactic:
rwa [eq_comm, span_singleton_eq_bot, ← mem_bot]

Result:
no goals

Proof state:
case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
x : R
this : DecidableEq (Ideal R) := Classical.decEq (Ideal R)
hx0 : x ≠ 0
hspan0 : span {x} ≠ ⊥
Q : Ideal R
hP : Q.IsPrime
x_mem : x ∈ Q
hxP2 : x ∉ Q ^ 2
hxQ : ∀ (Q_1 : Ideal R), Q_1.IsPrime → Q_1 ≠ Q → x ∉ Q_1
hP0 : ¬Q = ⊥
span_le : span {x} ≤ Q
⊢ Multiset.count Q (normalizedFactors (span {x})) ≤ 1

Tactic:
refine (Ideal.count_normalizedFactors_eq ?_ ?_).le <;>
    simp only [Ideal.span_singleton_le_iff_mem, pow_one] <;>
  assumption

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommRing R
P : Ideal R
hP : P.IsPrime
inst✝ : IsDedekindDomain R
x : R
x_mem : x ∈ P
hxP2 : x ∉ P ^ 2
hxQ : ∀ (Q : Ideal R), Q.IsPrime → Q ≠ P → x ∉ Q
this : DecidableEq (Ideal R) := Classical.decEq (Ideal R)
⊢ P = span {x}

Tactic:
have hx0 : x ≠ 0 := by
  rintro rfl
  exact hxP2 (zero_mem _)

Result:
R : Type u_1
inst✝¹ : CommRing R
P : Ideal R
hP : P.IsPrime
inst✝ : IsDedekindDomain R
x : R
x_mem : x ∈ P
hxP2 : x ∉ P ^ 2
hxQ : ∀ (Q : Ideal R), Q.IsPrime → Q ≠ P → x ∉ Q
this : DecidableEq (Ideal R) := Classical.decEq (Ideal R)
hx0 : x ≠ 0
⊢ P = span {x}

Proof state:
case neg.refine_2
R : Type u_1
inst✝¹ : CommRing R
P : Ideal R
hP : P.IsPrime
inst✝ : IsDedekindDomain R
x : R
x_mem : x ∈ P
hxP2 : x ∉ P ^ 2
hxQ : ∀ (Q : Ideal R), Q.IsPrime → Q ≠ P → x ∉ Q
this : DecidableEq (Ideal R) := Classical.decEq (Ideal R)
hx0 : x ≠ 0
hP0 : ¬P = ⊥
hspan0 : span {x} ≠ ⊥
span_le : span {x} ≤ P
⊢ normalizedFactors (span {x}) ≤ normalizedFactors P

Tactic:
simp only [normalizedFactors_irreducible (Ideal.prime_of_isPrime hP0 hP).irreducible,
  normalize_eq, Multiset.le_iff_count, Multiset.count_singleton]

Result:
case neg.refine_2
R : Type u_1
inst✝¹ : CommRing R
P : Ideal R
hP : P.IsPrime
inst✝ : IsDedekindDomain R
x : R
x_mem : x ∈ P
hxP2 : x ∉ P ^ 2
hxQ : ∀ (Q : Ideal R), Q.IsPrime → Q ≠ P → x ∉ Q
this : DecidableEq (Ideal R) := Classical.decEq (Ideal R)
hx0 : x ≠ 0
hP0 : ¬P = ⊥
hspan0 : span {x} ≠ ⊥
span_le : span {x} ≤ P
⊢ ∀ (a : Ideal R), Multiset.count a (normalizedFactors (span {x})) ≤ if a = P then 1 else 0

Proof state:
case pos.refine_2
R : Type u_1
inst✝¹ : CommRing R
P : Ideal R
hP : P.IsPrime
inst✝ : IsDedekindDomain R
x : R
x_mem : x ∈ P
hxP2 : x ∉ P ^ 2
hxQ : ∀ (Q : Ideal R), Q.IsPrime → Q ≠ P → x ∉ Q
this : DecidableEq (Ideal R) := Classical.decEq (Ideal R)
hx0 : x ≠ 0
hP0 : ¬P = ⊥
hspan0 : span {x} ≠ ⊥
span_le : span {x} ≤ P
Q : Ideal R
hQ : ¬Q = P
hQp : Q.IsPrime
⊢ x ∉ Q

Tactic:
exact hxQ _ hQp hQ

Result:
no goals

Proof state:
case pos
R : Type u_1
inst✝¹ : CommRing R
P : Ideal R
hP : P.IsPrime
inst✝ : IsDedekindDomain R
x : R
x_mem : x ∈ P
hxP2 : x ∉ P ^ 2
hxQ : ∀ (Q : Ideal R), Q.IsPrime → Q ≠ P → x ∉ Q
this : DecidableEq (Ideal R) := Classical.decEq (Ideal R)
hx0 : x ≠ 0
hP0 : ¬P = ⊥
hspan0 : span {x} ≠ ⊥
span_le : span {x} ≤ P
Q : Ideal R
hQ : Q = P
⊢ Multiset.count Q (normalizedFactors (span {x})) ≤ 1

Tactic:
subst hQ

Result:
case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
x : R
this : DecidableEq (Ideal R) := Classical.decEq (Ideal R)
hx0 : x ≠ 0
hspan0 : span {x} ≠ ⊥
Q : Ideal R
hP : Q.IsPrime
x_mem : x ∈ Q
hxP2 : x ∉ Q ^ 2
hxQ : ∀ (Q_1 : Ideal R), Q_1.IsPrime → Q_1 ≠ Q → x ∉ Q_1
hP0 : ¬Q = ⊥
span_le : span {x} ≤ Q
⊢ Multiset.count Q (normalizedFactors (span {x})) ≤ 1

Proof state:
case neg.refine_2
R : Type u_1
inst✝¹ : CommRing R
P : Ideal R
hP : P.IsPrime
inst✝ : IsDedekindDomain R
x : R
x_mem : x ∈ P
hxP2 : x ∉ P ^ 2
hxQ : ∀ (Q : Ideal R), Q.IsPrime → Q ≠ P → x ∉ Q
this : DecidableEq (Ideal R) := Classical.decEq (Ideal R)
hx0 : x ≠ 0
hP0 : ¬P = ⊥
hspan0 : span {x} ≠ ⊥
span_le : span {x} ≤ P
Q : Ideal R
⊢ Multiset.count Q (normalizedFactors (span {x})) ≤ if Q = P then 1 else 0

Tactic:
split_ifs with hQ

Result:
case pos
R : Type u_1
inst✝¹ : CommRing R
P : Ideal R
hP : P.IsPrime
inst✝ : IsDedekindDomain R
x : R
x_mem : x ∈ P
hxP2 : x ∉ P ^ 2
hxQ : ∀ (Q : Ideal R), Q.IsPrime → Q ≠ P → x ∉ Q
this : DecidableEq (Ideal R) := Classical.decEq (Ideal R)
hx0 : x ≠ 0
hP0 : ¬P = ⊥
hspan0 : span {x} ≠ ⊥
span_le : span {x} ≤ P
Q : Ideal R
hQ : Q = P
⊢ Multiset.count Q (normalizedFactors (span {x})) ≤ 1

case neg
R : Type u_1
inst✝¹ : CommRing R
P : Ideal R
hP : P.IsPrime
inst✝ : IsDedekindDomain R
x : R
x_mem : x ∈ P
hxP2 : x ∉ P ^ 2
hxQ : ∀ (Q : Ideal R), Q.IsPrime → Q ≠ P → x ∉ Q
this : DecidableEq (Ideal R) := Classical.decEq (Ideal R)
hx0 : x ≠ 0
hP0 : ¬P = ⊥
hspan0 : span {x} ≠ ⊥
span_le : span {x} ≤ P
Q : Ideal R
hQ : ¬Q = P
⊢ Multiset.count Q (normalizedFactors (span {x})) ≤ 0

Proof state:
case neg
R : Type u_1
inst✝¹ : CommRing R
P : Ideal R
hP : P.IsPrime
inst✝ : IsDedekindDomain R
x : R
x_mem : x ∈ P
hxP2 : x ∉ P ^ 2
hxQ : ∀ (Q : Ideal R), Q.IsPrime → Q ≠ P → x ∉ Q
this : DecidableEq (Ideal R) := Classical.decEq (Ideal R)
hx0 : x ≠ 0
hP0 : ¬P = ⊥
hspan0 : span {x} ≠ ⊥
span_le : span {x} ≤ P
Q : Ideal R
hQ : ¬Q = P
hQp : ¬Q.IsPrime
⊢ Multiset.count Q (normalizedFactors (span {x})) ≤ 0

Tactic:
exact
  (Multiset.count_eq_zero.mpr fun hQi =>
      hQp
        (isPrime_of_prime
          (irreducible_iff_prime.mp (irreducible_of_normalized_factor _ hQi)))).le

Result:
no goals