R : Type u_2
A : Type ?u.1194471
K : Type ?u.1194474
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
ι : Type u_1
s : Finset ι
f : ι → Ideal R
e : ι → ℕ
prime : ∀ (i : ι), i ∈ s → Prime (f i)
coprime : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → f i ≠ f j
this : DecidableEq ι := Classical.decEq ι
⊢ (Finset.inf s fun i => f i ^ e i) = ∏ i in s, f i ^ e i
R : Type u_2
A : Type ?u.1194471
K : Type ?u.1194474
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
ι : Type u_1
s : Finset ι
f : ι → Ideal R
e : ι → ℕ
prime : ∀ (i : ι), i ∈ s → Prime (f i)
coprime : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → f i ≠ f j
⊢ (Finset.inf s fun i => f i ^ e i) = ∏ i in s, f i ^ e i
letI := Classical.decEq ι
R : Type u_2
A : Type ?u.1194471
K : Type ?u.1194474
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
ι : Type u_1
s : Finset ι
f : ι → Ideal R
e : ι → ℕ
this : DecidableEq ι := Classical.decEq ι
⊢ (∀ (i : ι), i ∈ s → Prime (f i)) →
    (∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → f i ≠ f j) → (Finset.inf s fun i => f i ^ e i) = ∏ i in s, f i ^ e i
R : Type u_2
A : Type ?u.1194471
K : Type ?u.1194474
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
ι : Type u_1
s : Finset ι
f : ι → Ideal R
e : ι → ℕ
prime : ∀ (i : ι), i ∈ s → Prime (f i)
coprime : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → f i ≠ f j
this : DecidableEq ι := Classical.decEq ι
⊢ (Finset.inf s fun i => f i ^ e i) = ∏ i in s, f i ^ e i
revert prime coprime
case refine_1
R : Type u_2
A : Type ?u.1194471
K : Type ?u.1194474
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
ι : Type u_1
s : Finset ι
f : ι → Ideal R
e : ι → ℕ
this : DecidableEq ι := Classical.decEq ι
⊢ (∀ (i : ι), i ∈ ∅ → Prime (f i)) →
    (∀ (i : ι), i ∈ ∅ → ∀ (j : ι), j ∈ ∅ → i ≠ j → f i ≠ f j) → (Finset.inf ∅ fun i => f i ^ e i) = ∏ i in ∅, f i ^ e i

case refine_2
R : Type u_2
A : Type ?u.1194471
K : Type ?u.1194474
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
ι : Type u_1
s : Finset ι
f : ι → Ideal R
e : ι → ℕ
this : DecidableEq ι := Classical.decEq ι
⊢ ∀ ⦃a : ι⦄ {s : Finset ι},
    ¬a ∈ s →
      ((∀ (i : ι), i ∈ s → Prime (f i)) →
          (∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → f i ≠ f j) →
            (Finset.inf s fun i => f i ^ e i) = ∏ i in s, f i ^ e i) →
        (∀ (i : ι), i ∈ insert a s → Prime (f i)) →
          (∀ (i : ι), i ∈ insert a s → ∀ (j : ι), j ∈ insert a s → i ≠ j → f i ≠ f j) →
            (Finset.inf (insert a s) fun i => f i ^ e i) = ∏ i in insert a s, f i ^ e i
R : Type u_2
A : Type ?u.1194471
K : Type ?u.1194474
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
ι : Type u_1
s : Finset ι
f : ι → Ideal R
e : ι → ℕ
this : DecidableEq ι := Classical.decEq ι
⊢ (∀ (i : ι), i ∈ s → Prime (f i)) →
    (∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → f i ≠ f j) → (Finset.inf s fun i => f i ^ e i) = ∏ i in s, f i ^ e i
refine s.induction ?_ ?_
case refine_2
R : Type u_2
A : Type ?u.1194471
K : Type ?u.1194474
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
ι : Type u_1
s✝ : Finset ι
f : ι → Ideal R
e : ι → ℕ
this : DecidableEq ι := Classical.decEq ι
a : ι
s : Finset ι
ha : ¬a ∈ s
ih :
  (∀ (i : ι), i ∈ s → Prime (f i)) →
    (∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → f i ≠ f j) → (Finset.inf s fun i => f i ^ e i) = ∏ i in s, f i ^ e i
