-- Mathlib/Algebra/BigOperators/Associated.lean
theorem divisor_closure_eq_closure [CancelCommMonoidWithZero α]
    (x y : α) (hxy : x * y ∈ closure { r : α | IsUnit r ∨ Prime r}) :
    x ∈ closure { r : α | IsUnit r ∨ Prime r}

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

Tactic:
exact multiset_prod_mem _ _ (fun t ht => subset_closure (hs t ht))

Result:
no goals

Proof state:
case intro.intro.cons
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
c : α
s : Multiset α
hind :
  ∀ (x y : α),
    x * y ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → s.prod = x * y → x ∈ closure {r | IsUnit r ∨ Prime r}
x y : α
hxy : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hprod : (c ::ₘ s).prod = x * y
hm : (IsUnit c ∨ Prime c) ∧ ∀ a ∈ s, IsUnit a ∨ Prime a
⊢ x ∈ closure {r | IsUnit r ∨ Prime r}

Tactic:
simp only [Multiset.prod_cons] at hprod

Result:
case intro.intro.cons
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
c : α
s : Multiset α
hind :
  ∀ (x y : α),
    x * y ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → s.prod = x * y → x ∈ closure {r | IsUnit r ∨ Prime r}
x y : α
hxy : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hm : (IsUnit c ∨ Prime c) ∧ ∀ a ∈ s, IsUnit a ∨ Prime a
hprod : c * s.prod = x * y
⊢ x ∈ closure {r | IsUnit r ∨ Prime r}

Proof state:
case intro.intro.empty.a
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
x y : α
hxy : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hm : ∀ y ∈ 0, y ∈ {r | IsUnit r ∨ Prime r}
hprod : Multiset.prod 0 = x * y
⊢ IsUnit x ∨ Prime x

Tactic:
simp only [Multiset.prod_zero] at hprod

Result:
case intro.intro.empty.a
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
x y : α
hxy : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hm : ∀ y ∈ 0, y ∈ {r | IsUnit r ∨ Prime r}
hprod : 1 = x * y
⊢ IsUnit x ∨ Prime x

Proof state:
case intro.intro.empty.a.h
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
x y : α
hxy : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hm : ∀ y ∈ 0, y ∈ {r | IsUnit r ∨ Prime r}
hprod : 1 = x * y
⊢ IsUnit x

Tactic:
exact isUnit_of_mul_eq_one _ _ hprod.symm

Result:
no goals

Proof state:
case intro.intro.cons.intro.inr.inr.intro
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
c✝ : α
s : Multiset α
hind :
  ∀ (x y : α),
    x * y ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, IsUnit y ∨ Prime y) → s.prod = x * y → x ∈ closure {r | IsUnit r ∨ Prime r}
x y : α
hxy : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hprod : c✝ * s.prod = x * y
hs : ∀ a ∈ s, IsUnit a ∨ Prime a
ha₂ : Prime c✝
c : α
hc : y = c✝ * c
⊢ x ∈ closure {r | IsUnit r ∨ Prime r}

Tactic:
rw [hc, mul_comm x _, mul_assoc, mul_comm c _] at hprod

Result:
case intro.intro.cons.intro.inr.inr.intro
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
c✝ : α
s : Multiset α
hind :
  ∀ (x y : α),
    x * y ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, IsUnit y ∨ Prime y) → s.prod = x * y → x ∈ closure {r | IsUnit r ∨ Prime r}
x y : α
hxy : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ a ∈ s, IsUnit a ∨ Prime a
ha₂ : Prime c✝
c : α
hprod : c✝ * s.prod = c✝ * (x * c)
hc : y = c✝ * c
⊢ x ∈ closure {r | IsUnit r ∨ Prime r}

Proof state:
case intro.intro.cons
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
c : α
s : Multiset α
hind :
  ∀ (x y : α),
    x * y ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → s.prod = x * y → x ∈ closure {r | IsUnit r ∨ Prime r}
