awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Defs
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a : α
ha : Irreducible a
hf_1 : factors a ≠ 0
b : α
hb : b ∈ factors a
f : Multiset α
hf : factors a = b ::ₘ f
rw : ∀ (a : α), a ∉ f
⊢ (factors a).card = 1

Tactic:
rw [hf, card_cons, add_eq_right, card_eq_zero, eq_zero_iff_forall_notMem]

Premises used: Multiset.card_eq_zero, Multiset.eq_zero_iff_forall_notMem, Multiset.card_cons, add_eq_right
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Defs
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a : α
ha : Irreducible a
hf_1 : factors a ≠ 0
b : α
hb : b ∈ factors a
f : Multiset α
hf : factors a = b ::ₘ f
c : α
hc : c ∈ f
obtain : ∀ (f : Multiset α) (hf : factors a = b ::ₘ c ::ₘ f) (hc : c ∈ c ::ₘ f), False
⊢ False

Tactic:
obtain ⟨f, rfl⟩ := exists_cons_of_mem hc

Premises used: Multiset.exists_cons_of_mem, rfl
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Defs
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a : α
ha : Irreducible a
hf_1 : factors a ≠ 0
b : α
hb : b ∈ factors a
c : α
f : Multiset α
hf : factors a = b ::ₘ c ::ₘ f
hc : c ∈ c ::ₘ f
⊢ ¬IsUnit b

Tactic:
replace hb := (irreducible_of_factor b hb).not_isUnit
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Defs
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a : α
ha : Irreducible a
hf_1 : factors a ≠ 0
b c : α
f : Multiset α
hf : factors a = b ::ₘ c ::ₘ f
hc : c ∈ c ::ₘ f
hb : ¬IsUnit b
⊢ ¬IsUnit c

Tactic:
replace hc := (irreducible_of_factor c (hf ▸ mem_cons_of_mem hc)).not_isUnit
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Defs
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a : α
ha : Irreducible a
hf_1 : factors a ≠ 0
b c : α
f : Multiset α
hf : factors a = b ::ₘ c ::ₘ f
hb : ¬IsUnit b
hc : ¬IsUnit c
⊢ False

Tactic:
simp [← (factors_prod ha.ne_zero).irreducible_iff, hf, irreducible_mul_iff, hb, hc] at ha

