awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
p : α
this : DecidableEq α := Classical.decEq α
hpi : Irreducible p
a b : α
h : p ∣ a * b
x : α
hx : a * b = p * x
hab0 : ¬a * b = 0
hx0 : x ≠ 0
ha0 : a ≠ 0
⊢ b ≠ 0

Tactic:
have hb0 : b ≠ 0 := right_ne_zero_of_mul hab0
-- 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
p : α
this : DecidableEq α := Classical.decEq α
hpi : Irreducible p
a b : α
h : p ∣ a * b
x : α
hx : a * b = p * x
hab0 : ¬a * b = 0
hx0 : x ≠ 0
ha0 : a ≠ 0
hb0 : b ≠ 0
obtain : ∀ (fx : Multiset α) (hfx : (∀ b ∈ fx, Irreducible b) ∧ fx.prod ~ᵤ x), p ∣ a ∨ p ∣ b
⊢ p ∣ a ∨ p ∣ b

Tactic:
obtain ⟨fx, hfx⟩ := eif x hx0
-- 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
p : α
this : DecidableEq α := Classical.decEq α
hpi : Irreducible p
a b : α
h : p ∣ a * b
x : α
hx : a * b = p * x
hab0 : ¬a * b = 0
hx0 : x ≠ 0
ha0 : a ≠ 0
hb0 : b ≠ 0
fx : Multiset α
hfx : (∀ b ∈ fx, Irreducible b) ∧ fx.prod ~ᵤ x
obtain : ∀ (fa : Multiset α) (hfa : (∀ b ∈ fa, Irreducible b) ∧ fa.prod ~ᵤ a), p ∣ a ∨ p ∣ b
⊢ p ∣ a ∨ p ∣ b

Tactic:
obtain ⟨fa, hfa⟩ := eif a ha0
-- 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
p : α
this : DecidableEq α := Classical.decEq α
hpi : Irreducible p
a b : α
h : p ∣ a * b
x : α
hx : a * b = p * x
hab0 : ¬a * b = 0
hx0 : x ≠ 0
ha0 : a ≠ 0
hb0 : b ≠ 0
fx : Multiset α
hfx : (∀ b ∈ fx, Irreducible b) ∧ fx.prod ~ᵤ x
fa : Multiset α
hfa : (∀ b ∈ fa, Irreducible b) ∧ fa.prod ~ᵤ a
obtain : ∀ (fb : Multiset α) (hfb : (∀ b ∈ fb, Irreducible b) ∧ fb.prod ~ᵤ b), p ∣ a ∨ p ∣ b
⊢ p ∣ a ∨ p ∣ b

Tactic:
obtain ⟨fb, hfb⟩ := eif b hb0
-- 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
p : α
this : DecidableEq α := Classical.decEq α
hpi : Irreducible p
a b : α
h : p ∣ a * b
x : α
hx : a * b = p * x
hab0 : ¬a * b = 0
hx0 : x ≠ 0
ha0 : a ≠ 0
hb0 : b ≠ 0
fx : Multiset α
hfx : (∀ b ∈ fx, Irreducible b) ∧ fx.prod ~ᵤ x
fa : Multiset α
hfa : (∀ b ∈ fa, Irreducible b) ∧ fa.prod ~ᵤ a
fb : Multiset α
hfb : (∀ b ∈ fb, Irreducible b) ∧ fb.prod ~ᵤ b
a₁ : ∀ x ∈ p ::ₘ fx, Irreducible x
a₂ : ∀ x ∈ fa + fb, Irreducible x
a₃ : (p ::ₘ fx).prod ~ᵤ (fa + fb).prod
⊢ Multiset.Rel Associated (p ::ₘ fx) (fa + fb)

Tactic:
apply uif
-- 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
p : α
this : DecidableEq α := Classical.decEq α
hpi : Irreducible p
a b : α
h : p ∣ a * b
x : α
hx : a * b = p * x
hab0 : ¬a * b = 0
hx0 : x ≠ 0
ha0 : a ≠ 0
hb0 : b ≠ 0
fx : Multiset α
hfx : (∀ b ∈ fx, Irreducible b) ∧ fx.prod ~ᵤ x
fa : Multiset α
hfa : (∀ b ∈ fa, Irreducible b) ∧ fa.prod ~ᵤ a
fb : Multiset α
hfb : (∀ b ∈ fb, Irreducible b) ∧ fb.prod ~ᵤ b
⊢ ∀ x ∈ p ::ₘ fx, Irreducible x

