case pos
R : Type u_1
A : Type ?u.1348878
K : Type ?u.1348881
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Field K
inst✝⁵ : IsDomain A
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
inst✝² : NormalizationMonoid R
inst✝¹ : DecidableEq R
inst✝ : DecidableEq (Ideal R)
a b : R
ha : a ∈ normalizedFactors b
hb : b = 0
⊢ span {a} ∈ normalizedFactors (span {b})

case neg
R : Type u_1
A : Type ?u.1348878
K : Type ?u.1348881
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Field K
inst✝⁵ : IsDomain A
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
inst✝² : NormalizationMonoid R
inst✝¹ : DecidableEq R
inst✝ : DecidableEq (Ideal R)
a b : R
ha : a ∈ normalizedFactors b
hb : ¬b = 0
⊢ span {a} ∈ normalizedFactors (span {b})
R : Type u_1
A : Type ?u.1348878
K : Type ?u.1348881
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Field K
inst✝⁵ : IsDomain A
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
inst✝² : NormalizationMonoid R
inst✝¹ : DecidableEq R
inst✝ : DecidableEq (Ideal R)
a b : R
ha : a ∈ normalizedFactors b
⊢ span {a} ∈ normalizedFactors (span {b})
by_cases hb : b = 0
case pos
R : Type u_1
A : Type ?u.1348878
K : Type ?u.1348881
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Field K
inst✝⁵ : IsDomain A
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
inst✝² : NormalizationMonoid R
inst✝¹ : DecidableEq R
inst✝ : DecidableEq (Ideal R)
a b : R
ha : a ∈ normalizedFactors b
hb : b = 0
⊢ span {a} ∈ 0
case pos
R : Type u_1
A : Type ?u.1348878
K : Type ?u.1348881
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Field K
inst✝⁵ : IsDomain A
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
inst✝² : NormalizationMonoid R
inst✝¹ : DecidableEq R
inst✝ : DecidableEq (Ideal R)
a b : R
ha : a ∈ normalizedFactors b
hb : b = 0
⊢ span {a} ∈ normalizedFactors (span {b})
rw [Ideal.span_singleton_eq_bot.mpr hb, bot_eq_zero, normalizedFactors_zero]
case pos
R : Type u_1
A : Type ?u.1348878
K : Type ?u.1348881
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Field K
inst✝⁵ : IsDomain A
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
inst✝² : NormalizationMonoid R
inst✝¹ : DecidableEq R
inst✝ : DecidableEq (Ideal R)
a b : R
ha : a ∈ 0
hb : b = 0
⊢ span {a} ∈ 0
case pos
R : Type u_1
A : Type ?u.1348878
K : Type ?u.1348881
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Field K
inst✝⁵ : IsDomain A
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
inst✝² : NormalizationMonoid R
inst✝¹ : DecidableEq R
inst✝ : DecidableEq (Ideal R)
a b : R
ha : a ∈ normalizedFactors b
hb : b = 0
⊢ span {a} ∈ 0
rw [hb, normalizedFactors_zero] at ha
no goals
case pos
R : Type u_1
A : Type ?u.1348878
K : Type ?u.1348881
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Field K
inst✝⁵ : IsDomain A
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
inst✝² : NormalizationMonoid R
inst✝¹ : DecidableEq R
inst✝ : DecidableEq (Ideal R)
a b : R
ha : a ∈ 0
hb : b = 0
⊢ span {a} ∈ 0
exact absurd ha (Multiset.not_mem_zero a)
case neg.refine_2
R : Type u_1
A : Type ?u.1348878
K : Type ?u.1348881
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Field K
inst✝⁵ : IsDomain A
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
inst✝² : NormalizationMonoid R
inst✝¹ : DecidableEq R
inst✝ : DecidableEq (Ideal R)
a b : R
ha : a ∈ normalizedFactors b
hb : ¬b = 0
this : Prime (span {a})
⊢ span {b} ≠ 0