x y : α
hxy : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hm : ∀ y ∈ c ::ₘ s, y ∈ {r | IsUnit r ∨ Prime r}
hprod : (c ::ₘ s).prod = x * y
⊢ x ∈ closure {r | IsUnit r ∨ Prime r}

Tactic:
simp only [Multiset.mem_cons, forall_eq_or_imp, Set.mem_setOf] at hm

Result:
case intro.intro.cons
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
c : α
s : Multiset α
hind :
  ∀ (x y : α),
    x * y ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → s.prod = x * y → x ∈ closure {r | IsUnit r ∨ Prime r}
x y : α
hxy : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hprod : (c ::ₘ s).prod = x * y
hm : (IsUnit c ∨ Prime c) ∧ ∀ a ∈ s, IsUnit a ∨ Prime a
⊢ x ∈ closure {r | IsUnit r ∨ Prime r}

Proof state:
case intro.intro.cons.intro.inl.intro.refine_1
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
c : α
s : Multiset α
hind :
  ∀ (x y : α),
    x * y ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, IsUnit y ∨ Prime y) → s.prod = x * y → x ∈ closure {r | IsUnit r ∨ Prime r}
x y : α
hxy : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hprod : c * s.prod = x * y
hs : ∀ a ∈ s, IsUnit a ∨ Prime a
ha₁ : IsUnit c
k : α
hk : c * k = 1
⊢ x * (y * k) ∈ closure {r | IsUnit r ∨ Prime r}

Tactic:
simp only [← mul_assoc, ← hprod, ← Multiset.prod_cons, mul_comm]

Result:
case intro.intro.cons.intro.inl.intro.refine_1
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
c : α
s : Multiset α
hind :
  ∀ (x y : α),
    x * y ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, IsUnit y ∨ Prime y) → s.prod = x * y → x ∈ closure {r | IsUnit r ∨ Prime r}
x y : α
hxy : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hprod : c * s.prod = x * y
hs : ∀ a ∈ s, IsUnit a ∨ Prime a
ha₁ : IsUnit c
k : α
hk : c * k = 1
⊢ (k ::ₘ c ::ₘ s).prod ∈ closure {r | IsUnit r ∨ Prime r}

Proof state:
case intro.intro.cons.intro.inl.intro.refine_1.refine_1.h
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
c : α
s : Multiset α
hind :
  ∀ (x y : α),
    x * y ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, IsUnit y ∨ Prime y) → s.prod = x * y → x ∈ closure {r | IsUnit r ∨ Prime r}
x y : α
hxy : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hprod : c * s.prod = x * y
hs : ∀ a ∈ s, IsUnit a ∨ Prime a
ha₁ : IsUnit c
k : α
hk : c * k = 1
⊢ IsUnit k

Tactic:
exact isUnit_of_mul_eq_one_right _ _ hk

Result:
no goals

Proof state:
case intro.intro.cons.intro.inr.inl.intro
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
c✝ : α
s : Multiset α
hind :
  ∀ (x y : α),
    x * y ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, IsUnit y ∨ Prime y) → s.prod = x * y → x ∈ closure {r | IsUnit r ∨ Prime r}
x y : α
hxy : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ a ∈ s, IsUnit a ∨ Prime a
ha₂ : Prime c✝
c : α
hprod : c✝ * s.prod = c✝ * (c * y)
hc : x = c✝ * c
⊢ c✝ * c ∈ 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))

Result:
case intro.intro.cons.intro.inr.inl.intro.refine_1
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
c✝ : α
s : Multiset α
hind :
  ∀ (x y : α),
    x * y ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, IsUnit y ∨ Prime y) → s.prod = x * y → x ∈ closure {r | IsUnit r ∨ Prime r}
x y : α
hxy : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hs : ∀ a ∈ s, IsUnit a ∨ Prime a
ha₂ : Prime c✝
c : α
hprod : c✝ * s.prod = c✝ * (c * y)
hc : x = c✝ * c
⊢ {r | IsUnit r ∨ Prime r} c✝

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