awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
factors_unique : x * y ~ᵤ (factors x + factors y).prod
⊢ Rel Associated (factors (x * y)) (factors x + factors y)

Tactic:
refine
    factors_unique irreducible_of_factor
      (fun a ha =>
        (mem_add.mp ha).by_cases (irreducible_of_factor _) (irreducible_of_factor _))
      ((factors_prod (mul_ne_zero hx hy)).trans ?_)

Premises used: UniqueFactorizationMonoid.factors_unique, Associated.trans, Multiset.mem_add, UniqueFactorizationMonoid.irreducible_of_factor, Or.by_cases, UniqueFactorizationMonoid.factors_prod, Iff.mp, mul_ne_zero
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
rw : x * y ~ᵤ (factors x).prod * (factors y).prod
⊢ x * y ~ᵤ (factors x + factors y).prod

Tactic:
rw [prod_add]

Premises used: Multiset.prod_add
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
⊢ x * y ~ᵤ (factors x).prod * (factors y).prod

Tactic:
(Associated.mul_mul (factors_prod hx) (factors_prod hy)).symm

Premises used: Associated.symm, UniqueFactorizationMonoid.factors_prod, Associated.mul_mul
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
⊢ x * y ~ᵤ (factors x).prod * (factors y).prod

Tactic:
exact (Associated.mul_mul (factors_prod hx) (factors_prod hy)).symm

Premises used: Associated.symm, UniqueFactorizationMonoid.factors_prod, Associated.mul_mul
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
x : α
n : ℕ
rw : Rel Associated (factors (HPow.hPow (β := ℕ) x 0)) 0
rw₁ : Rel.{u_1, u_1} (α := α) Associated (factors 1) 0
rw₂ : Rel.{u_1, u_1} (α := α) Associated 0 0
rw₃ rw₄ : Eq.{u_1 + 1} (α := Multiset α) 0 0
⊢ Rel Associated (factors (HPow.hPow (β := ℕ) x 0)) (HSMul.hSMul (α := ℕ) 0 (factors x))

Tactic:
rw [zero_nsmul, pow_zero, factors_one, rel_zero_right]

Premises used: UniqueFactorizationMonoid.factors_one, pow_zero, zero_nsmul, Multiset.rel_zero_right
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
x : α
n_1 n : ℕ
pos : ∀ (h0 : x = 0), Rel Associated (factors (x ^ (n + 1))) ((n + 1) • factors x)
neg : ∀ (h0 : ¬x = 0), Rel Associated (factors (x ^ (n + 1))) ((n + 1) • factors x)
⊢ Rel Associated (factors (x ^ (n + 1))) ((n + 1) • factors x)

Tactic:
by_cases h0 : x = 0
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
x : α
n_1 n : ℕ
h0 : x = 0
⊢ Rel Associated (factors (x ^ (n + 1))) ((n + 1) • factors x)

Tactic:
simp [h0, zero_pow n.succ_ne_zero, nsmul_zero]

Premises used: nsmul_zero, Nat.succ_ne_zero, zero_pow
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
x : α
n_1 n : ℕ
h0 : ¬x = 0
neg : Rel Associated (factors (x * x ^ n)) (factors x + n • factors x)
⊢ Rel Associated (factors (x ^ (n + 1))) ((n + 1) • factors x)

Tactic:
rw [pow_succ', succ_nsmul']

Premises used: succ_nsmul', pow_succ'
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
x : α
n_1 n : ℕ
h0 : ¬x = 0
⊢ Rel Associated (factors (x * x ^ n)) (factors x + n • factors x)

Tactic:
Rel.trans _ (factors_mul h0 (pow_ne_zero n h0)) ?_

Premises used: pow_ne_zero, Multiset.Rel.trans, UniqueFactorizationMonoid.factors_mul
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
x : α
n_1 n : ℕ
h0 : ¬x = 0
neg : Rel Associated (factors x + factors (x ^ n)) (factors x + n • factors x)
⊢ Rel Associated (factors (x * x ^ n)) (factors x + n • factors x)

Tactic:
refine Rel.trans _ (factors_mul h0 (pow_ne_zero n h0)) ?_

Premises used: pow_ne_zero, Multiset.Rel.trans, UniqueFactorizationMonoid.factors_mul
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
x : α
n_1 n : ℕ
h0 : ¬x = 0
⊢ Rel Associated (factors x + factors (x ^ n)) (factors x + n • factors x)