prime : ∀ (i : ι), i ∈ insert a s → Prime (f i)
coprime : ∀ (i : ι), i ∈ insert a s → ∀ (j : ι), j ∈ insert a s → i ≠ j → f i ≠ f j
⊢ (Finset.inf (insert a s) fun i => f i ^ e i) = ∏ i in insert a s, f i ^ e i
case refine_2
R : Type u_2
A : Type ?u.1194471
K : Type ?u.1194474
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
ι : Type u_1
s : Finset ι
f : ι → Ideal R
e : ι → ℕ
this : DecidableEq ι := Classical.decEq ι
⊢ ∀ ⦃a : ι⦄ {s : Finset ι},
    ¬a ∈ s →
      ((∀ (i : ι), i ∈ s → Prime (f i)) →
          (∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → f i ≠ f j) →
            (Finset.inf s fun i => f i ^ e i) = ∏ i in s, f i ^ e i) →
        (∀ (i : ι), i ∈ insert a s → Prime (f i)) →
          (∀ (i : ι), i ∈ insert a s → ∀ (j : ι), j ∈ insert a s → i ≠ j → f i ≠ f j) →
            (Finset.inf (insert a s) fun i => f i ^ e i) = ∏ i in insert a s, f i ^ e i
intro a s ha ih prime coprime
case refine_2
R : Type u_2
A : Type ?u.1194471
K : Type ?u.1194474
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
ι : Type u_1
s✝ : Finset ι
f : ι → Ideal R
e : ι → ℕ
this : DecidableEq ι := Classical.decEq ι
a : ι
s : Finset ι
ha : ¬a ∈ s
prime : ∀ (i : ι), i ∈ insert a s → Prime (f i)
coprime : ∀ (i : ι), i ∈ insert a s → ∀ (j : ι), j ∈ insert a s → i ≠ j → f i ≠ f j
ih : (Finset.inf s fun i => f i ^ e i) = ∏ i in s, f i ^ e i
⊢ (Finset.inf (insert a s) fun i => f i ^ e i) = ∏ i in insert a s, f i ^ e i
case refine_2
R : Type u_2
A : Type ?u.1194471
K : Type ?u.1194474
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
ι : Type u_1
s✝ : Finset ι
f : ι → Ideal R
e : ι → ℕ
this : DecidableEq ι := Classical.decEq ι
a : ι
s : Finset ι
ha : ¬a ∈ s
ih :
  (∀ (i : ι), i ∈ s → Prime (f i)) →
    (∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → f i ≠ f j) → (Finset.inf s fun i => f i ^ e i) = ∏ i in s, f i ^ e i
prime : ∀ (i : ι), i ∈ insert a s → Prime (f i)
coprime : ∀ (i : ι), i ∈ insert a s → ∀ (j : ι), j ∈ insert a s → i ≠ j → f i ≠ f j
⊢ (Finset.inf (insert a s) fun i => f i ^ e i) = ∏ i in insert a s, f i ^ e i
specialize
  ih (fun i hi => prime i (Finset.mem_insert_of_mem hi)) fun i hi j hj =>
    coprime i (Finset.mem_insert_of_mem hi) j (Finset.mem_insert_of_mem hj)
