awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
pf : ∀ (a : α), a ≠ 0 → ∃ (f : Multiset α), (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
a b : α
ane0 : a ≠ 0
c : α
hc : ¬IsUnit c
b_eq : b = a * c
h : ¬b = 0
cne0 : c ≠ 0
h₁ : (Classical.choose (p := fun (x : Multiset α) ↦ (∀ b ∈ x, Prime b) ∧ x.prod ~ᵤ a) ⋯).prod ~ᵤ a
h₂ : (Classical.choose (p := fun (x : Multiset α) ↦ (∀ b ∈ x, Prime b) ∧ x.prod ~ᵤ c) ⋯).prod ~ᵤ c
⊢ (Classical.choose (p := fun (x : Multiset α) ↦ (∀ b ∈ x, Prime b) ∧ x.prod ~ᵤ a) ⋯).prod *
      (Classical.choose (p := fun (x : Multiset α) ↦ (∀ b ∈ x, Prime b) ∧ x.prod ~ᵤ c) ⋯).prod ~ᵤ
    a * c

Tactic:
apply Associated.mul_mul

Premises used: Associated.mul_mul
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
pf : ∀ (a : α), a ≠ 0 → ∃ (f : Multiset α), (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
a b : α
ane0 : a ≠ 0
c : α
hc : ¬IsUnit c
b_eq : b = a * c
h : ¬b = 0
cne0 : c ≠ 0
apply : a ≠ 0
⊢ (Classical.choose (p := fun (x : Multiset α) ↦ (∀ b ∈ x, Prime b) ∧ x.prod ~ᵤ a) ⋯).prod ~ᵤ a

Tactic:
apply (Classical.choose_spec (pf _ _)).2

Premises used: Classical.choose_spec, And.right
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
pf : ∀ (a : α), a ≠ 0 → ∃ (f : Multiset α), (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
a b : α
ane0 : a ≠ 0
c : α
hc : ¬IsUnit c
b_eq : b = a * c
h : ¬b = 0
cne0 apply : c ≠ 0
⊢ (Classical.choose (p := fun (x : Multiset α) ↦ (∀ b ∈ x, Prime b) ∧ x.prod ~ᵤ c) ⋯).prod ~ᵤ c

Tactic:
apply (Classical.choose_spec (pf _ _)).2

Premises used: Classical.choose_spec, And.right
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
pf : ∀ (a : α), a ≠ 0 → ∃ (f : Multiset α), (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
a b : α
ane0 : a ≠ 0
c : α
hc : ¬IsUnit c
b_eq : b = a * c
h : ¬b = 0
cne0 : c ≠ 0
⊢ a ≠ 0

Tactic:
assumption
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
pf : ∀ (a : α), a ≠ 0 → ∃ (f : Multiset α), (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
a b : α
ane0 : a ≠ 0
c : α
hc : ¬IsUnit c
b_eq : b = a * c
h : ¬b = 0
cne0 : c ≠ 0
⊢ c ≠ 0

Tactic:
assumption
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
pf : ∀ (a : α), a ≠ 0 → ∃ (f : Multiset α), (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
a b : α
ane0 : a ≠ 0
c : α
hc : ¬IsUnit c
b_eq : b = a * c
h : ¬b = 0
cne0 : c ≠ 0
rw : b ~ᵤ (Classical.choose (p := fun (x : Multiset α) ↦ (∀ b ∈ x, Prime b) ∧ x.prod ~ᵤ b) ⋯).prod
⊢ a * c ~ᵤ (Classical.choose (p := fun (x : Multiset α) ↦ (∀ b ∈ x, Prime b) ∧ x.prod ~ᵤ b) ⋯).prod

Tactic:
rw [← b_eq]
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
pf : ∀ (a : α), a ≠ 0 → ∃ (f : Multiset α), (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
a b : α
ane0 : a ≠ 0
c : α
hc : ¬IsUnit c
b_eq : b = a * c
h : ¬b = 0
cne0 : c ≠ 0
apply : b ≠ 0
⊢ b ~ᵤ (Classical.choose (p := fun (x : Multiset α) ↦ (∀ b ∈ x, Prime b) ∧ x.prod ~ᵤ b) ⋯).prod

Tactic:
apply (Classical.choose_spec (pf _ _)).2.symm

Premises used: Classical.choose_spec, Associated.symm, And.right
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
pf : ∀ (a : α), a ≠ 0 → ∃ (f : Multiset α), (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
a b : α
ane0 : a ≠ 0
c : α
hc : ¬IsUnit c
b_eq : b = a * c
h : ¬b = 0
cne0 : c ≠ 0
⊢ b ≠ 0

Tactic:
assumption
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
pf : ∀ (a : α), a ≠ 0 → ∃ (f : Multiset α), (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
p : α
pos : ∀ (hp0 : p = 0), Irreducible p ↔ Prime p
neg : ∀ (hp0 : ¬p = 0), Irreducible p ↔ Prime p
⊢ Irreducible p ↔ Prime p

Tactic:
by_cases hp0 : p = 0
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
pf : ∀ (a : α), a ≠ 0 → ∃ (f : Multiset α), (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
p : α
hp0 : p = 0
⊢ Irreducible p ↔ Prime p

Tactic:
simp [hp0]
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
pf : ∀ (a : α), a ≠ 0 → ∃ (f : Multiset α), (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
p : α
hp0 : ¬p = 0
⊢ Irreducible p ↔ Prime p

Tactic:
⟨fun h => ?_, Prime.irreducible⟩

Premises used: Prime.irreducible, Iff.intro
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
pf : ∀ (a : α), a ≠ 0 → ∃ (f : Multiset α), (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
p : α
hp0 : ¬p = 0
neg : ∀ (h : Irreducible p), Prime p
⊢ Irreducible p ↔ Prime p

Tactic:
refine ⟨fun h => ?_, Prime.irreducible⟩
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
pf : ∀ (a : α), a ≠ 0 → ∃ (f : Multiset α), (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
p : α
hp0 : ¬p = 0
h : Irreducible p
neg : ∀ (f : Multiset α) (hf : (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ p), Prime p
⊢ Prime p

Tactic:
obtain ⟨f, hf⟩ := pf p hp0
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
pf : ∀ (a : α), a ≠ 0 → ∃ (f : Multiset α), (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
p : α
hp0 : ¬p = 0
h : Irreducible p
f : Multiset α
hf : (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ p
neg :
  ∀ (q : α) (hq : p ~ᵤ q) (hf : (∀ (b : α), Membership.mem (γ := Multiset α) {q} b → Prime b) ∧ Multiset.prod {q} ~ᵤ p),
    Prime p
⊢ Prime p

Tactic:
obtain ⟨q, hq, rfl⟩ := prime_factors_irreducible h hf

Premises used: prime_factors_irreducible, rfl
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
pf : ∀ (a : α), a ≠ 0 → ∃ (f : Multiset α), (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
p : α
hp0 : ¬p = 0
h : Irreducible p
q : α
hq : p ~ᵤ q
hf : (∀ (b : α), Membership.mem (γ := Multiset α) {q} b → Prime b) ∧ Multiset.prod {q} ~ᵤ p
neg : Prime q
⊢ Prime p

Tactic:
rw [hq.prime_iff]

Premises used: Associated.prime_iff
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
pf : ∀ (a : α), a ≠ 0 → ∃ (f : Multiset α), (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
p : α
hp0 : ¬p = 0
h : Irreducible p
q : α
hq : p ~ᵤ q
hf : (∀ (b : α), Membership.mem (γ := Multiset α) {q} b → Prime b) ∧ Multiset.prod {q} ~ᵤ p
⊢ Prime q

Tactic:
hf.1 q (Multiset.mem_singleton_self _)

Premises used: And.left, Multiset.mem_singleton_self
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
pf : ∀ (a : α), a ≠ 0 → ∃ (f : Multiset α), (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
p : α
hp0 : ¬p = 0
h : Irreducible p
q : α
hq : p ~ᵤ q
hf : (∀ (b : α), Membership.mem (γ := Multiset α) {q} b → Prime b) ∧ Multiset.prod {q} ~ᵤ p
⊢ Prime q

Tactic:
exact hf.1 q (Multiset.mem_singleton_self _)

Premises used: And.left, Multiset.mem_singleton_self
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
pf : ∀ (a : α), a ≠ 0 → ∃ (f : Multiset α), (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
⊢ UniqueFactorizationMonoid α

Tactic:
{ WfDvdMonoid.of_exists_prime_factors pf with
    irreducible_iff_prime := irreducible_iff_prime_of_exists_prime_factors pf }

Premises used: irreducible_iff_prime_of_exists_prime_factors, UniqueFactorizationMonoid.mk, WfDvdMonoid.of_exists_prime_factors
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
⊢ UniqueFactorizationMonoid α ↔ ∀ (a : α), a ≠ 0 → ∃ (f : Multiset α), (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a

Tactic:
⟨fun h => @UniqueFactorizationMonoid.exists_prime_factors _ _ h,
    UniqueFactorizationMonoid.of_exists_prime_factors⟩

Premises used: UniqueFactorizationMonoid.exists_prime_factors, Iff.intro, UniqueFactorizationMonoid.of_exists_prime_factors
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoidWithZero α
inst_1 : CommMonoidWithZero β
e : α ≃* β
hα : UniqueFactorizationMonoid α
⊢ IsCancelMulZero β

Tactic:
have := e.isCancelMulZero_iff.mp inferInstance
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoidWithZero α
inst_1 : CommMonoidWithZero β
e : α ≃* β
hα : UniqueFactorizationMonoid α
this : IsCancelMulZero β
rw :
  ∀ (hα : ∀ (a : α), a ≠ 0 → ∃ (f : Multiset α), (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a) (this : IsCancelMulZero β) (a : β),
    a ≠ 0 → ∃ (f : Multiset β), (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
⊢ UniqueFactorizationMonoid β

Tactic:
rw [UniqueFactorizationMonoid.iff_exists_prime_factors] at hα ⊢

Premises used: UniqueFactorizationMonoid.iff_exists_prime_factors
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoidWithZero α
inst_1 : CommMonoidWithZero β
e : α ≃* β
hα : ∀ (a : α), a ≠ 0 → ∃ (f : Multiset α), (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
this : IsCancelMulZero β
a : β
ha : a ≠ 0
h : Eq.{u_1 + 1} (α := α) ((e.symm : (a : β) → α) a : α) (0 : α)
⊢ Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) 0 : β) (0 : β)

Tactic:
map_zero e

Premises used: map_zero
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoidWithZero α
inst_1 : CommMonoidWithZero β
e : α ≃* β
hα : ∀ (a : α), a ≠ 0 → ∃ (f : Multiset α), (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
this : IsCancelMulZero β
a : β
ha : a ≠ 0
h : Eq.{u_1 + 1} (α := α) ((e.symm : (a : β) → α) a : α) (0 : α)
h₁ : (e : (a : α) → β) 0 = a
⊢ a = 0

Tactic:
convert! ← map_zero e

Premises used: map_zero
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoidWithZero α
inst_1 : CommMonoidWithZero β
e : α ≃* β
hα : ∀ (a : α), a ≠ 0 → ∃ (f : Multiset α), (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
this : IsCancelMulZero β
a : β
ha : a ≠ 0
h : Eq.{u_1 + 1} (α := α) ((e.symm : (a : β) → α) a : α) (0 : α)
⊢ (e : (a : α) → β) 0 = a

Tactic:
simp [← h]
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoidWithZero α
inst_1 : CommMonoidWithZero β
e : α ≃* β
hα : ∀ (a : α), a ≠ 0 → ∃ (f : Multiset α), (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
this : IsCancelMulZero β
a : β
ha : a ≠ 0
obtain :
  ∀ (w : Multiset α) (hp : ∀ b ∈ w, Prime b) (u : αˣ) (h : w.prod * (↑u : α) = (e.symm : (a : β) → α) a),
    ∃ (f : Multiset β), (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
⊢ ∃ (f : Multiset β), (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a

Tactic:
obtain ⟨w, hp, u, h⟩ :=
    hα (e.symm a) fun h =>
      ha <| by
        convert! ← map_zero e
        simp [← h]

Premises used: MulEquiv.symm, DFunLike.coe
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoidWithZero α
inst_1 : CommMonoidWithZero β
e : α ≃* β
hα : ∀ (a : α), a ≠ 0 → ∃ (f : Multiset α), (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
this : IsCancelMulZero β
a : β
ha : a ≠ 0
w : Multiset α
hp : ∀ b ∈ w, Prime b
u : αˣ
h : w.prod * (↑u : α) = (e.symm : (a : β) → α) a
rw :
  HMul.hMul (α := β) (β := β) ((e : (a : α) → β) w.prod : β)
      ((↑((Units.map e.toMonoidHom : (a : αˣ) → βˣ) u) : β) : β) =
    a
rw₁ :
  HMul.hMul (α := β) (β := β) ((e : (a : α) → β) w.prod : β)
      ((↑(((Units.map (↑e : α →* β) : MonoidHom.{u_1, u_2} αˣ βˣ) : (a : αˣ) → βˣ) u) : β) : β) =
    a
rw₂ : HMul.hMul (α := β) (β := β) ((e : (a : α) → β) w.prod : β) (((↑e : α →* β) : (a : α) → β) (↑u : α) : β) = a
rw₃ : HMul.hMul (α := β) (β := β) ((e : (a : α) → β) w.prod : β) ((e : (a : α) → β) (↑u : α) : β) = a
rw₄ : (e : (a : α) → β) (w.prod * (↑u : α)) = a
rw₅ : (e : (a : α) → β) ((e.symm : (a : β) → α) a : α) = a
rw₆ rw₇ : a = a
⊢ HMul.hMul (α := β) (Multiset.prod (Multiset.map (⇑e : (a : α) → β) w))
      (↑((Units.map e.toMonoidHom : (a : αˣ) → βˣ) u) : β) =
    a

Tactic:
rw [Multiset.prod_hom, toMonoidHom_eq_coe, Units.coe_map, MonoidHom.coe_coe, ← map_mul e, h,
          apply_symm_apply]

Premises used: MulEquiv.toMonoidHom_eq_coe, Units.coe_map, MonoidHom.coe_coe, map_mul, Multiset.prod_hom, MulEquiv.apply_symm_apply
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoidWithZero α
inst_1 : CommMonoidWithZero β
e : α ≃* β
hα : ∀ (a : α), a ≠ 0 → ∃ (f : Multiset α), (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
this : IsCancelMulZero β
a : β
ha : a ≠ 0
w : Multiset α
hp : ∀ b ∈ w, Prime b
u : αˣ
h : w.prod * (↑u : α) = (e.symm : (a : β) → α) a
⊢ ∃ (f : Multiset β), (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a

Tactic:
exact
    ⟨w.map e, fun b hb =>
        let ⟨c, hc, he⟩ := Multiset.mem_map.1 hb
        he ▸ (prime_iff e).2 (hp c hc),
        Units.map e.toMonoidHom u,
      by
        rw [Multiset.prod_hom, toMonoidHom_eq_coe, Units.coe_map, MonoidHom.coe_coe, ← map_mul e, h,
          apply_symm_apply]⟩
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoidWithZero α
inst_1 : CommMonoidWithZero β
e : α ≃* β
⊢ UniqueFactorizationMonoid α ↔ UniqueFactorizationMonoid β

Tactic:
⟨e.uniqueFactorizationMonoid, e.symm.uniqueFactorizationMonoid⟩

Premises used: Iff.intro, MulEquiv.uniqueFactorizationMonoid, MulEquiv.symm
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
eif : ∀ (a : α), a ≠ 0 → ∃ (f : Multiset α), (∀ b ∈ f, Irreducible b) ∧ f.prod ~ᵤ a
uif :
  ∀ (f g : Multiset α),
    (∀ x ∈ f, Irreducible x) → (∀ x ∈ g, Irreducible x) → f.prod ~ᵤ g.prod → Multiset.Rel Associated f g
⊢ ∀ (a : α), a ≠ 0 → ∃ (f : Multiset α), (∀ b ∈ f, Irreducible b) ∧ f.prod ~ᵤ a

Tactic:
eif
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
eif : ∀ (a : α), a ≠ 0 → ∃ (f : Multiset α), (∀ b ∈ f, Irreducible b) ∧ f.prod ~ᵤ a
uif :
  ∀ (f g : Multiset α),
    (∀ x ∈ f, Irreducible x) → (∀ x ∈ g, Irreducible x) → f.prod ~ᵤ g.prod → Multiset.Rel Associated f g
h : ∀ (a : α), a ≠ 0 → ∀ (x : Multiset α), ∀ a ∈ x, Prime a ↔ Irreducible a
⊢ ∀ (a : α), a ≠ 0 → ∃ (f : Multiset α), (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a

Tactic:
convert! eif using 7
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
eif : ∀ (a : α), a ≠ 0 → ∃ (f : Multiset α), (∀ b ∈ f, Irreducible b) ∧ f.prod ~ᵤ a
uif :
  ∀ (f g : Multiset α),
    (∀ x ∈ f, Irreducible x) → (∀ x ∈ g, Irreducible x) → f.prod ~ᵤ g.prod → Multiset.Rel Associated f g
a : α
h : a ≠ 0
x : Multiset α
a_1 : α
h_1 : a_1 ∈ x
⊢ Prime a_1 ↔ Irreducible a_1

Tactic:
simp_rw [irreducible_iff_prime_of_existsUnique_irreducible_factors eif uif]

Premises used: irreducible_iff_prime_of_existsUnique_irreducible_factors
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
a b : R
ha : a ≠ 0
⊢ IsRelPrime a b ↔ ∀ ⦃d : R⦄, d ∣ a → d ∣ b → ¬Prime d

Tactic:
⟨fun h _ ha hb ↦ (·.not_unit <| h ha hb), fun h ↦ WfDvdMonoid.isRelPrime_of_no_irreducible_factors
    (ha ·.1) fun _ irr ha hb ↦ h ha hb (UniqueFactorizationMonoid.irreducible_iff_prime.mp irr)⟩

Premises used: WfDvdMonoid.isRelPrime_of_no_irreducible_factors, UniqueFactorizationMonoid.irreducible_iff_prime, Prime.not_unit, And.left, Iff.intro, Iff.mp
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
a b c : R
ha : a ≠ 0
h : ∀ ⦃d : R⦄, d ∣ a → d ∣ c → ¬Prime d
⊢ a ∣ b * c → a ∣ b

Tactic:
((isRelPrime_iff_no_prime_factors ha).mpr h).dvd_of_dvd_mul_right

Premises used: Iff.mpr, IsRelPrime.dvd_of_dvd_mul_right, UniqueFactorizationMonoid.isRelPrime_iff_no_prime_factors
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
a b c : R
ha : a ≠ 0
no_factors : ∀ {d : R}, d ∣ a → d ∣ b → ¬Prime d
⊢ a ∣ b * c → a ∣ c

Tactic:
simpa [mul_comm b c] using dvd_of_dvd_mul_left_of_no_prime_factors ha @no_factors

Premises used: UniqueFactorizationMonoid.dvd_of_dvd_mul_left_of_no_prime_factors, mul_comm
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
a : R
⊢ a ≠ 0 → ∀ (b : R), ∃ (a' : R) (b' : R) (c' : R), IsRelPrime a' b' ∧ c' * a' = a ∧ c' * b' = b

Tactic:
induction_on_prime a ?_ ?_ ?_

Premises used: UniqueFactorizationMonoid.induction_on_prime
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
a : R
refine_1 :
  Ne.{u_2 + 1} (α := R) 0 0 → ∀ (b : R), ∃ (a' : R) (b' : R) (c' : R), IsRelPrime a' b' ∧ c' * a' = 0 ∧ c' * b' = b
refine_2 :
  ∀ (x : R), IsUnit x → x ≠ 0 → ∀ (b : R), ∃ (a' : R) (b' : R) (c' : R), IsRelPrime a' b' ∧ c' * a' = x ∧ c' * b' = b
refine_3 :
  ∀ (a p : R),
    a ≠ 0 →
      Prime p →
        (a ≠ 0 → ∀ (b : R), ∃ (a' : R) (b' : R) (c' : R), IsRelPrime a' b' ∧ c' * a' = a ∧ c' * b' = b) →
          p * a ≠ 0 → ∀ (b : R), ∃ (a' : R) (b' : R) (c' : R), IsRelPrime a' b' ∧ c' * a' = p * a ∧ c' * b' = b
⊢ a ≠ 0 → ∀ (b : R), ∃ (a' : R) (b' : R) (c' : R), IsRelPrime a' b' ∧ c' * a' = a ∧ c' * b' = b

Tactic:
refine induction_on_prime a ?_ ?_ ?_
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
a : R
h : Ne.{u_2 + 1} (α := R) 0 0
b : R
⊢ ∃ (a' : R) (b' : R) (c' : R), IsRelPrime a' b' ∧ c' * a' = 0 ∧ c' * b' = b

Tactic:
contradiction
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
a_1 a : R
a_unit : IsUnit a
refine_2 : a ≠ 0 → ∀ (b : R), ∃ (a' : R) (b' : R) (c' : R), IsRelPrime a' b' ∧ c' * a' = a ∧ c' * b' = b
⊢ a ≠ 0 → ∀ (b : R), ∃ (a' : R) (b' : R) (c' : R), IsRelPrime a' b' ∧ c' * a' = a ∧ c' * b' = b

Tactic:
_
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
a_1 a : R
a_unit : IsUnit a
h_1 : a ≠ 0
b : R
h : IsRelPrime a b ∧ 1 * a = a ∧ 1 * b = b
⊢ ∃ (a' : R) (b' : R) (c' : R), IsRelPrime a' b' ∧ c' * a' = a ∧ c' * b' = b

Tactic:
use a, b, 1
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
a_1 a : R
a_unit : IsUnit a
h_1 : a ≠ 0
b : R
h : IsRelPrime a b
h₁ : 1 * a = a ∧ 1 * b = b
⊢ IsRelPrime a b ∧ 1 * a = a ∧ 1 * b = b

Tactic:
constructor
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
a_1 a : R
a_unit : IsUnit a
h_1 : a ≠ 0
b p : R
p_dvd_a : p ∣ a
h : p ∣ b → IsUnit p
⊢ p ∣ b → IsUnit p

Tactic:
_
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
a_1 a : R
a_unit : IsUnit a
h : a ≠ 0
b p : R
p_dvd_a : p ∣ a
h_1 : p ∣ b
⊢ IsUnit p

Tactic:
isUnit_of_dvd_unit p_dvd_a a_unit

Premises used: isUnit_of_dvd_unit
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
a_1 a : R
a_unit : IsUnit a
h : a ≠ 0
b p : R
p_dvd_a : p ∣ a
h_1 : p ∣ b
⊢ IsUnit p

Tactic:
exact isUnit_of_dvd_unit p_dvd_a a_unit

Premises used: isUnit_of_dvd_unit
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
a_1 a : R
a_unit : IsUnit a
h : a ≠ 0
b : R
⊢ 1 * a = a ∧ 1 * b = b

Tactic:
simp
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
a_1 a p : R
a_ne_zero : a ≠ 0
p_prime : Prime p
ih_a : a ≠ 0 → ∀ (b : R), ∃ (a' : R) (b' : R) (c' : R), IsRelPrime a' b' ∧ c' * a' = a ∧ c' * b' = b
pa_ne_zero : p * a ≠ 0
b : R
pos : ∀ (h : p ∣ b), ∃ (a' : R) (b' : R) (c' : R), IsRelPrime a' b' ∧ c' * a' = p * a ∧ c' * b' = b
neg : ∀ (h : ¬p ∣ b), ∃ (a' : R) (b' : R) (c' : R), IsRelPrime a' b' ∧ c' * a' = p * a ∧ c' * b' = b
⊢ ∃ (a' : R) (b' : R) (c' : R), IsRelPrime a' b' ∧ c' * a' = p * a ∧ c' * b' = b

Tactic:
by_cases h : p ∣ b
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
a_1 a p : R
a_ne_zero : a ≠ 0
p_prime : Prime p
ih_a : a ≠ 0 → ∀ (b : R), ∃ (a' : R) (b' : R) (c' : R), IsRelPrime a' b' ∧ c' * a' = a ∧ c' * b' = b
pa_ne_zero : p * a ≠ 0
b : R
h : p ∣ b
pos : ∀ (b : R), ∃ (a' : R) (b' : R) (c' : R), IsRelPrime a' b' ∧ c' * a' = p * a ∧ c' * b' = p * b
⊢ ∃ (a' : R) (b' : R) (c' : R), IsRelPrime a' b' ∧ c' * a' = p * a ∧ c' * b' = b

Tactic:
rcases h with ⟨b, rfl⟩

Premises used: rfl
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
a_1 a p : R
a_ne_zero : a ≠ 0
p_prime : Prime p
ih_a : a ≠ 0 → ∀ (b : R), ∃ (a' : R) (b' : R) (c' : R), IsRelPrime a' b' ∧ c' * a' = a ∧ c' * b' = b
pa_ne_zero : p * a ≠ 0
b : R
pos :
  ∀ (a' b' c' : R) (no_factor : IsRelPrime a' b') (ha' : c' * a' = a) (hb' : c' * b' = b),
    ∃ (a' : R) (b' : R) (c' : R), IsRelPrime a' b' ∧ c' * a' = p * a ∧ c' * b' = p * b
⊢ ∃ (a' : R) (b' : R) (c' : R), IsRelPrime a' b' ∧ c' * a' = p * a ∧ c' * b' = p * b

Tactic:
obtain ⟨a', b', c', no_factor, ha', hb'⟩ := ih_a a_ne_zero b
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
a_1 a p : R
a_ne_zero : a ≠ 0
p_prime : Prime p
ih_a : a ≠ 0 → ∀ (b : R), ∃ (a' : R) (b' : R) (c' : R), IsRelPrime a' b' ∧ c' * a' = a ∧ c' * b' = b
pa_ne_zero : p * a ≠ 0
b a' b' c' : R
no_factor : IsRelPrime a' b'
ha' : c' * a' = a
hb' : c' * b' = b
⊢ ∃ (a' : R) (b' : R) (c' : R), IsRelPrime a' b' ∧ c' * a' = p * a ∧ c' * b' = p * b

Tactic:
⟨a', b', p * c', @no_factor, ?_, ?_⟩

Premises used: HMul.hMul, And.intro, Exists.intro
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
a_1 a p : R
a_ne_zero : a ≠ 0
p_prime : Prime p
ih_a : a ≠ 0 → ∀ (b : R), ∃ (a' : R) (b' : R) (c' : R), IsRelPrime a' b' ∧ c' * a' = a ∧ c' * b' = b
pa_ne_zero : p * a ≠ 0
b a' b' c' : R
no_factor : IsRelPrime a' b'
ha' : c' * a' = a
hb' : c' * b' = b
pos : p * c' * a' = p * a
pos₁ : p * c' * b' = p * b
⊢ ∃ (a' : R) (b' : R) (c' : R), IsRelPrime a' b' ∧ c' * a' = p * a ∧ c' * b' = p * b

Tactic:
refine ⟨a', b', p * c', @no_factor, ?_, ?_⟩
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
a_1 a p : R
a_ne_zero : a ≠ 0
p_prime : Prime p
ih_a : a ≠ 0 → ∀ (b : R), ∃ (a' : R) (b' : R) (c' : R), IsRelPrime a' b' ∧ c' * a' = a ∧ c' * b' = b
pa_ne_zero : p * a ≠ 0
b a' b' c' : R
no_factor : IsRelPrime a' b'
ha' : c' * a' = a
hb' : c' * b' = b
pos : p * (c' * a') = p * a
pos₁ pos₂ : p * a = p * a
⊢ p * c' * a' = p * a

Tactic:
rw [mul_assoc, ha']

Premises used: mul_assoc