awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.BigOperators.Associated
Goal:
M₀ : Type u_3
inst : CommMonoidWithZero M₀
inst_1 : IsCancelMulZero M₀
c : M₀
s : Multiset M₀
hind :
  ∀ (x y : M₀) (hxy : Membership.mem (γ := Submonoid M₀) (closure {r : M₀ | IsUnit r ∨ Prime r}) (x * y))
    (hm : ∀ y ∈ s, IsUnit y ∨ Prime y) (hprod : s.prod = x * y),
    Membership.mem (γ := Submonoid M₀) (closure {r : M₀ | IsUnit r ∨ Prime r}) x
x y : M₀
hxy : Membership.mem (γ := Submonoid M₀) (closure {r : M₀ | IsUnit r ∨ Prime r}) (x * y)
hprod : c * s.prod = x * y
hs : ∀ a ∈ s, IsUnit a ∨ Prime a
ha₂ : Prime c
cons : ∀ (c_1 : M₀) (hc : x = c * c_1), Membership.mem (γ := Submonoid M₀) (closure {r : M₀ | IsUnit r ∨ Prime r}) x
cons₁ : ∀ (c_1 : M₀) (hc : y = c * c_1), Membership.mem (γ := Submonoid M₀) (closure {r : M₀ | IsUnit r ∨ Prime r}) x
⊢ Membership.mem (γ := Submonoid M₀) (closure {r : M₀ | IsUnit r ∨ Prime r}) x

Tactic:
rcases ha₂.dvd_mul.1 (Dvd.intro _ hprod) with ⟨c, hc⟩ | ⟨c, hc⟩

Premises used: Dvd.intro, Prime.dvd_mul, Iff.mp
-- Module: Mathlib.Algebra.BigOperators.Associated
Goal:
M₀ : Type u_3
inst : CommMonoidWithZero M₀
inst_1 : IsCancelMulZero M₀
c_1 : M₀
s : Multiset M₀
hind :
  ∀ (x y : M₀) (hxy : Membership.mem (γ := Submonoid M₀) (closure {r : M₀ | IsUnit r ∨ Prime r}) (x * y))
    (hm : ∀ y ∈ s, IsUnit y ∨ Prime y) (hprod : s.prod = x * y),
    Membership.mem (γ := Submonoid M₀) (closure {r : M₀ | IsUnit r ∨ Prime r}) x
x y : M₀
hxy : Membership.mem (γ := Submonoid M₀) (closure {r : M₀ | IsUnit r ∨ Prime r}) (x * y)
hprod : c_1 * s.prod = x * y
hs : ∀ a ∈ s, IsUnit a ∨ Prime a
ha₂ : Prime c_1
c : M₀
hc : x = c_1 * c
cons : Membership.mem (γ := Submonoid M₀) (closure {r : M₀ | IsUnit r ∨ Prime r}) (c_1 * c)
⊢ Membership.mem (γ := Submonoid M₀) (closure {r : M₀ | IsUnit r ∨ Prime r}) x

Tactic:
rw [hc]
-- Module: Mathlib.Algebra.BigOperators.Associated
Goal:
M₀ : Type u_3
inst : CommMonoidWithZero M₀
inst_1 : IsCancelMulZero M₀
c_1 : M₀
s : Multiset M₀
hind :
  ∀ (x y : M₀) (hxy : Membership.mem (γ := Submonoid M₀) (closure {r : M₀ | IsUnit r ∨ Prime r}) (x * y))
    (hm : ∀ y ∈ s, IsUnit y ∨ Prime y) (hprod : s.prod = x * y),
    Membership.mem (γ := Submonoid M₀) (closure {r : M₀ | IsUnit r ∨ Prime r}) x
x y : M₀
hxy : Membership.mem (γ := Submonoid M₀) (closure {r : M₀ | IsUnit r ∨ Prime r}) (x * y)
hprod : c_1 * s.prod = x * y
hs : ∀ a ∈ s, IsUnit a ∨ Prime a
ha₂ : Prime c_1
c : M₀
hc : x = c_1 * c
⊢ c_1 * s.prod = c_1 * (c * y)

Tactic:
rw [hc, mul_assoc] at hprod

Premises used: mul_assoc
-- Module: Mathlib.Algebra.BigOperators.Associated
Goal:
M₀ : Type u_3
inst : CommMonoidWithZero M₀
inst_1 : IsCancelMulZero M₀
c_1 : M₀
s : Multiset M₀
hind :
  ∀ (x y : M₀) (hxy : Membership.mem (γ := Submonoid M₀) (closure {r : M₀ | IsUnit r ∨ Prime r}) (x * y))
    (hm : ∀ y ∈ s, IsUnit y ∨ Prime y) (hprod : s.prod = x * y),
    Membership.mem (γ := Submonoid M₀) (closure {r : M₀ | IsUnit r ∨ Prime r}) x
