R : Type ?u.906300
A : Type ?u.906303
K : Type ?u.906306
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
T : Type u_1
inst✝² : CommRing T
inst✝¹ : IsDomain T
inst✝ : IsDedekindDomain T
I J : Ideal T
hI : I ≠ ⊥
hJ : J ≠ ⊥
H :
  normalizedFactors (Multiset.prod (normalizedFactors I ∩ normalizedFactors J)) =
    normalizedFactors I ∩ normalizedFactors J
⊢ I ⊔ J = Multiset.prod (normalizedFactors I ∩ normalizedFactors J)
R : Type ?u.906300
A : Type ?u.906303
K : Type ?u.906306
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
T : Type u_1
inst✝² : CommRing T
inst✝¹ : IsDomain T
inst✝ : IsDedekindDomain T
I J : Ideal T
hI : I ≠ ⊥
hJ : J ≠ ⊥
⊢ I ⊔ J = Multiset.prod (normalizedFactors I ∩ normalizedFactors J)
have H : normalizedFactors (normalizedFactors I ∩ normalizedFactors J).prod =
    normalizedFactors I ∩ normalizedFactors J := by
  apply normalizedFactors_prod_of_prime
  intro p hp
  rw [mem_inter] at hp
  exact prime_of_normalized_factor p hp.left
R : Type ?u.906300
A : Type ?u.906303
K : Type ?u.906306
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
T : Type u_1
inst✝² : CommRing T
inst✝¹ : IsDomain T
inst✝ : IsDedekindDomain T
I J : Ideal T
hI : I ≠ ⊥
hJ : J ≠ ⊥
H :
  normalizedFactors (Multiset.prod (normalizedFactors I ∩ normalizedFactors J)) =
    normalizedFactors I ∩ normalizedFactors J
this : Multiset.prod (normalizedFactors I ∩ normalizedFactors J) ≠ 0
⊢ I ⊔ J = Multiset.prod (normalizedFactors I ∩ normalizedFactors J)
R : Type ?u.906300
A : Type ?u.906303
K : Type ?u.906306
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
T : Type u_1
inst✝² : CommRing T
inst✝¹ : IsDomain T
inst✝ : IsDedekindDomain T
I J : Ideal T
hI : I ≠ ⊥
hJ : J ≠ ⊥
H :
  normalizedFactors (Multiset.prod (normalizedFactors I ∩ normalizedFactors J)) =
    normalizedFactors I ∩ normalizedFactors J
⊢ I ⊔ J = Multiset.prod (normalizedFactors I ∩ normalizedFactors J)
have := Multiset.prod_ne_zero_of_prime (normalizedFactors I ∩ normalizedFactors J) fun _ h =>
    prime_of_normalized_factor _ (Multiset.mem_inter.1 h).1
case a
R : Type ?u.906300
A : Type ?u.906303
K : Type ?u.906306
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
T : Type u_1
inst✝² : CommRing T
inst✝¹ : IsDomain T
inst✝ : IsDedekindDomain T
I J : Ideal T
hI : I ≠ ⊥
hJ : J ≠ ⊥
H :
  normalizedFactors (Multiset.prod (normalizedFactors I ∩ normalizedFactors J)) =
    normalizedFactors I ∩ normalizedFactors J
this : Multiset.prod (normalizedFactors I ∩ normalizedFactors J) ≠ 0
⊢ I ⊔ J ≤ Multiset.prod (normalizedFactors I ∩ normalizedFactors J)

case a
R : Type ?u.906300
A : Type ?u.906303
K : Type ?u.906306
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
T : Type u_1
inst✝² : CommRing T
inst✝¹ : IsDomain T
inst✝ : IsDedekindDomain T
I J : Ideal T
hI : I ≠ ⊥
hJ : J ≠ ⊥
H :
  normalizedFactors (Multiset.prod (normalizedFactors I ∩ normalizedFactors J)) =
    normalizedFactors I ∩ normalizedFactors J