Tactic:
Rel.add ?_ <| factors_pow n

Premises used: Multiset.Rel.add
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
x : α
n_1 n : ℕ
h0 : ¬x = 0
neg : Rel Associated (factors x) (factors x)
⊢ Rel Associated (factors x + factors (x ^ n)) (factors x + n • factors x)

Tactic:
refine Rel.add ?_ <| factors_pow n

Premises used: Multiset.Rel.add
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
x : α
n_1 n : ℕ
h0 : ¬x = 0
⊢ Rel Associated (factors x) (factors x)

Tactic:
rel_refl_of_refl_on fun y _ => Associated.refl _

Premises used: Multiset.rel_refl_of_refl_on, Associated.refl
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
x : α
n_1 n : ℕ
h0 : ¬x = 0
⊢ Rel Associated (factors x) (factors x)

Tactic:
exact rel_refl_of_refl_on fun y _ => Associated.refl _

Premises used: Multiset.rel_refl_of_refl_on, Associated.refl
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
x : α
n : ℕ
⊢ Rel Associated (factors (x ^ n)) (n • factors x)

Tactic:
match n with
  | 0 => rw [zero_nsmul, pow_zero, factors_one, rel_zero_right]
  | n + 1 =>
    by_cases h0 : x = 0
    · simp [h0, zero_pow n.succ_ne_zero, nsmul_zero]
    · rw [pow_succ', succ_nsmul']
      refine Rel.trans _ (factors_mul h0 (pow_ne_zero n h0)) ?_
      refine Rel.add ?_ <| factors_pow n
      exact rel_refl_of_refl_on fun y _ => Associated.refl _
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : DecidableEq α
x : α
hx : x ≠ 0
⊢ Eq (α := α) (∏ p ∈ (factors x).toFinset, p ^ count p (factors x))
    (prod (∑ a ∈ (factors x).toFinset, HSMul.hSMul (β := Multiset α) (count a (factors x)) {a}))

Tactic:
simp only [prod_sum, prod_nsmul, prod_singleton]

Premises used: Multiset.prod_sum, Multiset.prod_singleton, Multiset.prod_nsmul
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : DecidableEq α
x : α
hx : x ≠ 0
rw rw₁ : (factors x).prod = (factors x).prod
⊢ prod (∑ a ∈ (factors x).toFinset, HSMul.hSMul (β := Multiset α) (count a (factors x)) {a}) = (factors x).prod

Tactic:
rw [toFinset_sum_count_nsmul_eq (factors x)]

Premises used: UniqueFactorizationMonoid.factors, Multiset.toFinset_sum_count_nsmul_eq
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a b : α
h : a ~ᵤ b
inl : ∀ (h : Associated.{u_1} (M := α) 0 0), Rel.{u_1, u_1} (α := α) Associated (factors 0) (factors 0)
inr : ∀ (ha : ¬a = 0) (hb : ¬b = 0), Rel Associated (factors a) (factors b)
⊢ Rel Associated (factors a) (factors b)

Tactic:
rcases iff_iff_and_or_not_and_not.mp h.eq_zero_iff with (⟨rfl, rfl⟩ | ⟨ha, hb⟩)

Premises used: Associated.eq_zero_iff, iff_iff_and_or_not_and_not, Iff.mp, rfl
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
h : Associated.{u_1} (M := α) 0 0
⊢ Rel.{u_1, u_1} (α := α) Associated (factors 0) (factors 0)

Tactic:
simp
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a b : α
h : a ~ᵤ b
ha : ¬a = 0
hb : ¬b = 0
⊢ Rel Associated (factors a) (factors b)

Tactic:
factors_unique irreducible_of_factor irreducible_of_factor ?_

Premises used: UniqueFactorizationMonoid.factors_unique, UniqueFactorizationMonoid.irreducible_of_factor
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a b : α
h : a ~ᵤ b
ha : ¬a = 0
hb : ¬b = 0
inr : (factors a).prod ~ᵤ (factors b).prod
⊢ Rel Associated (factors a) (factors b)

Tactic:
refine factors_unique irreducible_of_factor irreducible_of_factor ?_

Premises used: UniqueFactorizationMonoid.factors_unique, UniqueFactorizationMonoid.irreducible_of_factor
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a b : α
h : a ~ᵤ b
ha : ¬a = 0
hb : ¬b = 0
⊢ (factors a).prod ~ᵤ (factors b).prod