x y : M₀
hxy : Membership.mem (γ := Submonoid M₀) (closure {r : M₀ | IsUnit r ∨ Prime r}) (x * y)
hprod : c_1 * s.prod = x * y
hs : ∀ a ∈ s, IsUnit a ∨ Prime a
ha₂ : Prime c_1
c : M₀
hc : x = c_1 * c
hprod₁ : c_1 * s.prod = c_1 * (c * y)
⊢ x = c_1 * c

Tactic:
rw [hc, mul_assoc] at hprod

Premises used: mul_assoc
-- Module: Mathlib.Algebra.BigOperators.Associated
Goal:
M₀ : Type u_3
inst : CommMonoidWithZero M₀
inst_1 : IsCancelMulZero M₀
c_1 : M₀
s : Multiset M₀
hind :
  ∀ (x y : M₀) (hxy : Membership.mem (γ := Submonoid M₀) (closure {r : M₀ | IsUnit r ∨ Prime r}) (x * y))
    (hm : ∀ y ∈ s, IsUnit y ∨ Prime y) (hprod : s.prod = x * y),
    Membership.mem (γ := Submonoid M₀) (closure {r : M₀ | IsUnit r ∨ Prime r}) x
x y : M₀
hxy : Membership.mem (γ := Submonoid M₀) (closure {r : M₀ | IsUnit r ∨ Prime r}) (x * y)
hs : ∀ a ∈ s, IsUnit a ∨ Prime a
ha₂ : Prime c_1
c : M₀
hprod : c_1 * s.prod = c_1 * (c * y)
hc : x = c_1 * c
⊢ Membership.mem (γ := Submonoid M₀) (closure {r : M₀ | IsUnit r ∨ Prime r}) (c_1 * c)

Tactic:
Submonoid.mul_mem _ (subset_closure ?_)
          (hind _ _ ?_ hs (mul_left_cancel₀ ha₂.ne_zero hprod))

Premises used: Submonoid.mul_mem, Set.Mem, mul_left_cancel₀, Prime.ne_zero, Submonoid.subset_closure
-- Module: Mathlib.Algebra.BigOperators.Associated
Goal:
M₀ : Type u_3
inst : CommMonoidWithZero M₀
inst_1 : IsCancelMulZero M₀
c_1 : M₀
s : Multiset M₀
hind :
  ∀ (x y : M₀) (hxy : Membership.mem (γ := Submonoid M₀) (closure {r : M₀ | IsUnit r ∨ Prime r}) (x * y))
    (hm : ∀ y ∈ s, IsUnit y ∨ Prime y) (hprod : s.prod = x * y),
    Membership.mem (γ := Submonoid M₀) (closure {r : M₀ | IsUnit r ∨ Prime r}) x
x y : M₀
hxy : Membership.mem (γ := Submonoid M₀) (closure {r : M₀ | IsUnit r ∨ Prime r}) (x * y)
hs : ∀ a ∈ s, IsUnit a ∨ Prime a
ha₂ : Prime c_1
c : M₀
hprod : c_1 * s.prod = c_1 * (c * y)
hc : x = c_1 * c
cons : Membership.mem (γ := Set M₀) {r : M₀ | IsUnit r ∨ Prime r} c_1
cons₁ : Membership.mem (γ := Submonoid M₀) (closure {r : M₀ | IsUnit r ∨ Prime r}) (c * y)
⊢ Membership.mem (γ := Submonoid M₀) (closure {r : M₀ | IsUnit r ∨ Prime r}) (c_1 * c)

Tactic:
refine Submonoid.mul_mem _ (subset_closure ?_)
          (hind _ _ ?_ hs (mul_left_cancel₀ ha₂.ne_zero hprod))

Premises used: Submonoid.mul_mem, mul_left_cancel₀, Prime.ne_zero, Submonoid.subset_closure
-- Module: Mathlib.Algebra.BigOperators.Associated
Goal:
M₀ : Type u_3
inst : CommMonoidWithZero M₀
inst_1 : IsCancelMulZero M₀
c_1 : M₀
s : Multiset M₀
hind :
  ∀ (x y : M₀) (hxy : Membership.mem (γ := Submonoid M₀) (closure {r : M₀ | IsUnit r ∨ Prime r}) (x * y))
    (hm : ∀ y ∈ s, IsUnit y ∨ Prime y) (hprod : s.prod = x * y),
    Membership.mem (γ := Submonoid M₀) (closure {r : M₀ | IsUnit r ∨ Prime r}) x
x y : M₀
hxy : Membership.mem (γ := Submonoid M₀) (closure {r : M₀ | IsUnit r ∨ Prime r}) (x * y)
hs : ∀ a ∈ s, IsUnit a ∨ Prime a
ha₂ : Prime c_1
c : M₀
hprod : c_1 * s.prod = c_1 * (c * y)
hc : x = c_1 * c
cons : Prime c_1
⊢ Membership.mem (γ := Set M₀) {r : M₀ | IsUnit r ∨ Prime r} c_1

