Theorem: uniqueFactorizationMonoid_of_exists_prime (Kaplanski4/Kaplanski.lean)

State before:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
H : ∀ (I : Ideal R), I ≠ ⊥ → Ideal.IsPrime I → ∃ x ∈ I, Prime x
hP : Set.Nonempty {r | Prime r}
⊢ UniqueFactorizationMonoid R
Tactic:
refine' UniqueFactorizationMonoid.of_exists_prime_factors fun a ha => _
State after:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
H : ∀ (I : Ideal R), I ≠ ⊥ → Ideal.IsPrime I → ∃ x ∈ I, Prime x
hP : Set.Nonempty {r | Prime r}
a : R
ha : a ≠ 0
⊢ ∃ f, (∀ b ∈ f, Prime b) ∧ Associated (Multiset.prod f) a

State before:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
H : ∀ (I : Ideal R), I ≠ ⊥ → Ideal.IsPrime I → ∃ x ∈ I, Prime x
hP : Set.Nonempty {r | Prime r}
a : R
ha : a ≠ 0
⊢ ∃ f, (∀ b ∈ f, Prime b) ∧ Associated (Multiset.prod f) a
Tactic:
have ha₂ := ideal.span_ne_mem_kaplanski.set ha H
State after:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
H : ∀ (I : Ideal R), I ≠ ⊥ → Ideal.IsPrime I → ∃ x ∈ I, Prime x
hP : Set.Nonempty {r | Prime r}
a : R
ha : a ≠ 0
ha₂ : Set.Nonempty {r | Prime r} → Ideal.span {a} ∉ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup
⊢ ∃ f, (∀ b ∈ f, Prime b) ∧ Associated (Multiset.prod f) a

State before:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
H : ∀ (I : Ideal R), I ≠ ⊥ → Ideal.IsPrime I → ∃ x ∈ I, Prime x
hP : Set.Nonempty {r | Prime r}
a : R
ha : a ≠ 0
ha₂ : Set.Nonempty {r | Prime r} → Ideal.span {a} ∉ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup
⊢ ∃ f, (∀ b ∈ f, Prime b) ∧ Associated (Multiset.prod f) a
Tactic:
rw [Kaplansky.set_def, ← Ne.def] at ha₂
State after:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
H : ∀ (I : Ideal R), I ≠ ⊥ → Ideal.IsPrime I → ∃ x ∈ I, Prime x
hP : Set.Nonempty {r | Prime r}
a : R
ha : a ≠ 0
ha₂ : Set.Nonempty {r | Prime r} → ↑(Ideal.span {a}) ∩ ↑(Submonoid.closure {r | Prime r}).toSubsemigroup ≠ ∅
⊢ ∃ f, (∀ b ∈ f, Prime b) ∧ Associated (Multiset.prod f) a

State before:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
H : ∀ (I : Ideal R), I ≠ ⊥ → Ideal.IsPrime I → ∃ x ∈ I, Prime x
hP : Set.Nonempty {r | Prime r}
a : R
ha : a ≠ 0
ha₂ : Set.Nonempty {r | Prime r} → ↑(Ideal.span {a}) ∩ ↑(Submonoid.closure {r | Prime r}).toSubsemigroup ≠ ∅
⊢ ∃ f, (∀ b ∈ f, Prime b) ∧ Associated (Multiset.prod f) a
Tactic:
rcases Set.nonempty_iff_ne_empty.2 (ha₂ hP) with ⟨x, ⟨hx, hx₂⟩⟩
State after:
case intro.intro
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
H : ∀ (I : Ideal R), I ≠ ⊥ → Ideal.IsPrime I → ∃ x ∈ I, Prime x
hP : Set.Nonempty {r | Prime r}
a : R
ha : a ≠ 0
ha₂ : Set.Nonempty {r | Prime r} → ↑(Ideal.span {a}) ∩ ↑(Submonoid.closure {r | Prime r}).toSubsemigroup ≠ ∅
x : R
hx : x ∈ ↑(Ideal.span {a})
hx₂ : x ∈ ↑(Submonoid.closure {r | Prime r}).toSubsemigroup
⊢ ∃ f, (∀ b ∈ f, Prime b) ∧ Associated (Multiset.prod f) a

