awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
sa sb : Multiset { p : Associates α // Irreducible p }
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 }))
a₁ : ∀ (a : { p : Associates α // Irreducible p }), Multiset.count a sa = Multiset.count a sb
⊢ sa = sb

Tactic:
ext
-- 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
sa sb : Multiset { p : Associates α // Irreducible p }
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 }))
a_1 : { p : Associates α // Irreducible p }
⊢ Multiset.count a_1 sa = Multiset.count a_1 sb

Tactic:
grind
-- 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
⊢ a = b

Tactic:
eq_of_factors_eq_factors (eq_factors_of_eq_counts ha hb h)

Premises used: Associates.eq_of_factors_eq_factors, Associates.eq_factors_of_eq_counts
-- 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 p : Associates α
hb : b ≠ 0
hp : Irreducible p
h : a.factors ≤ b.factors
pos : ∀ (ha : a = 0), p.count a.factors ≤ p.count b.factors
neg : ∀ (ha : ¬a = 0), p.count a.factors ≤ p.count b.factors
⊢ p.count a.factors ≤ p.count b.factors

Tactic:
by_cases ha : a = 0
-- 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 p : Associates α
hb : b ≠ 0
hp : Irreducible p
h : a.factors ≤ b.factors
ha : a = 0
⊢ p.count a.factors ≤ p.count b.factors

Tactic:
simp_all
-- 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 p : Associates α
hb : b ≠ 0
hp : Irreducible p
h : a.factors ≤ b.factors
ha : ¬a = 0
neg :
  ∀ (sa : Multiset { p : Associates α // Irreducible p })
    (h_sa : a.factors = (↑sa : WithTop (Multiset { p : Associates α // Irreducible p }))),
    p.count a.factors ≤ p.count b.factors
⊢ p.count a.factors ≤ p.count 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 p : Associates α
hb : b ≠ 0
hp : Irreducible p
h : a.factors ≤ b.factors
ha : ¬a = 0
sa : Multiset { p : Associates α // Irreducible p }
h_sa : a.factors = (↑sa : WithTop (Multiset { p : Associates α // Irreducible p }))
neg :
  ∀ (sb : Multiset { p : Associates α // Irreducible p })
    (h_sb : b.factors = (↑sb : WithTop (Multiset { p : Associates α // Irreducible p }))),
    p.count a.factors ≤ p.count b.factors
⊢ p.count a.factors ≤ p.count 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 p : Associates α
hb : b ≠ 0
hp : Irreducible p
h : a.factors ≤ b.factors
ha : ¬a = 0
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 }))
neg :
  ∀ (h_sa : a.factors = (↑sa : WithTop (Multiset { p : Associates α // Irreducible p })))
    (sb : Multiset { p : Associates α // Irreducible p })
    (h :
      (↑sa : WithTop (Multiset { p : Associates α // Irreducible p })) ≤
        (↑sb : WithTop (Multiset { p : Associates α // Irreducible p })))
    (h_sb : b.factors = (↑sb : WithTop (Multiset { p : Associates α // Irreducible p }))),
    p.count (↑sa : WithTop (Multiset { p : Associates α // Irreducible p })) ≤
      p.count (↑sb : WithTop (Multiset { p : Associates α // Irreducible p }))
⊢ p.count a.factors ≤ p.count b.factors

Tactic:
rw [h_sa, h_sb] at h ⊢
-- 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 p : Associates α
hb : b ≠ 0
hp : Irreducible p
ha : ¬a = 0
sa : Multiset { p : Associates α // Irreducible p }
h_sa : a.factors = (↑sa : WithTop (Multiset { p : Associates α // Irreducible p }))
sb : Multiset { p : Associates α // Irreducible p }
h :
  (↑sa : WithTop (Multiset { p : Associates α // Irreducible p })) ≤
    (↑sb : WithTop (Multiset { p : Associates α // Irreducible p }))
h_sb : b.factors = (↑sb : WithTop (Multiset { p : Associates α // Irreducible p }))
neg :
  Multiset.count (Subtype.mk (p := fun (a : Associates α) ↦ Irreducible a) p hp) sa ≤
    Multiset.count (Subtype.mk (p := fun (a : Associates α) ↦ Irreducible a) p hp) sb
⊢ p.count (↑sa : WithTop (Multiset { p : Associates α // Irreducible p })) ≤
    p.count (↑sb : WithTop (Multiset { p : Associates α // Irreducible p }))

Tactic:
rw [count_some hp, count_some hp]

Premises used: Associates.count_some
-- 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 p : Associates α
hb : b ≠ 0
hp : Irreducible p
ha : ¬a = 0
sa : Multiset { p : Associates α // Irreducible p }
h_sa : a.factors = (↑sa : WithTop (Multiset { p : Associates α // Irreducible p }))
sb : Multiset { p : Associates α // Irreducible p }
h :
  (↑sa : WithTop (Multiset { p : Associates α // Irreducible p })) ≤
    (↑sb : WithTop (Multiset { p : Associates α // Irreducible p }))
h_sb : b.factors = (↑sb : WithTop (Multiset { p : Associates α // Irreducible p }))
⊢ sa ≤ sb

Tactic:
rw [WithTop.coe_le_coe] at h

Premises used: WithTop.coe_le_coe
-- 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 p : Associates α
hb : b ≠ 0
hp : Irreducible p
ha : ¬a = 0
sa : Multiset { p : Associates α // Irreducible p }
h_sa : a.factors = (↑sa : WithTop (Multiset { p : Associates α // Irreducible p }))
sb : Multiset { p : Associates α // Irreducible p }
h :
  (↑sa : WithTop (Multiset { p : Associates α // Irreducible p })) ≤
    (↑sb : WithTop (Multiset { p : Associates α // Irreducible p }))
h_sb : b.factors = (↑sb : WithTop (Multiset { p : Associates α // Irreducible p }))
h₁ : sa ≤ sb
⊢ b.factors = (↑sb : WithTop (Multiset { p : Associates α // Irreducible p }))

Tactic:
rw [WithTop.coe_le_coe] at h

Premises used: WithTop.coe_le_coe
-- 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 p : Associates α
hb : b ≠ 0
hp : Irreducible p
ha : ¬a = 0
sa : Multiset { p : Associates α // Irreducible p }
h_sa : a.factors = (↑sa : WithTop (Multiset { p : Associates α // Irreducible p }))
sb : Multiset { p : Associates α // Irreducible p }
h : sa ≤ sb
h_sb : b.factors = (↑sb : WithTop (Multiset { p : Associates α // Irreducible p }))
⊢ Multiset.count (Subtype.mk (p := fun (a : Associates α) ↦ Irreducible a) p hp) sa ≤
    Multiset.count (Subtype.mk (p := fun (a : Associates α) ↦ Irreducible a) p hp) sb

Tactic:
Multiset.count_le_of_le _ h

Premises used: Multiset.count_le_of_le
-- 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 p : Associates α
hb : b ≠ 0
hp : Irreducible p
ha : ¬a = 0
sa : Multiset { p : Associates α // Irreducible p }
h_sa : a.factors = (↑sa : WithTop (Multiset { p : Associates α // Irreducible p }))
sb : Multiset { p : Associates α // Irreducible p }
h : sa ≤ sb
h_sb : b.factors = (↑sb : WithTop (Multiset { p : Associates α // Irreducible p }))
⊢ Multiset.count (Subtype.mk (p := fun (a : Associates α) ↦ Irreducible a) p hp) sa ≤
    Multiset.count (Subtype.mk (p := fun (a : Associates α) ↦ Irreducible a) p hp) sb

Tactic:
exact Multiset.count_le_of_le _ h

Premises used: Multiset.count_le_of_le
-- 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 p : Associates α
hb : b ≠ 0
hp : Irreducible p
h : a ≤ b
⊢ p.count a.factors ≤ p.count b.factors

Tactic:
count_le_count_of_factors_le hb hp <| factors_mono h

Premises used: Associates.factors_mono, Associates.count_le_count_of_factors_le
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : Nontrivial α
a b : FactorSet α
⊢ a.prod ≤ b.prod ↔ a ≤ b

Tactic:
⟨fun h ↦ ?_, prod_mono⟩

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

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

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

Tactic:
rwa [prod_factors, prod_factors] at this

Premises used: Associates.prod_factors
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a b : Associates α
h : Nontrivial α
⊢ (a.factors ⊔ b.factors).prod * (a.factors ⊓ b.factors).prod = a * b

Tactic:
eq_of_factors_eq_factors ?_

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

Tactic:
refine eq_of_factors_eq_factors ?_

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

Tactic:
rw [← prod_add, prod_factors, factors_mul, FactorSet.sup_add_inf_eq_add]

Premises used: Associates.factors_mul, Associates.prod_add, Associates.prod_factors, Associates.FactorSet.sup_add_inf_eq_add
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a p : Associates α
hm : p ∈ a.factors
inl : ∀ (hm : Membership.mem (γ := FactorSet α) (factors 0) p), p ∣ 0
inr : ∀ (ha0 : a ≠ 0), p ∣ a
⊢ p ∣ a

Tactic:
rcases eq_or_ne a 0 with rfl | ha0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
p : Associates α
hm : Membership.mem (γ := FactorSet α) (factors 0) p
⊢ p ∣ 0

Tactic:
dvd_zero p

Premises used: dvd_zero
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
p : Associates α
hm : Membership.mem (γ := FactorSet α) (factors 0) p
⊢ p ∣ 0

Tactic:
exact dvd_zero p

Premises used: dvd_zero
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a p : Associates α
hm : p ∈ a.factors
ha0 : a ≠ 0
inr : ∀ (a0 : α) (nza : a0 ≠ 0) (ha' : Associates.mk a0 = a), p ∣ a
⊢ p ∣ a

Tactic:
obtain ⟨a0, nza, ha'⟩ := exists_non_zero_rep ha0

Premises used: Associates.exists_non_zero_rep
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a p : Associates α
hm : p ∈ a.factors
ha0 : a ≠ 0
a0 : α
nza : a0 ≠ 0
ha' : Associates.mk a0 = a
inr : p ∣ a.factors.prod
⊢ p ∣ a

Tactic:
rw [← Associates.factors_prod a]

Premises used: Associates.factors_prod
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a p : Associates α
hm : p ∈ a.factors
ha0 : a ≠ 0
a0 : α
nza : a0 ≠ 0
ha' : Associates.mk a0 = a
inr :
  ∀
    (hm :
      Membership.mem (γ := FactorSet α) (↑(factors' a0) : WithTop (Multiset { a : Associates α // Irreducible a })) p)
    (nza : a0 ≠ 0) (ha' : Associates.mk a0 = a),
    p ∣ FactorSet.prod (↑(factors' a0) : WithTop (Multiset { a : Associates α // Irreducible a }))
⊢ p ∣ a.factors.prod

Tactic:
rw [← ha', factors_mk a0 nza] at hm ⊢

Premises used: Associates.factors_mk
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a p : Associates α
ha0 : a ≠ 0
a0 : α
hm : Membership.mem (γ := FactorSet α) (↑(factors' a0) : WithTop (Multiset { a : Associates α // Irreducible a })) p
nza : a0 ≠ 0
ha' : Associates.mk a0 = a
inr :
  Membership.mem (γ := Multiset (Associates α))
    (Multiset.map (Subtype.val (p := fun (a : Associates α) ↦ Irreducible a)) (factors' a0)) p
⊢ p ∣ Multiset.prod (Multiset.map (Subtype.val (p := fun (a : Associates α) ↦ Irreducible a)) (factors' a0))

Tactic:
apply Multiset.dvd_prod

Premises used: Multiset.dvd_prod
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a p : Associates α
ha0 : a ≠ 0
a0 : α
hm : Membership.mem (γ := FactorSet α) (↑(factors' a0) : WithTop (Multiset { a : Associates α // Irreducible a })) p
nza : a0 ≠ 0
ha' : Associates.mk a0 = a
inr :
  ∃ (a : { a : Associates α // Irreducible a }),
    Membership.mem (γ := Multiset { a : Associates α // Irreducible a }) (factors' a0) a ∧ (↑a : Associates α) = p
⊢ Membership.mem (γ := Multiset (Associates α))
    (Multiset.map (Subtype.val (p := fun (a : Associates α) ↦ Irreducible a)) (factors' a0)) p

Tactic:
apply Multiset.mem_map.mpr

Premises used: Iff.mpr, Multiset.mem_map
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a p : Associates α
ha0 : a ≠ 0
a0 : α
hm : Membership.mem (γ := FactorSet α) (↑(factors' a0) : WithTop (Multiset { a : Associates α // Irreducible a })) p
nza : a0 ≠ 0
ha' : Associates.mk a0 = a
⊢ ∃ (a : { a : Associates α // Irreducible a }),
    Membership.mem (γ := Multiset { a : Associates α // Irreducible a }) (factors' a0) a ∧ (↑a : Associates α) = p

Tactic:
⟨⟨p, irreducible_of_mem_factorSet hm⟩, mem_factorSet_some.mp hm, rfl⟩

Premises used: Associates.mem_factorSet_some, Subtype.mk, Associates.irreducible_of_mem_factorSet, And.intro, Exists.intro, Iff.mp, rfl
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a p : Associates α
ha0 : a ≠ 0
a0 : α
hm : Membership.mem (γ := FactorSet α) (↑(factors' a0) : WithTop (Multiset { a : Associates α // Irreducible a })) p
nza : a0 ≠ 0
ha' : Associates.mk a0 = a
⊢ ∃ (a : { a : Associates α // Irreducible a }),
    Membership.mem (γ := Multiset { a : Associates α // Irreducible a }) (factors' a0) a ∧ (↑a : Associates α) = p

Tactic:
exact ⟨⟨p, irreducible_of_mem_factorSet hm⟩, mem_factorSet_some.mp hm, rfl⟩
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a : α
p : Associates α
hp : Irreducible p
hz : a ≠ 0
h_mem :
  Membership.mem (γ := Multiset { a : Associates α // Irreducible a }) (factors' a) (Subtype.mk (p := Irreducible) p hp)
haveI : ∀ (this : DecidableEq (Associates α)), p ∣ Associates.mk a
⊢ p ∣ Associates.mk a

Tactic:
haveI := Classical.decEq (Associates α)
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a : α
p : Associates α
hp : Irreducible p
hz : a ≠ 0
h_mem :
  Membership.mem (γ := Multiset { a : Associates α // Irreducible a }) (factors' a) (Subtype.mk (p := Irreducible) p hp)
this : DecidableEq (Associates α)
hm : Membership.mem (γ := FactorSet α) (factors (Associates.mk a)) p
⊢ p ∣ Associates.mk a

Tactic:
apply dvd_of_mem_factors

Premises used: Associates.dvd_of_mem_factors
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a : α
p : Associates α
hp : Irreducible p
hz : a ≠ 0
h_mem :
  Membership.mem (γ := Multiset { a : Associates α // Irreducible a }) (factors' a) (Subtype.mk (p := Irreducible) p hp)
this : DecidableEq (Associates α)
hm : Membership.mem (γ := FactorSet α) (↑(factors' a) : WithTop (Multiset { a : Associates α // Irreducible a })) p
⊢ Membership.mem (γ := FactorSet α) (factors (Associates.mk a)) p

Tactic:
rw [factors_mk _ hz]

Premises used: Associates.factors_mk
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a : α
p : Associates α
hp : Irreducible p
hz : a ≠ 0
h_mem :
  Membership.mem (γ := Multiset { a : Associates α // Irreducible a }) (factors' a) (Subtype.mk (p := Irreducible) p hp)
this : DecidableEq (Associates α)
⊢ Membership.mem (γ := FactorSet α) (↑(factors' a) : WithTop (Multiset { a : Associates α // Irreducible a })) p

Tactic:
apply mem_factorSet_some.2 h_mem

Premises used: Iff.mpr, Associates.mem_factorSet_some
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a p : α
ha0 : a ≠ 0
hp : Irreducible p
hd : p ∣ a
obtain :
  ∀ (q : α) (hq : q ∈ UniqueFactorizationMonoid.factors a) (hpq : p ~ᵤ q),
    Membership.mem (γ := Multiset { a : Associates α // Irreducible a }) (factors' a)
      (Subtype.mk (p := Irreducible) (Associates.mk p) ⋯)
⊢ Membership.mem (γ := Multiset { a : Associates α // Irreducible a }) (factors' a)
    (Subtype.mk (p := Irreducible) (Associates.mk p) ⋯)

Tactic:
obtain ⟨q, hq, hpq⟩ := exists_mem_factors_of_dvd ha0 hp hd

Premises used: UniqueFactorizationMonoid.exists_mem_factors_of_dvd
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a p : α
ha0 : a ≠ 0
hp : Irreducible p
hd : p ∣ a
q : α
hq : q ∈ UniqueFactorizationMonoid.factors a
hpq : p ~ᵤ q
apply :
  ∃ (a_1 : α) (h : a_1 ∈ UniqueFactorizationMonoid.factors a),
    Subtype.mk (p := fun (a : Associates α) ↦ Irreducible a) (Associates.mk a_1) ⋯ =
      Subtype.mk (p := Irreducible) (Associates.mk p) ⋯
⊢ Membership.mem (γ := Multiset { a : Associates α // Irreducible a }) (factors' a)
    (Subtype.mk (p := Irreducible) (Associates.mk p) ⋯)

Tactic:
apply Multiset.mem_pmap.mpr

Premises used: Iff.mpr, Multiset.mem_pmap
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a p : α
ha0 : a ≠ 0
hp : Irreducible p
hd : p ∣ a
q : α
hq : q ∈ UniqueFactorizationMonoid.factors a
hpq : p ~ᵤ q
h :
  ∃ (h : q ∈ UniqueFactorizationMonoid.factors a),
    Subtype.mk (p := fun (a : Associates α) ↦ Irreducible a) (Associates.mk q) ⋯ =
      Subtype.mk (p := Irreducible) (Associates.mk p) ⋯
⊢ ∃ (a_1 : α) (h : a_1 ∈ UniqueFactorizationMonoid.factors a),
    Subtype.mk (p := fun (a : Associates α) ↦ Irreducible a) (Associates.mk a_1) ⋯ =
      Subtype.mk (p := Irreducible) (Associates.mk p) ⋯

Tactic:
use q
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a p : α
ha0 : a ≠ 0
hp : Irreducible p
hd : p ∣ a
q : α
hq : q ∈ UniqueFactorizationMonoid.factors a
hpq : p ~ᵤ q
h :
  Subtype.mk (p := fun (a : Associates α) ↦ Irreducible a) (Associates.mk q) ⋯ =
    Subtype.mk (p := Irreducible) (Associates.mk p) ⋯
⊢ ∃ (h : q ∈ UniqueFactorizationMonoid.factors a),
    Subtype.mk (p := fun (a : Associates α) ↦ Irreducible a) (Associates.mk q) ⋯ =
      Subtype.mk (p := Irreducible) (Associates.mk p) ⋯

Tactic:
use hq
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a p : α
ha0 : a ≠ 0
hp : Irreducible p
hd : p ∣ a
q : α
hq : q ∈ UniqueFactorizationMonoid.factors a
hpq : p ~ᵤ q
⊢ Subtype.mk (p := fun (a : Associates α) ↦ Irreducible a) (Associates.mk q) ⋯ =
    Subtype.mk (p := Irreducible) (Associates.mk p) ⋯

Tactic:
Subtype.ext (Eq.symm (mk_eq_mk_iff_associated.mpr hpq))

Premises used: Iff.mpr, Associates.mk_eq_mk_iff_associated, Eq.symm, Subtype.ext