this : Multiset.prod (normalizedFactors I ∩ normalizedFactors J) ≠ 0
⊢ Multiset.prod (normalizedFactors I ∩ normalizedFactors J) ≤ I ⊔ J
R : Type ?u.906300
A : Type ?u.906303
K : Type ?u.906306
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
T : Type u_1
inst✝² : CommRing T
inst✝¹ : IsDomain T
inst✝ : IsDedekindDomain T
I J : Ideal T
hI : I ≠ ⊥
hJ : J ≠ ⊥
H :
  normalizedFactors (Multiset.prod (normalizedFactors I ∩ normalizedFactors J)) =
    normalizedFactors I ∩ normalizedFactors J
this : Multiset.prod (normalizedFactors I ∩ normalizedFactors J) ≠ 0
⊢ I ⊔ J = Multiset.prod (normalizedFactors I ∩ normalizedFactors J)
apply le_antisymm
case h
R : Type ?u.906300
A : Type ?u.906303
K : Type ?u.906306
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
T : Type u_1
inst✝² : CommRing T
inst✝¹ : IsDomain T
inst✝ : IsDedekindDomain T
I J : Ideal T
hI : I ≠ ⊥
hJ : J ≠ ⊥
⊢ ∀ (p : Ideal T), p ∈ normalizedFactors I ∩ normalizedFactors J → Prime p
R : Type ?u.906300
A : Type ?u.906303
K : Type ?u.906306
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
T : Type u_1
inst✝² : CommRing T
inst✝¹ : IsDomain T
inst✝ : IsDedekindDomain T
I J : Ideal T
hI : I ≠ ⊥
hJ : J ≠ ⊥
⊢ normalizedFactors (Multiset.prod (normalizedFactors I ∩ normalizedFactors J)) =
    normalizedFactors I ∩ normalizedFactors J
apply normalizedFactors_prod_of_prime
case h
R : Type ?u.906300
A : Type ?u.906303
K : Type ?u.906306
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
T : Type u_1
inst✝² : CommRing T
inst✝¹ : IsDomain T
inst✝ : IsDedekindDomain T
I J : Ideal T
hI : I ≠ ⊥
hJ : J ≠ ⊥
p : Ideal T
hp : p ∈ normalizedFactors I ∩ normalizedFactors J
⊢ Prime p
case h
R : Type ?u.906300
A : Type ?u.906303
K : Type ?u.906306
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
T : Type u_1
inst✝² : CommRing T
inst✝¹ : IsDomain T
inst✝ : IsDedekindDomain T
I J : Ideal T
hI : I ≠ ⊥
hJ : J ≠ ⊥
⊢ ∀ (p : Ideal T), p ∈ normalizedFactors I ∩ normalizedFactors J → Prime p
intro p hp
case h
R : Type ?u.906300
A : Type ?u.906303
K : Type ?u.906306
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
T : Type u_1
inst✝² : CommRing T
inst✝¹ : IsDomain T
inst✝ : IsDedekindDomain T
I J : Ideal T
hI : I ≠ ⊥
hJ : J ≠ ⊥
p : Ideal T
hp : p ∈ normalizedFactors I ∧ p ∈ normalizedFactors J
⊢ Prime p
case h
R : Type ?u.906300
A : Type ?u.906303
K : Type ?u.906306
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
T : Type u_1
inst✝² : CommRing T
inst✝¹ : IsDomain T
inst✝ : IsDedekindDomain T
I J : Ideal T
hI : I ≠ ⊥
hJ : J ≠ ⊥
p : Ideal T
hp : p ∈ normalizedFactors I ∩ normalizedFactors J
⊢ Prime p
rw [mem_inter] at hp
no goals
case h
R : Type ?u.906300
A : Type ?u.906303
K : Type ?u.906306
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
T : Type u_1
inst✝² : CommRing T
inst✝¹ : IsDomain T
inst✝ : IsDedekindDomain T
I J : Ideal T
hI : I ≠ ⊥
hJ : J ≠ ⊥
p : Ideal T
hp : p ∈ normalizedFactors I ∧ p ∈ normalizedFactors J
⊢ Prime p
exact prime_of_normalized_factor p hp.left
case a
R : Type ?u.906300
A : Type ?u.906303
K : Type ?u.906306
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
T : Type u_1
inst✝² : CommRing T
inst✝¹ : IsDomain T
inst✝ : IsDedekindDomain T
I J : Ideal T
hI : I ≠ ⊥
hJ : J ≠ ⊥
H :
  normalizedFactors (Multiset.prod (normalizedFactors I ∩ normalizedFactors J)) =
    normalizedFactors I ∩ normalizedFactors J