case refine_2
R : Type u_2
A : Type ?u.1194471
K : Type ?u.1194474
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
ι : Type u_1
s✝ : Finset ι
f : ι → Ideal R
e : ι → ℕ
this : DecidableEq ι := Classical.decEq ι
a : ι
s : Finset ι
ha : ¬a ∈ s
prime : ∀ (i : ι), i ∈ insert a s → Prime (f i)
coprime : ∀ (i : ι), i ∈ insert a s → ∀ (j : ι), j ∈ insert a s → i ≠ j → f i ≠ f j
ih : (Finset.inf s fun i => f i ^ e i) = ∏ i in s, f i ^ e i
⊢ f a ^ e a ⊓ ∏ i in s, f i ^ e i = f a ^ e a * ∏ x in s, f x ^ e x
case refine_2
R : Type u_2
A : Type ?u.1194471
K : Type ?u.1194474
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
ι : Type u_1
s✝ : Finset ι
f : ι → Ideal R
e : ι → ℕ
this : DecidableEq ι := Classical.decEq ι
a : ι
s : Finset ι
ha : ¬a ∈ s
prime : ∀ (i : ι), i ∈ insert a s → Prime (f i)
coprime : ∀ (i : ι), i ∈ insert a s → ∀ (j : ι), j ∈ insert a s → i ≠ j → f i ≠ f j
ih : (Finset.inf s fun i => f i ^ e i) = ∏ i in s, f i ^ e i
⊢ (Finset.inf (insert a s) fun i => f i ^ e i) = ∏ i in insert a s, f i ^ e i
rw [Finset.inf_insert, Finset.prod_insert ha, ih]
case refine_2
R : Type u_2
A : Type ?u.1194471
K : Type ?u.1194474
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
ι : Type u_1
s✝ : Finset ι
f : ι → Ideal R
e : ι → ℕ
this : DecidableEq ι := Classical.decEq ι
a : ι
s : Finset ι
ha : ¬a ∈ s
prime : ∀ (i : ι), i ∈ insert a s → Prime (f i)
coprime : ∀ (i : ι), i ∈ insert a s → ∀ (j : ι), j ∈ insert a s → i ≠ j → f i ≠ f j
ih : (Finset.inf s fun i => f i ^ e i) = ∏ i in s, f i ^ e i
⊢ ∀ (P : Ideal R), f a ^ e a ≤ P → ∏ x in s, f x ^ e x ≤ P → ¬IsPrime P
case refine_2
R : Type u_2
A : Type ?u.1194471
K : Type ?u.1194474
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
ι : Type u_1
s✝ : Finset ι
f : ι → Ideal R
e : ι → ℕ
this : DecidableEq ι := Classical.decEq ι
a : ι
s : Finset ι
ha : ¬a ∈ s
prime : ∀ (i : ι), i ∈ insert a s → Prime (f i)
coprime : ∀ (i : ι), i ∈ insert a s → ∀ (j : ι), j ∈ insert a s → i ≠ j → f i ≠ f j
ih : (Finset.inf s fun i => f i ^ e i) = ∏ i in s, f i ^ e i
⊢ f a ^ e a ⊓ ∏ i in s, f i ^ e i = f a ^ e a * ∏ x in s, f x ^ e x
refine' le_antisymm (Ideal.le_mul_of_no_prime_factors _ inf_le_left inf_le_right) Ideal.mul_le_inf
case refine_2
R : Type u_2
A : Type ?u.1194471
K : Type ?u.1194474
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
ι : Type u_1
s✝ : Finset ι
f : ι → Ideal R
e : ι → ℕ
this : DecidableEq ι := Classical.decEq ι
a : ι
s : Finset ι
ha : ¬a ∈ s
prime : ∀ (i : ι), i ∈ insert a s → Prime (f i)
coprime : ∀ (i : ι), i ∈ insert a s → ∀ (j : ι), j ∈ insert a s → i ≠ j → f i ≠ f j
ih : (Finset.inf s fun i => f i ^ e i) = ∏ i in s, f i ^ e i
P : Ideal R
hPa : f a ^ e a ≤ P
hPs : ∏ x in s, f x ^ e x ≤ P
hPp : IsPrime P
⊢ False
case refine_2
R : Type u_2
A : Type ?u.1194471
K : Type ?u.1194474
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
ι : Type u_1
s✝ : Finset ι
f : ι → Ideal R
e : ι → ℕ
this : DecidableEq ι := Classical.decEq ι
a : ι
s : Finset ι
ha : ¬a ∈ s
prime : ∀ (i : ι), i ∈ insert a s → Prime (f i)
coprime : ∀ (i : ι), i ∈ insert a s → ∀ (j : ι), j ∈ insert a s → i ≠ j → f i ≠ f j
ih : (Finset.inf s fun i => f i ^ e i) = ∏ i in s, f i ^ e i
⊢ ∀ (P : Ideal R), f a ^ e a ≤ P → ∏ x in s, f x ^ e x ≤ P → ¬IsPrime P
intro P hPa hPs hPp
case refine_2
R : Type u_2
A : Type ?u.1194471
K : Type ?u.1194474
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
ι : Type u_1
s✝ : Finset ι
f : ι → Ideal R
e : ι → ℕ
this✝ : DecidableEq ι := Classical.decEq ι
a : ι
s : Finset ι
ha : ¬a ∈ s
prime : ∀ (i : ι), i ∈ insert a s → Prime (f i)
coprime : ∀ (i : ι), i ∈ insert a s → ∀ (j : ι), j ∈ insert a s → i ≠ j → f i ≠ f j
ih : (Finset.inf s fun i => f i ^ e i) = ∏ i in s, f i ^ e i
P : Ideal R
hPa : f a ^ e a ≤ P
hPs : ∏ x in s, f x ^ e x ≤ P
hPp this : IsPrime P
⊢ False
case refine_2
R : Type u_2
A : Type ?u.1194471
K : Type ?u.1194474
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
ι : Type u_1
s✝ : Finset ι
f : ι → Ideal R
e : ι → ℕ
this : DecidableEq ι := Classical.decEq ι
a : ι
s : Finset ι
ha : ¬a ∈ s
prime : ∀ (i : ι), i ∈ insert a s → Prime (f i)
coprime : ∀ (i : ι), i ∈ insert a s → ∀ (j : ι), j ∈ insert a s → i ≠ j → f i ≠ f j
ih : (Finset.inf s fun i => f i ^ e i) = ∏ i in s, f i ^ e i
P : Ideal R
hPa : f a ^ e a ≤ P
hPs : ∏ x in s, f x ^ e x ≤ P
hPp : IsPrime P
⊢ False
haveI := hPp
case refine_2.intro.intro
R : Type u_2
A : Type ?u.1194471
K : Type ?u.1194474
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
ι : Type u_1
s✝ : Finset ι
f : ι → Ideal R
e : ι → ℕ
this✝ : DecidableEq ι := Classical.decEq ι
a : ι
s : Finset ι
ha : ¬a ∈ s
prime : ∀ (i : ι), i ∈ insert a s → Prime (f i)
coprime : ∀ (i : ι), i ∈ insert a s → ∀ (j : ι), j ∈ insert a s → i ≠ j → f i ≠ f j
ih : (Finset.inf s fun i => f i ^ e i) = ∏ i in s, f i ^ e i
P : Ideal R
hPa : f a ^ e a ≤ P
hPs : ∏ x in s, f x ^ e x ≤ P
hPp this : IsPrime P
b : ι
hb : b ∈ s
hPb : f b ^ e b ≤ P
⊢ False
case refine_2
R : Type u_2
A : Type ?u.1194471
K : Type ?u.1194474
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
ι : Type u_1
s✝ : Finset ι
f : ι → Ideal R
e : ι → ℕ
this✝ : DecidableEq ι := Classical.decEq ι
a : ι
s : Finset ι
ha : ¬a ∈ s
prime : ∀ (i : ι), i ∈ insert a s → Prime (f i)
coprime : ∀ (i : ι), i ∈ insert a s → ∀ (j : ι), j ∈ insert a s → i ≠ j → f i ≠ f j
ih : (Finset.inf s fun i => f i ^ e i) = ∏ i in s, f i ^ e i
P : Ideal R
hPa : f a ^ e a ≤ P
hPs : ∏ x in s, f x ^ e x ≤ P
hPp this : IsPrime P
⊢ False
obtain ⟨b, hb, hPb⟩ := Ideal.prod_le_prime.mp hPs
case refine_2.intro.intro
R : Type u_2
A : Type ?u.1194471
K : Type ?u.1194474
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
ι : Type u_1
s✝ : Finset ι
f : ι → Ideal R
e : ι → ℕ
this✝¹ : DecidableEq ι := Classical.decEq ι
a : ι
s : Finset ι
ha : ¬a ∈ s
prime : ∀ (i : ι), i ∈ insert a s → Prime (f i)
coprime : ∀ (i : ι), i ∈ insert a s → ∀ (j : ι), j ∈ insert a s → i ≠ j → f i ≠ f j
ih : (Finset.inf s fun i => f i ^ e i) = ∏ i in s, f i ^ e i
P : Ideal R
hPa : f a ^ e a ≤ P
hPs : ∏ x in s, f x ^ e x ≤ P
hPp this✝ : IsPrime P
b : ι
hb : b ∈ s
hPb : f b ^ e b ≤ P
this : IsPrime (f a)
⊢ False
case refine_2.intro.intro
R : Type u_2
A : Type ?u.1194471
K : Type ?u.1194474
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
ι : Type u_1
s✝ : Finset ι
f : ι → Ideal R
e : ι → ℕ
this✝ : DecidableEq ι := Classical.decEq ι
a : ι
s : Finset ι
ha : ¬a ∈ s
prime : ∀ (i : ι), i ∈ insert a s → Prime (f i)
coprime : ∀ (i : ι), i ∈ insert a s → ∀ (j : ι), j ∈ insert a s → i ≠ j → f i ≠ f j
ih : (Finset.inf s fun i => f i ^ e i) = ∏ i in s, f i ^ e i
P : Ideal R
hPa : f a ^ e a ≤ P
hPs : ∏ x in s, f x ^ e x ≤ P
hPp this : IsPrime P
b : ι
hb : b ∈ s
hPb : f b ^ e b ≤ P
⊢ False
haveI := Ideal.isPrime_of_prime (prime a (Finset.mem_insert_self a s))
case refine_2.intro.intro
R : Type u_2
A : Type ?u.1194471
K : Type ?u.1194474
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
ι : Type u_1
s✝ : Finset ι
f : ι → Ideal R
e : ι → ℕ
this✝² : DecidableEq ι := Classical.decEq ι
a : ι
s : Finset ι
ha : ¬a ∈ s
prime : ∀ (i : ι), i ∈ insert a s → Prime (f i)
coprime : ∀ (i : ι), i ∈ insert a s → ∀ (j : ι), j ∈ insert a s → i ≠ j → f i ≠ f j
ih : (Finset.inf s fun i => f i ^ e i) = ∏ i in s, f i ^ e i
P : Ideal R
hPa : f a ^ e a ≤ P
hPs : ∏ x in s, f x ^ e x ≤ P
hPp this✝¹ : IsPrime P
b : ι
hb : b ∈ s
hPb : f b ^ e b ≤ P
this✝ : IsPrime (f a)
this : IsPrime (f b)
⊢ False
case refine_2.intro.intro
R : Type u_2
A : Type ?u.1194471
K : Type ?u.1194474
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
ι : Type u_1
s✝ : Finset ι
f : ι → Ideal R
e : ι → ℕ
this✝¹ : DecidableEq ι := Classical.decEq ι
a : ι
s : Finset ι
ha : ¬a ∈ s
prime : ∀ (i : ι), i ∈ insert a s → Prime (f i)
coprime : ∀ (i : ι), i ∈ insert a s → ∀ (j : ι), j ∈ insert a s → i ≠ j → f i ≠ f j
ih : (Finset.inf s fun i => f i ^ e i) = ∏ i in s, f i ^ e i
P : Ideal R
hPa : f a ^ e a ≤ P
hPs : ∏ x in s, f x ^ e x ≤ P
hPp this✝ : IsPrime P
b : ι
hb : b ∈ s
hPb : f b ^ e b ≤ P
this : IsPrime (f a)
⊢ False
haveI := Ideal.isPrime_of_prime (prime b (Finset.mem_insert_of_mem hb))
case refine_2.intro.intro.refine_1
R : Type u_2
A : Type ?u.1194471
K : Type ?u.1194474
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
ι : Type u_1
s✝ : Finset ι
f : ι → Ideal R
e : ι → ℕ
this✝² : DecidableEq ι := Classical.decEq ι
a : ι
s : Finset ι
ha : ¬a ∈ s
prime : ∀ (i : ι), i ∈ insert a s → Prime (f i)
coprime : ∀ (i : ι), i ∈ insert a s → ∀ (j : ι), j ∈ insert a s → i ≠ j → f i ≠ f j
ih : (Finset.inf s fun i => f i ^ e i) = ∏ i in s, f i ^ e i
P : Ideal R
hPa : f a ^ e a ≤ P
hPs : ∏ x in s, f x ^ e x ≤ P
hPp this✝¹ : IsPrime P
b : ι
hb : b ∈ s
hPb : f b ^ e b ≤ P
this✝ : IsPrime (f a)
this : IsPrime (f b)
⊢ a ≠ b