Tactic:
((factors_prod ha).trans h).trans (factors_prod hb).symm

Premises used: Associated.trans, Associated.symm, UniqueFactorizationMonoid.factors_prod
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a b : α
h : a ~ᵤ b
ha : ¬a = 0
hb : ¬b = 0
⊢ (factors a).prod ~ᵤ (factors b).prod

Tactic:
exact ((factors_prod ha).trans h).trans (factors_prod hb).symm

Premises used: Associated.trans, Associated.symm, UniqueFactorizationMonoid.factors_prod
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
x : α
hx : IsUnit x
⊢ factors x = 0

Tactic:
simpa using factors_rel_of_associated (associated_one_iff_isUnit.mpr hx)

Premises used: Iff.mpr, associated_one_iff_isUnit, UniqueFactorizationMonoid.factors_rel_of_associated
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
x : α
hx : x ≠ 0
h : factors x = 0
contrapose! : ∀ (h : ¬IsUnit x), factors x ≠ 0
⊢ IsUnit x

Tactic:
contrapose! h
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
x : α
hx : x ≠ 0
h : ¬IsUnit x
⊢ factors x ≠ 0

Tactic:
simpa [eq_zero_iff_forall_notMem] using exists_mem_factors hx h

Premises used: UniqueFactorizationMonoid.exists_mem_factors, Multiset.eq_zero_iff_forall_notMem
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
x : α
hx : x ≠ 0
⊢ 0 < factors x ↔ ¬IsUnit x

Tactic:
bot_lt_iff_ne_bot.trans (not_iff_not.mpr (factors_eq_zero hx))

Premises used: not_iff_not, Iff.mpr, bot_lt_iff_ne_bot, Iff.trans, UniqueFactorizationMonoid.factors_eq_zero
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
p q : Multiset (Associates α)
apply :
  ∀ (s : Multiset α),
    (∀ (a : Associates α),
        Membership.mem (γ := Multiset (Associates α)) (map (Quot.mk (⇑(Associated.setoid α) : α → α → Prop)) s) a →
          Irreducible a) →
      (∀ a ∈ q, Irreducible a) →
        prod (map (Quot.mk (⇑(Associated.setoid α) : α → α → Prop)) s) = q.prod →
          map (Quot.mk (⇑(Associated.setoid α) : α → α → Prop)) s = q
⊢ (∀ a ∈ p, Irreducible a) → (∀ a ∈ q, Irreducible a) → p.prod = q.prod → p = q

Tactic:
apply Multiset.induction_on_multiset_quot p

Premises used: Multiset.induction_on_multiset_quot
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
p q : Multiset (Associates α)
apply :
  ∀ (s s_1 : Multiset α),
    (∀ (a : Associates α),
        Membership.mem (γ := Multiset (Associates α)) (map (Quot.mk (⇑(Associated.setoid α) : α → α → Prop)) s_1) a →
          Irreducible a) →
      (∀ (a : Associates α),
          Membership.mem (γ := Multiset (Associates α)) (map (Quot.mk (⇑(Associated.setoid α) : α → α → Prop)) s) a →
            Irreducible a) →
        Eq (α := Associates α) (prod (map (Quot.mk (⇑(Associated.setoid α) : α → α → Prop)) s_1))
            (prod (map (Quot.mk (⇑(Associated.setoid α) : α → α → Prop)) s)) →
          Eq (α := Multiset (Associates α)) (map (Quot.mk (⇑(Associated.setoid α) : α → α → Prop)) s_1)
            (map (Quot.mk (⇑(Associated.setoid α) : α → α → Prop)) s)
⊢ ∀ (s : Multiset α),
    (∀ (a : Associates α),
        Membership.mem (γ := Multiset (Associates α)) (map (Quot.mk (⇑(Associated.setoid α) : α → α → Prop)) s) a →
          Irreducible a) →
      (∀ a ∈ q, Irreducible a) →
        prod (map (Quot.mk (⇑(Associated.setoid α) : α → α → Prop)) s) = q.prod →
          map (Quot.mk (⇑(Associated.setoid α) : α → α → Prop)) s = q

Tactic:
apply Multiset.induction_on_multiset_quot q