Tactic:
fun i hi => (Multiset.mem_cons.1 hi).elim (fun hip => hip.symm ▸ hpi) (hfx.1 _)

Premises used: Eq.rec, Multiset.mem_cons, And.left, Iff.mp, Or.elim, Eq.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
p : α
this : DecidableEq α := Classical.decEq α
hpi : Irreducible p
a b : α
h : p ∣ a * b
x : α
hx : a * b = p * x
hab0 : ¬a * b = 0
hx0 : x ≠ 0
ha0 : a ≠ 0
hb0 : b ≠ 0
fx : Multiset α
hfx : (∀ b ∈ fx, Irreducible b) ∧ fx.prod ~ᵤ x
fa : Multiset α
hfa : (∀ b ∈ fa, Irreducible b) ∧ fa.prod ~ᵤ a
fb : Multiset α
hfb : (∀ b ∈ fb, Irreducible b) ∧ fb.prod ~ᵤ b
⊢ ∀ x ∈ p ::ₘ fx, Irreducible x

Tactic:
exact fun i hi => (Multiset.mem_cons.1 hi).elim (fun hip => hip.symm ▸ hpi) (hfx.1 _)

Premises used: Multiset.mem_cons, And.left, Iff.mp, Or.elim
-- 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
p : α
this : DecidableEq α := Classical.decEq α
hpi : Irreducible p
a b : α
h : p ∣ a * b
x : α
hx : a * b = p * x
hab0 : ¬a * b = 0
hx0 : x ≠ 0
ha0 : a ≠ 0
hb0 : b ≠ 0
fx : Multiset α
hfx : (∀ b ∈ fx, Irreducible b) ∧ fx.prod ~ᵤ x
fa : Multiset α
hfa : (∀ b ∈ fa, Irreducible b) ∧ fa.prod ~ᵤ a
fb : Multiset α
hfb : (∀ b ∈ fb, Irreducible b) ∧ fb.prod ~ᵤ b
⊢ ∀ x ∈ fa + fb, Irreducible x

Tactic:
fun i hi => (Multiset.mem_add.1 hi).elim (hfa.1 _) (hfb.1 _)

Premises used: Multiset.mem_add, And.left, Iff.mp, Or.elim
-- 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
p : α
this : DecidableEq α := Classical.decEq α
hpi : Irreducible p
a b : α
h : p ∣ a * b
x : α
hx : a * b = p * x
hab0 : ¬a * b = 0
hx0 : x ≠ 0
ha0 : a ≠ 0
hb0 : b ≠ 0
fx : Multiset α
hfx : (∀ b ∈ fx, Irreducible b) ∧ fx.prod ~ᵤ x
fa : Multiset α
hfa : (∀ b ∈ fa, Irreducible b) ∧ fa.prod ~ᵤ a
fb : Multiset α
hfb : (∀ b ∈ fb, Irreducible b) ∧ fb.prod ~ᵤ b
⊢ ∀ x ∈ fa + fb, Irreducible x

Tactic:
exact fun i hi => (Multiset.mem_add.1 hi).elim (hfa.1 _) (hfb.1 _)

Premises used: Multiset.mem_add, And.left, Iff.mp, Or.elim
-- 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
p : α
this : DecidableEq α := Classical.decEq α
hpi : Irreducible p
a b : α
h : p ∣ a * b
x : α
hx : a * b = p * x
hab0 : ¬a * b = 0
hx0 : x ≠ 0
ha0 : a ≠ 0
hb0 : b ≠ 0
fx : Multiset α
hfx : (∀ b ∈ fx, Irreducible b) ∧ fx.prod ~ᵤ x
fa : Multiset α
hfa : (∀ b ∈ fa, Irreducible b) ∧ fa.prod ~ᵤ a
fb : Multiset α
hfb : (∀ b ∈ fb, Irreducible b) ∧ fb.prod ~ᵤ b
rw : p * fx.prod ~ᵤ p * x
⊢ (p ::ₘ fx).prod ~ᵤ a * b

