internlm/Lean-Github huggingface dataset:
Theorem: Submonoid.closure_mem_of_prod_mem
Proof state before:
case intro.refine_2.inr.inl.intro
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
a✝¹ : R
s : Multiset R
hind :
  ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → Multiset.prod s = a * b → a ∈ closure {r | IsUnit r ∨ Prime r}
x y : R
a✝ : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}
hprod : a✝¹ * Multiset.prod s = x * y
ha₂ : Prime a✝¹
c : R
hc : x = a✝¹ * c
⊢ a✝¹ * c ∈ closure {r | IsUnit r ∨ Prime r}

case intro.refine_2.inr.inr.intro
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
a✝¹ : R
s : Multiset R
hind :
  ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → Multiset.prod s = a * b → a ∈ closure {r | IsUnit r ∨ Prime r}
x y : R
a✝ : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}
hprod : a✝¹ * Multiset.prod s = x * y
ha₂ : Prime a✝¹
c : R
hc : y = a✝¹ * c
⊢ x ∈ closure {r | IsUnit r ∨ Prime r}
Tactic:
rw [hc, mul_assoc] at hprod
Proof state after:
case intro.refine_2.inr.inl.intro
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
a✝¹ : R
s : Multiset R
hind :
  ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → Multiset.prod s = a * b → a ∈ closure {r | IsUnit r ∨ Prime r}
x y : R
a✝ : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}
ha₂ : Prime a✝¹
c : R
hprod : a✝¹ * Multiset.prod s = a✝¹ * (c * y)
hc : x = a✝¹ * c
⊢ a✝¹ * c ∈ closure {r | IsUnit r ∨ Prime r}

case intro.refine_2.inr.inr.intro
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
a✝¹ : R
s : Multiset R
hind :
  ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → Multiset.prod s = a * b → a ∈ closure {r | IsUnit r ∨ Prime r}
x y : R
a✝ : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}
hprod : a✝¹ * Multiset.prod s = x * y
ha₂ : Prime a✝¹
c : R
hc : y = a✝¹ * c
⊢ x ∈ closure {r | IsUnit r ∨ Prime r}
Theorem: Submonoid.closure_mem_of_prod_mem
Proof state before:
case intro.refine_2.inr.inl.intro
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
a✝¹ : R
s : Multiset R
hind :
  ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → Multiset.prod s = a * b → a ∈ closure {r | IsUnit r ∨ Prime r}
x y : R
a✝ : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}
ha₂ : Prime a✝¹
c : R
hprod : a✝¹ * Multiset.prod s = a✝¹ * (c * y)
hc : x = a✝¹ * c
⊢ a✝¹ * c ∈ closure {r | IsUnit r ∨ Prime r}

case intro.refine_2.inr.inr.intro
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
a✝¹ : R
s : Multiset R
hind :
  ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → Multiset.prod s = a * b → a ∈ closure {r | IsUnit r ∨ Prime r}
x y : R
a✝ : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}
hprod : a✝¹ * Multiset.prod s = x * y
ha₂ : Prime a✝¹
c : R
hc : y = a✝¹ * c
⊢ x ∈ closure {r | IsUnit r ∨ Prime r}
Tactic:
refine' Submonoid.mul_mem _ (subset_closure (Set.mem_def.2 _))
  (hind _ _ _ hs (mul_left_cancel₀ ha₂.ne_zero hprod))
Proof state after:
case intro.refine_2.inr.inl.intro.refine'_1
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
a✝¹ : R
s : Multiset R
hind :
  ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → Multiset.prod s = a * b → a ∈ closure {r | IsUnit r ∨ Prime r}
x y : R
a✝ : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}
ha₂ : Prime a✝¹
c : R
hprod : a✝¹ * Multiset.prod s = a✝¹ * (c * y)
hc : x = a✝¹ * c
⊢ {r | IsUnit r ∨ Prime r} a✝¹

case intro.refine_2.inr.inl.intro.refine'_2
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
a✝¹ : R
s : Multiset R
hind :
  ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → Multiset.prod s = a * b → a ∈ closure {r | IsUnit r ∨ Prime r}