Premises used: Multiset.induction_on_multiset_quot
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
p q : Multiset (Associates α)
s t : Multiset α
hs :
  ∀ (a : Associates α),
    Membership.mem (γ := Multiset (Associates α)) (map (Quot.mk (⇑(Associated.setoid α) : α → α → Prop)) t) a →
      Irreducible a
ht :
  ∀ (a : Associates α),
    Membership.mem (γ := Multiset (Associates α)) (map (Quot.mk (⇑(Associated.setoid α) : α → α → Prop)) s) a →
      Irreducible a
eq :
  Eq (α := Associates α) (prod (map (Quot.mk (⇑(Associated.setoid α) : α → α → Prop)) t))
    (prod (map (Quot.mk (⇑(Associated.setoid α) : α → α → Prop)) s))
⊢ Eq (α := Multiset (Associates α)) (map (Quot.mk (⇑(Associated.setoid α) : α → α → Prop)) t)
    (map (Quot.mk (⇑(Associated.setoid α) : α → α → Prop)) s)

Tactic:
Multiset.map_mk_eq_map_mk_of_rel (UniqueFactorizationMonoid.factors_unique ?_ ?_ ?_)

Premises used: Multiset.map_mk_eq_map_mk_of_rel, UniqueFactorizationMonoid.factors_unique, Quotient
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
p q : Multiset (Associates α)
s t : Multiset α
hs :
  ∀ (a : Associates α),
    Membership.mem (γ := Multiset (Associates α)) (map (Quot.mk (⇑(Associated.setoid α) : α → α → Prop)) t) a →
      Irreducible a
ht :
  ∀ (a : Associates α),
    Membership.mem (γ := Multiset (Associates α)) (map (Quot.mk (⇑(Associated.setoid α) : α → α → Prop)) s) a →
      Irreducible a
eq :
  Eq (α := Associates α) (prod (map (Quot.mk (⇑(Associated.setoid α) : α → α → Prop)) t))
    (prod (map (Quot.mk (⇑(Associated.setoid α) : α → α → Prop)) s))
refine_1 : ∀ x ∈ t, Irreducible x
refine_2 : ∀ x ∈ s, Irreducible x
refine_3 : t.prod ~ᵤ s.prod
⊢ Eq (α := Multiset (Associates α)) (map (Quot.mk (⇑(Associated.setoid α) : α → α → Prop)) t)
    (map (Quot.mk (⇑(Associated.setoid α) : α → α → Prop)) s)

Tactic:
refine Multiset.map_mk_eq_map_mk_of_rel (UniqueFactorizationMonoid.factors_unique ?_ ?_ ?_)

Premises used: Multiset.map_mk_eq_map_mk_of_rel, UniqueFactorizationMonoid.factors_unique
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
p q : Multiset (Associates α)
s t : Multiset α
hs :
  ∀ (a : Associates α),
    Membership.mem (γ := Multiset (Associates α)) (map (Quot.mk (⇑(Associated.setoid α) : α → α → Prop)) t) a →
      Irreducible a
ht :
  ∀ (a : Associates α),
    Membership.mem (γ := Multiset (Associates α)) (map (Quot.mk (⇑(Associated.setoid α) : α → α → Prop)) s) a →
      Irreducible a
eq :
  Eq (α := Associates α) (prod (map (Quot.mk (⇑(Associated.setoid α) : α → α → Prop)) t))
    (prod (map (Quot.mk (⇑(Associated.setoid α) : α → α → Prop)) s))
⊢ ∀ x ∈ t, Irreducible x

Tactic:
fun a ha => irreducible_mk.1 <| hs _ <| Multiset.mem_map_of_mem _ ha

Premises used: Associates.mk, Associates.irreducible_mk, Multiset.mem_map_of_mem, Iff.mp, Setoid.r, Quot.mk
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
p q : Multiset (Associates α)
s t : Multiset α
hs :
  ∀ (a : Associates α),
    Membership.mem (γ := Multiset (Associates α)) (map (Quot.mk (⇑(Associated.setoid α) : α → α → Prop)) t) a →
      Irreducible a
ht :
  ∀ (a : Associates α),
    Membership.mem (γ := Multiset (Associates α)) (map (Quot.mk (⇑(Associated.setoid α) : α → α → Prop)) s) a →
      Irreducible a