Tactic:
right
-- Module: Mathlib.Algebra.BigOperators.Associated
Goal:
M₀ : Type u_3
inst : CommMonoidWithZero M₀
inst_1 : IsCancelMulZero M₀
c_1 : M₀
s : Multiset M₀
hind :
  ∀ (x y : M₀) (hxy : Membership.mem (γ := Submonoid M₀) (closure {r : M₀ | IsUnit r ∨ Prime r}) (x * y))
    (hm : ∀ y ∈ s, IsUnit y ∨ Prime y) (hprod : s.prod = x * y),
    Membership.mem (γ := Submonoid M₀) (closure {r : M₀ | IsUnit r ∨ Prime r}) x
x y : M₀
hxy : Membership.mem (γ := Submonoid M₀) (closure {r : M₀ | IsUnit r ∨ Prime r}) (x * y)
hs : ∀ a ∈ s, IsUnit a ∨ Prime a
ha₂ : Prime c_1
c : M₀
hprod : c_1 * s.prod = c_1 * (c * y)
hc : x = c_1 * c
⊢ Prime c_1

Tactic:
ha₂
-- Module: Mathlib.Algebra.BigOperators.Associated
Goal:
M₀ : Type u_3
inst : CommMonoidWithZero M₀
inst_1 : IsCancelMulZero M₀
c_1 : M₀
s : Multiset M₀
hind :
  ∀ (x y : M₀) (hxy : Membership.mem (γ := Submonoid M₀) (closure {r : M₀ | IsUnit r ∨ Prime r}) (x * y))
    (hm : ∀ y ∈ s, IsUnit y ∨ Prime y) (hprod : s.prod = x * y),
    Membership.mem (γ := Submonoid M₀) (closure {r : M₀ | IsUnit r ∨ Prime r}) x
x y : M₀
hxy : Membership.mem (γ := Submonoid M₀) (closure {r : M₀ | IsUnit r ∨ Prime r}) (x * y)
hs : ∀ a ∈ s, IsUnit a ∨ Prime a
ha₂ : Prime c_1
c : M₀
hprod : c_1 * s.prod = c_1 * (c * y)
hc : x = c_1 * c
⊢ Prime c_1

Tactic:
exact ha₂
-- Module: Mathlib.Algebra.BigOperators.Associated
Goal:
M₀ : Type u_3
inst : CommMonoidWithZero M₀
inst_1 : IsCancelMulZero M₀
c_1 : M₀
s : Multiset M₀
hind :
  ∀ (x y : M₀) (hxy : Membership.mem (γ := Submonoid M₀) (closure {r : M₀ | IsUnit r ∨ Prime r}) (x * y))
    (hm : ∀ y ∈ s, IsUnit y ∨ Prime y) (hprod : s.prod = x * y),
    Membership.mem (γ := Submonoid M₀) (closure {r : M₀ | IsUnit r ∨ Prime r}) x
x y : M₀
hxy : Membership.mem (γ := Submonoid M₀) (closure {r : M₀ | IsUnit r ∨ Prime r}) (x * y)
hs : ∀ a ∈ s, IsUnit a ∨ Prime a
ha₂ : Prime c_1
c : M₀
hprod : c_1 * s.prod = c_1 * (c * y)
hc : x = c_1 * c
cons : Membership.mem (γ := Submonoid M₀) (closure {r : M₀ | IsUnit r ∨ Prime r}) s.prod
⊢ Membership.mem (γ := Submonoid M₀) (closure {r : M₀ | IsUnit r ∨ Prime r}) (c * y)

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

Premises used: mul_left_cancel₀, Prime.ne_zero
-- Module: Mathlib.Algebra.BigOperators.Associated
Goal:
M₀ : Type u_3
inst : CommMonoidWithZero M₀
inst_1 : IsCancelMulZero M₀
c_1 : M₀
s : Multiset M₀
hind :
  ∀ (x y : M₀) (hxy : Membership.mem (γ := Submonoid M₀) (closure {r : M₀ | IsUnit r ∨ Prime r}) (x * y))
    (hm : ∀ y ∈ s, IsUnit y ∨ Prime y) (hprod : s.prod = x * y),
    Membership.mem (γ := Submonoid M₀) (closure {r : M₀ | IsUnit r ∨ Prime r}) x
x y : M₀
hxy : Membership.mem (γ := Submonoid M₀) (closure {r : M₀ | IsUnit r ∨ Prime r}) (x * y)
hs : ∀ a ∈ s, IsUnit a ∨ Prime a
ha₂ : Prime c_1
c : M₀
hprod : c_1 * s.prod = c_1 * (c * y)
hc : x = c_1 * c
⊢ Membership.mem (γ := Submonoid M₀) (closure {r : M₀ | IsUnit r ∨ Prime r}) s.prod

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

Premises used: Set.Mem, Submonoid.multiset_prod_mem, Submonoid.subset_closure
-- Module: Mathlib.Algebra.BigOperators.Associated
Goal:
M₀ : Type u_3
inst : CommMonoidWithZero M₀
inst_1 : IsCancelMulZero M₀
c_1 : M₀
s : Multiset M₀
hind :
  ∀ (x y : M₀) (hxy : Membership.mem (γ := Submonoid M₀) (closure {r : M₀ | IsUnit r ∨ Prime r}) (x * y))
    (hm : ∀ y ∈ s, IsUnit y ∨ Prime y) (hprod : s.prod = x * y),
    Membership.mem (γ := Submonoid M₀) (closure {r : M₀ | IsUnit r ∨ Prime r}) x