State before:
case intro.intro
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
H : ∀ (I : Ideal R), I ≠ ⊥ → Ideal.IsPrime I → ∃ x ∈ I, Prime x
hP : Set.Nonempty {r | Prime r}
a : R
ha : a ≠ 0
ha₂ : Set.Nonempty {r | Prime r} → ↑(Ideal.span {a}) ∩ ↑(Submonoid.closure {r | Prime r}).toSubsemigroup ≠ ∅
x : R
hx : x ∈ ↑(Ideal.span {a})
hx₂ : x ∈ ↑(Submonoid.closure {r | Prime r}).toSubsemigroup
⊢ ∃ f, (∀ b ∈ f, Prime b) ∧ Associated (Multiset.prod f) a
Tactic:
cases' Ideal.mem_span_singleton'.1 (SetLike.mem_coe.1 hx) with b hb
State after:
case intro.intro.intro
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
H : ∀ (I : Ideal R), I ≠ ⊥ → Ideal.IsPrime I → ∃ x ∈ I, Prime x
hP : Set.Nonempty {r | Prime r}
a : R
ha : a ≠ 0
ha₂ : Set.Nonempty {r | Prime r} → ↑(Ideal.span {a}) ∩ ↑(Submonoid.closure {r | Prime r}).toSubsemigroup ≠ ∅
x : R
hx : x ∈ ↑(Ideal.span {a})
hx₂ : x ∈ ↑(Submonoid.closure {r | Prime r}).toSubsemigroup
b : R
hb : b * a = x
⊢ ∃ f, (∀ b ∈ f, Prime b) ∧ Associated (Multiset.prod f) a

State before:
case intro.intro.intro
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
H : ∀ (I : Ideal R), I ≠ ⊥ → Ideal.IsPrime I → ∃ x ∈ I, Prime x
hP : Set.Nonempty {r | Prime r}
a : R
ha : a ≠ 0
ha₂ : Set.Nonempty {r | Prime r} → ↑(Ideal.span {a}) ∩ ↑(Submonoid.closure {r | Prime r}).toSubsemigroup ≠ ∅
x : R
hx : x ∈ ↑(Ideal.span {a})
hx₂ : x ∈ ↑(Submonoid.closure {r | Prime r}).toSubsemigroup
b : R
hb : b * a = x
⊢ ∃ f, (∀ b ∈ f, Prime b) ∧ Associated (Multiset.prod f) a
Tactic:
rw [← hb, mul_comm] at hx₂
State after:
case intro.intro.intro
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
H : ∀ (I : Ideal R), I ≠ ⊥ → Ideal.IsPrime I → ∃ x ∈ I, Prime x
hP : Set.Nonempty {r | Prime r}
a : R
ha : a ≠ 0
ha₂ : Set.Nonempty {r | Prime r} → ↑(Ideal.span {a}) ∩ ↑(Submonoid.closure {r | Prime r}).toSubsemigroup ≠ ∅
x : R
hx : x ∈ ↑(Ideal.span {a})
b : R
hx₂ : a * b ∈ ↑(Submonoid.closure {r | Prime r}).toSubsemigroup
hb : b * a = x
⊢ ∃ f, (∀ b ∈ f, Prime b) ∧ Associated (Multiset.prod f) a

State before:
case intro.intro.intro
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
H : ∀ (I : Ideal R), I ≠ ⊥ → Ideal.IsPrime I → ∃ x ∈ I, Prime x
hP : Set.Nonempty {r | Prime r}
a : R
ha : a ≠ 0
ha₂ : Set.Nonempty {r | Prime r} → ↑(Ideal.span {a}) ∩ ↑(Submonoid.closure {r | Prime r}).toSubsemigroup ≠ ∅
x : R
hx : x ∈ ↑(Ideal.span {a})
b : R
hx₂ : a * b ∈ ↑(Submonoid.closure {r | Prime r}).toSubsemigroup
hb : b * a = x
⊢ ∃ f, (∀ b ∈ f, Prime b) ∧ Associated (Multiset.prod f) a
Tactic:
have hsubset : Submonoid.closure {r : R | Prime r} ≤
    Submonoid.closure {r : R | IsUnit r ∨ Prime r} := by
  refine' Submonoid.closure_mono (Set.setOf_subset_setOf.2 (fun _ ha => _))
  right
  exact ha
State after:
case intro.intro.intro
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
H : ∀ (I : Ideal R), I ≠ ⊥ → Ideal.IsPrime I → ∃ x ∈ I, Prime x
hP : Set.Nonempty {r | Prime r}
a : R
ha : a ≠ 0
ha₂ : Set.Nonempty {r | Prime r} → ↑(Ideal.span {a}) ∩ ↑(Submonoid.closure {r | Prime r}).toSubsemigroup ≠ ∅
x : R
hx : x ∈ ↑(Ideal.span {a})
b : R
hx₂ : a * b ∈ ↑(Submonoid.closure {r | Prime r}).toSubsemigroup
hb : b * a = x
hsubset : Submonoid.closure {r | Prime r} ≤ Submonoid.closure {r | IsUnit r ∨ Prime r}
⊢ ∃ f, (∀ b ∈ f, Prime b) ∧ Associated (Multiset.prod f) a

