-- 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.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 * c ∈ closure {r | IsUnit r ∨ Prime r}

Tactic:
rw [← mul_left_cancel₀ ha₂.ne_zero 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
⊢ s.prod ∈ closure {r | IsUnit r ∨ Prime r}

Proof state:
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}

Tactic:
rcases ha₂.dvd_mul.1 (Dvd.intro _ hprod) with ⟨c, hc⟩ | ⟨c, 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
⊢ x ∈ closure {r | IsUnit r ∨ Prime r}

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}

Proof state:
case intro.intro.cons.intro.inl.intro.refine_1.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
⊢ {r | IsUnit r ∨ Prime r} k

Tactic:
left

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

Proof state:
case intro.intro.cons.intro.inl.intro.refine_1.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
⊢ {r | IsUnit r ∨ Prime r} c

Tactic:
left

Result:
case intro.intro.cons.intro.inl.intro.refine_1.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
⊢ IsUnit c

Proof state:
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
⊢ c * s.prod = x * y ∨ k = 0

Tactic:
left

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

Proof state:
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)

Tactic:
rw [← mul_one s.prod, ← hk, ← mul_assoc, ← mul_assoc, mul_eq_mul_right_iff, mul_comm]

Result:
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
⊢ c * s.prod = x * y ∨ k = 0

Proof state:
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}

Tactic:
rcases ha₁.exists_right_inv with ⟨k, hk⟩

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