x y : R
a✝ : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}
ha₂ : Prime a✝¹
c : R
hprod : a✝¹ * Multiset.prod s = a✝¹ * (c * y)
hc : x = a✝¹ * c
⊢ c * y ∈ closure {r | IsUnit r ∨ Prime r}

case intro.refine_2.inr.inr.intro
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
a✝¹ : R
s : Multiset R
hind :
  ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → Multiset.prod s = a * b → a ∈ closure {r | IsUnit r ∨ Prime r}
x y : R
a✝ : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}
hprod : a✝¹ * Multiset.prod s = x * y
ha₂ : Prime a✝¹
c : R
hc : y = a✝¹ * c
⊢ x ∈ closure {r | IsUnit r ∨ Prime r}
Theorem: Submonoid.closure_mem_of_prod_mem
Proof state before:
case intro.refine_2.inr.inl.intro.refine'_1.h
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
a✝¹ : R
s : Multiset R
hind :
  ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → Multiset.prod s = a * b → a ∈ closure {r | IsUnit r ∨ Prime r}
x y : R
a✝ : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}
ha₂ : Prime a✝¹
c : R
hprod : a✝¹ * Multiset.prod s = a✝¹ * (c * y)
hc : x = a✝¹ * c
⊢ Prime a✝¹

case intro.refine_2.inr.inl.intro.refine'_2
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
a✝¹ : R
s : Multiset R
hind :
  ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → Multiset.prod s = a * b → a ∈ closure {r | IsUnit r ∨ Prime r}
x y : R
a✝ : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}
ha₂ : Prime a✝¹
c : R
hprod : a✝¹ * Multiset.prod s = a✝¹ * (c * y)
hc : x = a✝¹ * c
⊢ c * y ∈ closure {r | IsUnit r ∨ Prime r}

case intro.refine_2.inr.inr.intro
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
a✝¹ : R
s : Multiset R
hind :
  ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → Multiset.prod s = a * b → a ∈ closure {r | IsUnit r ∨ Prime r}
x y : R
a✝ : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}
hprod : a✝¹ * Multiset.prod s = x * y
ha₂ : Prime a✝¹
c : R
hc : y = a✝¹ * c
⊢ x ∈ closure {r | IsUnit r ∨ Prime r}
Tactic:
exact ha₂
Proof state after:
case intro.refine_2.inr.inl.intro.refine'_2
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
a✝¹ : R
s : Multiset R
hind :
  ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → Multiset.prod s = a * b → a ∈ closure {r | IsUnit r ∨ Prime r}
x y : R
a✝ : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}
ha₂ : Prime a✝¹
c : R
hprod : a✝¹ * Multiset.prod s = a✝¹ * (c * y)
hc : x = a✝¹ * c
⊢ c * y ∈ closure {r | IsUnit r ∨ Prime r}

case intro.refine_2.inr.inr.intro
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
a✝¹ : R
s : Multiset R
hind :
  ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → Multiset.prod s = a * b → a ∈ closure {r | IsUnit r ∨ Prime r}
x y : R
a✝ : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}
hprod : a✝¹ * Multiset.prod s = x * y
ha₂ : Prime a✝¹
c : R
hc : y = a✝¹ * c
⊢ x ∈ closure {r | IsUnit r ∨ Prime r}
Theorem: Submonoid.closure_mem_of_prod_mem
Proof state before:
case intro.refine_2.inr.inl.intro.refine'_2
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
a✝¹ : R
s : Multiset R
hind :
  ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → Multiset.prod s = a * b → a ∈ closure {r | IsUnit r ∨ Prime r}
x y : R
a✝ : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}
ha₂ : Prime a✝¹
c : R
hprod : a✝¹ * Multiset.prod s = a✝¹ * (c * y)
hc : x = a✝¹ * c
⊢ c * y ∈ closure {r | IsUnit r ∨ Prime r}

case intro.refine_2.inr.inr.intro
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
a✝¹ : R
s : Multiset R
hind :
  ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → Multiset.prod s = a * b → a ∈ closure {r | IsUnit r ∨ Prime r}