Premises used: UniqueFactorizationMonoid.factors_prod, Irreducible.ne_zero, irreducible_mul_iff, Associated.irreducible_iff
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
a b : Multiset { a : Associates α // Irreducible a }
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : a + b = a + b
⊢ (↑(a + b) : WithTop (Multiset { a : Associates α // Irreducible a })) =
    (↑a : WithTop (Multiset { a : Associates α // Irreducible a })) +
      (↑b : WithTop (Multiset { a : Associates α // Irreducible a }))

Tactic:
norm_cast
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : DecidableEq (Associates α)
b : FactorSet α
⊢ ⊤ ⊔ b + ⊤ ⊓ b = ⊤ + b

Tactic:
simp
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : DecidableEq (Associates α)
a : FactorSet α
⊢ a ⊔ ⊤ + a ⊓ ⊤ = a + ⊤

Tactic:
simp
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : DecidableEq (Associates α)
a b : Multiset { a : Associates α // Irreducible a }
rw : a ⊔ b + a ⊓ b = a + b
⊢ (↑a : WithTop (Multiset { a : Associates α // Irreducible a })) ⊔
        (↑b : WithTop (Multiset { a : Associates α // Irreducible a })) +
      (↑a : WithTop (Multiset { a : Associates α // Irreducible a })) ⊓
        (↑b : WithTop (Multiset { a : Associates α // Irreducible a })) =
    (↑a : WithTop (Multiset { a : Associates α // Irreducible a })) +
      (↑b : WithTop (Multiset { a : Associates α // Irreducible a }))

Tactic:
rw [← WithTop.coe_sup, ← WithTop.coe_inf, ← WithTop.coe_add, ← WithTop.coe_add,
        WithTop.coe_eq_coe]

Premises used: WithTop.coe_sup, WithTop.coe_eq_coe, WithTop.coe_inf, WithTop.coe_add
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : DecidableEq (Associates α)
a b : Multiset { a : Associates α // Irreducible a }
⊢ a ⊔ b + a ⊓ b = a + b

Tactic:
Multiset.union_add_inter _ _

Premises used: Multiset.union_add_inter
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : DecidableEq (Associates α)
a b : Multiset { a : Associates α // Irreducible a }
⊢ a ⊔ b + a ⊓ b = a + b

Tactic:
exact Multiset.union_add_inter _ _

Premises used: Multiset.union_add_inter
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
⊢ Eq.{u_1 + 1} (α := Associates α) (FactorSet.prod ⊤) 0

Tactic:
rfl

Premises used: Associates.FactorSet.prod, rfl
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
s : Multiset { a : Associates α // Irreducible a }
⊢ FactorSet.prod (↑s : WithTop (Multiset { a : Associates α // Irreducible a })) =
    (Multiset.map (Subtype.val (p := fun (a : Associates α) ↦ Irreducible a)) s).prod

Tactic:
rfl

Premises used: Associates.FactorSet.prod, rfl
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
b : FactorSet α
⊢ (⊤ + b).prod = FactorSet.prod ⊤ * b.prod

Tactic:
simp
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
a : FactorSet α
⊢ (a + ⊤).prod = a.prod * FactorSet.prod ⊤

Tactic:
simp
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
a b : Multiset { a : Associates α // Irreducible a }
rw :
  FactorSet.prod (↑(a + b) : WithTop (Multiset { a : Associates α // Irreducible a })) =
    FactorSet.prod (↑a : WithTop (Multiset { a : Associates α // Irreducible a })) *
      FactorSet.prod (↑b : WithTop (Multiset { a : Associates α // Irreducible a }))
rw₁ :
  (Multiset.map (Subtype.val (p := fun (a : Associates α) ↦ Irreducible a)) (a + b)).prod =
    FactorSet.prod (↑a : WithTop (Multiset { a : Associates α // Irreducible a })) *
      FactorSet.prod (↑b : WithTop (Multiset { a : Associates α // Irreducible a }))
rw₂ :
  (Multiset.map (Subtype.val (p := fun (a : Associates α) ↦ Irreducible a)) (a + b)).prod =
    (Multiset.map (Subtype.val (p := fun (a : Associates α) ↦ Irreducible a)) a).prod *
      FactorSet.prod (↑b : WithTop (Multiset { a : Associates α // Irreducible a }))
rw₃ :
  (Multiset.map (Subtype.val (p := fun (a : Associates α) ↦ Irreducible a)) (a + b)).prod =
    (Multiset.map (Subtype.val (p := fun (a : Associates α) ↦ Irreducible a)) a).prod *
      (Multiset.map (Subtype.val (p := fun (a : Associates α) ↦ Irreducible a)) b).prod
rw₄ :
  (Multiset.map (Subtype.val (p := fun (a : Associates α) ↦ Irreducible a)) a +
        Multiset.map (Subtype.val (p := fun (a : Associates α) ↦ Irreducible a)) b).prod =
    (Multiset.map (Subtype.val (p := fun (a : Associates α) ↦ Irreducible a)) a).prod *
      (Multiset.map (Subtype.val (p := fun (a : Associates α) ↦ Irreducible a)) b).prod
rw₅ rw₆ :
  (Multiset.map (Subtype.val (p := fun (a : Associates α) ↦ Irreducible a)) a).prod *
      (Multiset.map (Subtype.val (p := fun (a : Associates α) ↦ Irreducible a)) b).prod =
    (Multiset.map (Subtype.val (p := fun (a : Associates α) ↦ Irreducible a)) a).prod *
      (Multiset.map (Subtype.val (p := fun (a : Associates α) ↦ Irreducible a)) b).prod
⊢ ((↑a : WithTop (Multiset { a : Associates α // Irreducible a })) +
        (↑b : WithTop (Multiset { a : Associates α // Irreducible a }))).prod =
    FactorSet.prod (↑a : WithTop (Multiset { a : Associates α // Irreducible a })) *
      FactorSet.prod (↑b : WithTop (Multiset { a : Associates α // Irreducible a }))

Tactic:
rw [← FactorSet.coe_add, prod_coe, prod_coe, prod_coe, Multiset.map_add, Multiset.prod_add]

Premises used: Multiset.prod_add, Associates.FactorSet.coe_add, Multiset.map_add, Associates.prod_coe
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
b : FactorSet α
h : ⊤ ≤ b
⊢ b = ⊤

Tactic:
have : b = ⊤ := top_unique h
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
b : FactorSet α
h : ⊤ ≤ b
this : b = ⊤
rw : LE.le.{u_1} (α := Associates α) (FactorSet.prod ⊤) (FactorSet.prod ⊤)
rw₁ rw₂ : LE.le.{u_1} (α := Associates α) 0 0
⊢ FactorSet.prod ⊤ ≤ b.prod

Tactic:
rw [this, prod_top]

Premises used: Associates.prod_top
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
a : FactorSet α
h : a ≤ ⊤
⊢ a.prod ≤ FactorSet.prod ⊤

Tactic:
simp
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
inst_2 : Nontrivial α
p : WithTop (Multiset { a : Associates α // Irreducible a })
top : Eq.{u_1 + 1} (α := Associates α) (prod ⊤) 0 ↔ Eq.{u_1 + 1} (α := FactorSet α) ⊤ ⊤
coe :
  ∀ (a : Multiset { a : Associates α // Irreducible a }),
    prod (↑a : WithTop (Multiset { a : Associates α // Irreducible a })) = 0 ↔
      (↑a : WithTop (Multiset { a : Associates α // Irreducible a })) = ⊤
⊢ prod p = 0 ↔ p = ⊤

Tactic:
induction p
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
inst_2 : Nontrivial α
⊢ Eq.{u_1 + 1} (α := Associates α) (prod ⊤) 0 ↔ Eq.{u_1 + 1} (α := FactorSet α) ⊤ ⊤

Tactic:
simp only [Associates.prod_top]

Premises used: Associates.prod_top
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
inst_2 : Nontrivial α
a : Multiset { a : Associates α // Irreducible a }
coe : ∀ (x : { a : Associates α // Irreducible a }), ¬(x ∈ a ∧ (↑x : Associates α) = 0)
⊢ prod (↑a : WithTop (Multiset { a : Associates α // Irreducible a })) = 0 ↔
    (↑a : WithTop (Multiset { a : Associates α // Irreducible a })) = ⊤

Tactic:
rw [prod_coe, Multiset.prod_eq_zero_iff, Multiset.mem_map, eq_false WithTop.coe_ne_top,
      iff_false, not_exists]

Premises used: eq_false, iff_false, Multiset.mem_map, Multiset.prod_eq_zero_iff, not_exists, WithTop.coe_ne_top, Associates.prod_coe
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
inst_2 : Nontrivial α
a : Multiset { a : Associates α // Irreducible a }
⊢ ∀ (x : { a : Associates α // Irreducible a }), ¬(x ∈ a ∧ (↑x : Associates α) = 0)

Tactic:
fun a => not_and_of_not_right _ a.prop.ne_zero

Premises used: Membership.mem, not_and_of_not_right, Subtype.prop, Irreducible.ne_zero
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
inst_2 : Nontrivial α
a : Multiset { a : Associates α // Irreducible a }
⊢ ∀ (x : { a : Associates α // Irreducible a }), ¬(x ∈ a ∧ (↑x : Associates α) = 0)

Tactic:
exact fun a => not_and_of_not_right _ a.prop.ne_zero

Premises used: not_and_of_not_right
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : DecidableEq (Associates α)
inst_2 : (p : Associates α) → Decidable (Irreducible p)
p : Associates α
hp : Irreducible p
s : Multiset { a : Associates α // Irreducible a }
⊢ p.count (↑s : WithTop (Multiset { a : Associates α // Irreducible a })) =
    Multiset.count (Subtype.mk (p := fun (a : Associates α) ↦ Irreducible a) p hp) s

Tactic:
simp only [count, dif_pos hp, bcount]

Premises used: Associates.count, dif_pos, Associates.bcount
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : DecidableEq (Associates α)
inst_2 : (p : Associates α) → Decidable (Irreducible p)
p : Associates α
hp : Irreducible p
⊢ p.count 0 = 0

Tactic:
simp only [count, dif_pos hp, bcount, Multiset.count_zero]

Premises used: Associates.count, dif_pos, Multiset.count_zero, Associates.bcount
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : DecidableEq (Associates α)
inst_2 : (p : Associates α) → Decidable (Irreducible p)
p : Associates α
hp : ¬Irreducible p
⊢ p.count = 0

Tactic:
dif_neg hp

Premises used: Associates.count, dif_neg
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
p : Associates α
s : FactorSet α
⊢ FactorSetMem s p = (p ∈ s)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
p : Associates α
hp : Irreducible p
split_ifs : BfactorSetMem (Subtype.mk (p := fun (a : Associates α) ↦ Irreducible a) p hp) ⊤
⊢ if hp : Irreducible p then BfactorSetMem (Subtype.mk (p := fun (a : Associates α) ↦ Irreducible a) p hp) ⊤ else False

Tactic:
split_ifs
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
p : Associates α
hp : Irreducible p
⊢ BfactorSetMem (Subtype.mk (p := fun (a : Associates α) ↦ Irreducible a) p hp) ⊤

Tactic:
trivial

Premises used: Associates.BfactorSetMem, trivial
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
p : Associates α
hp : Irreducible p
⊢ BfactorSetMem (Subtype.mk (p := fun (a : Associates α) ↦ Irreducible a) p hp) ⊤

Tactic:
exact trivial

Premises used: trivial
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
p : Associates α
hp : Irreducible p
l : Multiset { a : Associates α // Irreducible a }
split_ifs :
  BfactorSetMem (Subtype.mk (p := fun (a : Associates α) ↦ Irreducible a) p hp)
      (↑l : WithTop (Multiset { a : Associates α // Irreducible a })) ↔
    l.Mem (Subtype.mk (p := Irreducible) p hp)
⊢ (if hp : Irreducible p then
      BfactorSetMem (Subtype.mk (p := fun (a : Associates α) ↦ Irreducible a) p hp)
        (↑l : WithTop (Multiset { a : Associates α // Irreducible a }))
    else False) ↔
    l.Mem (Subtype.mk (p := Irreducible) p hp)

Tactic:
split_ifs
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
p : Associates α
hp : Irreducible p
l : Multiset { a : Associates α // Irreducible a }
⊢ BfactorSetMem (Subtype.mk (p := fun (a : Associates α) ↦ Irreducible a) p hp)
      (↑l : WithTop (Multiset { a : Associates α // Irreducible a })) ↔
    l.Mem (Subtype.mk (p := Irreducible) p hp)

Tactic:
rfl
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
p : Associates α
hp : ¬Irreducible p
s : FactorSet α
h : p ∈ s
rwa : ∀ (h : FactorSetMem s p), False
rwa₁ :
  ∀
    (h :
      if hp : Irreducible p then BfactorSetMem (Subtype.mk (p := fun (a : Associates α) ↦ Irreducible a) p hp) s
      else False),
    False
rwa₂ rwa₃ rwa₄ rwa₅ : ∀ (h : False), False
⊢ False

Tactic:
rwa [← factorSetMem_eq_mem, FactorSetMem, dif_neg hp] at h

Premises used: Associates.factorSetMem_eq_mem, Associates.FactorSetMem, dif_neg
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
p : Associates α
s : FactorSet α
h : p ∈ s
⊢ Irreducible p

Tactic:
by_contra fun hp ↦ reducible_notMem_factorSet hp s h

Premises used: Associates.reducible_notMem_factorSet, by_contra
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : Nontrivial α
p q : WithTop (Multiset { a : Associates α // Irreducible a })
h : prod p = prod q
top : ∀ (h : prod ⊤ = prod q), ⊤ = q
coe :
  ∀ (a : Multiset { a : Associates α // Irreducible a })
    (h : prod (↑a : WithTop (Multiset { a : Associates α // Irreducible a })) = prod q),
    (↑a : WithTop (Multiset { a : Associates α // Irreducible a })) = q
⊢ p = q

Tactic:
induction p
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : Nontrivial α
q : WithTop (Multiset { a : Associates α // Irreducible a })
h : prod ⊤ = prod q
top : ∀ (h : Eq.{u_1 + 1} (α := Associates α) (prod ⊤) (prod ⊤)), Eq.{u_1 + 1} (α := FactorSet α) ⊤ ⊤
top₁ :
  ∀ (a : Multiset { a : Associates α // Irreducible a })
    (h : prod ⊤ = prod (↑a : WithTop (Multiset { a : Associates α // Irreducible a }))),
    ⊤ = (↑a : WithTop (Multiset { a : Associates α // Irreducible a }))
⊢ ⊤ = q

Tactic:
induction q
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : Nontrivial α
q : WithTop (Multiset { a : Associates α // Irreducible a })
a : Multiset { a : Associates α // Irreducible a }
h : prod (↑a : WithTop (Multiset { a : Associates α // Irreducible a })) = prod q
coe :
  ∀ (h : prod (↑a : WithTop (Multiset { a : Associates α // Irreducible a })) = prod ⊤),
    (↑a : WithTop (Multiset { a : Associates α // Irreducible a })) = ⊤
coe₁ :
  ∀ (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 : WithTop (Multiset { a : Associates α // Irreducible a })) =
      (↑a_1 : WithTop (Multiset { a : Associates α // Irreducible a }))
⊢ (↑a : WithTop (Multiset { a : Associates α // Irreducible a })) = q

Tactic:
induction q
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : Nontrivial α
h : Eq.{u_1 + 1} (α := Associates α) (prod ⊤) (prod ⊤)
⊢ Eq.{u_1 + 1} (α := FactorSet α) ⊤ ⊤

Tactic:
rfl
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : Nontrivial α
a : Multiset { a : Associates α // Irreducible a }
h : prod ⊤ = prod (↑a : WithTop (Multiset { a : Associates α // Irreducible a }))
top : (↑a : WithTop (Multiset { a : Associates α // Irreducible a })) = ⊤
top₁ : prod (↑a : WithTop (Multiset { a : Associates α // Irreducible a })) = 0
top₂ : Eq.{u_1 + 1} (α := Associates α) (prod ⊤) 0
top₃ top₄ : Eq.{u_1 + 1} (α := Associates α) 0 0
⊢ ⊤ = (↑a : WithTop (Multiset { a : Associates α // Irreducible a }))

Tactic:
rw [eq_comm, ← FactorSet.prod_eq_zero_iff, ← h, Associates.prod_top]

Premises used: Associates.prod_top, eq_comm, Associates.FactorSet.prod_eq_zero_iff
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : Nontrivial α
a : Multiset { a : Associates α // Irreducible a }
h : prod (↑a : WithTop (Multiset { a : Associates α // Irreducible a })) = prod ⊤
coe : prod (↑a : WithTop (Multiset { a : Associates α // Irreducible a })) = 0
coe₁ : Eq.{u_1 + 1} (α := Associates α) (prod ⊤) 0
coe₂ coe₃ : Eq.{u_1 + 1} (α := Associates α) 0 0
⊢ (↑a : WithTop (Multiset { a : Associates α // Irreducible a })) = ⊤

Tactic:
rw [← FactorSet.prod_eq_zero_iff, h, Associates.prod_top]

Premises used: Associates.prod_top, Associates.FactorSet.prod_eq_zero_iff
-- 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 }))
coe : a = a_1
⊢ (↑a : WithTop (Multiset { a : Associates α // Irreducible a })) =
    (↑a_1 : WithTop (Multiset { a : Associates α // Irreducible a }))

Tactic:
congr 1
-- 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 }))
coe :
  Eq (α := Multiset (Associates α))
    (Multiset.map (fun (a : { a : Associates α // Irreducible a }) ↦ (↑a : Associates α)) a)
    (Multiset.map (fun (a : { a : Associates α // Irreducible a }) ↦ (↑a : Associates α)) a_1)
⊢ a = a_1

Tactic:
rw [← Multiset.map_eq_map Subtype.coe_injective]

Premises used: Multiset.map_eq_map, Subtype.coe_injective
-- 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 }))
apply : ∀ a_2 ∈ Multiset.map (Subtype.val (p := fun (a : Associates α) ↦ Irreducible a)) a, Irreducible a_2
apply₁ : ∀ a ∈ Multiset.map (Subtype.val (p := fun (a : Associates α) ↦ Irreducible a)) a_1, Irreducible a
⊢ Eq (α := Multiset (Associates α))
    (Multiset.map (fun (a : { a : Associates α // Irreducible a }) ↦ (↑a : Associates α)) a)
    (Multiset.map (fun (a : { a : Associates α // Irreducible a }) ↦ (↑a : Associates α)) a_1)

Tactic:
apply unique' _ _ h

Premises used: Associates.unique'
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : Nontrivial α
a_1 a_2 : Multiset { a : Associates α // Irreducible a }
h :
  prod (↑a_1 : WithTop (Multiset { a : Associates α // Irreducible a })) =
    prod (↑a_2 : WithTop (Multiset { a : Associates α // Irreducible a }))
a : Associates α
ha : a ∈ Multiset.map (Subtype.val (p := fun (a : Associates α) ↦ Irreducible a)) a_1
obtain :
  ∀ (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),
    Irreducible (↑(Subtype.mk (p := fun (a : Associates α) ↦ Irreducible a) a' irred) : Associates α)
⊢ Irreducible a

Tactic:
obtain ⟨⟨a', irred⟩, -, rfl⟩ := Multiset.mem_map.mp ha

Premises used: Multiset.mem_map, Iff.mp, rfl
-- 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
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 α
inst_2 : Nontrivial α
a_1 a_2 : Multiset { a : Associates α // Irreducible a }
h :
  prod (↑a_1 : WithTop (Multiset { a : Associates α // Irreducible a })) =
    prod (↑a_2 : WithTop (Multiset { a : Associates α // Irreducible a }))
a : Associates α
ha : a ∈ Multiset.map (Subtype.val (p := fun (a : Associates α) ↦ Irreducible a)) a_2
obtain :
  ∀ (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_2),
    Irreducible (↑(Subtype.mk (p := fun (a : Associates α) ↦ Irreducible a) a' irred) : Associates α)
⊢ Irreducible a

Tactic:
obtain ⟨⟨a', irred⟩, -, rfl⟩ := Multiset.mem_map.mp ha

Premises used: Multiset.mem_map, Iff.mp, rfl