this : Multiset.prod (normalizedFactors I ∩ normalizedFactors J) ≠ 0
⊢ Multiset.prod (normalizedFactors I ∩ normalizedFactors J) ∣ I ∧
    Multiset.prod (normalizedFactors I ∩ normalizedFactors J) ∣ J
case a
R : Type ?u.906300
A : Type ?u.906303
K : Type ?u.906306
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
T : Type u_1
inst✝² : CommRing T
inst✝¹ : IsDomain T
inst✝ : IsDedekindDomain T
I J : Ideal T
hI : I ≠ ⊥
hJ : J ≠ ⊥
H :
  normalizedFactors (Multiset.prod (normalizedFactors I ∩ normalizedFactors J)) =
    normalizedFactors I ∩ normalizedFactors J
this : Multiset.prod (normalizedFactors I ∩ normalizedFactors J) ≠ 0
⊢ I ⊔ J ≤ Multiset.prod (normalizedFactors I ∩ normalizedFactors J)
rw [sup_le_iff, ← dvd_iff_le, ← dvd_iff_le]
case a.left
R : Type ?u.906300
A : Type ?u.906303
K : Type ?u.906306
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
T : Type u_1
inst✝² : CommRing T
inst✝¹ : IsDomain T
inst✝ : IsDedekindDomain T
I J : Ideal T
hI : I ≠ ⊥
hJ : J ≠ ⊥
H :
  normalizedFactors (Multiset.prod (normalizedFactors I ∩ normalizedFactors J)) =
    normalizedFactors I ∩ normalizedFactors J
this : Multiset.prod (normalizedFactors I ∩ normalizedFactors J) ≠ 0
⊢ Multiset.prod (normalizedFactors I ∩ normalizedFactors J) ∣ I

case a.right
R : Type ?u.906300
A : Type ?u.906303
K : Type ?u.906306
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
T : Type u_1
inst✝² : CommRing T
inst✝¹ : IsDomain T
inst✝ : IsDedekindDomain T
I J : Ideal T
hI : I ≠ ⊥
hJ : J ≠ ⊥
H :
  normalizedFactors (Multiset.prod (normalizedFactors I ∩ normalizedFactors J)) =
    normalizedFactors I ∩ normalizedFactors J
this : Multiset.prod (normalizedFactors I ∩ normalizedFactors J) ≠ 0
⊢ Multiset.prod (normalizedFactors I ∩ normalizedFactors J) ∣ J
case a
R : Type ?u.906300
A : Type ?u.906303
K : Type ?u.906306
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
T : Type u_1
inst✝² : CommRing T
inst✝¹ : IsDomain T
inst✝ : IsDedekindDomain T
I J : Ideal T
hI : I ≠ ⊥
hJ : J ≠ ⊥
H :
  normalizedFactors (Multiset.prod (normalizedFactors I ∩ normalizedFactors J)) =
    normalizedFactors I ∩ normalizedFactors J
this : Multiset.prod (normalizedFactors I ∩ normalizedFactors J) ≠ 0
⊢ Multiset.prod (normalizedFactors I ∩ normalizedFactors J) ∣ I ∧
    Multiset.prod (normalizedFactors I ∩ normalizedFactors J) ∣ J
constructor
case a.left
R : Type ?u.906300
A : Type ?u.906303
K : Type ?u.906306
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
T : Type u_1
inst✝² : CommRing T
inst✝¹ : IsDomain T
inst✝ : IsDedekindDomain T
I J : Ideal T
hI : I ≠ ⊥
hJ : J ≠ ⊥
H :
  normalizedFactors (Multiset.prod (normalizedFactors I ∩ normalizedFactors J)) =
    normalizedFactors I ∩ normalizedFactors J