x y : M₀
hxy : Membership.mem (γ := Submonoid M₀) (closure {r : M₀ | IsUnit r ∨ Prime r}) (x * y)
hs : ∀ a ∈ s, IsUnit a ∨ Prime a
ha₂ : Prime c_1
c : M₀
hprod : c_1 * s.prod = c_1 * (c * y)
hc : x = c_1 * c
⊢ Membership.mem (γ := Submonoid M₀) (closure {r : M₀ | IsUnit r ∨ Prime r}) s.prod

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

Premises used: Submonoid.multiset_prod_mem, Submonoid.subset_closure
-- Module: Mathlib.Algebra.BigOperators.Associated
Goal:
M₀ : Type u_3
inst : CommMonoidWithZero M₀
inst_1 : IsCancelMulZero M₀
c_1 : M₀
s : Multiset M₀
hind :
  ∀ (x y : M₀) (hxy : Membership.mem (γ := Submonoid M₀) (closure {r : M₀ | IsUnit r ∨ Prime r}) (x * y))
    (hm : ∀ y ∈ s, IsUnit y ∨ Prime y) (hprod : s.prod = x * y),
    Membership.mem (γ := Submonoid M₀) (closure {r : M₀ | IsUnit r ∨ Prime r}) x
x y : M₀
hxy : Membership.mem (γ := Submonoid M₀) (closure {r : M₀ | IsUnit r ∨ Prime r}) (x * y)
hprod : c_1 * s.prod = x * y
hs : ∀ a ∈ s, IsUnit a ∨ Prime a
ha₂ : Prime c_1
c : M₀
hc : y = c_1 * c
⊢ c_1 * s.prod = c_1 * (x * c)

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

Premises used: mul_assoc, mul_comm
-- Module: Mathlib.Algebra.BigOperators.Associated
Goal:
M₀ : Type u_3
inst : CommMonoidWithZero M₀
inst_1 : IsCancelMulZero M₀
c_1 : M₀
s : Multiset M₀
hind :
  ∀ (x y : M₀) (hxy : Membership.mem (γ := Submonoid M₀) (closure {r : M₀ | IsUnit r ∨ Prime r}) (x * y))
    (hm : ∀ y ∈ s, IsUnit y ∨ Prime y) (hprod : s.prod = x * y),
    Membership.mem (γ := Submonoid M₀) (closure {r : M₀ | IsUnit r ∨ Prime r}) x
x y : M₀
hxy : Membership.mem (γ := Submonoid M₀) (closure {r : M₀ | IsUnit r ∨ Prime r}) (x * y)
hprod : c_1 * s.prod = x * y
hs : ∀ a ∈ s, IsUnit a ∨ Prime a
ha₂ : Prime c_1
c : M₀
hc : y = c_1 * c
hprod₁ : c_1 * s.prod = c_1 * (x * c)
⊢ y = c_1 * c

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

Premises used: mul_assoc, mul_comm
-- Module: Mathlib.Algebra.BigOperators.Associated
Goal:
M₀ : Type u_3
inst : CommMonoidWithZero M₀
inst_1 : IsCancelMulZero M₀
c_1 : M₀
s : Multiset M₀
hind :
  ∀ (x y : M₀) (hxy : Membership.mem (γ := Submonoid M₀) (closure {r : M₀ | IsUnit r ∨ Prime r}) (x * y))
    (hm : ∀ y ∈ s, IsUnit y ∨ Prime y) (hprod : s.prod = x * y),
    Membership.mem (γ := Submonoid M₀) (closure {r : M₀ | IsUnit r ∨ Prime r}) x
x y : M₀
hxy : Membership.mem (γ := Submonoid M₀) (closure {r : M₀ | IsUnit r ∨ Prime r}) (x * y)
hs : ∀ a ∈ s, IsUnit a ∨ Prime a
ha₂ : Prime c_1
c : M₀
hprod : c_1 * s.prod = c_1 * (x * c)
hc : y = c_1 * c
⊢ Membership.mem (γ := Submonoid M₀) (closure {r : M₀ | IsUnit r ∨ Prime r}) x

Tactic:
hind x c ?_ hs (mul_left_cancel₀ ha₂.ne_zero hprod)

Premises used: mul_left_cancel₀, Prime.ne_zero
-- Module: Mathlib.Algebra.BigOperators.Associated
Goal:
M₀ : Type u_3
inst : CommMonoidWithZero M₀
inst_1 : IsCancelMulZero M₀
c_1 : M₀
s : Multiset M₀
hind :
  ∀ (x y : M₀) (hxy : Membership.mem (γ := Submonoid M₀) (closure {r : M₀ | IsUnit r ∨ Prime r}) (x * y))
    (hm : ∀ y ∈ s, IsUnit y ∨ Prime y) (hprod : s.prod = x * y),
    Membership.mem (γ := Submonoid M₀) (closure {r : M₀ | IsUnit r ∨ Prime r}) x
