internlm/Lean-Github huggingface dataset:
Theorem: ideal.span_ne_mem_kaplanski.set
Proof state before:
case intro.intro.intro
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
a : R
ha : a ≠ 0
H : ∀ (I : Ideal R), I ≠ ⊥ → Ideal.IsPrime I → ∃ x ∈ I, Prime x
hzero : 0 ∉ Submonoid.closure {r | Prime r}
h : Ideal.span {a} ∈ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup
T : Ideal R
hT : T ∈ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup
hT₂ : ∀ I ∈ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup, T ≤ I → I = T
hT₃ : T ≠ ⊥
x : R
hx : x ∈ {r | Prime r}
this : x ∈ Submonoid.closure {r | Prime r}
⊢ False
Tactic:
rw [← Submonoid.mem_toSubsemigroup] at this
Proof state after:
case intro.intro.intro
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
a : R
ha : a ≠ 0
H : ∀ (I : Ideal R), I ≠ ⊥ → Ideal.IsPrime I → ∃ x ∈ I, Prime x
hzero : 0 ∉ Submonoid.closure {r | Prime r}
h : Ideal.span {a} ∈ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup
T : Ideal R
hT : T ∈ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup
hT₂ : ∀ I ∈ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup, T ≤ I → I = T
hT₃ : T ≠ ⊥
x : R
hx : x ∈ {r | Prime r}
this : x ∈ (Submonoid.closure {r | Prime r}).toSubsemigroup
⊢ False
Theorem: ideal.span_ne_mem_kaplanski.set
Proof state before:
case intro.intro.intro
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
a : R
ha : a ≠ 0
H : ∀ (I : Ideal R), I ≠ ⊥ → Ideal.IsPrime I → ∃ x ∈ I, Prime x
hzero : 0 ∉ Submonoid.closure {r | Prime r}
h : Ideal.span {a} ∈ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup
T : Ideal R
hT : T ∈ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup
hT₂ : ∀ I ∈ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup, T ≤ I → I = T
hT₃ : T ≠ ⊥
x : R
hx : x ∈ {r | Prime r}
this : x ∈ (Submonoid.closure {r | Prime r}).toSubsemigroup
⊢ False
Tactic:
have := Set.nonempty_def.2 ⟨x, this⟩
Proof state after:
case intro.intro.intro
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
a : R
ha : a ≠ 0
H : ∀ (I : Ideal R), I ≠ ⊥ → Ideal.IsPrime I → ∃ x ∈ I, Prime x
hzero : 0 ∉ Submonoid.closure {r | Prime r}
h : Ideal.span {a} ∈ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup
T : Ideal R
hT : T ∈ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup
hT₂ : ∀ I ∈ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup, T ≤ I → I = T
hT₃ : T ≠ ⊥
x : R
hx : x ∈ {r | Prime r}
this✝ : x ∈ (Submonoid.closure {r | Prime r}).toSubsemigroup
this : Set.Nonempty ↑(Submonoid.closure {r | Prime r}).toSubsemigroup
⊢ False
Theorem: ideal.span_ne_mem_kaplanski.set
Proof state before:
case intro.intro.intro
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
a : R
ha : a ≠ 0
H : ∀ (I : Ideal R), I ≠ ⊥ → Ideal.IsPrime I → ∃ x ∈ I, Prime x
hzero : 0 ∉ Submonoid.closure {r | Prime r}
h : Ideal.span {a} ∈ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup
T : Ideal R
hT : T ∈ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup
hT₂ : ∀ I ∈ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup, T ≤ I → I = T
hT₃ : T ≠ ⊥
x : R
hx : x ∈ {r | Prime r}
this✝ : x ∈ (Submonoid.closure {r | Prime r}).toSubsemigroup
this : Set.Nonempty ↑(Submonoid.closure {r | Prime r}).toSubsemigroup
⊢ False
Tactic:
rcases (H T) hT₃ (isPrime_of_maximal this hT hT₂) with ⟨x, H₃, H₄⟩
Proof state after:
case intro.intro.intro.intro.intro
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
a : R
ha : a ≠ 0
H : ∀ (I : Ideal R), I ≠ ⊥ → Ideal.IsPrime I → ∃ x ∈ I, Prime x
hzero : 0 ∉ Submonoid.closure {r | Prime r}
h : Ideal.span {a} ∈ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup
T : Ideal R
hT : T ∈ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup
hT₂ : ∀ I ∈ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup, T ≤ I → I = T
hT₃ : T ≠ ⊥
x✝ : R
hx : x✝ ∈ {r | Prime r}
this✝ : x✝ ∈ (Submonoid.closure {r | Prime r}).toSubsemigroup
this : Set.Nonempty ↑(Submonoid.closure {r | Prime r}).toSubsemigroup
x : R
H₃ : x ∈ T
H₄ : Prime x
⊢ False
Theorem: ideal.span_ne_mem_kaplanski.set
Proof state before:
case intro.intro.intro.intro.intro
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
a : R
ha : a ≠ 0
H : ∀ (I : Ideal R), I ≠ ⊥ → Ideal.IsPrime I → ∃ x ∈ I, Prime x
hzero : 0 ∉ Submonoid.closure {r | Prime r}
h : Ideal.span {a} ∈ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup
T : Ideal R
hT : T ∈ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup
hT₂ : ∀ I ∈ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup, T ≤ I → I = T
hT₃ : T ≠ ⊥
x✝ : R
hx : x✝ ∈ {r | Prime r}
this✝ : x✝ ∈ (Submonoid.closure {r | Prime r}).toSubsemigroup
this : Set.Nonempty ↑(Submonoid.closure {r | Prime r}).toSubsemigroup
x : R
H₃ : x ∈ T
H₄ : Prime x
⊢ False
Tactic:
rw [Kaplansky.set_def, Set.eq_empty_iff_forall_not_mem] at hT
Proof state after:
case intro.intro.intro.intro.intro
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
a : R
ha : a ≠ 0
H : ∀ (I : Ideal R), I ≠ ⊥ → Ideal.IsPrime I → ∃ x ∈ I, Prime x
hzero : 0 ∉ Submonoid.closure {r | Prime r}
h : Ideal.span {a} ∈ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup
T : Ideal R
hT : ∀ (x : R), x ∉ ↑T ∩ ↑(Submonoid.closure {r | Prime r}).toSubsemigroup
hT₂ : ∀ I ∈ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup, T ≤ I → I = T
hT₃ : T ≠ ⊥
x✝ : R
hx : x✝ ∈ {r | Prime r}
this✝ : x✝ ∈ (Submonoid.closure {r | Prime r}).toSubsemigroup
this : Set.Nonempty ↑(Submonoid.closure {r | Prime r}).toSubsemigroup
x : R
H₃ : x ∈ T
H₄ : Prime x
⊢ False
Theorem: ideal.span_ne_mem_kaplanski.set
Proof state before:
case intro.intro.intro.intro.intro
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
a : R
ha : a ≠ 0
H : ∀ (I : Ideal R), I ≠ ⊥ → Ideal.IsPrime I → ∃ x ∈ I, Prime x
hzero : 0 ∉ Submonoid.closure {r | Prime r}
h : Ideal.span {a} ∈ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup
T : Ideal R
hT : ∀ (x : R), x ∉ ↑T ∩ ↑(Submonoid.closure {r | Prime r}).toSubsemigroup
hT₂ : ∀ I ∈ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup, T ≤ I → I = T
hT₃ : T ≠ ⊥
x✝ : R
hx : x✝ ∈ {r | Prime r}
this✝ : x✝ ∈ (Submonoid.closure {r | Prime r}).toSubsemigroup
this : Set.Nonempty ↑(Submonoid.closure {r | Prime r}).toSubsemigroup
x : R
H₃ : x ∈ T
H₄ : Prime x
⊢ False
Tactic:
exact hT x ⟨H₃, Submonoid.subset_closure H₄⟩
Proof state after:
no goals
Theorem: ideal.span_ne_mem_kaplanski.set
Proof state before:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
a : R
ha : a ≠ 0
H : ∀ (I : Ideal R), I ≠ ⊥ → Ideal.IsPrime I → ∃ x ∈ I, Prime x
hP : Set.Nonempty {r | Prime r}
⊢ 0 ∉ Submonoid.closure {r | Prime r}
Tactic:
intro h
Proof state after:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
a : R
ha : a ≠ 0
H : ∀ (I : Ideal R), I ≠ ⊥ → Ideal.IsPrime I → ∃ x ∈ I, Prime x
hP : Set.Nonempty {r | Prime r}
h : 0 ∈ Submonoid.closure {r | Prime r}
⊢ False
Theorem: ideal.span_ne_mem_kaplanski.set
Proof state before:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
a : R
ha : a ≠ 0
H : ∀ (I : Ideal R), I ≠ ⊥ → Ideal.IsPrime I → ∃ x ∈ I, Prime x
hP : Set.Nonempty {r | Prime r}
h : 0 ∈ Submonoid.closure {r | Prime r}
⊢ False
Tactic:
rcases Submonoid.exists_multiset_of_mem_closure h with ⟨l, ⟨hl, hprod⟩⟩
Proof state after:
case intro.intro
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
a : R
ha : a ≠ 0
H : ∀ (I : Ideal R), I ≠ ⊥ → Ideal.IsPrime I → ∃ x ∈ I, Prime x
hP : Set.Nonempty {r | Prime r}
h : 0 ∈ Submonoid.closure {r | Prime r}
l : Multiset R
hl : ∀ y ∈ l, y ∈ {r | Prime r}
hprod : Multiset.prod l = 0
⊢ False
Theorem: ideal.span_ne_mem_kaplanski.set
Proof state before:
case intro.intro
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
a : R
ha : a ≠ 0
H : ∀ (I : Ideal R), I ≠ ⊥ → Ideal.IsPrime I → ∃ x ∈ I, Prime x
hP : Set.Nonempty {r | Prime r}
h : 0 ∈ Submonoid.closure {r | Prime r}
l : Multiset R
hl : ∀ y ∈ l, y ∈ {r | Prime r}
hprod : Multiset.prod l = 0
⊢ False
Tactic:
exact not_prime_zero (hl 0 (Multiset.prod_eq_zero_iff.1 hprod))
Proof state after:
no goals
Theorem: ideal.span_ne_mem_kaplanski.set
Proof state before:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
a : R
ha : a ≠ 0
H : ∀ (I : Ideal R), I ≠ ⊥ → Ideal.IsPrime I → ∃ x ∈ I, Prime x
hP : Set.Nonempty {r | Prime r}
hzero : 0 ∉ Submonoid.closure {r | Prime r}
h : Ideal.span {a} ∈ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup
T : Ideal R
hT : T ∈ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup
hT₂ : ∀ I ∈ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup, T ≤ I → I = T
⊢ T ≠ ⊥
Tactic:
intro h₂
Proof state after:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
a : R
ha : a ≠ 0
H : ∀ (I : Ideal R), I ≠ ⊥ → Ideal.IsPrime I → ∃ x ∈ I, Prime x
hP : Set.Nonempty {r | Prime r}
hzero : 0 ∉ Submonoid.closure {r | Prime r}
h : Ideal.span {a} ∈ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup
T : Ideal R
hT : T ∈ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup
hT₂ : ∀ I ∈ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup, T ≤ I → I = T
h₂ : T = ⊥
⊢ False
Theorem: ideal.span_ne_mem_kaplanski.set
Proof state before:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
a : R
ha : a ≠ 0
H : ∀ (I : Ideal R), I ≠ ⊥ → Ideal.IsPrime I → ∃ x ∈ I, Prime x
hP : Set.Nonempty {r | Prime r}
hzero : 0 ∉ Submonoid.closure {r | Prime r}
h : Ideal.span {a} ∈ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup
T : Ideal R
hT : T ∈ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup
hT₂ : ∀ I ∈ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup, T ≤ I → I = T
h₂ : T = ⊥
⊢ False
Tactic:
rw [h₂] at hT₂
Proof state after:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
a : R
ha : a ≠ 0
H : ∀ (I : Ideal R), I ≠ ⊥ → Ideal.IsPrime I → ∃ x ∈ I, Prime x
hP : Set.Nonempty {r | Prime r}
hzero : 0 ∉ Submonoid.closure {r | Prime r}
h : Ideal.span {a} ∈ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup
T : Ideal R
hT : T ∈ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup
hT₂ : ∀ I ∈ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup, ⊥ ≤ I → I = ⊥
h₂ : T = ⊥
⊢ False
Theorem: ideal.span_ne_mem_kaplanski.set
Proof state before:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
a : R
ha : a ≠ 0
H : ∀ (I : Ideal R), I ≠ ⊥ → Ideal.IsPrime I → ∃ x ∈ I, Prime x
hP : Set.Nonempty {r | Prime r}
hzero : 0 ∉ Submonoid.closure {r | Prime r}
h : Ideal.span {a} ∈ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup
T : Ideal R
hT : T ∈ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup
hT₂ : ∀ I ∈ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup, ⊥ ≤ I → I = ⊥
h₂ : T = ⊥
⊢ False
Tactic:
exact ha (Ideal.span_singleton_eq_bot.1 (hT₂ (Ideal.span {a}) h (zero_le (Ideal.span {a}))))
Proof state after:
no goals
Theorem: exists_prime_factors_of_exists_multiset
Proof state before:
R : Type u_1
inst✝ : CommMonoidWithZero R
a : R
h : ∃ l, ∃ (_ : ∀ y ∈ l, y ∈ {r | IsUnit r ∨ Prime r}), Multiset.prod l = a
⊢ ∃ f, (∀ b ∈ f, Prime b) ∧ Associated (Multiset.prod f) a
Tactic:
rcases h with ⟨l ,hl, hl₂⟩
Proof state after:
case intro.intro
R : Type u_1
inst✝ : CommMonoidWithZero R
a : R
l : Multiset R
hl : ∀ y ∈ l, y ∈ {r | IsUnit r ∨ Prime r}
hl₂ : Multiset.prod l = a
⊢ ∃ f, (∀ b ∈ f, Prime b) ∧ Associated (Multiset.prod f) a
Theorem: exists_prime_factors_of_exists_multiset
Proof state before:
case intro.intro
R : Type u_1
inst✝ : CommMonoidWithZero R
a : R
l : Multiset R
hl : ∀ y ∈ l, y ∈ {r | IsUnit r ∨ Prime r}
hl₂ : Multiset.prod l = a
⊢ ∃ f, (∀ b ∈ f, Prime b) ∧ Associated (Multiset.prod f) a
Tactic:
revert a hl hl₂
Proof state after:
case intro.intro
R : Type u_1
inst✝ : CommMonoidWithZero R
l : Multiset R
⊢ ∀ (a : R),
    (∀ y ∈ l, y ∈ {r | IsUnit r ∨ Prime r}) →
      Multiset.prod l = a → ∃ f, (∀ b ∈ f, Prime b) ∧ Associated (Multiset.prod f) a