this : Multiset.prod (normalizedFactors I ∩ normalizedFactors J) ≠ 0
⊢ normalizedFactors I ∩ normalizedFactors J ≤ normalizedFactors I
case a.left
R : Type ?u.906300
A : Type ?u.906303
K : Type ?u.906306
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
T : Type u_1
inst✝² : CommRing T
inst✝¹ : IsDomain T
inst✝ : IsDedekindDomain T
I J : Ideal T
hI : I ≠ ⊥
hJ : J ≠ ⊥
H :
  normalizedFactors (Multiset.prod (normalizedFactors I ∩ normalizedFactors J)) =
    normalizedFactors I ∩ normalizedFactors J
this : Multiset.prod (normalizedFactors I ∩ normalizedFactors J) ≠ 0
⊢ Multiset.prod (normalizedFactors I ∩ normalizedFactors J) ∣ I
rw [dvd_iff_normalizedFactors_le_normalizedFactors this hI, H]
no goals
case a.left
R : Type ?u.906300
A : Type ?u.906303
K : Type ?u.906306
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
T : Type u_1
inst✝² : CommRing T
inst✝¹ : IsDomain T
inst✝ : IsDedekindDomain T
I J : Ideal T
hI : I ≠ ⊥
hJ : J ≠ ⊥
H :
  normalizedFactors (Multiset.prod (normalizedFactors I ∩ normalizedFactors J)) =
    normalizedFactors I ∩ normalizedFactors J
this : Multiset.prod (normalizedFactors I ∩ normalizedFactors J) ≠ 0
⊢ normalizedFactors I ∩ normalizedFactors J ≤ normalizedFactors I
exact inf_le_left
case a.right
R : Type ?u.906300
A : Type ?u.906303
K : Type ?u.906306
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
T : Type u_1
inst✝² : CommRing T
inst✝¹ : IsDomain T
inst✝ : IsDedekindDomain T
I J : Ideal T
hI : I ≠ ⊥
hJ : J ≠ ⊥
H :
  normalizedFactors (Multiset.prod (normalizedFactors I ∩ normalizedFactors J)) =
    normalizedFactors I ∩ normalizedFactors J
this : Multiset.prod (normalizedFactors I ∩ normalizedFactors J) ≠ 0
⊢ normalizedFactors I ∩ normalizedFactors J ≤ normalizedFactors J
case a.right
R : Type ?u.906300
A : Type ?u.906303
K : Type ?u.906306
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
T : Type u_1
inst✝² : CommRing T
inst✝¹ : IsDomain T
inst✝ : IsDedekindDomain T
I J : Ideal T
hI : I ≠ ⊥
hJ : J ≠ ⊥
H :
  normalizedFactors (Multiset.prod (normalizedFactors I ∩ normalizedFactors J)) =
    normalizedFactors I ∩ normalizedFactors J
this : Multiset.prod (normalizedFactors I ∩ normalizedFactors J) ≠ 0
⊢ Multiset.prod (normalizedFactors I ∩ normalizedFactors J) ∣ J
rw [dvd_iff_normalizedFactors_le_normalizedFactors this hJ, H]
no goals
case a.right
R : Type ?u.906300
A : Type ?u.906303
K : Type ?u.906306
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
T : Type u_1
inst✝² : CommRing T
inst✝¹ : IsDomain T
inst✝ : IsDedekindDomain T
I J : Ideal T
hI : I ≠ ⊥
hJ : J ≠ ⊥
H :
  normalizedFactors (Multiset.prod (normalizedFactors I ∩ normalizedFactors J)) =
    normalizedFactors I ∩ normalizedFactors J
this : Multiset.prod (normalizedFactors I ∩ normalizedFactors J) ≠ 0
⊢ normalizedFactors I ∩ normalizedFactors J ≤ normalizedFactors J
exact inf_le_right
case a
R : Type ?u.906300
A : Type ?u.906303
K : Type ?u.906306
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
T : Type u_1
inst✝² : CommRing T
inst✝¹ : IsDomain T
inst✝ : IsDedekindDomain T
I J : Ideal T
hI : I ≠ ⊥
hJ : J ≠ ⊥
H :
  normalizedFactors (Multiset.prod (normalizedFactors I ∩ normalizedFactors J)) =
    normalizedFactors I ∩ normalizedFactors J