Tactic:
rw [hx, Multiset.prod_cons]

Premises used: Multiset.prod_cons
-- 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
p : α
this : DecidableEq α := Classical.decEq α
hpi : Irreducible p
a b : α
h : p ∣ a * b
x : α
hx : a * b = p * x
hab0 : ¬a * b = 0
hx0 : x ≠ 0
ha0 : a ≠ 0
hb0 : b ≠ 0
fx : Multiset α
hfx : (∀ b ∈ fx, Irreducible b) ∧ fx.prod ~ᵤ x
fa : Multiset α
hfa : (∀ b ∈ fa, Irreducible b) ∧ fa.prod ~ᵤ a
fb : Multiset α
hfb : (∀ b ∈ fb, Irreducible b) ∧ fb.prod ~ᵤ b
⊢ p * fx.prod ~ᵤ p * x

Tactic:
hfx.2.mul_left _

Premises used: And.right, Associated.mul_left
-- 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
p : α
this : DecidableEq α := Classical.decEq α
hpi : Irreducible p
a b : α
h : p ∣ a * b
x : α
hx : a * b = p * x
hab0 : ¬a * b = 0
hx0 : x ≠ 0
ha0 : a ≠ 0
hb0 : b ≠ 0
fx : Multiset α
hfx : (∀ b ∈ fx, Irreducible b) ∧ fx.prod ~ᵤ x
fa : Multiset α
hfa : (∀ b ∈ fa, Irreducible b) ∧ fa.prod ~ᵤ a
fb : Multiset α
hfb : (∀ b ∈ fb, Irreducible b) ∧ fb.prod ~ᵤ b
⊢ p * fx.prod ~ᵤ p * x

Tactic:
exact hfx.2.mul_left _

Premises used: And.right, Associated.mul_left
-- 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
p : α
this : DecidableEq α := Classical.decEq α
hpi : Irreducible p
a b : α
h : p ∣ a * b
x : α
hx : a * b = p * x
hab0 : ¬a * b = 0
hx0 : x ≠ 0
ha0 : a ≠ 0
hb0 : b ≠ 0
fx : Multiset α
hfx : (∀ b ∈ fx, Irreducible b) ∧ fx.prod ~ᵤ x
fa : Multiset α
hfa : (∀ b ∈ fa, Irreducible b) ∧ fa.prod ~ᵤ a
fb : Multiset α
hfb : (∀ b ∈ fb, Irreducible b) ∧ fb.prod ~ᵤ b
⊢ a * b ~ᵤ fa.prod * fb.prod

Tactic:
hfa.2.symm.mul_mul hfb.2.symm

Premises used: Associated.symm, And.right, Associated.mul_mul
-- 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
p : α
this : DecidableEq α := Classical.decEq α
hpi : Irreducible p
a b : α
h : p ∣ a * b
x : α
hx : a * b = p * x
hab0 : ¬a * b = 0
hx0 : x ≠ 0
ha0 : a ≠ 0
hb0 : b ≠ 0
fx : Multiset α
hfx : (∀ b ∈ fx, Irreducible b) ∧ fx.prod ~ᵤ x
fa : Multiset α
hfa : (∀ b ∈ fa, Irreducible b) ∧ fa.prod ~ᵤ a
fb : Multiset α
hfb : (∀ b ∈ fb, Irreducible b) ∧ fb.prod ~ᵤ b
rw rw₁ : fa.prod * fb.prod = fa.prod * fb.prod
⊢ fa.prod * fb.prod = (fa + fb).prod

Tactic:
rw [Multiset.prod_add]

Premises used: Multiset.prod_add
-- 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
p : α
this : DecidableEq α := Classical.decEq α
hpi : Irreducible p
a b : α
h : p ∣ a * b
x : α
hx : a * b = p * x
hab0 : ¬a * b = 0
hx0 : x ≠ 0
ha0 : a ≠ 0
hb0 : b ≠ 0
fx : Multiset α
hfx : (∀ b ∈ fx, Irreducible b) ∧ fx.prod ~ᵤ x
fa : Multiset α
hfa : (∀ b ∈ fa, Irreducible b) ∧ fa.prod ~ᵤ a
fb : Multiset α
hfb : (∀ b ∈ fb, Irreducible b) ∧ fb.prod ~ᵤ b
a₁ : (p ::ₘ fx).prod ~ᵤ a * b
a₂ : fa.prod * fb.prod = (fa + fb).prod
⊢ (p ::ₘ fx).prod ~ᵤ (fa + fb).prod