case refine_2.intro.intro.refine_2
R : Type u_2
A : Type ?u.1194471
K : Type ?u.1194474
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
ι : Type u_1
s✝ : Finset ι
f : ι → Ideal R
e : ι → ℕ
this✝² : DecidableEq ι := Classical.decEq ι
a : ι
s : Finset ι
ha : ¬a ∈ s
prime : ∀ (i : ι), i ∈ insert a s → Prime (f i)
coprime : ∀ (i : ι), i ∈ insert a s → ∀ (j : ι), j ∈ insert a s → i ≠ j → f i ≠ f j
ih : (Finset.inf s fun i => f i ^ e i) = ∏ i in s, f i ^ e i
P : Ideal R
hPa : f a ^ e a ≤ P
hPs : ∏ x in s, f x ^ e x ≤ P
hPp this✝¹ : IsPrime P
b : ι
hb : b ∈ s
hPb : f b ^ e b ≤ P
this✝ : IsPrime (f a)
this : IsPrime (f b)
⊢ f a = f b
case refine_2.intro.intro
R : Type u_2
A : Type ?u.1194471
K : Type ?u.1194474
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
ι : Type u_1
s✝ : Finset ι
f : ι → Ideal R
e : ι → ℕ
this✝² : DecidableEq ι := Classical.decEq ι
a : ι
s : Finset ι
ha : ¬a ∈ s
prime : ∀ (i : ι), i ∈ insert a s → Prime (f i)
coprime : ∀ (i : ι), i ∈ insert a s → ∀ (j : ι), j ∈ insert a s → i ≠ j → f i ≠ f j
ih : (Finset.inf s fun i => f i ^ e i) = ∏ i in s, f i ^ e i
P : Ideal R
hPa : f a ^ e a ≤ P
hPs : ∏ x in s, f x ^ e x ≤ P
hPp this✝¹ : IsPrime P
b : ι
hb : b ∈ s
hPb : f b ^ e b ≤ P
this✝ : IsPrime (f a)
this : IsPrime (f b)
⊢ False
refine coprime a (Finset.mem_insert_self a s) b (Finset.mem_insert_of_mem hb) ?_ ?_
no goals
case refine_1
R : Type u_2
A : Type ?u.1194471
K : Type ?u.1194474
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
ι : Type u_1
s : Finset ι
f : ι → Ideal R
e : ι → ℕ
this : DecidableEq ι := Classical.decEq ι
⊢ (∀ (i : ι), i ∈ ∅ → Prime (f i)) →
    (∀ (i : ι), i ∈ ∅ → ∀ (j : ι), j ∈ ∅ → i ≠ j → f i ≠ f j) → (Finset.inf ∅ fun i => f i ^ e i) = ∏ i in ∅, f i ^ e i