eq :
  Eq (α := Associates α) (prod (map (Quot.mk (⇑(Associated.setoid α) : α → α → Prop)) t))
    (prod (map (Quot.mk (⇑(Associated.setoid α) : α → α → Prop)) s))
⊢ ∀ x ∈ t, Irreducible x

Tactic:
exact fun a ha => irreducible_mk.1 <| hs _ <| Multiset.mem_map_of_mem _ ha

Premises used: Associates.mk, Associates.irreducible_mk, Multiset.mem_map_of_mem, Iff.mp, Setoid.r, Quot.mk
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
p q : Multiset (Associates α)
s t : Multiset α
hs :
  ∀ (a : Associates α),
    Membership.mem (γ := Multiset (Associates α)) (map (Quot.mk (⇑(Associated.setoid α) : α → α → Prop)) t) a →
      Irreducible a
ht :
  ∀ (a : Associates α),
    Membership.mem (γ := Multiset (Associates α)) (map (Quot.mk (⇑(Associated.setoid α) : α → α → Prop)) s) a →
      Irreducible a
eq :
  Eq (α := Associates α) (prod (map (Quot.mk (⇑(Associated.setoid α) : α → α → Prop)) t))
    (prod (map (Quot.mk (⇑(Associated.setoid α) : α → α → Prop)) s))
⊢ ∀ x ∈ s, Irreducible x

Tactic:
fun a ha => irreducible_mk.1 <| ht _ <| Multiset.mem_map_of_mem _ ha

Premises used: Associates.mk, Associates.irreducible_mk, Multiset.mem_map_of_mem, Iff.mp, Setoid.r, Quot.mk
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
p q : Multiset (Associates α)
s t : Multiset α
hs :
  ∀ (a : Associates α),
    Membership.mem (γ := Multiset (Associates α)) (map (Quot.mk (⇑(Associated.setoid α) : α → α → Prop)) t) a →
      Irreducible a
ht :
  ∀ (a : Associates α),
    Membership.mem (γ := Multiset (Associates α)) (map (Quot.mk (⇑(Associated.setoid α) : α → α → Prop)) s) a →
      Irreducible a
eq :
  Eq (α := Associates α) (prod (map (Quot.mk (⇑(Associated.setoid α) : α → α → Prop)) t))
    (prod (map (Quot.mk (⇑(Associated.setoid α) : α → α → Prop)) s))
⊢ ∀ x ∈ s, Irreducible x

Tactic:
exact fun a ha => irreducible_mk.1 <| ht _ <| Multiset.mem_map_of_mem _ ha

Premises used: Associates.mk, Associates.irreducible_mk, Multiset.mem_map_of_mem, Iff.mp, Setoid.r, Quot.mk
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
p q : Multiset (Associates α)
s t : Multiset α
hs :
  ∀ (a : Associates α),
    Membership.mem (γ := Multiset (Associates α)) (map (Quot.mk (⇑(Associated.setoid α) : α → α → Prop)) t) a →
      Irreducible a
ht :
  ∀ (a : Associates α),
    Membership.mem (γ := Multiset (Associates α)) (map (Quot.mk (⇑(Associated.setoid α) : α → α → Prop)) s) a →
      Irreducible a
eq :
  Eq (α := Associates α) (prod (map (Quot.mk (⇑(Associated.setoid α) : α → α → Prop)) t))
    (prod (map (Quot.mk (⇑(Associated.setoid α) : α → α → Prop)) s))
⊢ Eq.{u_1 + 1} (α := (a : α) → Quot (α := α) (⇑(Associated.setoid α) : α → α → Prop))
    (Quot.mk (⇑(Associated.setoid α) : α → α → Prop)) Associates.mk

Tactic:
have eq' : (Quot.mk Setoid.r : α → Associates α) = Associates.mk := funext quot_mk_eq_mk
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
p q : Multiset (Associates α)
s t : Multiset α
hs :
  ∀ (a : Associates α),
    Membership.mem (γ := Multiset (Associates α)) (map (Quot.mk (⇑(Associated.setoid α) : α → α → Prop)) t) a →
      Irreducible a
ht :
  ∀ (a : Associates α),
    Membership.mem (γ := Multiset (Associates α)) (map (Quot.mk (⇑(Associated.setoid α) : α → α → Prop)) s) a →
      Irreducible a
