-- 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.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

Tactic:
refine ((Ring.DimensionLeOne.prime_le_prime_iff_eq ?_).mp (hPp.le_of_pow_le hPa)).trans
  ((Ring.DimensionLeOne.prime_le_prime_iff_eq ?_).mp (hPp.le_of_pow_le hPb)).symm

Result:
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 ≠ ⊥

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 ≠ ⊥

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
⊢ (s.inf fun i => f i ^ e i) = ∏ i ∈ s, f i ^ e i

Tactic:
letI := Classical.decEq ι

Result:
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

Proof state:
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

Tactic:
exact (ne_of_mem_of_not_mem hb ha).symm

Result:
no goals