this : Multiset.prod (normalizedFactors I ∩ normalizedFactors J) ≠ 0
⊢ ∀ (a : Ideal T), count a (normalizedFactors (I ⊔ J)) ≤ count a (normalizedFactors I ∩ normalizedFactors J)

case a
R : Type ?u.906300
A : Type ?u.906303
K : Type ?u.906306
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
T : Type u_1
inst✝² : CommRing T
inst✝¹ : IsDomain T
inst✝ : IsDedekindDomain T
I J : Ideal T
hI : I ≠ ⊥
hJ : J ≠ ⊥
H :
  normalizedFactors (Multiset.prod (normalizedFactors I ∩ normalizedFactors J)) =
    normalizedFactors I ∩ normalizedFactors J
this : Multiset.prod (normalizedFactors I ∩ normalizedFactors J) ≠ 0
⊢ ∀ (p : Ideal T), p ∈ normalizedFactors I ∩ normalizedFactors J → Prime p

case a.hx
R : Type ?u.906300
A : Type ?u.906303
K : Type ?u.906306
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
T : Type u_1
inst✝² : CommRing T
inst✝¹ : IsDomain T
inst✝ : IsDedekindDomain T
I J : Ideal T
hI : I ≠ ⊥
hJ : J ≠ ⊥
H :
  normalizedFactors (Multiset.prod (normalizedFactors I ∩ normalizedFactors J)) =
    normalizedFactors I ∩ normalizedFactors J
this : Multiset.prod (normalizedFactors I ∩ normalizedFactors J) ≠ 0
⊢ I ⊔ J ≠ 0

case a.hy
R : Type ?u.906300
A : Type ?u.906303
K : Type ?u.906306
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
T : Type u_1
inst✝² : CommRing T
inst✝¹ : IsDomain T
inst✝ : IsDedekindDomain T
I J : Ideal T
hI : I ≠ ⊥
hJ : J ≠ ⊥
H :
  normalizedFactors (Multiset.prod (normalizedFactors I ∩ normalizedFactors J)) =
    normalizedFactors I ∩ normalizedFactors J
this : Multiset.prod (normalizedFactors I ∩ normalizedFactors J) ≠ 0
⊢ Multiset.prod (normalizedFactors I ∩ normalizedFactors J) ≠ 0
case a
R : Type ?u.906300
A : Type ?u.906303
K : Type ?u.906306
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
T : Type u_1
inst✝² : CommRing T
inst✝¹ : IsDomain T
inst✝ : IsDedekindDomain T
I J : Ideal T
hI : I ≠ ⊥
hJ : J ≠ ⊥
H :
  normalizedFactors (Multiset.prod (normalizedFactors I ∩ normalizedFactors J)) =
    normalizedFactors I ∩ normalizedFactors J
this : Multiset.prod (normalizedFactors I ∩ normalizedFactors J) ≠ 0
⊢ Multiset.prod (normalizedFactors I ∩ normalizedFactors J) ≤ I ⊔ J
rw [← dvd_iff_le, dvd_iff_normalizedFactors_le_normalizedFactors,
  normalizedFactors_prod_of_prime, le_iff_count]
case a
R : Type ?u.906300
A : Type ?u.906303
K : Type ?u.906306
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
T : Type u_1
inst✝² : CommRing T
inst✝¹ : IsDomain T
inst✝ : IsDedekindDomain T
I J : Ideal T
hI : I ≠ ⊥
hJ : J ≠ ⊥
H :
  normalizedFactors (Multiset.prod (normalizedFactors I ∩ normalizedFactors J)) =
    normalizedFactors I ∩ normalizedFactors J