Tactic:
calc
            Multiset.prod (p ::ₘ fx) ~ᵤ a * b := by
              rw [hx, Multiset.prod_cons]; exact hfx.2.mul_left _
            _ ~ᵤ fa.prod * fb.prod := hfa.2.symm.mul_mul hfb.2.symm
            _ = _ := by rw [Multiset.prod_add]

Premises used: Multiset.prod, Multiset.cons, Associated.symm, And.right, Associated.mul_mul
-- 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
p : α
this : DecidableEq α := Classical.decEq α
hpi : Irreducible p
a b : α
h : p ∣ a * b
x : α
hx : a * b = p * x
hab0 : ¬a * b = 0
hx0 : x ≠ 0
ha0 : a ≠ 0
hb0 : b ≠ 0
fx : Multiset α
hfx : (∀ b ∈ fx, Irreducible b) ∧ fx.prod ~ᵤ x
fa : Multiset α
hfa : (∀ b ∈ fa, Irreducible b) ∧ fa.prod ~ᵤ a
fb : Multiset α
hfb : (∀ b ∈ fb, Irreducible b) ∧ fb.prod ~ᵤ b
⊢ Multiset.Rel Associated (p ::ₘ fx) (fa + fb)

Tactic:
have h : Multiset.Rel Associated (p ::ₘ fx) (fa + fb) := by
          apply uif
          · exact fun i hi => (Multiset.mem_cons.1 hi).elim (fun hip => hip.symm ▸ hpi) (hfx.1 _)
          · exact fun i hi => (Multiset.mem_add.1 hi).elim (hfa.1 _) (hfb.1 _)
          calc
            Multiset.prod (p ::ₘ fx) ~ᵤ a * b := by
              rw [hx, Multiset.prod_cons]; exact hfx.2.mul_left _
            _ ~ᵤ fa.prod * fb.prod := hfa.2.symm.mul_mul hfb.2.symm
            _ = _ := by rw [Multiset.prod_add]
-- 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
p : α
this : DecidableEq α := Classical.decEq α
hpi : Irreducible p
a b : α
h_1 : p ∣ a * b
x : α
hx : a * b = p * x
hab0 : ¬a * b = 0
hx0 : x ≠ 0
ha0 : a ≠ 0
hb0 : b ≠ 0
fx : Multiset α
hfx : (∀ b ∈ fx, Irreducible b) ∧ fx.prod ~ᵤ x
fa : Multiset α
hfa : (∀ b ∈ fa, Irreducible b) ∧ fa.prod ~ᵤ a
fb : Multiset α
hfb : (∀ b ∈ fb, Irreducible b) ∧ fb.prod ~ᵤ b
h : Multiset.Rel Associated (p ::ₘ fx) (fa + fb)
⊢ p ∣ a ∨ p ∣ b

Tactic:
let ⟨q, hqf, hq⟩ := Multiset.exists_mem_of_rel_of_mem h (Multiset.mem_cons_self p _)
          (Multiset.mem_add.1 hqf).elim
            (fun hqa =>
              Or.inl <| hq.dvd_iff_dvd_left.2 <| hfa.2.dvd_iff_dvd_right.1 (Multiset.dvd_prod hqa))
            fun hqb =>
            Or.inr <| hq.dvd_iff_dvd_left.2 <| hfb.2.dvd_iff_dvd_right.1 (Multiset.dvd_prod hqb)

