awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : Nontrivial α
a a_1 : Multiset { a : Associates α // Irreducible a }
h :
  prod (↑a : WithTop (Multiset { a : Associates α // Irreducible a })) =
    prod (↑a_1 : WithTop (Multiset { a : Associates α // Irreducible a }))
a' : Associates α
irred : Irreducible a'
ha :
  (↑(Subtype.mk (p := fun (a : Associates α) ↦ Irreducible a) a' irred) : Associates α) ∈
    Multiset.map (Subtype.val (p := fun (a : Associates α) ↦ Irreducible a)) a_1
rwa rwa₁ rwa₂ rwa₃ : Irreducible a'
⊢ Irreducible (↑(Subtype.mk (p := fun (a : Associates α) ↦ Irreducible a) a' irred) : Associates α)

Tactic:
rwa [Subtype.coe_mk]

Premises used: Subtype.coe_mk
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a : α
⊢ Eq (α := Multiset (Associates α))
    (Multiset.map (Subtype.val (p := fun (a : Associates α) ↦ Irreducible a)) (factors' a))
    (Multiset.map Associates.mk (factors a))

Tactic:
simp [factors', Multiset.map_pmap, Multiset.pmap_eq_map]

Premises used: Multiset.pmap_eq_map, Multiset.map_pmap, Associates.factors'
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a b : α
h : a ~ᵤ b
inl : ∀ (h : a ~ᵤ 0), Eq (α := Multiset { a : Associates α // Irreducible a }) (factors' a) (factors' 0)
inr : ∀ (hb : b ≠ 0), Eq (α := Multiset { a : Associates α // Irreducible a }) (factors' a) (factors' b)
⊢ Eq (α := Multiset { a : Associates α // Irreducible a }) (factors' a) (factors' b)

Tactic:
obtain rfl | hb := eq_or_ne b 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a : α
h : a ~ᵤ 0
⊢ a = 0

Tactic:
rw [associated_zero_iff_eq_zero] at h

Premises used: associated_zero_iff_eq_zero
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a : α
h : a = 0
inl inl₁ : Eq.{u_1 + 1} (α := Multiset { a : Associates α // Irreducible a }) (factors' 0) (factors' 0)
⊢ Eq (α := Multiset { a : Associates α // Irreducible a }) (factors' a) (factors' 0)

Tactic:
rw [h]
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a b : α
h : a ~ᵤ b
hb : b ≠ 0
contrapose : ∀ (ha : a = 0), b = 0
⊢ a ≠ 0

Tactic:
contrapose hb with ha
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a b : α
h : a ~ᵤ b
ha : a = 0
rw : b ~ᵤ a
⊢ b = 0

Tactic:
rw [← associated_zero_iff_eq_zero, ← ha]

Premises used: associated_zero_iff_eq_zero
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a b : α
h : a ~ᵤ b
ha : a = 0
⊢ b ~ᵤ a

Tactic:
h.symm

Premises used: Associated.symm
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a b : α
h : a ~ᵤ b
ha : a = 0
⊢ b ~ᵤ a

Tactic:
exact h.symm

Premises used: Associated.symm
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a b : α
h : a ~ᵤ b
hb : b ≠ 0
⊢ a ≠ 0

Tactic:
have ha : a ≠ 0 := by
    contrapose hb with ha
    rw [← associated_zero_iff_eq_zero, ← ha]
    exact h.symm
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a b : α
h : a ~ᵤ b
hb : b ≠ 0
ha : a ≠ 0
inr : Rel Associated (factors a) (factors b)
⊢ Eq (α := Multiset { a : Associates α // Irreducible a }) (factors' a) (factors' b)

Tactic:
rw [← Multiset.map_eq_map Subtype.coe_injective, map_subtype_coe_factors',
    map_subtype_coe_factors', ← rel_associated_iff_map_eq_map]

Premises used: Multiset.map_eq_map, Associates.map_subtype_coe_factors', Subtype.coe_injective, Associates.rel_associated_iff_map_eq_map
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a b : α
h : a ~ᵤ b
hb : b ≠ 0
ha : a ≠ 0
⊢ Rel Associated (factors a) (factors b)

Tactic:
factors_unique irreducible_of_factor irreducible_of_factor
      ((factors_prod ha).trans <| h.trans <| (factors_prod hb).symm)

Premises used: UniqueFactorizationMonoid.factors_unique, Associated.trans, UniqueFactorizationMonoid.irreducible_of_factor, Associated.symm, UniqueFactorizationMonoid.factors_prod
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a b : α
h : a ~ᵤ b
hb : b ≠ 0
ha : a ≠ 0
⊢ Rel Associated (factors a) (factors b)

Tactic:
exact
    factors_unique irreducible_of_factor irreducible_of_factor
      ((factors_prod ha).trans <| h.trans <| (factors_prod hb).symm)

Premises used: UniqueFactorizationMonoid.factors_unique, Associated.trans, UniqueFactorizationMonoid.irreducible_of_factor, Associated.symm, UniqueFactorizationMonoid.factors_prod
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a : Associates α
refine :
  ∀ (h : ¬a = 0) (a b : α) (p : a ≈ b),
    HEq.{u_1 + 1} (α := ¬⟦a⟧ = 0 → FactorSet α) fun (x : ¬⟦a⟧ = 0) ↦
      (↑(factors' a) : WithTop (Multiset { a : Associates α // Irreducible a })) (β := ¬⟦b⟧ = 0 → FactorSet α)
      fun (x : ¬⟦b⟧ = 0) ↦ (↑(factors' b) : WithTop (Multiset { a : Associates α // Irreducible a }))
⊢ FactorSet α

Tactic:
refine if h : a = 0 then ⊤ else Quotient.hrecOn a (fun x _ => factors' x) ?_ h
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a : Associates α
classical :
  ∀ (h : ¬a = 0) (a b : α) (p : a ≈ b),
    HEq.{u_1 + 1} (α := ¬⟦a⟧ = 0 → FactorSet α) fun (x : ¬⟦a⟧ = 0) ↦
      (↑(factors' a) : WithTop (Multiset { a : Associates α // Irreducible a })) (β := ¬⟦b⟧ = 0 → FactorSet α)
      fun (x : ¬⟦b⟧ = 0) ↦ (↑(factors' b) : WithTop (Multiset { a : Associates α // Irreducible a }))
⊢ FactorSet α

Tactic:
classical refine if h : a = 0 then ⊤ else Quotient.hrecOn a (fun x _ => factors' x) ?_ h
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a_1 : Associates α
h : ¬a_1 = 0
a b : α
hab : a ≈ b
hα : (¬⟦a⟧ = 0) = ¬⟦b⟧ = 0
h₁ :
  ∀ (a_2 : ¬⟦a⟧ = 0) (a' : ¬⟦b⟧ = 0),
    a_2 ≍ a' →
      HEq (α := WithTop (Multiset { a : Associates α // Irreducible a }))
        (↑(factors' a) : WithTop (Multiset { a : Associates α // Irreducible a })) (β :=
        WithTop (Multiset { a : Associates α // Irreducible a }))
        (↑(factors' b) : WithTop (Multiset { a : Associates α // Irreducible a }))
⊢ HEq.{u_1 + 1} (α := ¬⟦a⟧ = 0 → FactorSet α) fun (x : ¬⟦a⟧ = 0) ↦
    (↑(factors' a) : WithTop (Multiset { a : Associates α // Irreducible a })) (β := ¬⟦b⟧ = 0 → FactorSet α)
    fun (x : ¬⟦b⟧ = 0) ↦ (↑(factors' b) : WithTop (Multiset { a : Associates α // Irreducible a }))

Tactic:
apply Function.hfunext

Premises used: Function.hfunext
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a_1 : Associates α
h : ¬a_1 = 0
a b : α
hab : a ≈ b
⊢ a ~ᵤ 0 ↔ b ~ᵤ 0

Tactic:
have : a ~ᵤ 0 ↔ b ~ᵤ 0 := Iff.intro (fun ha0 => hab.symm.trans ha0) fun hb0 => hab.trans hb0
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a_1 : Associates α
h : ¬a_1 = 0
a b : α
hab : a ≈ b
this : a ~ᵤ 0 ↔ b ~ᵤ 0
⊢ a = 0 ↔ b = 0

Tactic:
simp only [associated_zero_iff_eq_zero] at this

Premises used: associated_zero_iff_eq_zero
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a_1 : Associates α
h : ¬a_1 = 0
a b : α
hab : a ≈ b
this : a = 0 ↔ b = 0
⊢ (¬⟦a⟧ = 0) = ¬⟦b⟧ = 0

Tactic:
simp only [quotient_mk_eq_mk, this, mk_eq_zero]

Premises used: Associates.quotient_mk_eq_mk, Associates.mk_eq_zero
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a_1 : Associates α
h : ¬a_1 = 0
a b : α
hab : a ≈ b
⊢ ∀ (a_2 : ¬⟦a⟧ = 0) (a' : ¬⟦b⟧ = 0),
    a_2 ≍ a' →
      HEq (α := WithTop (Multiset { a : Associates α // Irreducible a }))
        (↑(factors' a) : WithTop (Multiset { a : Associates α // Irreducible a })) (β :=
        WithTop (Multiset { a : Associates α // Irreducible a }))
        (↑(factors' b) : WithTop (Multiset { a : Associates α // Irreducible a }))

Tactic:
fun ha hb _ => heq_of_eq <| congr_arg some <| factors'_cong hab

Premises used: Option.some, congr_arg, heq_of_eq, Associates.factors'_cong
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a_1 : Associates α
h : ¬a_1 = 0
a b : α
hab : a ≈ b
⊢ ∀ (a_2 : ¬⟦a⟧ = 0) (a' : ¬⟦b⟧ = 0),
    a_2 ≍ a' →
      HEq (α := WithTop (Multiset { a : Associates α // Irreducible a }))
        (↑(factors' a) : WithTop (Multiset { a : Associates α // Irreducible a })) (β :=
        WithTop (Multiset { a : Associates α // Irreducible a }))
        (↑(factors' b) : WithTop (Multiset { a : Associates α // Irreducible a }))

Tactic:
exact fun ha hb _ => heq_of_eq <| congr_arg some <| factors'_cong hab

Premises used: Option.some, congr_arg, heq_of_eq, Associates.factors'_cong
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
⊢ Eq.{u_1 + 1} (α := FactorSet α) (factors 0) ⊤

Tactic:
dif_pos rfl

Premises used: dif_pos, Associates.factors, rfl
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a : α
h : a ≠ 0
hnc : ¬Eq (α := Associates α) (Associates.mk a) 0
⊢ Eq (α := FactorSet α) (factors (Associates.mk a))
    (↑(factors' a) : WithTop (Multiset { a : Associates α // Irreducible a }))

Tactic:
apply dif_neg

Premises used: dif_neg
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a : α
h : a ≠ 0
⊢ ¬Eq (α := Associates α) (Associates.mk a) 0

Tactic:
apply mt mk_eq_zero.1 h

Premises used: mt, Iff.mp, Associates.mk_eq_zero
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a : α
h : a ≠ 0
hnc : ¬Eq (α := Associates α) (Associates.mk a) 0
⊢ Eq (α := FactorSet α) (factors (Associates.mk a))
    (↑(factors' a) : WithTop (Multiset { a : Associates α // Irreducible a }))

Tactic:
classical
    apply dif_neg
    apply mt mk_eq_zero.1 h

Premises used: mt, dif_neg, Iff.mp, Associates.mk_eq_zero
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a : Associates α
rcases : ∀ (a : α), Eq (α := Associates α) (FactorSet.prod (factors (Associates.mk a))) (Associates.mk a)
⊢ a.factors.prod = a

Tactic:
rcases Associates.mk_surjective a with ⟨a, rfl⟩

Premises used: Associates.mk_surjective, rfl
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a : α
inl : Eq.{u_1 + 1} (α := Associates α) (FactorSet.prod (factors (Associates.mk 0))) (Associates.mk 0)
inr : ∀ (ha : a ≠ 0), Eq (α := Associates α) (FactorSet.prod (factors (Associates.mk a))) (Associates.mk a)
⊢ Eq (α := Associates α) (FactorSet.prod (factors (Associates.mk a))) (Associates.mk a)

Tactic:
rcases eq_or_ne a 0 with rfl | ha

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
⊢ Eq.{u_1 + 1} (α := Associates α) (FactorSet.prod (factors (Associates.mk 0))) (Associates.mk 0)

Tactic:
simp
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a : α
ha : a ≠ 0
⊢ Eq (α := Associates α) (FactorSet.prod (factors (Associates.mk a))) (Associates.mk a)

Tactic:
simp [ha, prod_mk, mk_eq_mk_iff_associated, UniqueFactorizationMonoid.factors_prod]

Premises used: Associates.mk_eq_mk_iff_associated, Associates.prod_mk, UniqueFactorizationMonoid.factors_prod
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : Nontrivial α
s : FactorSet α
⊢ s.prod.factors = s

Tactic:
FactorSet.unique <| factors_prod _

Premises used: Associates.FactorSet.unique, Associates.factors_prod
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : Subsingleton α
a : Associates α
⊢ Subsingleton.{u_1 + 1} (Associates α)

Tactic:
have : Subsingleton (Associates α) := inferInstance
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : Subsingleton α
a : Associates α
this : Subsingleton.{u_1 + 1} (Associates α)
⊢ Eq.{u_1 + 1} (α := FactorSet α) (factors 0) ⊤

Tactic:
factors_zero

Premises used: Associates.factors_zero
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : Subsingleton α
a : Associates α
this : Subsingleton.{u_1 + 1} (Associates α)
⊢ a.factors = ⊤

Tactic:
convert! factors_zero

Premises used: Associates.factors_zero
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a : Associates α
⊢ Nontrivial α

Tactic:
nontriviality α
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a : Associates α
h_1 : Nontrivial α
h : a.factors = ⊤
rwa : a.factors.prod = 0
rwa₁ rwa₂ rwa₃ rwa₄ : a.factors = ⊤
⊢ a = 0

Tactic:
rwa [← factors_prod a, FactorSet.prod_eq_zero_iff]

Premises used: Associates.factors_prod, Associates.FactorSet.prod_eq_zero_iff
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a : Associates α
h : Nontrivial α
⊢ a.factors = ⊤ ↔ a = 0

Tactic:
exact ⟨fun h ↦ by rwa [← factors_prod a, FactorSet.prod_eq_zero_iff], fun h ↦ h ▸ factors_zero⟩
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a : Associates α
simp_rw : a.factors ≠ ⊤ ↔ a ≠ 0
⊢ (∃ (s : Multiset { p : Associates α // Irreducible p }),
      a.factors = (↑s : WithTop (Multiset { p : Associates α // Irreducible p }))) ↔
    a ≠ 0

Tactic:
simp_rw [@eq_comm _ a.factors, ← WithTop.ne_top_iff_exists]

Premises used: WithTop.ne_top_iff_exists, eq_comm
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a : Associates α
⊢ a.factors ≠ ⊤ ↔ a ≠ 0

Tactic:
factors_eq_top_iff_zero.not

Premises used: Iff.not, Associates.factors_eq_top_iff_zero
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a : Associates α
⊢ a.factors ≠ ⊤ ↔ a ≠ 0

Tactic:
exact factors_eq_top_iff_zero.not

Premises used: Iff.not, Associates.factors_eq_top_iff_zero
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a b : Associates α
h : a.factors = b.factors
rw rw₁ : b.factors.prod = b.factors.prod
⊢ a.factors.prod = b.factors.prod

Tactic:
rw [h]
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a b : Associates α
h : a.factors = b.factors
⊢ a.factors.prod = b.factors.prod

Tactic:
have : a.factors.prod = b.factors.prod := by rw [h]
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a b : Associates α
h : a.factors = b.factors
this : a.factors.prod = b.factors.prod
rwa : ∀ (this : a = b.factors.prod), a = b
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (this : a = b), a = b
⊢ a = b

Tactic:
rwa [factors_prod, factors_prod] at this

Premises used: Associates.factors_prod
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a b : Associates α
⊢ Nontrivial α

Tactic:
nontriviality α
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a b : Associates α
h : Nontrivial α
⊢ (a * b).factors = a.factors + b.factors

Tactic:
FactorSet.unique <| eq_of_factors_eq_factors ?_

Premises used: Associates.eq_of_factors_eq_factors, Associates.FactorSet.unique
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a b : Associates α
h : Nontrivial α
refine : (a * b).factors.prod.factors = (a.factors + b.factors).prod.factors
⊢ (a * b).factors = a.factors + b.factors

Tactic:
refine FactorSet.unique <| eq_of_factors_eq_factors ?_

Premises used: Associates.eq_of_factors_eq_factors, Associates.FactorSet.unique
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a b : Associates α
h : Nontrivial α
rw : (a * b).factors.prod.factors = (a.factors.prod * b.factors.prod).factors
rw₁ : (a * b).factors = (a.factors.prod * b.factors.prod).factors
rw₂ : (a * b).factors = (a * b.factors.prod).factors
rw₃ rw₄ : (a * b).factors = (a * b).factors
⊢ (a * b).factors.prod.factors = (a.factors + b.factors).prod.factors

Tactic:
rw [prod_add, factors_prod, factors_prod, factors_prod]

Premises used: Associates.prod_add, Associates.factors_prod
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
s t : Associates α
d : Associates α
eq : t = s * d
rw : s.factors ≤ s.factors + d.factors
⊢ s.factors ≤ t.factors

Tactic:
rw [eq, factors_mul]

Premises used: Associates.factors_mul
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
s t : Associates α
d : Associates α
eq : t = s * d
⊢ s.factors ≤ s.factors + d.factors

Tactic:
le_add_of_nonneg_right bot_le

Premises used: le_add_of_nonneg_right, bot_le
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
s t : Associates α
d : Associates α
eq : t = s * d
⊢ s.factors ≤ s.factors + d.factors

Tactic:
exact le_add_of_nonneg_right bot_le

Premises used: le_add_of_nonneg_right
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a b : Associates α
⊢ a.factors ≤ b.factors ↔ a ≤ b

Tactic:
⟨fun h ↦ ?_, factors_mono⟩

Premises used: Associates.factors_mono, Iff.intro
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a b : Associates α
refine : ∀ (h : a.factors ≤ b.factors), a ≤ b
⊢ a.factors ≤ b.factors ↔ a ≤ b

Tactic:
refine ⟨fun h ↦ ?_, factors_mono⟩
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a b : Associates α
h : a.factors ≤ b.factors
⊢ a.factors.prod ≤ b.factors.prod

Tactic:
have : a.factors.prod ≤ b.factors.prod := prod_mono h
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a b : Associates α
h : a.factors ≤ b.factors
this : a.factors.prod ≤ b.factors.prod
rwa : ∀ (this : a ≤ b.factors.prod), a ≤ b
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (this : a ≤ b), a ≤ b
⊢ a ≤ b

Tactic:
rwa [factors_prod, factors_prod] at this

Premises used: Associates.factors_prod
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : DecidableEq (Associates α)
inst_3 : (p : Associates α) → Decidable (Irreducible p)
a b : Associates α
ha : a ≠ 0
hb : b ≠ 0
h : ∀ (p : Associates α), Irreducible p → p.count a.factors = p.count b.factors
obtain :
  ∀ (sa : Multiset { p : Associates α // Irreducible p })
    (h_sa : a.factors = (↑sa : WithTop (Multiset { p : Associates α // Irreducible p }))), a.factors = b.factors
⊢ a.factors = b.factors

Tactic:
obtain ⟨sa, h_sa⟩ := factors_eq_some_iff_ne_zero.mpr ha

Premises used: Iff.mpr, Associates.factors_eq_some_iff_ne_zero
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : DecidableEq (Associates α)
inst_3 : (p : Associates α) → Decidable (Irreducible p)
a b : Associates α
ha : a ≠ 0
hb : b ≠ 0
h : ∀ (p : Associates α), Irreducible p → p.count a.factors = p.count b.factors
sa : Multiset { p : Associates α // Irreducible p }
h_sa : a.factors = (↑sa : WithTop (Multiset { p : Associates α // Irreducible p }))
obtain :
  ∀ (sb : Multiset { p : Associates α // Irreducible p })
    (h_sb : b.factors = (↑sb : WithTop (Multiset { p : Associates α // Irreducible p }))), a.factors = b.factors
⊢ a.factors = b.factors

Tactic:
obtain ⟨sb, h_sb⟩ := factors_eq_some_iff_ne_zero.mpr hb

Premises used: Iff.mpr, Associates.factors_eq_some_iff_ne_zero
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : DecidableEq (Associates α)
inst_3 : (p : Associates α) → Decidable (Irreducible p)
a b : Associates α
ha : a ≠ 0
hb : b ≠ 0
h : ∀ (p : Associates α), Irreducible p → p.count a.factors = p.count b.factors
sa : Multiset { p : Associates α // Irreducible p }
h_sa : a.factors = (↑sa : WithTop (Multiset { p : Associates α // Irreducible p }))
sb : Multiset { p : Associates α // Irreducible p }
h_sb : b.factors = (↑sb : WithTop (Multiset { p : Associates α // Irreducible p }))
simp_all :
  ∀
    (h :
      ∀ (p : Associates α) (a : Irreducible p),
        Multiset.count (Subtype.mk (p := fun (a : Associates α) ↦ Irreducible a) p a) sa =
          Multiset.count (Subtype.mk (p := fun (a : Associates α) ↦ Irreducible a) p a) sb)
    (h_sa : a.factors = (↑sa : WithTop (Multiset { p : Associates α // Irreducible p })))
    (h_sb : b.factors = (↑sb : WithTop (Multiset { p : Associates α // Irreducible p }))), sa = sb
⊢ a.factors = b.factors

Tactic:
simp_all only [count_some, WithTop.coe_eq_coe]

Premises used: Associates.count_some, WithTop.coe_eq_coe