x y : R
a✝ : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}
hprod : a✝¹ * Multiset.prod s = x * y
ha₂ : Prime a✝¹
c : R
hc : y = a✝¹ * c
⊢ x ∈ closure {r | IsUnit r ∨ Prime r}
Tactic:
rw [← mul_left_cancel₀ ha₂.ne_zero hprod]
Proof state after:
case intro.refine_2.inr.inl.intro.refine'_2
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
a✝¹ : R
s : Multiset R
hind :
  ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → Multiset.prod s = a * b → a ∈ closure {r | IsUnit r ∨ Prime r}
x y : R
a✝ : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}
ha₂ : Prime a✝¹
c : R
hprod : a✝¹ * Multiset.prod s = a✝¹ * (c * y)
hc : x = a✝¹ * c
⊢ Multiset.prod s ∈ closure {r | IsUnit r ∨ Prime r}

case intro.refine_2.inr.inr.intro
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
a✝¹ : R
s : Multiset R
hind :
  ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → Multiset.prod s = a * b → a ∈ closure {r | IsUnit r ∨ Prime r}
x y : R
a✝ : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}
hprod : a✝¹ * Multiset.prod s = x * y
ha₂ : Prime a✝¹
c : R
hc : y = a✝¹ * c
⊢ x ∈ closure {r | IsUnit r ∨ Prime r}
Theorem: Submonoid.closure_mem_of_prod_mem
Proof state before:
case intro.refine_2.inr.inl.intro.refine'_2
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
a✝¹ : R
s : Multiset R
hind :
  ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → Multiset.prod s = a * b → a ∈ closure {r | IsUnit r ∨ Prime r}
x y : R
a✝ : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}
ha₂ : Prime a✝¹
c : R
hprod : a✝¹ * Multiset.prod s = a✝¹ * (c * y)
hc : x = a✝¹ * c
⊢ Multiset.prod s ∈ closure {r | IsUnit r ∨ Prime r}

case intro.refine_2.inr.inr.intro
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
a✝¹ : R
s : Multiset R
hind :
  ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → Multiset.prod s = a * b → a ∈ closure {r | IsUnit r ∨ Prime r}
x y : R
a✝ : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}
hprod : a✝¹ * Multiset.prod s = x * y
ha₂ : Prime a✝¹
c : R
hc : y = a✝¹ * c
⊢ x ∈ closure {r | IsUnit r ∨ Prime r}
Tactic:
exact multiset_prod_mem _ _ (fun t ht => subset_closure (hs t ht))
Proof state after:
case intro.refine_2.inr.inr.intro
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
a✝¹ : R
s : Multiset R
hind :
  ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → Multiset.prod s = a * b → a ∈ closure {r | IsUnit r ∨ Prime r}
x y : R
a✝ : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}
hprod : a✝¹ * Multiset.prod s = x * y
ha₂ : Prime a✝¹
c : R
hc : y = a✝¹ * c
⊢ x ∈ closure {r | IsUnit r ∨ Prime r}
Theorem: Submonoid.closure_mem_of_prod_mem
Proof state before:
case intro.refine_2.inr.inr.intro
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
a✝¹ : R
s : Multiset R
hind :
  ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → Multiset.prod s = a * b → a ∈ closure {r | IsUnit r ∨ Prime r}
x y : R
a✝ : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}
hprod : a✝¹ * Multiset.prod s = x * y
ha₂ : Prime a✝¹
c : R
hc : y = a✝¹ * c
⊢ x ∈ closure {r | IsUnit r ∨ Prime r}
Tactic:
rw [hc, mul_comm x _, mul_assoc, mul_comm c _] at hprod
Proof state after:
case intro.refine_2.inr.inr.intro
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
a✝¹ : R
s : Multiset R
hind :
  ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → Multiset.prod s = a * b → a ∈ closure {r | IsUnit r ∨ Prime r}
x y : R
a✝ : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}
ha₂ : Prime a✝¹
c : R
hprod : a✝¹ * Multiset.prod s = a✝¹ * (x * c)
hc : y = a✝¹ * c
⊢ x ∈ closure {r | IsUnit r ∨ Prime r}
Theorem: Submonoid.closure_mem_of_prod_mem
Proof state before:
case intro.refine_2.inr.inr.intro
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
a✝¹ : R
s : Multiset R
hind :
  ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → Multiset.prod s = a * b → a ∈ closure {r | IsUnit r ∨ Prime r}