x y : M₀
hxy : Membership.mem (γ := Submonoid M₀) (closure {r : M₀ | IsUnit r ∨ Prime r}) (x * y)
hs : ∀ a ∈ s, IsUnit a ∨ Prime a
ha₂ : Prime c_1
c : M₀
hprod : c_1 * s.prod = c_1 * (x * c)
hc : y = c_1 * c
cons : Membership.mem (γ := Submonoid M₀) (closure {r : M₀ | IsUnit r ∨ Prime r}) (x * c)
⊢ Membership.mem (γ := Submonoid M₀) (closure {r : M₀ | IsUnit r ∨ Prime r}) x

Tactic:
refine hind x c ?_ hs (mul_left_cancel₀ ha₂.ne_zero hprod)

Premises used: mul_left_cancel₀, Prime.ne_zero
-- Module: Mathlib.Algebra.BigOperators.Associated
Goal:
M₀ : Type u_3
inst : CommMonoidWithZero M₀
inst_1 : IsCancelMulZero M₀
c_1 : M₀
s : Multiset M₀
hind :
  ∀ (x y : M₀) (hxy : Membership.mem (γ := Submonoid M₀) (closure {r : M₀ | IsUnit r ∨ Prime r}) (x * y))
    (hm : ∀ y ∈ s, IsUnit y ∨ Prime y) (hprod : s.prod = x * y),
    Membership.mem (γ := Submonoid M₀) (closure {r : M₀ | IsUnit r ∨ Prime r}) x
x y : M₀
hxy : Membership.mem (γ := Submonoid M₀) (closure {r : M₀ | IsUnit r ∨ Prime r}) (x * y)
hs : ∀ a ∈ s, IsUnit a ∨ Prime a
ha₂ : Prime c_1
c : M₀
hprod : c_1 * s.prod = c_1 * (x * c)
hc : y = c_1 * c
cons : Membership.mem (γ := Submonoid M₀) (closure {r : M₀ | IsUnit r ∨ Prime r}) s.prod
⊢ Membership.mem (γ := Submonoid M₀) (closure {r : M₀ | IsUnit r ∨ Prime r}) (x * c)

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

Premises used: mul_left_cancel₀, Prime.ne_zero
-- Module: Mathlib.Algebra.BigOperators.Associated
Goal:
M₀ : Type u_3
inst : CommMonoidWithZero M₀
inst_1 : IsCancelMulZero M₀
c_1 : M₀
s : Multiset M₀
hind :
  ∀ (x y : M₀) (hxy : Membership.mem (γ := Submonoid M₀) (closure {r : M₀ | IsUnit r ∨ Prime r}) (x * y))
    (hm : ∀ y ∈ s, IsUnit y ∨ Prime y) (hprod : s.prod = x * y),
    Membership.mem (γ := Submonoid M₀) (closure {r : M₀ | IsUnit r ∨ Prime r}) x
x y : M₀
hxy : Membership.mem (γ := Submonoid M₀) (closure {r : M₀ | IsUnit r ∨ Prime r}) (x * y)
hs : ∀ a ∈ s, IsUnit a ∨ Prime a
ha₂ : Prime c_1
c : M₀
hprod : c_1 * s.prod = c_1 * (x * c)
hc : y = c_1 * c
⊢ Membership.mem (γ := Submonoid M₀) (closure {r : M₀ | IsUnit r ∨ Prime r}) s.prod

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

Premises used: Set.Mem, Submonoid.multiset_prod_mem, Submonoid.subset_closure
-- Module: Mathlib.Algebra.BigOperators.Associated
Goal:
M₀ : Type u_3
inst : CommMonoidWithZero M₀
inst_1 : IsCancelMulZero M₀
c_1 : M₀
s : Multiset M₀
hind :
  ∀ (x y : M₀) (hxy : Membership.mem (γ := Submonoid M₀) (closure {r : M₀ | IsUnit r ∨ Prime r}) (x * y))
    (hm : ∀ y ∈ s, IsUnit y ∨ Prime y) (hprod : s.prod = x * y),
    Membership.mem (γ := Submonoid M₀) (closure {r : M₀ | IsUnit r ∨ Prime r}) x
x y : M₀
hxy : Membership.mem (γ := Submonoid M₀) (closure {r : M₀ | IsUnit r ∨ Prime r}) (x * y)
hs : ∀ a ∈ s, IsUnit a ∨ Prime a
ha₂ : Prime c_1
c : M₀
hprod : c_1 * s.prod = c_1 * (x * c)
hc : y = c_1 * c
⊢ Membership.mem (γ := Submonoid M₀) (closure {r : M₀ | IsUnit r ∨ Prime r}) s.prod

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