this : Multiset.prod (normalizedFactors I ∩ normalizedFactors J) ≠ 0
a : Ideal T
⊢ count a (normalizedFactors (I ⊔ J)) ≤ count a (normalizedFactors I ∩ normalizedFactors J)
case a
R : Type ?u.906300
A : Type ?u.906303
K : Type ?u.906306
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
T : Type u_1
inst✝² : CommRing T
inst✝¹ : IsDomain T
inst✝ : IsDedekindDomain T
I J : Ideal T
hI : I ≠ ⊥
hJ : J ≠ ⊥
H :
  normalizedFactors (Multiset.prod (normalizedFactors I ∩ normalizedFactors J)) =
    normalizedFactors I ∩ normalizedFactors J
this : Multiset.prod (normalizedFactors I ∩ normalizedFactors J) ≠ 0
⊢ ∀ (a : Ideal T), count a (normalizedFactors (I ⊔ J)) ≤ count a (normalizedFactors I ∩ normalizedFactors J)
intro a
case a
R : Type ?u.906300
A : Type ?u.906303
K : Type ?u.906306
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
T : Type u_1
inst✝² : CommRing T
inst✝¹ : IsDomain T
inst✝ : IsDedekindDomain T
I J : Ideal T
hI : I ≠ ⊥
hJ : J ≠ ⊥
H :
  normalizedFactors (Multiset.prod (normalizedFactors I ∩ normalizedFactors J)) =
    normalizedFactors I ∩ normalizedFactors J
this : Multiset.prod (normalizedFactors I ∩ normalizedFactors J) ≠ 0
a : Ideal T
⊢ count a (normalizedFactors (I ⊔ J)) ≤ min (count a (normalizedFactors I)) (count a (normalizedFactors J))
case a
R : Type ?u.906300
A : Type ?u.906303
K : Type ?u.906306
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
T : Type u_1
inst✝² : CommRing T
inst✝¹ : IsDomain T
inst✝ : IsDedekindDomain T
I J : Ideal T
hI : I ≠ ⊥
hJ : J ≠ ⊥
H :
  normalizedFactors (Multiset.prod (normalizedFactors I ∩ normalizedFactors J)) =
    normalizedFactors I ∩ normalizedFactors J
this : Multiset.prod (normalizedFactors I ∩ normalizedFactors J) ≠ 0
a : Ideal T
⊢ count a (normalizedFactors (I ⊔ J)) ≤ count a (normalizedFactors I ∩ normalizedFactors J)
rw [Multiset.count_inter]
no goals
case a
R : Type ?u.906300
A : Type ?u.906303
K : Type ?u.906306
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
T : Type u_1
inst✝² : CommRing T
inst✝¹ : IsDomain T
inst✝ : IsDedekindDomain T
I J : Ideal T
hI : I ≠ ⊥
hJ : J ≠ ⊥
H :
  normalizedFactors (Multiset.prod (normalizedFactors I ∩ normalizedFactors J)) =
    normalizedFactors I ∩ normalizedFactors J
this : Multiset.prod (normalizedFactors I ∩ normalizedFactors J) ≠ 0
a : Ideal T
⊢ count a (normalizedFactors (I ⊔ J)) ≤ min (count a (normalizedFactors I)) (count a (normalizedFactors J))
exact le_min (count_le_of_ideal_ge le_sup_left hI a) (count_le_of_ideal_ge le_sup_right hJ a)
case a
R : Type ?u.906300
A : Type ?u.906303
K : Type ?u.906306
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
T : Type u_1
inst✝² : CommRing T
inst✝¹ : IsDomain T
inst✝ : IsDedekindDomain T
I J : Ideal T
hI : I ≠ ⊥
hJ : J ≠ ⊥
H :
  normalizedFactors (Multiset.prod (normalizedFactors I ∩ normalizedFactors J)) =
    normalizedFactors I ∩ normalizedFactors J
this : Multiset.prod (normalizedFactors I ∩ normalizedFactors J) ≠ 0
p : Ideal T
hp : p ∈ normalizedFactors I ∩ normalizedFactors J
⊢ Prime p
case a
R : Type ?u.906300
A : Type ?u.906303
K : Type ?u.906306
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
T : Type u_1
inst✝² : CommRing T
inst✝¹ : IsDomain T
inst✝ : IsDedekindDomain T
I J : Ideal T
hI : I ≠ ⊥
hJ : J ≠ ⊥
H :
  normalizedFactors (Multiset.prod (normalizedFactors I ∩ normalizedFactors J)) =
    normalizedFactors I ∩ normalizedFactors J
