-- 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.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}
hprod : c * s.prod = x * y
hs : ∀ a ∈ s, IsUnit a ∨ Prime a
ha₁ : IsUnit c
k : α
hk : c * k = 1
⊢ x ∈ closure {r | IsUnit r ∨ Prime r}

Tactic:
refine hind x (y*k) ?_ hs ?_

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
⊢ x * (y * k) ∈ closure {r | IsUnit r ∨ Prime r}

case intro.intro.cons.intro.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}
hprod : c * s.prod = x * y
hs : ∀ a ∈ s, IsUnit a ∨ Prime a
ha₁ : IsUnit c
k : α
hk : c * k = 1
⊢ s.prod = x * (y * k)

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
⊢ x ∈ {r | IsUnit r ∨ Prime r}

Tactic:
simp only [Set.mem_setOf]

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 : Multiset.prod 0 = x * y
⊢ IsUnit x ∨ Prime x

Proof state:
case intro.intro.empty
α : 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
⊢ x ∈ closure {r | IsUnit r ∨ Prime r}

Tactic:
apply subset_closure

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 : Multiset.prod 0 = x * y
⊢ x ∈ {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, 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}
hm : (IsUnit c ∨ Prime c) ∧ ∀ a ∈ s, IsUnit a ∨ Prime a
hprod : c * s.prod = x * y
⊢ x ∈ closure {r | IsUnit r ∨ Prime r}

Tactic:
obtain ⟨ha₁ | ha₂, hs⟩ := hm

Result:
case intro.intro.cons.intro.inl
α : 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
⊢ x ∈ closure {r | IsUnit r ∨ Prime r}

case intro.intro.cons.intro.inr
α : 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
⊢ 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
⊢ c * y ∈ closure {r | IsUnit r ∨ Prime r}

Tactic:
rw [← mul_left_cancel₀ ha₂.ne_zero hprod]

Result:
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}

Proof state:
case intro.intro.cons.intro.inl.intro.refine_2.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
⊢ c * s.prod = x * y

Tactic:
exact hprod

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}
hprod : c✝ * s.prod = x * y
hs : ∀ a ∈ s, IsUnit a ∨ Prime a
ha₂ : Prime c✝
c : α
hc : x = c✝ * c
⊢ x ∈ closure {r | IsUnit r ∨ Prime r}

Tactic:
rw [hc]

Result:
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}
hprod : c✝ * s.prod = x * y
hs : ∀ a ∈ s, IsUnit a ∨ Prime a
ha₂ : Prime c✝
c : α
hc : x = c✝ * c
⊢ c✝ * c ∈ 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 : 1 = x * y
⊢ IsUnit x ∨ Prime x

Tactic:
left

Result:
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