Premises used: Iff.mpr, Dvd.dvd, Multiset.exists_mem_of_rel_of_mem, Multiset.mem_add, Multiset.dvd_prod, And.right, Iff.mp, Associated.dvd_iff_dvd_left, Or.inl, Or, Multiset.mem_cons_self, Associated.dvd_iff_dvd_right, Or.elim, _private.0.irreducible_iff_prime_of_existsUnique_irreducible_factors.match_2, Or.inr
-- 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
p : α
this : DecidableEq α := Classical.decEq α
hpi : Irreducible p
a b : α
h_1 : p ∣ a * b
x : α
hx : a * b = p * x
hab0 : ¬a * b = 0
hx0 : x ≠ 0
ha0 : a ≠ 0
hb0 : b ≠ 0
fx : Multiset α
hfx : (∀ b ∈ fx, Irreducible b) ∧ fx.prod ~ᵤ x
fa : Multiset α
hfa : (∀ b ∈ fa, Irreducible b) ∧ fa.prod ~ᵤ a
fb : Multiset α
hfb : (∀ b ∈ fb, Irreducible b) ∧ fb.prod ~ᵤ b
h : Multiset.Rel Associated (p ::ₘ fx) (fa + fb)
⊢ p ∣ a ∨ p ∣ b

Tactic:
exact
          let ⟨q, hqf, hq⟩ := Multiset.exists_mem_of_rel_of_mem h (Multiset.mem_cons_self p _)
          (Multiset.mem_add.1 hqf).elim
            (fun hqa =>
              Or.inl <| hq.dvd_iff_dvd_left.2 <| hfa.2.dvd_iff_dvd_right.1 (Multiset.dvd_prod hqa))
            fun hqb =>
            Or.inr <| hq.dvd_iff_dvd_left.2 <| hfb.2.dvd_iff_dvd_right.1 (Multiset.dvd_prod hqb)
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
⊢ Nontrivial α

Tactic:
nontriviality α using factors

Premises used: UniqueFactorizationMonoid.factors
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
h : Nontrivial α
rw : Rel.{u_1, u_1} (α := α) Associated (factors 1) 0
rw₁ : Type u_1
rw₂ : α → α → Prop
⊢ Eq.{u_1 + 1} (α := Multiset α) (factors 1) 0

Tactic:
rw [← rel_zero_right]

Premises used: Multiset.rel_zero_right
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
h : Nontrivial α
⊢ Rel.{u_1, u_1} (α := α) Associated (factors 1) 0

Tactic:
factors_unique irreducible_of_factor (fun x hx => (notMem_zero x hx).elim) ?_

Premises used: Multiset.notMem_zero, False.elim, UniqueFactorizationMonoid.factors_unique, UniqueFactorizationMonoid.irreducible_of_factor
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
h : Nontrivial α
rw : Associated.{u_1} (M := α) (prod (factors 1)) 1
⊢ Associated.{u_1} (M := α) (prod (factors 1)) (prod 0)

Tactic:
rw [prod_zero]

Premises used: Multiset.prod_zero
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
h : Nontrivial α
⊢ Associated.{u_1} (M := α) (prod (factors 1)) 1

Tactic:
factors_prod one_ne_zero

Premises used: UniqueFactorizationMonoid.factors_prod, one_ne_zero
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
h : Nontrivial α
⊢ Associated.{u_1} (M := α) (prod (factors 1)) 1

Tactic:
exact factors_prod one_ne_zero

Premises used: UniqueFactorizationMonoid.factors_prod, one_ne_zero
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a p : α
ha0 : a ≠ 0
hp : Irreducible p
h : p ∣ a
b : α
hb : a = p * b
hb0 : b = 0
⊢ False

Tactic:
simp_all
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a p : α
ha0 : a ≠ 0
hp : Irreducible p
h : p ∣ a
b : α
hb : a = p * b
hb0 : b ≠ 0
rw : p * b ~ᵤ p * (factors b).prod
⊢ p * b ~ᵤ (p ::ₘ factors b).prod

Tactic:
rw [prod_cons]

Premises used: Multiset.prod_cons
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a p : α
ha0 : a ≠ 0
hp : Irreducible p
h : p ∣ a
b : α
hb : a = p * b
hb0 : b ≠ 0
⊢ p * b ~ᵤ p * (factors b).prod

Tactic:
(factors_prod hb0).symm.mul_left _

Premises used: Associated.symm, UniqueFactorizationMonoid.factors_prod, Associated.mul_left
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a p : α
ha0 : a ≠ 0
hp : Irreducible p
h : p ∣ a
b : α
hb : a = p * b
hb0 : b ≠ 0
⊢ p * b ~ᵤ p * (factors b).prod