simp
case refine_2.intro.intro.refine_1
R : Type u_2
A : Type ?u.1194471
K : Type ?u.1194474
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
ι : Type u_1
s✝ : Finset ι
f : ι → Ideal R
e : ι → ℕ
this✝² : DecidableEq ι := Classical.decEq ι
a : ι
s : Finset ι
ha : ¬a ∈ s
prime : ∀ (i : ι), i ∈ insert a s → Prime (f i)
coprime : ∀ (i : ι), i ∈ insert a s → ∀ (j : ι), j ∈ insert a s → i ≠ j → f i ≠ f j
ih : (Finset.inf s fun i => f i ^ e i) = ∏ i in s, f i ^ e i
P : Ideal R
hPa : f a ^ e a ≤ P
hPs : ∏ x in s, f x ^ e x ≤ P
hPp this✝¹ : IsPrime P
this✝ : IsPrime (f a)
hb : a ∈ s
hPb : f a ^ e a ≤ P
this : IsPrime (f a)
⊢ False
case refine_2.intro.intro.refine_1
R : Type u_2
A : Type ?u.1194471
K : Type ?u.1194474
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
ι : Type u_1
s✝ : Finset ι
f : ι → Ideal R
e : ι → ℕ
this✝² : DecidableEq ι := Classical.decEq ι
a : ι
s : Finset ι
ha : ¬a ∈ s
prime : ∀ (i : ι), i ∈ insert a s → Prime (f i)
coprime : ∀ (i : ι), i ∈ insert a s → ∀ (j : ι), j ∈ insert a s → i ≠ j → f i ≠ f j
ih : (Finset.inf s fun i => f i ^ e i) = ∏ i in s, f i ^ e i
P : Ideal R
hPa : f a ^ e a ≤ P
hPs : ∏ x in s, f x ^ e x ≤ P
hPp this✝¹ : IsPrime P
b : ι
hb : b ∈ s
hPb : f b ^ e b ≤ P
this✝ : IsPrime (f a)
this : IsPrime (f b)
⊢ a ≠ b
rintro rfl
no goals
case refine_2.intro.intro.refine_1
R : Type u_2
A : Type ?u.1194471
K : Type ?u.1194474
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
ι : Type u_1
s✝ : Finset ι
f : ι → Ideal R
e : ι → ℕ
this✝² : DecidableEq ι := Classical.decEq ι
a : ι
s : Finset ι
ha : ¬a ∈ s
prime : ∀ (i : ι), i ∈ insert a s → Prime (f i)
coprime : ∀ (i : ι), i ∈ insert a s → ∀ (j : ι), j ∈ insert a s → i ≠ j → f i ≠ f j
ih : (Finset.inf s fun i => f i ^ e i) = ∏ i in s, f i ^ e i
P : Ideal R
hPa : f a ^ e a ≤ P
hPs : ∏ x in s, f x ^ e x ≤ P
hPp this✝¹ : IsPrime P
this✝ : IsPrime (f a)
hb : a ∈ s
hPb : f a ^ e a ≤ P
this : IsPrime (f a)
⊢ False
contradiction
case refine_2.intro.intro.refine_2.refine_1
R : Type u_2
A : Type ?u.1194471
K : Type ?u.1194474
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
ι : Type u_1
s✝ : Finset ι
f : ι → Ideal R
e : ι → ℕ
this✝² : DecidableEq ι := Classical.decEq ι
a : ι
s : Finset ι
ha : ¬a ∈ s
prime : ∀ (i : ι), i ∈ insert a s → Prime (f i)
coprime : ∀ (i : ι), i ∈ insert a s → ∀ (j : ι), j ∈ insert a s → i ≠ j → f i ≠ f j
ih : (Finset.inf s fun i => f i ^ e i) = ∏ i in s, f i ^ e i
P : Ideal R
hPa : f a ^ e a ≤ P
hPs : ∏ x in s, f x ^ e x ≤ P
hPp this✝¹ : IsPrime P
b : ι
hb : b ∈ s
hPb : f b ^ e b ≤ P
this✝ : IsPrime (f a)
this : IsPrime (f b)
⊢ f a ≠ ⊥

