-- Mathlib/RingTheory/DedekindDomain/Ideal.lean
theorem IsDedekindDomain.inf_prime_pow_eq_prod {ι : Type*} (s : Finset ι) (f : ι → Ideal R)
    (e : ι → ℕ) (prime : ∀ i ∈ s, Prime (f i))
    (coprime : ∀ᵉ (i ∈ s) (j ∈ s), i ≠ j → f i ≠ f j) :
    (s.inf fun i => f i ^ e i) = ∏ i ∈ s, f i ^ e i

Proof state:
case refine_2.intro.intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
ι : Type u_4
s✝ : Finset ι
f : ι → Ideal R
e : ι → ℕ
this✝¹ : DecidableEq ι := Classical.decEq ι
a : ι
s : Finset ι
ha : a ∉ s
prime : ∀ i ∈ insert a s, Prime (f i)
coprime : ∀ i ∈ insert a s, ∀ j ∈ insert a s, i ≠ j → f i ≠ f j
ih : (s.inf fun i => f i ^ e i) = ∏ i ∈ s, f i ^ e i
P : Ideal R
hPa : f a ^ e a ≤ P
hPs : ∏ x ∈ s, f x ^ e x ≤ P
hPp : P.IsPrime
b : ι
hb : b ∈ s
hPb : f b ^ e b ≤ P
this✝ : (f a).IsPrime
this : (f b).IsPrime
⊢ False

Tactic:
refine coprime a (Finset.mem_insert_self a s) b (Finset.mem_insert_of_mem hb) ?_ ?_

Result:
case refine_2.intro.intro.refine_1
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
ι : Type u_4
s✝ : Finset ι
f : ι → Ideal R
e : ι → ℕ
this✝¹ : DecidableEq ι := Classical.decEq ι
a : ι
s : Finset ι
ha : a ∉ s
prime : ∀ i ∈ insert a s, Prime (f i)
coprime : ∀ i ∈ insert a s, ∀ j ∈ insert a s, i ≠ j → f i ≠ f j
ih : (s.inf fun i => f i ^ e i) = ∏ i ∈ s, f i ^ e i
P : Ideal R
hPa : f a ^ e a ≤ P
hPs : ∏ x ∈ s, f x ^ e x ≤ P
hPp : P.IsPrime
b : ι
hb : b ∈ s
hPb : f b ^ e b ≤ P
this✝ : (f a).IsPrime
this : (f b).IsPrime
⊢ a ≠ b

case refine_2.intro.intro.refine_2
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
ι : Type u_4
s✝ : Finset ι
f : ι → Ideal R
e : ι → ℕ
this✝¹ : DecidableEq ι := Classical.decEq ι
a : ι
s : Finset ι
ha : a ∉ s
prime : ∀ i ∈ insert a s, Prime (f i)
coprime : ∀ i ∈ insert a s, ∀ j ∈ insert a s, i ≠ j → f i ≠ f j
ih : (s.inf fun i => f i ^ e i) = ∏ i ∈ s, f i ^ e i
P : Ideal R
hPa : f a ^ e a ≤ P
hPs : ∏ x ∈ s, f x ^ e x ≤ P
hPp : P.IsPrime
b : ι
hb : b ∈ s
hPb : f b ^ e b ≤ P
this✝ : (f a).IsPrime
this : (f b).IsPrime
⊢ f a = f b

Proof state:
case refine_2.intro.intro.refine_2.refine_1
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
ι : Type u_4
s✝ : Finset ι
f : ι → Ideal R
e : ι → ℕ
this✝¹ : DecidableEq ι := Classical.decEq ι
a : ι
s : Finset ι
ha : a ∉ s
prime : ∀ i ∈ insert a s, Prime (f i)
coprime : ∀ i ∈ insert a s, ∀ j ∈ insert a s, i ≠ j → f i ≠ f j
ih : (s.inf fun i => f i ^ e i) = ∏ i ∈ s, f i ^ e i
P : Ideal R
hPa : f a ^ e a ≤ P
hPs : ∏ x ∈ s, f x ^ e x ≤ P
hPp : P.IsPrime
b : ι
hb : b ∈ s
hPb : f b ^ e b ≤ P
this✝ : (f a).IsPrime
this : (f b).IsPrime
⊢ f a ≠ ⊥

Tactic:
exact (prime a (Finset.mem_insert_self a s)).ne_zero

Result:
no goals

Proof state:
case refine_1
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
ι : Type u_4
s : Finset ι
f : ι → Ideal R
e : ι → ℕ
this : DecidableEq ι := Classical.decEq ι
⊢ (∀ i ∈ ∅, Prime (f i)) → (∀ i ∈ ∅, ∀ j ∈ ∅, i ≠ j → f i ≠ f j) → (∅.inf fun i => f i ^ e i) = ∏ i ∈ ∅, f i ^ e i

Tactic:
simp

Result:
no goals