case neg.refine_1
R : Type u_1
A : Type ?u.1348878
K : Type ?u.1348881
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Field K
inst✝⁵ : IsDomain A
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
inst✝² : NormalizationMonoid R
inst✝¹ : DecidableEq R
inst✝ : DecidableEq (Ideal R)
a b : R
ha : a ∈ normalizedFactors b
hb : ¬b = 0
⊢ Prime (span {a})
case neg
R : Type u_1
A : Type ?u.1348878
K : Type ?u.1348881
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Field K
inst✝⁵ : IsDomain A
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
inst✝² : NormalizationMonoid R
inst✝¹ : DecidableEq R
inst✝ : DecidableEq (Ideal R)
a b : R
ha : a ∈ normalizedFactors b
hb : ¬b = 0
⊢ span {a} ∈ normalizedFactors (span {b})
suffices Prime (Ideal.span ({a} : Set R)) by
  obtain ⟨c, hc, hc'⟩ := exists_mem_normalizedFactors_of_dvd ?_ this.irreducible
      (dvd_iff_le.mpr (span_singleton_le_span_singleton.mpr (dvd_of_mem_normalizedFactors ha)))
  rwa [associated_iff_eq.mp hc']
case neg.refine_1
R : Type u_1
A : Type ?u.1348878
K : Type ?u.1348881
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Field K
inst✝⁵ : IsDomain A
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
inst✝² : NormalizationMonoid R
inst✝¹ : DecidableEq R
inst✝ : DecidableEq (Ideal R)
a b : R
ha : a ∈ normalizedFactors b
hb : ¬b = 0
⊢ IsPrime (span {a})

case neg.refine_1
R : Type u_1
A : Type ?u.1348878
K : Type ?u.1348881
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Field K
inst✝⁵ : IsDomain A
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
inst✝² : NormalizationMonoid R
inst✝¹ : DecidableEq R
inst✝ : DecidableEq (Ideal R)
a b : R
ha : a ∈ normalizedFactors b
hb : ¬b = 0
⊢ span {a} ≠ ⊥
case neg.refine_1
R : Type u_1
A : Type ?u.1348878
K : Type ?u.1348881
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Field K
inst✝⁵ : IsDomain A
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
inst✝² : NormalizationMonoid R
inst✝¹ : DecidableEq R
inst✝ : DecidableEq (Ideal R)
a b : R
ha : a ∈ normalizedFactors b
hb : ¬b = 0
⊢ Prime (span {a})
rw [prime_iff_isPrime]
case intro.intro
R : Type u_1
A : Type ?u.1348878
K : Type ?u.1348881
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Field K
inst✝⁵ : IsDomain A
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
inst✝² : NormalizationMonoid R
inst✝¹ : DecidableEq R
inst✝ : DecidableEq (Ideal R)
a b : R
ha : a ∈ normalizedFactors b
hb : ¬b = 0
this : Prime (span {a})
c : Ideal R
hc : c ∈ normalizedFactors (span {b})
hc' : Associated (span {a}) c
⊢ span {a} ∈ normalizedFactors (span {b})
R : Type u_1
A : Type ?u.1348878
K : Type ?u.1348881
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Field K
inst✝⁵ : IsDomain A
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
inst✝² : NormalizationMonoid R
inst✝¹ : DecidableEq R
inst✝ : DecidableEq (Ideal R)
a b : R
ha : a ∈ normalizedFactors b
hb : ¬b = 0
this : Prime (span {a})
⊢ span {a} ∈ normalizedFactors (span {b})
obtain ⟨c, hc, hc'⟩ := exists_mem_normalizedFactors_of_dvd ?_ this.irreducible
    (dvd_iff_le.mpr (span_singleton_le_span_singleton.mpr (dvd_of_mem_normalizedFactors ha)))
no goals
case intro.intro
R : Type u_1
A : Type ?u.1348878
K : Type ?u.1348881
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Field K
inst✝⁵ : IsDomain A
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
inst✝² : NormalizationMonoid R
inst✝¹ : DecidableEq R
inst✝ : DecidableEq (Ideal R)
a b : R
ha : a ∈ normalizedFactors b
hb : ¬b = 0
this : Prime (span {a})
c : Ideal R
hc : c ∈ normalizedFactors (span {b})
hc' : Associated (span {a}) c
⊢ span {a} ∈ normalizedFactors (span {b})
rwa [associated_iff_eq.mp hc']
case neg.refine_2
R : Type u_1
A : Type ?u.1348878
K : Type ?u.1348881
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Field K
inst✝⁵ : IsDomain A
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
inst✝² : NormalizationMonoid R
inst✝¹ : DecidableEq R
inst✝ : DecidableEq (Ideal R)
a b : R
ha : a ∈ normalizedFactors b
hb : ¬b = 0
this : Prime (span {a})
h : span {b} = 0
⊢ False
case neg.refine_2
R : Type u_1
A : Type ?u.1348878
K : Type ?u.1348881
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Field K
inst✝⁵ : IsDomain A
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
inst✝² : NormalizationMonoid R
inst✝¹ : DecidableEq R
inst✝ : DecidableEq (Ideal R)
a b : R
ha : a ∈ normalizedFactors b
hb : ¬b = 0
this : Prime (span {a})
⊢ span {b} ≠ 0
by_contra h
no goals
case neg.refine_2
R : Type u_1
A : Type ?u.1348878
K : Type ?u.1348881
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Field K
inst✝⁵ : IsDomain A
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
inst✝² : NormalizationMonoid R
inst✝¹ : DecidableEq R
inst✝ : DecidableEq (Ideal R)
a b : R
ha : a ∈ normalizedFactors b
hb : ¬b = 0
this : Prime (span {a})
h : span {b} = 0
⊢ False
exact hb (span_singleton_eq_bot.mp h)
no goals
case neg.refine_1
R : Type u_1
A : Type ?u.1348878
K : Type ?u.1348881
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Field K
inst✝⁵ : IsDomain A
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
inst✝² : NormalizationMonoid R
inst✝¹ : DecidableEq R
inst✝ : DecidableEq (Ideal R)
a b : R
ha : a ∈ normalizedFactors b
hb : ¬b = 0
⊢ IsPrime (span {a})
exact (span_singleton_prime (prime_of_normalized_factor a ha).ne_zero).mpr
  (prime_of_normalized_factor a ha)
case neg.refine_1
R : Type u_1
A : Type ?u.1348878
K : Type ?u.1348881
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Field K
inst✝⁵ : IsDomain A
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
inst✝² : NormalizationMonoid R
inst✝¹ : DecidableEq R
inst✝ : DecidableEq (Ideal R)
a b : R
ha : a ∈ normalizedFactors b
hb : ¬b = 0
h : span {a} = ⊥
⊢ False
case neg.refine_1
R : Type u_1
A : Type ?u.1348878
K : Type ?u.1348881
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Field K
inst✝⁵ : IsDomain A
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
inst✝² : NormalizationMonoid R
inst✝¹ : DecidableEq R
inst✝ : DecidableEq (Ideal R)
a b : R
ha : a ∈ normalizedFactors b
hb : ¬b = 0
⊢ span {a} ≠ ⊥
by_contra h
no goals
case neg.refine_1
R : Type u_1
A : Type ?u.1348878
K : Type ?u.1348881
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Field K
inst✝⁵ : IsDomain A
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
inst✝² : NormalizationMonoid R
inst✝¹ : DecidableEq R
inst✝ : DecidableEq (Ideal R)
a b : R
ha : a ∈ normalizedFactors b
hb : ¬b = 0
h : span {a} = ⊥
⊢ False
exact (prime_of_normalized_factor a ha).ne_zero (span_singleton_eq_bot.mp h)