case refine_2.intro.intro.refine_2.refine_2
R : Type u_2
A : Type ?u.1194471
K : Type ?u.1194474
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
ι : Type u_1
s✝ : Finset ι
f : ι → Ideal R
e : ι → ℕ
this✝² : DecidableEq ι := Classical.decEq ι
a : ι
s : Finset ι
ha : ¬a ∈ s
prime : ∀ (i : ι), i ∈ insert a s → Prime (f i)
coprime : ∀ (i : ι), i ∈ insert a s → ∀ (j : ι), j ∈ insert a s → i ≠ j → f i ≠ f j
ih : (Finset.inf s fun i => f i ^ e i) = ∏ i in s, f i ^ e i
P : Ideal R
hPa : f a ^ e a ≤ P
hPs : ∏ x in s, f x ^ e x ≤ P
hPp this✝¹ : IsPrime P
b : ι
hb : b ∈ s
hPb : f b ^ e b ≤ P
this✝ : IsPrime (f a)
this : IsPrime (f b)
⊢ f b ≠ ⊥
case refine_2.intro.intro.refine_2
R : Type u_2
A : Type ?u.1194471
K : Type ?u.1194474
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
ι : Type u_1
s✝ : Finset ι
f : ι → Ideal R
e : ι → ℕ
this✝² : DecidableEq ι := Classical.decEq ι
a : ι
s : Finset ι
ha : ¬a ∈ s
prime : ∀ (i : ι), i ∈ insert a s → Prime (f i)
coprime : ∀ (i : ι), i ∈ insert a s → ∀ (j : ι), j ∈ insert a s → i ≠ j → f i ≠ f j
ih : (Finset.inf s fun i => f i ^ e i) = ∏ i in s, f i ^ e i
P : Ideal R
hPa : f a ^ e a ≤ P
hPs : ∏ x in s, f x ^ e x ≤ P
hPp this✝¹ : IsPrime P
b : ι
hb : b ∈ s
hPb : f b ^ e b ≤ P
this✝ : IsPrime (f a)
this : IsPrime (f b)
⊢ f a = f b
refine ((Ring.DimensionLeOne.prime_le_prime_iff_eq IsDedekindDomain.dimensionLEOne ?_).mp
  (Ideal.le_of_pow_le_prime hPa)).trans
  ((Ring.DimensionLeOne.prime_le_prime_iff_eq IsDedekindDomain.dimensionLEOne ?_).mp
  (Ideal.le_of_pow_le_prime hPb)).symm
