-- Mathlib/RingTheory/UniqueFactorizationDomain/Ideal.lean
theorem Ideal.IsPrime.exists_mem_prime_of_ne_bot {R : Type*} [CommSemiring R] [IsDomain R]
    [UniqueFactorizationMonoid R] {I : Ideal R} (hI₂ : I.IsPrime) (hI : I ≠ ⊥) :
    ∃ x ∈ I, Prime x

Proof state:
R : Type u_2
inst✝² : CommSemiring R
inst✝¹ : IsDomain R
inst✝ : UniqueFactorizationMonoid R
I : Ideal R
hI₂ : I.IsPrime
hI : I ≠ ⊥
⊢ ∃ x ∈ I, Prime x

Tactic:
classical
obtain ⟨a : R, ha₁ : a ∈ I, ha₂ : a ≠ 0⟩ := Submodule.exists_mem_ne_zero_of_ne_bot hI
replace ha₁ : (factors a).prod ∈ I := by
  obtain ⟨u : Rˣ, hu : (factors a).prod * u = a⟩ := factors_prod ha₂
  rwa [← hu, mul_unit_mem_iff_mem _ u.isUnit] at ha₁
obtain ⟨p : R, hp₁ : p ∈ factors a, hp₂ : p ∈ I⟩ :=
  (hI₂.multiset_prod_mem_iff_exists_mem <| factors a).1 ha₁
exact ⟨p, hp₂, prime_of_factor p hp₁⟩

Result:
no goals

Proof state:
case intro
R : Type u_2
inst✝² : CommSemiring R
inst✝¹ : IsDomain R
inst✝ : UniqueFactorizationMonoid R
I : Ideal R
hI₂ : I.IsPrime
hI : I ≠ ⊥
a : R
ha₁ : a ∈ I
ha₂ : a ≠ 0
u : Rˣ
hu : (factors a).prod * ↑u = a
⊢ (factors a).prod ∈ I

Tactic:
rwa [← hu, mul_unit_mem_iff_mem _ u.isUnit] at ha₁

Result:
no goals

Proof state:
R : Type u_2
inst✝² : CommSemiring R
inst✝¹ : IsDomain R
inst✝ : UniqueFactorizationMonoid R
I : Ideal R
hI₂ : I.IsPrime
hI : I ≠ ⊥
⊢ ∃ x ∈ I, Prime x

Tactic:
obtain ⟨a : R, ha₁ : a ∈ I, ha₂ : a ≠ 0⟩ := Submodule.exists_mem_ne_zero_of_ne_bot hI

Result:
case intro.intro
R : Type u_2
inst✝² : CommSemiring R
inst✝¹ : IsDomain R
inst✝ : UniqueFactorizationMonoid R
I : Ideal R
hI₂ : I.IsPrime
hI : I ≠ ⊥
a : R
ha₁ : a ∈ I
ha₂ : a ≠ 0
⊢ ∃ x ∈ I, Prime x

Proof state:
R : Type u_2
inst✝² : CommSemiring R
inst✝¹ : IsDomain R
inst✝ : UniqueFactorizationMonoid R
I : Ideal R
hI₂ : I.IsPrime
hI : I ≠ ⊥
a : R
ha₁ : a ∈ I
ha₂ : a ≠ 0
⊢ (factors a).prod ∈ I

Tactic:
obtain ⟨u : Rˣ, hu : (factors a).prod * u = a⟩ := factors_prod ha₂

Result:
case intro
R : Type u_2
inst✝² : CommSemiring R
inst✝¹ : IsDomain R
inst✝ : UniqueFactorizationMonoid R
I : Ideal R
hI₂ : I.IsPrime
hI : I ≠ ⊥
a : R
ha₁ : a ∈ I
ha₂ : a ≠ 0
u : Rˣ
hu : (factors a).prod * ↑u = a
⊢ (factors a).prod ∈ I

Proof state:
case intro.intro
R : Type u_2
inst✝² : CommSemiring R
inst✝¹ : IsDomain R
inst✝ : UniqueFactorizationMonoid R
I : Ideal R
hI₂ : I.IsPrime
hI : I ≠ ⊥
a : R
ha₂ : a ≠ 0
ha₁ : (factors a).prod ∈ I
⊢ ∃ x ∈ I, Prime x

Tactic:
obtain ⟨p : R, hp₁ : p ∈ factors a, hp₂ : p ∈ I⟩ :=
  (hI₂.multiset_prod_mem_iff_exists_mem <| factors a).1 ha₁

Result:
case intro.intro.intro.intro
R : Type u_2
inst✝² : CommSemiring R
inst✝¹ : IsDomain R
inst✝ : UniqueFactorizationMonoid R
I : Ideal R
hI₂ : I.IsPrime
hI : I ≠ ⊥
a : R
ha₂ : a ≠ 0
ha₁ : (factors a).prod ∈ I
p : R
hp₁ : p ∈ factors a
hp₂ : p ∈ I
⊢ ∃ x ∈ I, Prime x

Proof state:
case intro.intro
R : Type u_2
inst✝² : CommSemiring R
inst✝¹ : IsDomain R
inst✝ : UniqueFactorizationMonoid R
I : Ideal R
hI₂ : I.IsPrime
hI : I ≠ ⊥
a : R
ha₁ : a ∈ I
ha₂ : a ≠ 0
⊢ ∃ x ∈ I, Prime x

Tactic:
replace ha₁ : (factors a).prod ∈ I := by
  obtain ⟨u : Rˣ, hu : (factors a).prod * u = a⟩ := factors_prod ha₂
  rwa [← hu, mul_unit_mem_iff_mem _ u.isUnit] at ha₁

Result:
case intro.intro
R : Type u_2
inst✝² : CommSemiring R
inst✝¹ : IsDomain R
inst✝ : UniqueFactorizationMonoid R
I : Ideal R
hI₂ : I.IsPrime
hI : I ≠ ⊥
a : R
ha₂ : a ≠ 0
ha₁ : (factors a).prod ∈ I
⊢ ∃ x ∈ I, Prime x

Proof state:
case intro.intro.intro.intro
R : Type u_2
inst✝² : CommSemiring R
inst✝¹ : IsDomain R
inst✝ : UniqueFactorizationMonoid R
I : Ideal R
hI₂ : I.IsPrime
hI : I ≠ ⊥
a : R
ha₂ : a ≠ 0
ha₁ : (factors a).prod ∈ I
p : R
hp₁ : p ∈ factors a
hp₂ : p ∈ I
⊢ ∃ x ∈ I, Prime x

Tactic:
exact ⟨p, hp₂, prime_of_factor p hp₁⟩

Result:
no goals