Premises used: Submonoid.multiset_prod_mem, Submonoid.subset_closure
-- Module: Mathlib.Algebra.BigOperators.Associated
Goal:
M₀ : Type u_3
inst : CommMonoidWithZero M₀
inst_1 : IsCancelMulZero M₀
inst_2 : (a : M₀) → DecidablePred (Associated a)
n : M₀
h : ∀ (a : M₀), Membership.mem (γ := Multiset M₀) 0 a → Prime a
div : ∀ (a : M₀), Membership.mem (γ := Multiset M₀) 0 a → a ∣ n
uniq : ∀ (a : M₀), countP (Associated a) 0 ≤ 1
⊢ prod 0 ∣ n

Tactic:
simp only [Multiset.prod_zero, one_dvd]

Premises used: Multiset.prod_zero, one_dvd
-- Module: Mathlib.Algebra.BigOperators.Associated
Goal:
M₀ : Type u_3
inst : CommMonoidWithZero M₀
inst_1 : IsCancelMulZero M₀
inst_2 : (a : M₀) → DecidablePred (Associated a)
a : M₀
s : Multiset M₀
induct :
  ∀ (n : M₀) (h : ∀ a ∈ s, Prime a) (div : ∀ a ∈ s, a ∣ n) (uniq : ∀ (a : M₀), countP (Associated a) s ≤ 1), s.prod ∣ n
n : M₀
h : ∀ a_1 ∈ a ::ₘ s, Prime a_1
div : ∀ a_1 ∈ a ::ₘ s, a_1 ∣ n
uniq : ∀ (a_1 : M₀), countP (Associated a_1) (a ::ₘ s) ≤ 1
cons : a * s.prod ∣ n
⊢ (a ::ₘ s).prod ∣ n

Tactic:
rw [Multiset.prod_cons]

Premises used: Multiset.prod_cons
-- Module: Mathlib.Algebra.BigOperators.Associated
Goal:
M₀ : Type u_3
inst : CommMonoidWithZero M₀
inst_1 : IsCancelMulZero M₀
inst_2 : (a : M₀) → DecidablePred (Associated a)
a : M₀
s : Multiset M₀
induct :
  ∀ (n : M₀) (h : ∀ a ∈ s, Prime a) (div : ∀ a ∈ s, a ∣ n) (uniq : ∀ (a : M₀), countP (Associated a) s ≤ 1), s.prod ∣ n
n : M₀
h : ∀ a_1 ∈ a ::ₘ s, Prime a_1
div : ∀ a_1 ∈ a ::ₘ s, a_1 ∣ n
uniq : ∀ (a_1 : M₀), countP (Associated a_1) (a ::ₘ s) ≤ 1
⊢ a ∣ n

Tactic:
div a (Multiset.mem_cons_self a s)

Premises used: Multiset.mem_cons_self
-- Module: Mathlib.Algebra.BigOperators.Associated
Goal:
M₀ : Type u_3
inst : CommMonoidWithZero M₀
inst_1 : IsCancelMulZero M₀
inst_2 : (a : M₀) → DecidablePred (Associated a)
a : M₀
s : Multiset M₀
induct :
  ∀ (n : M₀) (h : ∀ a ∈ s, Prime a) (div : ∀ a ∈ s, a ∣ n) (uniq : ∀ (a : M₀), countP (Associated a) s ≤ 1), s.prod ∣ n
n : M₀
h : ∀ a_1 ∈ a ::ₘ s, Prime a_1
div : ∀ a_1 ∈ a ::ₘ s, a_1 ∣ n
uniq : ∀ (a_1 : M₀), countP (Associated a_1) (a ::ₘ s) ≤ 1
cons : ∀ (k : M₀) (div : ∀ a_1 ∈ a ::ₘ s, a_1 ∣ a * k), a * s.prod ∣ a * k
⊢ a * s.prod ∣ n

Tactic:
obtain ⟨k, rfl⟩ : a ∣ n := div a (Multiset.mem_cons_self a s)

Premises used: Multiset.mem_cons_self, rfl
-- Module: Mathlib.Algebra.BigOperators.Associated
Goal:
M₀ : Type u_3
inst : CommMonoidWithZero M₀
inst_1 : IsCancelMulZero M₀
inst_2 : (a : M₀) → DecidablePred (Associated a)
a : M₀
s : Multiset M₀
induct :
  ∀ (n : M₀) (h : ∀ a ∈ s, Prime a) (div : ∀ a ∈ s, a ∣ n) (uniq : ∀ (a : M₀), countP (Associated a) s ≤ 1), s.prod ∣ n
h : ∀ a_1 ∈ a ::ₘ s, Prime a_1
uniq : ∀ (a_1 : M₀), countP (Associated a_1) (a ::ₘ s) ≤ 1
k : M₀
div : ∀ a_1 ∈ a ::ₘ s, a_1 ∣ a * k
cons : s.prod ∣ k
⊢ a * s.prod ∣ a * k

Tactic:
gcongr
-- Module: Mathlib.Algebra.BigOperators.Associated
Goal:
M₀ : Type u_3
inst : CommMonoidWithZero M₀
inst_1 : IsCancelMulZero M₀
inst_2 : (a : M₀) → DecidablePred (Associated a)
a : M₀
s : Multiset M₀
induct :
  ∀ (n : M₀) (h : ∀ a ∈ s, Prime a) (div : ∀ a ∈ s, a ∣ n) (uniq : ∀ (a : M₀), countP (Associated a) s ≤ 1), s.prod ∣ n
