Theorem: Submonoid.closure_mem_of_prod_mem
Proof state before:
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}
Tactic:
right
Proof state after:
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}