State before:
case intro.intro.intro
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
H : ∀ (I : Ideal R), I ≠ ⊥ → Ideal.IsPrime I → ∃ x ∈ I, Prime x
hP : Set.Nonempty {r | Prime r}
a : R
ha : a ≠ 0
ha₂ : Set.Nonempty {r | Prime r} → ↑(Ideal.span {a}) ∩ ↑(Submonoid.closure {r | Prime r}).toSubsemigroup ≠ ∅
x : R
hx : x ∈ ↑(Ideal.span {a})
b : R
hx₂ : a * b ∈ ↑(Submonoid.closure {r | Prime r}).toSubsemigroup
hb : b * a = x
hsubset : Submonoid.closure {r | Prime r} ≤ Submonoid.closure {r | IsUnit r ∨ Prime r}
⊢ ∃ f, (∀ b ∈ f, Prime b) ∧ Associated (Multiset.prod f) a
Tactic:
exact exists_prime_factors_of_exists_multiset a (Submonoid.exists_multiset_of_mem_closure
  (Submonoid.closure_mem_of_prod_mem _ _ (hsubset hx₂)))
State after:
no goals

State before:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
H : ∀ (I : Ideal R), I ≠ ⊥ → Ideal.IsPrime I → ∃ x ∈ I, Prime x
hP : Set.Nonempty {r | Prime r}
a : R
ha : a ≠ 0
ha₂ : Set.Nonempty {r | Prime r} → ↑(Ideal.span {a}) ∩ ↑(Submonoid.closure {r | Prime r}).toSubsemigroup ≠ ∅
x : R
hx : x ∈ ↑(Ideal.span {a})
b : R
hx₂ : a * b ∈ ↑(Submonoid.closure {r | Prime r}).toSubsemigroup
hb : b * a = x
⊢ Submonoid.closure {r | Prime r} ≤ Submonoid.closure {r | IsUnit r ∨ Prime r}
Tactic:
refine' Submonoid.closure_mono (Set.setOf_subset_setOf.2 (fun _ ha => _))
State after:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
H : ∀ (I : Ideal R), I ≠ ⊥ → Ideal.IsPrime I → ∃ x ∈ I, Prime x
hP : Set.Nonempty {r | Prime r}
a : R
ha✝ : a ≠ 0
ha₂ : Set.Nonempty {r | Prime r} → ↑(Ideal.span {a}) ∩ ↑(Submonoid.closure {r | Prime r}).toSubsemigroup ≠ ∅
x : R
hx : x ∈ ↑(Ideal.span {a})
b : R
hx₂ : a * b ∈ ↑(Submonoid.closure {r | Prime r}).toSubsemigroup
hb : b * a = x
x✝ : R
ha : Prime x✝
⊢ IsUnit x✝ ∨ Prime x✝

State before:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
H : ∀ (I : Ideal R), I ≠ ⊥ → Ideal.IsPrime I → ∃ x ∈ I, Prime x
hP : Set.Nonempty {r | Prime r}
a : R
ha✝ : a ≠ 0
ha₂ : Set.Nonempty {r | Prime r} → ↑(Ideal.span {a}) ∩ ↑(Submonoid.closure {r | Prime r}).toSubsemigroup ≠ ∅
x : R
hx : x ∈ ↑(Ideal.span {a})
b : R
hx₂ : a * b ∈ ↑(Submonoid.closure {r | Prime r}).toSubsemigroup
hb : b * a = x
x✝ : R
ha : Prime x✝
⊢ IsUnit x✝ ∨ Prime x✝
Tactic:
right
State after:
case h
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
H : ∀ (I : Ideal R), I ≠ ⊥ → Ideal.IsPrime I → ∃ x ∈ I, Prime x
hP : Set.Nonempty {r | Prime r}
a : R
ha✝ : a ≠ 0
ha₂ : Set.Nonempty {r | Prime r} → ↑(Ideal.span {a}) ∩ ↑(Submonoid.closure {r | Prime r}).toSubsemigroup ≠ ∅
x : R
hx : x ∈ ↑(Ideal.span {a})
b : R
hx₂ : a * b ∈ ↑(Submonoid.closure {r | Prime r}).toSubsemigroup
hb : b * a = x
x✝ : R
ha : Prime x✝
⊢ Prime x✝

State before:
case h
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
H : ∀ (I : Ideal R), I ≠ ⊥ → Ideal.IsPrime I → ∃ x ∈ I, Prime x
hP : Set.Nonempty {r | Prime r}
a : R
ha✝ : a ≠ 0
ha₂ : Set.Nonempty {r | Prime r} → ↑(Ideal.span {a}) ∩ ↑(Submonoid.closure {r | Prime r}).toSubsemigroup ≠ ∅
x : R
hx : x ∈ ↑(Ideal.span {a})
b : R
hx₂ : a * b ∈ ↑(Submonoid.closure {r | Prime r}).toSubsemigroup
hb : b * a = x
x✝ : R
ha : Prime x✝
⊢ Prime x✝
Tactic:
exact ha
State after:
no goals