case refine_2.intro.intro.refine_2.refine_2
R : Type u_2
A : Type ?u.1194471
K : Type ?u.1194474
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
ι : Type u_1
s✝ : Finset ι
f : ι → Ideal R
e : ι → ℕ
this✝² : DecidableEq ι := Classical.decEq ι
a : ι
s : Finset ι
ha : ¬a ∈ s
prime : ∀ (i : ι), i ∈ insert a s → Prime (f i)
coprime : ∀ (i : ι), i ∈ insert a s → ∀ (j : ι), j ∈ insert a s → i ≠ j → f i ≠ f j
ih : (Finset.inf s fun i => f i ^ e i) = ∏ i in s, f i ^ e i
P : Ideal R
hPa : f a ^ e a ≤ P
hPs : ∏ x in s, f x ^ e x ≤ P
hPp this✝¹ : IsPrime P
b : ι
hb : b ∈ s
hPb : f b ^ e b ≤ P
this✝ : IsPrime (f a)
this : IsPrime (f b)
⊢ f b ≠ ⊥
case refine_2.intro.intro.refine_2.refine_1
R : Type u_2
A : Type ?u.1194471
K : Type ?u.1194474
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
ι : Type u_1
s✝ : Finset ι
f : ι → Ideal R
e : ι → ℕ
this✝² : DecidableEq ι := Classical.decEq ι
a : ι
s : Finset ι
ha : ¬a ∈ s
prime : ∀ (i : ι), i ∈ insert a s → Prime (f i)
coprime : ∀ (i : ι), i ∈ insert a s → ∀ (j : ι), j ∈ insert a s → i ≠ j → f i ≠ f j
ih : (Finset.inf s fun i => f i ^ e i) = ∏ i in s, f i ^ e i
P : Ideal R
hPa : f a ^ e a ≤ P
hPs : ∏ x in s, f x ^ e x ≤ P
hPp this✝¹ : IsPrime P
b : ι
hb : b ∈ s
hPb : f b ^ e b ≤ P
this✝ : IsPrime (f a)
this : IsPrime (f b)
⊢ f a ≠ ⊥