Theorem: exists_prime_factors_of_exists_multiset
Proof state before:
case intro.intro
R : Type u_1
inst✝ : CommMonoidWithZero R
l : Multiset R
⊢ ∀ (a : R),
    (∀ y ∈ l, y ∈ {r | IsUnit r ∨ Prime r}) →
      Multiset.prod l = a → ∃ f, (∀ b ∈ f, Prime b) ∧ Associated (Multiset.prod f) a
Tactic:
refine' l.induction (p := fun l => ∀ a, (∀ y ∈ l, y ∈ {r | IsUnit r ∨ Prime r}) →
  l.prod = a → ∃ (f : Multiset R), (∀ b ∈ f, Prime b) ∧ Associated f.prod a) _ _
Proof state after:
case intro.intro.refine'_1
R : Type u_1
inst✝ : CommMonoidWithZero R
l : Multiset R
⊢ (fun l =>
      ∀ (a : R),
        (∀ y ∈ l, y ∈ {r | IsUnit r ∨ Prime r}) →
          Multiset.prod l = a → ∃ f, (∀ b ∈ f, Prime b) ∧ Associated (Multiset.prod f) a)
    0

case intro.intro.refine'_2
R : Type u_1
inst✝ : CommMonoidWithZero R
l : Multiset R
⊢ ∀ ⦃a : R⦄ {s : Multiset R},
    (fun l =>
          ∀ (a : R),
            (∀ y ∈ l, y ∈ {r | IsUnit r ∨ Prime r}) →
              Multiset.prod l = a → ∃ f, (∀ b ∈ f, Prime b) ∧ Associated (Multiset.prod f) a)
        s →
      (fun l =>
          ∀ (a : R),
            (∀ y ∈ l, y ∈ {r | IsUnit r ∨ Prime r}) →
              Multiset.prod l = a → ∃ f, (∀ b ∈ f, Prime b) ∧ Associated (Multiset.prod f) a)
        (a ::ₘ s)