eq :
  Eq (α := Associates α) (prod (map (Quot.mk (⇑(Associated.setoid α) : α → α → Prop)) t))
    (prod (map (Quot.mk (⇑(Associated.setoid α) : α → α → Prop)) s))
eq' :
  Eq.{u_1 + 1} (α := (a : α) → Quot (α := α) (⇑(Associated.setoid α) : α → α → Prop))
    (Quot.mk (⇑(Associated.setoid α) : α → α → Prop)) Associates.mk
refine_3 :
  ∀ (eq : Eq (α := Associates α) (prod (map Associates.mk t)) (prod (map Associates.mk s)))
    (eq' :
      Eq.{u_1 + 1} (α := (a : α) → Quot (α := α) (⇑(Associated.setoid α) : α → α → Prop))
        (Quot.mk (⇑(Associated.setoid α) : α → α → Prop)) Associates.mk),
    t.prod ~ᵤ s.prod
refine_3₁ :
  ∀ (eq : Eq (α := Associates α) (Associates.mk t.prod) (prod (map Associates.mk s)))
    (eq' :
      Eq.{u_1 + 1} (α := (a : α) → Quot (α := α) (⇑(Associated.setoid α) : α → α → Prop))
        (Quot.mk (⇑(Associated.setoid α) : α → α → Prop)) Associates.mk),
    t.prod ~ᵤ s.prod
refine_3₂ :
  ∀ (eq : Eq (α := Associates α) (Associates.mk t.prod) (Associates.mk s.prod))
    (eq' :
      Eq.{u_1 + 1} (α := (a : α) → Quot (α := α) (⇑(Associated.setoid α) : α → α → Prop))
        (Quot.mk (⇑(Associated.setoid α) : α → α → Prop)) Associates.mk),
    t.prod ~ᵤ s.prod
refine_3₃ refine_3₄ refine_3₅ refine_3₆ :
  ∀ (eq : t.prod ~ᵤ s.prod)
    (eq' :
      Eq.{u_1 + 1} (α := (a : α) → Quot (α := α) (⇑(Associated.setoid α) : α → α → Prop))
        (Quot.mk (⇑(Associated.setoid α) : α → α → Prop)) Associates.mk),
    t.prod ~ᵤ s.prod
⊢ t.prod ~ᵤ s.prod

Tactic:
rwa [eq', prod_mk, prod_mk, mk_eq_mk_iff_associated] at eq

Premises used: Associates.mk_eq_mk_iff_associated, Associates.prod_mk
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : Nontrivial α
p q : Multiset (Associates α)
hp : ∀ a ∈ p, Irreducible a
hq : ∀ a ∈ q, Irreducible a
⊢ p.prod ≤ q.prod ↔ p ≤ q

Tactic:
⟨?_, prod_le_prod⟩

Premises used: Associates.prod_le_prod, Iff.intro
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : Nontrivial α
p q : Multiset (Associates α)
hp : ∀ a ∈ p, Irreducible a
hq : ∀ a ∈ q, Irreducible a
refine : p.prod ≤ q.prod → p ≤ q
⊢ p.prod ≤ q.prod ↔ p ≤ q

Tactic:
refine ⟨?_, prod_le_prod⟩
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : Nontrivial α
p q : Multiset (Associates α)
hp : ∀ a ∈ p, Irreducible a
hq : ∀ a ∈ q, Irreducible a
c : Associates α
eqc : q.prod = p.prod * c
⊢ p ≤ q

Tactic:
Multiset.le_iff_exists_add.2 ⟨factors c, unique' hq (fun x hx ↦ ?_) ?_⟩

Premises used: Iff.mpr, Associates.unique', UniqueFactorizationMonoid.factors, Exists.intro, Multiset.le_iff_exists_add
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : Nontrivial α
p q : Multiset (Associates α)
hp : ∀ a ∈ p, Irreducible a
hq : ∀ a ∈ q, Irreducible a
c : Associates α
eqc : q.prod = p.prod * c
refine_1 : ∀ (x : Associates α) (hx : x ∈ p + factors c), Irreducible x
refine_2 : q.prod = (p + factors c).prod
⊢ p ≤ q

Tactic:
refine Multiset.le_iff_exists_add.2 ⟨factors c, unique' hq (fun x hx ↦ ?_) ?_⟩

Premises used: Iff.mpr, Associates.unique', UniqueFactorizationMonoid.factors, Exists.intro, Multiset.le_iff_exists_add