case refine_2.intro.intro.refine_2.refine_2
R : Type u_2
A : Type ?u.1194471
K : Type ?u.1194474
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
ι : Type u_1
s✝ : Finset ι
f : ι → Ideal R
e : ι → ℕ
this✝² : DecidableEq ι := Classical.decEq ι
a : ι
s : Finset ι
ha : ¬a ∈ s
prime : ∀ (i : ι), i ∈ insert a s → Prime (f i)
coprime : ∀ (i : ι), i ∈ insert a s → ∀ (j : ι), j ∈ insert a s → i ≠ j → f i ≠ f j
ih : (Finset.inf s fun i => f i ^ e i) = ∏ i in s, f i ^ e i
P : Ideal R
hPa : f a ^ e a ≤ P
hPs : ∏ x in s, f x ^ e x ≤ P
hPp this✝¹ : IsPrime P
b : ι
hb : b ∈ s
hPb : f b ^ e b ≤ P
this✝ : IsPrime (f a)
this : IsPrime (f b)
⊢ f b ≠ ⊥
exact (prime a (Finset.mem_insert_self a s)).ne_zero
no goals
case refine_2.intro.intro.refine_2.refine_2
R : Type u_2
A : Type ?u.1194471
K : Type ?u.1194474
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
ι : Type u_1
s✝ : Finset ι
f : ι → Ideal R
e : ι → ℕ
this✝² : DecidableEq ι := Classical.decEq ι
a : ι
s : Finset ι
ha : ¬a ∈ s
prime : ∀ (i : ι), i ∈ insert a s → Prime (f i)
coprime : ∀ (i : ι), i ∈ insert a s → ∀ (j : ι), j ∈ insert a s → i ≠ j → f i ≠ f j
ih : (Finset.inf s fun i => f i ^ e i) = ∏ i in s, f i ^ e i
P : Ideal R
hPa : f a ^ e a ≤ P
hPs : ∏ x in s, f x ^ e x ≤ P
hPp this✝¹ : IsPrime P
b : ι
hb : b ∈ s
hPb : f b ^ e b ≤ P
this✝ : IsPrime (f a)
this : IsPrime (f b)
⊢ f b ≠ ⊥
exact (prime b (Finset.mem_insert_of_mem hb)).ne_zero