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

Tactic:
refine hind x c ?_ hs (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
⊢ x * c ∈ closure {r | IsUnit r ∨ Prime r}

Proof state:
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
x y : α
hxy : x * y ∈ closure {r | IsUnit r ∨ Prime r}
⊢ x ∈ closure {r | IsUnit r ∨ Prime r}

Tactic:
obtain ⟨m, hm, hprod⟩ := exists_multiset_of_mem_closure hxy

Result:
case intro.intro
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
x y : α
hxy : x * y ∈ closure {r | IsUnit r ∨ Prime r}
m : Multiset α
hm : ∀ y ∈ m, y ∈ {r | IsUnit r ∨ Prime r}
hprod : m.prod = x * y
⊢ 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
⊢ (k ::ₘ c ::ₘ s).prod ∈ closure {r | IsUnit r ∨ Prime r}

Tactic:
refine multiset_prod_mem _ _ (Multiset.forall_mem_cons.2 ⟨subset_closure (Set.mem_def.2 ?_),
  Multiset.forall_mem_cons.2 ⟨subset_closure (Set.mem_def.2 ?_), (fun t ht =>
  subset_closure (hs t ht))⟩⟩)

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

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

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

Tactic:
simp only [Set.mem_setOf_eq] at hind

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, 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}

Proof state:
case intro.intro.cons.intro.inr.inl.intro.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}
hs : ∀ a ∈ s, IsUnit a ∨ Prime a
ha₂ : Prime c✝
c : α
hprod : c✝ * s.prod = c✝ * (c * y)
hc : x = c✝ * c
⊢ Prime c✝

Tactic:
exact ha₂

Result:
no goals

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

Tactic:
right

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

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

Tactic:
rw [hc, mul_assoc] at hprod

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

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

Tactic:
exact ha₁

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

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

Result:
no goals