Proof state:
case refine_2.intro.intro.refine_2.refine_2
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
ι : Type u_4
s✝ : Finset ι
f : ι → Ideal R
e : ι → ℕ
this✝¹ : DecidableEq ι := Classical.decEq ι
a : ι
s : Finset ι
ha : a ∉ s
prime : ∀ i ∈ insert a s, Prime (f i)
coprime : ∀ i ∈ insert a s, ∀ j ∈ insert a s, i ≠ j → f i ≠ f j
ih : (s.inf fun i => f i ^ e i) = ∏ i ∈ s, f i ^ e i
P : Ideal R
hPa : f a ^ e a ≤ P
hPs : ∏ x ∈ s, f x ^ e x ≤ P
hPp : P.IsPrime
b : ι
hb : b ∈ s
hPb : f b ^ e b ≤ P
this✝ : (f a).IsPrime
this : (f b).IsPrime
⊢ f b ≠ ⊥

Tactic:
exact (prime b (Finset.mem_insert_of_mem hb)).ne_zero

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
ι : Type u_4
s : Finset ι
f : ι → Ideal R
e : ι → ℕ
prime : ∀ i ∈ s, Prime (f i)
coprime : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → f i ≠ f j
this : DecidableEq ι := Classical.decEq ι
⊢ (s.inf fun i => f i ^ e i) = ∏ i ∈ s, f i ^ e i

Tactic:
revert prime coprime

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
ι : Type u_4
s : Finset ι
f : ι → Ideal R
e : ι → ℕ
this : DecidableEq ι := Classical.decEq ι
⊢ (∀ i ∈ s, Prime (f i)) → (∀ i ∈ s, ∀ j ∈ s, i ≠ j → f i ≠ f j) → (s.inf fun i => f i ^ e i) = ∏ i ∈ s, f i ^ e i

Proof state:
case refine_2
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
ι : Type u_4
s : Finset ι
f : ι → Ideal R
e : ι → ℕ
this : DecidableEq ι := Classical.decEq ι
⊢ ∀ ⦃a : ι⦄ {s : Finset ι},
    a ∉ s →
      ((∀ i ∈ s, Prime (f i)) →
          (∀ i ∈ s, ∀ j ∈ s, i ≠ j → f i ≠ f j) → (s.inf fun i => f i ^ e i) = ∏ i ∈ s, f i ^ e i) →
        (∀ i ∈ insert a s, Prime (f i)) →
          (∀ i ∈ insert a s, ∀ j ∈ insert a s, i ≠ j → f i ≠ f j) →
            ((insert a s).inf fun i => f i ^ e i) = ∏ i ∈ insert a s, f i ^ e i

Tactic:
intro a s ha ih prime coprime

Result:
case refine_2
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
ι : Type u_4
s✝ : Finset ι
f : ι → Ideal R
e : ι → ℕ
this : DecidableEq ι := Classical.decEq ι
a : ι
s : Finset ι
ha : a ∉ s
ih : (∀ i ∈ s, Prime (f i)) → (∀ i ∈ s, ∀ j ∈ s, i ≠ j → f i ≠ f j) → (s.inf fun i => f i ^ e i) = ∏ i ∈ s, f i ^ e i
prime : ∀ i ∈ insert a s, Prime (f i)
coprime : ∀ i ∈ insert a s, ∀ j ∈ insert a s, i ≠ j → f i ≠ f j
⊢ ((insert a s).inf fun i => f i ^ e i) = ∏ i ∈ insert a s, f i ^ e i

Proof state:
case refine_2
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
ι : Type u_4
s✝ : Finset ι
f : ι → Ideal R
e : ι → ℕ
this : DecidableEq ι := Classical.decEq ι
a : ι
s : Finset ι
ha : a ∉ s
prime : ∀ i ∈ insert a s, Prime (f i)
coprime : ∀ i ∈ insert a s, ∀ j ∈ insert a s, i ≠ j → f i ≠ f j
ih : (s.inf fun i => f i ^ e i) = ∏ i ∈ s, f i ^ e i
⊢ f a ^ e a ⊓ ∏ i ∈ s, f i ^ e i = f a ^ e a * ∏ x ∈ s, f x ^ e x

Tactic:
refine le_antisymm (Ideal.le_mul_of_no_prime_factors ?_ inf_le_left inf_le_right) Ideal.mul_le_inf

Result:
case refine_2
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
ι : Type u_4
s✝ : Finset ι
f : ι → Ideal R
e : ι → ℕ
this : DecidableEq ι := Classical.decEq ι
a : ι
s : Finset ι
ha : a ∉ s
prime : ∀ i ∈ insert a s, Prime (f i)
coprime : ∀ i ∈ insert a s, ∀ j ∈ insert a s, i ≠ j → f i ≠ f j
ih : (s.inf fun i => f i ^ e i) = ∏ i ∈ s, f i ^ e i
⊢ ∀ (P : Ideal R), f a ^ e a ≤ P → ∏ x ∈ s, f x ^ e x ≤ P → ¬P.IsPrime