h : ∀ a_1 ∈ a ::ₘ s, Prime a_1
uniq : ∀ (a_1 : M₀), countP (Associated a_1) (a ::ₘ s) ≤ 1
k : M₀
div : ∀ a_1 ∈ a ::ₘ s, a_1 ∣ a * k
⊢ s.prod ∣ k

Tactic:
induct _ (fun a ha => h a (Multiset.mem_cons_of_mem ha)) (fun b b_in_s => ?_)
      fun a => (Multiset.countP_le_of_le _ (Multiset.le_cons_self _ _)).trans (uniq a)

Premises used: Multiset.mem_cons_of_mem, Multiset.countP_le_of_le, Associated, Multiset.le_cons_self, LE.le.trans
-- Module: Mathlib.Algebra.BigOperators.Associated
Goal:
M₀ : Type u_3
inst : CommMonoidWithZero M₀
inst_1 : IsCancelMulZero M₀
inst_2 : (a : M₀) → DecidablePred (Associated a)
a : M₀
s : Multiset M₀
induct :
  ∀ (n : M₀) (h : ∀ a ∈ s, Prime a) (div : ∀ a ∈ s, a ∣ n) (uniq : ∀ (a : M₀), countP (Associated a) s ≤ 1), s.prod ∣ n
h : ∀ a_1 ∈ a ::ₘ s, Prime a_1
uniq : ∀ (a_1 : M₀), countP (Associated a_1) (a ::ₘ s) ≤ 1
k : M₀
div : ∀ a_1 ∈ a ::ₘ s, a_1 ∣ a * k
cons : ∀ (b : M₀) (b_in_s : b ∈ s), b ∣ k
⊢ s.prod ∣ k

Tactic:
refine induct _ (fun a ha => h a (Multiset.mem_cons_of_mem ha)) (fun b b_in_s => ?_)
      fun a => (Multiset.countP_le_of_le _ (Multiset.le_cons_self _ _)).trans (uniq a)

Premises used: Multiset.mem_cons_of_mem, Multiset.countP_le_of_le, Associated, Multiset.le_cons_self, LE.le.trans
-- Module: Mathlib.Algebra.BigOperators.Associated
Goal:
M₀ : Type u_3
inst : CommMonoidWithZero M₀
inst_1 : IsCancelMulZero M₀
inst_2 : (a : M₀) → DecidablePred (Associated a)
a : M₀
s : Multiset M₀
induct :
  ∀ (n : M₀) (h : ∀ a ∈ s, Prime a) (div : ∀ a ∈ s, a ∣ n) (uniq : ∀ (a : M₀), countP (Associated a) s ≤ 1), s.prod ∣ n
h : ∀ a_1 ∈ a ::ₘ s, Prime a_1
uniq : ∀ (a_1 : M₀), countP (Associated a_1) (a ::ₘ s) ≤ 1
k : M₀
div : ∀ a_1 ∈ a ::ₘ s, a_1 ∣ a * k
b : M₀
b_in_s : b ∈ s
⊢ b ∣ a * k

Tactic:
have b_div_n := div b (Multiset.mem_cons_of_mem b_in_s)
-- Module: Mathlib.Algebra.BigOperators.Associated
Goal:
M₀ : Type u_3
inst : CommMonoidWithZero M₀
inst_1 : IsCancelMulZero M₀
inst_2 : (a : M₀) → DecidablePred (Associated a)
a : M₀
s : Multiset M₀
induct :
  ∀ (n : M₀) (h : ∀ a ∈ s, Prime a) (div : ∀ a ∈ s, a ∣ n) (uniq : ∀ (a : M₀), countP (Associated a) s ≤ 1), s.prod ∣ n
h : ∀ a_1 ∈ a ::ₘ s, Prime a_1
uniq : ∀ (a_1 : M₀), countP (Associated a_1) (a ::ₘ s) ≤ 1
k : M₀
div : ∀ a_1 ∈ a ::ₘ s, a_1 ∣ a * k
b : M₀
b_in_s : b ∈ s
b_div_n : b ∣ a * k
⊢ Prime a

Tactic:
have a_prime := h a (Multiset.mem_cons_self a s)
-- Module: Mathlib.Algebra.BigOperators.Associated
Goal:
M₀ : Type u_3
inst : CommMonoidWithZero M₀
inst_1 : IsCancelMulZero M₀
inst_2 : (a : M₀) → DecidablePred (Associated a)
a : M₀
s : Multiset M₀
induct :
  ∀ (n : M₀) (h : ∀ a ∈ s, Prime a) (div : ∀ a ∈ s, a ∣ n) (uniq : ∀ (a : M₀), countP (Associated a) s ≤ 1), s.prod ∣ n
