Theorem: uniqueFactorizationMonoid_iff (Kaplanski4/Kaplanski.lean)

State before:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
hP : Set.Nonempty {r | Prime r}
⊢ UniqueFactorizationMonoid R ↔ ∀ (I : Ideal R), I ≠ ⊥ → Ideal.IsPrime I → ∃ x ∈ I, Prime x
Tactic:
classical
constructor
intro _ _ hI hI₂
exact Ideal.IsPrime.exists_mem_prime_of_ne_bot hI₂ hI
intro H
exact uniqueFactorizationMonoid_of_exists_prime H hP
State after:
no goals

State before:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
hP : Set.Nonempty {r | Prime r}
⊢ UniqueFactorizationMonoid R ↔ ∀ (I : Ideal R), I ≠ ⊥ → Ideal.IsPrime I → ∃ x ∈ I, Prime x
Tactic:
constructor
State after:
case mp
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
hP : Set.Nonempty {r | Prime r}
⊢ UniqueFactorizationMonoid R → ∀ (I : Ideal R), I ≠ ⊥ → Ideal.IsPrime I → ∃ x ∈ I, Prime x

case mpr
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
hP : Set.Nonempty {r | Prime r}
⊢ (∀ (I : Ideal R), I ≠ ⊥ → Ideal.IsPrime I → ∃ x ∈ I, Prime x) → UniqueFactorizationMonoid R

State before:
case mp
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
hP : Set.Nonempty {r | Prime r}
⊢ UniqueFactorizationMonoid R → ∀ (I : Ideal R), I ≠ ⊥ → Ideal.IsPrime I → ∃ x ∈ I, Prime x

case mpr
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
hP : Set.Nonempty {r | Prime r}
⊢ (∀ (I : Ideal R), I ≠ ⊥ → Ideal.IsPrime I → ∃ x ∈ I, Prime x) → UniqueFactorizationMonoid R
Tactic:
intro _ _ hI hI₂
State after:
case mp
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
hP : Set.Nonempty {r | Prime r}
a✝ : UniqueFactorizationMonoid R
I✝ : Ideal R
hI : I✝ ≠ ⊥
hI₂ : Ideal.IsPrime I✝
⊢ ∃ x ∈ I✝, Prime x

case mpr
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
hP : Set.Nonempty {r | Prime r}
⊢ (∀ (I : Ideal R), I ≠ ⊥ → Ideal.IsPrime I → ∃ x ∈ I, Prime x) → UniqueFactorizationMonoid R

State before:
case mp
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
hP : Set.Nonempty {r | Prime r}
a✝ : UniqueFactorizationMonoid R
I✝ : Ideal R
hI : I✝ ≠ ⊥
hI₂ : Ideal.IsPrime I✝
⊢ ∃ x ∈ I✝, Prime x

case mpr
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
hP : Set.Nonempty {r | Prime r}
⊢ (∀ (I : Ideal R), I ≠ ⊥ → Ideal.IsPrime I → ∃ x ∈ I, Prime x) → UniqueFactorizationMonoid R
Tactic:
exact Ideal.IsPrime.exists_mem_prime_of_ne_bot hI₂ hI
State after:
case mpr
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
hP : Set.Nonempty {r | Prime r}
⊢ (∀ (I : Ideal R), I ≠ ⊥ → Ideal.IsPrime I → ∃ x ∈ I, Prime x) → UniqueFactorizationMonoid R

State before:
case mpr
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
hP : Set.Nonempty {r | Prime r}
⊢ (∀ (I : Ideal R), I ≠ ⊥ → Ideal.IsPrime I → ∃ x ∈ I, Prime x) → UniqueFactorizationMonoid R
Tactic:
intro H
State after:
case mpr
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
hP : Set.Nonempty {r | Prime r}
H : ∀ (I : Ideal R), I ≠ ⊥ → Ideal.IsPrime I → ∃ x ∈ I, Prime x
⊢ UniqueFactorizationMonoid R

State before:
case mpr
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
hP : Set.Nonempty {r | Prime r}
H : ∀ (I : Ideal R), I ≠ ⊥ → Ideal.IsPrime I → ∃ x ∈ I, Prime x
⊢ UniqueFactorizationMonoid R
Tactic:
exact uniqueFactorizationMonoid_of_exists_prime H hP
State after:
no goals