x y : R
a✝ : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}
ha₂ : Prime a✝¹
c : R
hprod : a✝¹ * Multiset.prod s = a✝¹ * (x * c)
hc : y = a✝¹ * c
⊢ x ∈ closure {r | IsUnit r ∨ Prime r}
Tactic:
refine' hind x c _ hs (mul_left_cancel₀ ha₂.ne_zero hprod)
Proof state after:
case intro.refine_2.inr.inr.intro
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
a✝¹ : R
s : Multiset R
hind :
  ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → Multiset.prod s = a * b → a ∈ closure {r | IsUnit r ∨ Prime r}
x y : R
a✝ : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}
ha₂ : Prime a✝¹
c : R
hprod : a✝¹ * Multiset.prod s = a✝¹ * (x * c)
hc : y = a✝¹ * c
⊢ x * c ∈ closure {r | IsUnit r ∨ Prime r}
Theorem: Submonoid.closure_mem_of_prod_mem
Proof state before:
case intro.refine_2.inr.inr.intro
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
a✝¹ : R
s : Multiset R
hind :
  ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → Multiset.prod s = a * b → a ∈ closure {r | IsUnit r ∨ Prime r}
x y : R
a✝ : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}
ha₂ : Prime a✝¹
c : R
hprod : a✝¹ * Multiset.prod s = a✝¹ * (x * c)
hc : y = a✝¹ * c
⊢ x * c ∈ closure {r | IsUnit r ∨ Prime r}
Tactic:
rw [← mul_left_cancel₀ ha₂.ne_zero hprod]
Proof state after:
case intro.refine_2.inr.inr.intro
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
a✝¹ : R
s : Multiset R
hind :
  ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → Multiset.prod s = a * b → a ∈ closure {r | IsUnit r ∨ Prime r}
x y : R
a✝ : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}
ha₂ : Prime a✝¹
c : R
hprod : a✝¹ * Multiset.prod s = a✝¹ * (x * c)
hc : y = a✝¹ * c
⊢ Multiset.prod s ∈ closure {r | IsUnit r ∨ Prime r}
Theorem: Submonoid.closure_mem_of_prod_mem
Proof state before:
case intro.refine_2.inr.inr.intro
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
a✝¹ : R
s : Multiset R
hind :
  ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → Multiset.prod s = a * b → a ∈ closure {r | IsUnit r ∨ Prime r}
x y : R
a✝ : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}
ha₂ : Prime a✝¹
c : R
hprod : a✝¹ * Multiset.prod s = a✝¹ * (x * c)
hc : y = a✝¹ * c
⊢ Multiset.prod s ∈ closure {r | IsUnit r ∨ Prime r}
Tactic:
exact multiset_prod_mem _ _ (fun t ht => subset_closure (hs t ht))
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}
⊢ Ideal.span {a} ∉ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup
Tactic:
have hzero : 0 ∉ S := by
  intro h
  rcases Submonoid.exists_multiset_of_mem_closure h with ⟨l, ⟨hl, hprod⟩⟩
  exact not_prime_zero (hl 0 (Multiset.prod_eq_zero_iff.1 hprod))
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}
⊢ Ideal.span {a} ∉ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup
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}
⊢ Ideal.span {a} ∉ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup
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
⊢ 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
⊢ False
Tactic:
rcases exists_maximal_ideal _ hzero with ⟨T, hT, hT₂⟩
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}
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
⊢ 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}
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
⊢ False
Tactic:
have hT₃ : T ≠ ⊥ := by
  intro h₂
  rw [h₂] at hT₂
  exact ha (Ideal.span_singleton_eq_bot.1 (hT₂ (Ideal.span {a}) h (zero_le (Ideal.span {a}))))
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}
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 ≠ ⊥
⊢ 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}
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 ≠ ⊥
⊢ False
Tactic:
rw [Set.nonempty_def] at hP
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 : ∃ x, x ∈ {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
hT₃ : T ≠ ⊥
⊢ 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 : ∃ x, x ∈ {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
hT₃ : T ≠ ⊥
⊢ False
Tactic:
cases' hP with x hx
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}
⊢ 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}
⊢ False
Tactic:
have := Set.mem_of_subset_of_mem Submonoid.subset_closure hx
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})
⊢ 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})
⊢ False
Tactic:
simp 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}
⊢ False