h : ∀ a_1 ∈ a ::ₘ s, Prime a_1
uniq : ∀ (a_1 : M₀), countP (Associated a_1) (a ::ₘ s) ≤ 1
k : M₀
div : ∀ a_1 ∈ a ::ₘ s, a_1 ∣ a * k
b : M₀
b_in_s : b ∈ s
b_div_n : b ∣ a * k
a_prime : Prime a
⊢ Prime b

Tactic:
have b_prime := h b (Multiset.mem_cons_of_mem b_in_s)
-- Module: Mathlib.Algebra.BigOperators.Associated
Goal:
M₀ : Type u_3
inst : CommMonoidWithZero M₀
inst_1 : IsCancelMulZero M₀
inst_2 : (a : M₀) → DecidablePred (Associated a)
a : M₀
s : Multiset M₀
induct :
  ∀ (n : M₀) (h : ∀ a ∈ s, Prime a) (div : ∀ a ∈ s, a ∣ n) (uniq : ∀ (a : M₀), countP (Associated a) s ≤ 1), s.prod ∣ n
h : ∀ a_1 ∈ a ::ₘ s, Prime a_1
uniq : ∀ (a_1 : M₀), countP (Associated a_1) (a ::ₘ s) ≤ 1
k : M₀
div : ∀ a_1 ∈ a ::ₘ s, a_1 ∣ a * k
b : M₀
b_in_s : b ∈ s
b_div_n : b ∣ a * k
a_prime : Prime a
b_prime : Prime b
⊢ b ∣ k

Tactic:
(b_prime.dvd_or_dvd b_div_n).resolve_left fun b_div_a => ?_

Premises used: Prime.dvd_or_dvd, Or.resolve_left
-- Module: Mathlib.Algebra.BigOperators.Associated
Goal:
M₀ : Type u_3
inst : CommMonoidWithZero M₀
inst_1 : IsCancelMulZero M₀
inst_2 : (a : M₀) → DecidablePred (Associated a)
a : M₀
s : Multiset M₀
induct :
  ∀ (n : M₀) (h : ∀ a ∈ s, Prime a) (div : ∀ a ∈ s, a ∣ n) (uniq : ∀ (a : M₀), countP (Associated a) s ≤ 1), s.prod ∣ n
h : ∀ a_1 ∈ a ::ₘ s, Prime a_1
uniq : ∀ (a_1 : M₀), countP (Associated a_1) (a ::ₘ s) ≤ 1
k : M₀
div : ∀ a_1 ∈ a ::ₘ s, a_1 ∣ a * k
b : M₀
b_in_s : b ∈ s
b_div_n : b ∣ a * k
a_prime : Prime a
b_prime : Prime b
cons : ∀ (b_div_a : b ∣ a), False
⊢ b ∣ k

Tactic:
refine (b_prime.dvd_or_dvd b_div_n).resolve_left fun b_div_a => ?_

Premises used: Prime.dvd_or_dvd, Or.resolve_left
-- Module: Mathlib.Algebra.BigOperators.Associated
Goal:
M₀ : Type u_3
inst : CommMonoidWithZero M₀
inst_1 : IsCancelMulZero M₀
inst_2 : (a : M₀) → DecidablePred (Associated a)
a : M₀
s : Multiset M₀
induct :
  ∀ (n : M₀) (h : ∀ a ∈ s, Prime a) (div : ∀ a ∈ s, a ∣ n) (uniq : ∀ (a : M₀), countP (Associated a) s ≤ 1), s.prod ∣ n
h : ∀ a_1 ∈ a ::ₘ s, Prime a_1
uniq : ∀ (a_1 : M₀), countP (Associated a_1) (a ::ₘ s) ≤ 1
k : M₀
div : ∀ a_1 ∈ a ::ₘ s, a_1 ∣ a * k
b : M₀
b_in_s : b ∈ s
b_div_n : b ∣ a * k
a_prime : Prime a
b_prime : Prime b
b_div_a : b ∣ a
⊢ b ~ᵤ a

Tactic:
have assoc := b_prime.associated_of_dvd a_prime b_div_a
-- Module: Mathlib.Algebra.BigOperators.Associated
Goal:
M₀ : Type u_3
inst : CommMonoidWithZero M₀
inst_1 : IsCancelMulZero M₀
inst_2 : (a : M₀) → DecidablePred (Associated a)
a : M₀
s : Multiset M₀
induct :
  ∀ (n : M₀) (h : ∀ a ∈ s, Prime a) (div : ∀ a ∈ s, a ∣ n) (uniq : ∀ (a : M₀), countP (Associated a) s ≤ 1), s.prod ∣ n
h : ∀ a_1 ∈ a ::ₘ s, Prime a_1
uniq : ∀ (a_1 : M₀), countP (Associated a_1) (a ::ₘ s) ≤ 1
k : M₀
div : ∀ a_1 ∈ a ::ₘ s, a_1 ∣ a * k
b : M₀
b_in_s : b ∈ s
b_div_n : b ∣ a * k
a_prime : Prime a
b_prime : Prime b
b_div_a : b ∣ a
assoc : b ~ᵤ a
⊢ countP (Associated a) (a ::ₘ s) ≤ 1

Tactic:
have := uniq a