Theorem: exists_prime_factors_of_exists_multiset
Proof state before:
case intro.intro.refine'_1
R : Type u_1
inst✝ : CommMonoidWithZero R
l : Multiset R
⊢ (fun l =>
      ∀ (a : R),
        (∀ y ∈ l, y ∈ {r | IsUnit r ∨ Prime r}) →
          Multiset.prod l = a → ∃ f, (∀ b ∈ f, Prime b) ∧ Associated (Multiset.prod f) a)
    0
Tactic:
simp only [Multiset.not_mem_zero, Set.mem_setOf_eq, IsEmpty.forall_iff, forall_const,
  Multiset.prod_zero, forall_true_left, forall_eq']
Proof state after:
case intro.intro.refine'_1
R : Type u_1
inst✝ : CommMonoidWithZero R
l : Multiset R
⊢ ∃ f, (∀ b ∈ f, Prime b) ∧ Associated (Multiset.prod f) 1
Theorem: exists_prime_factors_of_exists_multiset
Proof state before:
case intro.intro.refine'_1
R : Type u_1
inst✝ : CommMonoidWithZero R
l : Multiset R
⊢ ∃ f, (∀ b ∈ f, Prime b) ∧ Associated (Multiset.prod f) 1
Tactic:
use 0
Proof state after:
case h
R : Type u_1
inst✝ : CommMonoidWithZero R
l : Multiset R
⊢ (∀ b ∈ 0, Prime b) ∧ Associated (Multiset.prod 0) 1
Theorem: exists_prime_factors_of_exists_multiset
Proof state before:
case h
R : Type u_1
inst✝ : CommMonoidWithZero R
l : Multiset R
⊢ (∀ b ∈ 0, Prime b) ∧ Associated (Multiset.prod 0) 1
Tactic:
simp only [Multiset.not_mem_zero, IsEmpty.forall_iff, forall_const, Multiset.prod_zero,
  true_and]
Proof state after:
case h
R : Type u_1
inst✝ : CommMonoidWithZero R
l : Multiset R
⊢ Associated 1 1
Theorem: exists_prime_factors_of_exists_multiset
Proof state before:
case h
R : Type u_1
inst✝ : CommMonoidWithZero R
l : Multiset R
⊢ Associated 1 1
Tactic:
exact Associated.refl 1
Proof state after:
no goals
Theorem: exists_prime_factors_of_exists_multiset
Proof state before:
case intro.intro.refine'_2
R : Type u_1
inst✝ : CommMonoidWithZero R
l : Multiset R
⊢ ∀ ⦃a : R⦄ {s : Multiset R},
    (fun l =>
          ∀ (a : R),
            (∀ y ∈ l, y ∈ {r | IsUnit r ∨ Prime r}) →
              Multiset.prod l = a → ∃ f, (∀ b ∈ f, Prime b) ∧ Associated (Multiset.prod f) a)
        s →
      (fun l =>
          ∀ (a : R),
            (∀ y ∈ l, y ∈ {r | IsUnit r ∨ Prime r}) →
              Multiset.prod l = a → ∃ f, (∀ b ∈ f, Prime b) ∧ Associated (Multiset.prod f) a)
        (a ::ₘ s)
Tactic:
simp only [Set.mem_setOf_eq, forall_apply_eq_imp_iff, Multiset.mem_cons, forall_eq_or_imp,
  Multiset.prod_cons, and_imp, forall_apply_eq_imp_iff₂]
Proof state after:
case intro.intro.refine'_2
R : Type u_1
inst✝ : CommMonoidWithZero R
l : Multiset R
⊢ ∀ ⦃a : R⦄ {s : Multiset R},
    ((∀ y ∈ s, IsUnit y ∨ Prime y) → ∃ f, (∀ b ∈ f, Prime b) ∧ Associated (Multiset.prod f) (Multiset.prod s)) →
      IsUnit a ∨ Prime a →
        (∀ y ∈ s, IsUnit y ∨ Prime y) → ∃ f, (∀ b ∈ f, Prime b) ∧ Associated (Multiset.prod f) (a * Multiset.prod s)
Theorem: exists_prime_factors_of_exists_multiset
Proof state before:
case intro.intro.refine'_2
R : Type u_1
inst✝ : CommMonoidWithZero R
l : Multiset R
⊢ ∀ ⦃a : R⦄ {s : Multiset R},
    ((∀ y ∈ s, IsUnit y ∨ Prime y) → ∃ f, (∀ b ∈ f, Prime b) ∧ Associated (Multiset.prod f) (Multiset.prod s)) →
      IsUnit a ∨ Prime a →
        (∀ y ∈ s, IsUnit y ∨ Prime y) → ∃ f, (∀ b ∈ f, Prime b) ∧ Associated (Multiset.prod f) (a * Multiset.prod s)
Tactic:
intros a s hind ha hs
Proof state after:
case intro.intro.refine'_2
R : Type u_1
inst✝ : CommMonoidWithZero R
l : Multiset R
a : R
s : Multiset R
hind : (∀ y ∈ s, IsUnit y ∨ Prime y) → ∃ f, (∀ b ∈ f, Prime b) ∧ Associated (Multiset.prod f) (Multiset.prod s)
ha : IsUnit a ∨ Prime a
hs : ∀ y ∈ s, IsUnit y ∨ Prime y
⊢ ∃ f, (∀ b ∈ f, Prime b) ∧ Associated (Multiset.prod f) (a * Multiset.prod s)
Theorem: exists_prime_factors_of_exists_multiset
Proof state before:
case intro.intro.refine'_2
R : Type u_1
inst✝ : CommMonoidWithZero R
l : Multiset R
a : R
s : Multiset R
hind : (∀ y ∈ s, IsUnit y ∨ Prime y) → ∃ f, (∀ b ∈ f, Prime b) ∧ Associated (Multiset.prod f) (Multiset.prod s)
ha : IsUnit a ∨ Prime a
hs : ∀ y ∈ s, IsUnit y ∨ Prime y
⊢ ∃ f, (∀ b ∈ f, Prime b) ∧ Associated (Multiset.prod f) (a * Multiset.prod s)
Tactic:
rcases ha with ha₁ | ha₂
Proof state after:
case intro.intro.refine'_2.inl
R : Type u_1
inst✝ : CommMonoidWithZero R
l : Multiset R
a : R
s : Multiset R
hind : (∀ y ∈ s, IsUnit y ∨ Prime y) → ∃ f, (∀ b ∈ f, Prime b) ∧ Associated (Multiset.prod f) (Multiset.prod s)
hs : ∀ y ∈ s, IsUnit y ∨ Prime y
ha₁ : IsUnit a
⊢ ∃ f, (∀ b ∈ f, Prime b) ∧ Associated (Multiset.prod f) (a * Multiset.prod s)

case intro.intro.refine'_2.inr
R : Type u_1
inst✝ : CommMonoidWithZero R
l : Multiset R
a : R
s : Multiset R
hind : (∀ y ∈ s, IsUnit y ∨ Prime y) → ∃ f, (∀ b ∈ f, Prime b) ∧ Associated (Multiset.prod f) (Multiset.prod s)
hs : ∀ y ∈ s, IsUnit y ∨ Prime y
ha₂ : Prime a
⊢ ∃ f, (∀ b ∈ f, Prime b) ∧ Associated (Multiset.prod f) (a * Multiset.prod s)
Theorem: exists_prime_factors_of_exists_multiset
Proof state before:
case intro.intro.refine'_2.inl
R : Type u_1
inst✝ : CommMonoidWithZero R
l : Multiset R
a : R
s : Multiset R
hind : (∀ y ∈ s, IsUnit y ∨ Prime y) → ∃ f, (∀ b ∈ f, Prime b) ∧ Associated (Multiset.prod f) (Multiset.prod s)
hs : ∀ y ∈ s, IsUnit y ∨ Prime y
ha₁ : IsUnit a
⊢ ∃ f, (∀ b ∈ f, Prime b) ∧ Associated (Multiset.prod f) (a * Multiset.prod s)
Tactic:
rcases (hind hs) with ⟨f, hf, hf₂⟩
Proof state after:
case intro.intro.refine'_2.inl.intro.intro
R : Type u_1
inst✝ : CommMonoidWithZero R
l : Multiset R
a : R
s : Multiset R
hind : (∀ y ∈ s, IsUnit y ∨ Prime y) → ∃ f, (∀ b ∈ f, Prime b) ∧ Associated (Multiset.prod f) (Multiset.prod s)
hs : ∀ y ∈ s, IsUnit y ∨ Prime y
ha₁ : IsUnit a
f : Multiset R
hf : ∀ b ∈ f, Prime b
hf₂ : Associated (Multiset.prod f) (Multiset.prod s)
⊢ ∃ f, (∀ b ∈ f, Prime b) ∧ Associated (Multiset.prod f) (a * Multiset.prod s)
Theorem: exists_prime_factors_of_exists_multiset
Proof state before:
case intro.intro.refine'_2.inl.intro.intro
R : Type u_1
inst✝ : CommMonoidWithZero R
l : Multiset R
a : R
s : Multiset R
hind : (∀ y ∈ s, IsUnit y ∨ Prime y) → ∃ f, (∀ b ∈ f, Prime b) ∧ Associated (Multiset.prod f) (Multiset.prod s)
hs : ∀ y ∈ s, IsUnit y ∨ Prime y
ha₁ : IsUnit a
f : Multiset R
hf : ∀ b ∈ f, Prime b
hf₂ : Associated (Multiset.prod f) (Multiset.prod s)
⊢ ∃ f, (∀ b ∈ f, Prime b) ∧ Associated (Multiset.prod f) (a * Multiset.prod s)
Tactic:
exact ⟨f, hf, (associated_isUnit_mul_right_iff ha₁).2 hf₂⟩
Proof state after:
no goals
Theorem: exists_prime_factors_of_exists_multiset
Proof state before:
case intro.intro.refine'_2.inr
R : Type u_1
inst✝ : CommMonoidWithZero R
l : Multiset R
a : R
s : Multiset R
hind : (∀ y ∈ s, IsUnit y ∨ Prime y) → ∃ f, (∀ b ∈ f, Prime b) ∧ Associated (Multiset.prod f) (Multiset.prod s)
hs : ∀ y ∈ s, IsUnit y ∨ Prime y
ha₂ : Prime a
⊢ ∃ f, (∀ b ∈ f, Prime b) ∧ Associated (Multiset.prod f) (a * Multiset.prod s)
Tactic:
rcases (hind hs) with ⟨f, hf, hf₂⟩
Proof state after:
case intro.intro.refine'_2.inr.intro.intro
R : Type u_1
inst✝ : CommMonoidWithZero R
l : Multiset R
a : R
s : Multiset R
hind : (∀ y ∈ s, IsUnit y ∨ Prime y) → ∃ f, (∀ b ∈ f, Prime b) ∧ Associated (Multiset.prod f) (Multiset.prod s)
hs : ∀ y ∈ s, IsUnit y ∨ Prime y
ha₂ : Prime a
f : Multiset R
hf : ∀ b ∈ f, Prime b
hf₂ : Associated (Multiset.prod f) (Multiset.prod s)
⊢ ∃ f, (∀ b ∈ f, Prime b) ∧ Associated (Multiset.prod f) (a * Multiset.prod s)
Theorem: exists_prime_factors_of_exists_multiset
Proof state before:
case intro.intro.refine'_2.inr.intro.intro
R : Type u_1
inst✝ : CommMonoidWithZero R
l : Multiset R
a : R
s : Multiset R
hind : (∀ y ∈ s, IsUnit y ∨ Prime y) → ∃ f, (∀ b ∈ f, Prime b) ∧ Associated (Multiset.prod f) (Multiset.prod s)
hs : ∀ y ∈ s, IsUnit y ∨ Prime y
ha₂ : Prime a
f : Multiset R
hf : ∀ b ∈ f, Prime b
hf₂ : Associated (Multiset.prod f) (Multiset.prod s)
⊢ ∃ f, (∀ b ∈ f, Prime b) ∧ Associated (Multiset.prod f) (a * Multiset.prod s)
Tactic:
refine' ⟨f.cons a, Multiset.forall_mem_cons.2 ⟨ha₂, hf⟩, _⟩
Proof state after:
case intro.intro.refine'_2.inr.intro.intro
R : Type u_1
inst✝ : CommMonoidWithZero R
l : Multiset R
a : R
s : Multiset R
hind : (∀ y ∈ s, IsUnit y ∨ Prime y) → ∃ f, (∀ b ∈ f, Prime b) ∧ Associated (Multiset.prod f) (Multiset.prod s)
hs : ∀ y ∈ s, IsUnit y ∨ Prime y
ha₂ : Prime a
f : Multiset R
hf : ∀ b ∈ f, Prime b
hf₂ : Associated (Multiset.prod f) (Multiset.prod s)
⊢ Associated (Multiset.prod (a ::ₘ f)) (a * Multiset.prod s)
Theorem: exists_prime_factors_of_exists_multiset
Proof state before:
case intro.intro.refine'_2.inr.intro.intro
R : Type u_1
inst✝ : CommMonoidWithZero R
l : Multiset R
a : R
s : Multiset R
hind : (∀ y ∈ s, IsUnit y ∨ Prime y) → ∃ f, (∀ b ∈ f, Prime b) ∧ Associated (Multiset.prod f) (Multiset.prod s)
hs : ∀ y ∈ s, IsUnit y ∨ Prime y
ha₂ : Prime a
f : Multiset R
hf : ∀ b ∈ f, Prime b
hf₂ : Associated (Multiset.prod f) (Multiset.prod s)
⊢ Associated (Multiset.prod (a ::ₘ f)) (a * Multiset.prod s)
Tactic:
rw [Multiset.prod_cons]
Proof state after:
case intro.intro.refine'_2.inr.intro.intro
R : Type u_1
inst✝ : CommMonoidWithZero R
l : Multiset R
a : R
s : Multiset R
hind : (∀ y ∈ s, IsUnit y ∨ Prime y) → ∃ f, (∀ b ∈ f, Prime b) ∧ Associated (Multiset.prod f) (Multiset.prod s)
hs : ∀ y ∈ s, IsUnit y ∨ Prime y
ha₂ : Prime a
f : Multiset R
hf : ∀ b ∈ f, Prime b
hf₂ : Associated (Multiset.prod f) (Multiset.prod s)
⊢ Associated (a * Multiset.prod f) (a * Multiset.prod s)
Theorem: exists_prime_factors_of_exists_multiset
Proof state before:
case intro.intro.refine'_2.inr.intro.intro
R : Type u_1
inst✝ : CommMonoidWithZero R
l : Multiset R
a : R
s : Multiset R
hind : (∀ y ∈ s, IsUnit y ∨ Prime y) → ∃ f, (∀ b ∈ f, Prime b) ∧ Associated (Multiset.prod f) (Multiset.prod s)
hs : ∀ y ∈ s, IsUnit y ∨ Prime y
ha₂ : Prime a
f : Multiset R
hf : ∀ b ∈ f, Prime b
hf₂ : Associated (Multiset.prod f) (Multiset.prod s)
⊢ Associated (a * Multiset.prod f) (a * Multiset.prod s)
Tactic:
exact Associated.mul_left a hf₂
Proof state after:
no goals
Theorem: uniqueFactorizationMonoid_of_exists_prime
Proof 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 => _
Proof 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
Theorem: uniqueFactorizationMonoid_of_exists_prime
Proof 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
Proof 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