Tactic:
exact (factors_prod hb0).symm.mul_left _

Premises used: Associated.symm, UniqueFactorizationMonoid.factors_prod, Associated.mul_left
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a p : α
ha0 : a ≠ 0
hp : Irreducible p
h : p ∣ a
b : α
hb : a = p * b
hb0 : b ≠ 0
this : Rel Associated (p ::ₘ factors b) (factors a)
⊢ p ∈ p ::ₘ factors b

Tactic:
simp
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
x : α
hx : x ≠ 0
h : ¬IsUnit x
obtain : ∀ (p' : α) (hp' : Irreducible p') (hp'x : p' ∣ x), ∃ (p : α), p ∈ factors x
⊢ ∃ (p : α), p ∈ factors x

Tactic:
obtain ⟨p', hp', hp'x⟩ := WfDvdMonoid.exists_irreducible_factor h hx

Premises used: WfDvdMonoid.exists_irreducible_factor
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
x : α
hx : x ≠ 0
h : ¬IsUnit x
p' : α
hp' : Irreducible p'
hp'x : p' ∣ x
obtain : ∀ (p : α) (hp : p ∈ factors x), p' ~ᵤ p → ∃ (p : α), p ∈ factors x
⊢ ∃ (p : α), p ∈ factors x

Tactic:
obtain ⟨p, hp, _⟩ := exists_mem_factors_of_dvd hx hp' hp'x

Premises used: UniqueFactorizationMonoid.exists_mem_factors_of_dvd
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
x : α
hx : x ≠ 0
h : ¬IsUnit x
p' : α
hp' : Irreducible p'
hp'x : p' ∣ x
p : α
hp : p ∈ factors x
right : p' ~ᵤ p
⊢ ∃ (p : α), p ∈ factors x

Tactic:
⟨p, hp⟩

Premises used: Exists.intro
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
x : α
hx : x ≠ 0
h : ¬IsUnit x
p' : α
hp' : Irreducible p'
hp'x : p' ∣ x
p : α
hp : p ∈ factors x
right : p' ~ᵤ p
⊢ ∃ (p : α), p ∈ factors x

Tactic:
exact ⟨p, hp⟩
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a : α
ha : Irreducible a
obtain : ∀ (b : α) (hbmem : b ∈ factors a) (hab : a ~ᵤ b), ∃ (b : α), a ~ᵤ b ∧ factors a = {b}
⊢ ∃ (b : α), a ~ᵤ b ∧ factors a = {b}

Tactic:
obtain ⟨b, hbmem, hab⟩ := exists_mem_factors_of_dvd ha.ne_zero ha dvd_rfl

Premises used: Irreducible.ne_zero, dvd_rfl, UniqueFactorizationMonoid.exists_mem_factors_of_dvd
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a : α
ha : Irreducible a
b : α
hbmem : b ∈ factors a
hab : a ~ᵤ b
rw : 1 ≤ card (α := α) {b}
rw₁ rw₂ : LE.le (α := ℕ) 1 1
⊢ (factors a).card ≤ card (α := α) {b}

Tactic:
rw [card_factors_of_irreducible ha, Multiset.card_singleton]

Premises used: Multiset.card_singleton, UniqueFactorizationMonoid.card_factors_of_irreducible
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a : α
ha : Irreducible a
b : α
hbmem : b ∈ factors a
hab : a ~ᵤ b
⊢ ∃ (b : α), a ~ᵤ b ∧ factors a = {b}

Tactic:
exact ⟨b, hab, .symm <| Multiset.eq_of_le_of_card_le (Multiset.singleton_le.mpr hbmem)
    (by rw [card_factors_of_irreducible ha, Multiset.card_singleton])⟩
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
⊢ Rel Associated (factors (x * y)) (factors x + factors y)

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

Premises used: UniqueFactorizationMonoid.factors_unique, Associated.trans, Multiset.mem_add, UniqueFactorizationMonoid.irreducible_of_factor, Or.by_cases, UniqueFactorizationMonoid.factors_prod, Iff.mp, mul_ne_zero