this : Multiset.prod (normalizedFactors I ∩ normalizedFactors J) ≠ 0
⊢ ∀ (p : Ideal T), p ∈ normalizedFactors I ∩ normalizedFactors J → Prime p
intro p hp
case a
R : Type ?u.906300
A : Type ?u.906303
K : Type ?u.906306
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
T : Type u_1
inst✝² : CommRing T
inst✝¹ : IsDomain T
inst✝ : IsDedekindDomain T
I J : Ideal T
hI : I ≠ ⊥
hJ : J ≠ ⊥
H :
  normalizedFactors (Multiset.prod (normalizedFactors I ∩ normalizedFactors J)) =
    normalizedFactors I ∩ normalizedFactors J
this : Multiset.prod (normalizedFactors I ∩ normalizedFactors J) ≠ 0
p : Ideal T
hp : p ∈ normalizedFactors I ∧ p ∈ normalizedFactors J
⊢ Prime p
case a
R : Type ?u.906300
A : Type ?u.906303
K : Type ?u.906306
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
T : Type u_1
inst✝² : CommRing T
inst✝¹ : IsDomain T
inst✝ : IsDedekindDomain T
I J : Ideal T
hI : I ≠ ⊥
hJ : J ≠ ⊥
H :
  normalizedFactors (Multiset.prod (normalizedFactors I ∩ normalizedFactors J)) =
    normalizedFactors I ∩ normalizedFactors J
this : Multiset.prod (normalizedFactors I ∩ normalizedFactors J) ≠ 0
p : Ideal T
hp : p ∈ normalizedFactors I ∩ normalizedFactors J
⊢ Prime p
rw [mem_inter] at hp
no goals
case a
R : Type ?u.906300
A : Type ?u.906303
K : Type ?u.906306
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
T : Type u_1
inst✝² : CommRing T
inst✝¹ : IsDomain T
inst✝ : IsDedekindDomain T
I J : Ideal T
hI : I ≠ ⊥
hJ : J ≠ ⊥
H :
  normalizedFactors (Multiset.prod (normalizedFactors I ∩ normalizedFactors J)) =
    normalizedFactors I ∩ normalizedFactors J
this : Multiset.prod (normalizedFactors I ∩ normalizedFactors J) ≠ 0
p : Ideal T
hp : p ∈ normalizedFactors I ∧ p ∈ normalizedFactors J
⊢ Prime p
exact prime_of_normalized_factor p hp.left
no goals
case a.hx
R : Type ?u.906300
A : Type ?u.906303
K : Type ?u.906306
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
T : Type u_1
inst✝² : CommRing T
inst✝¹ : IsDomain T
inst✝ : IsDedekindDomain T
I J : Ideal T
hI : I ≠ ⊥
hJ : J ≠ ⊥
H :
  normalizedFactors (Multiset.prod (normalizedFactors I ∩ normalizedFactors J)) =
    normalizedFactors I ∩ normalizedFactors J
this : Multiset.prod (normalizedFactors I ∩ normalizedFactors J) ≠ 0
⊢ I ⊔ J ≠ 0
exact ne_bot_of_le_ne_bot hI le_sup_left
no goals
case a.hy
R : Type ?u.906300
A : Type ?u.906303
K : Type ?u.906306
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDomain A
T : Type u_1
inst✝² : CommRing T
inst✝¹ : IsDomain T
inst✝ : IsDedekindDomain T
I J : Ideal T
hI : I ≠ ⊥
hJ : J ≠ ⊥
H :
  normalizedFactors (Multiset.prod (normalizedFactors I ∩ normalizedFactors J)) =
    normalizedFactors I ∩ normalizedFactors J
this : Multiset.prod (normalizedFactors I ∩ normalizedFactors J) ≠ 0
⊢ Multiset.prod (normalizedFactors I ∩ normalizedFactors J) ≠ 0
exact this