awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
a : α
f : Multiset α
ha : Irreducible a
pfa : (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
this : DecidableEq α
p : α
s : Multiset α
h : s.prod ~ᵤ a → (∀ b ∈ s, Prime b) → ∃ (p : α), a ~ᵤ p ∧ s = {p}
u : αˣ
hu : (p ::ₘ s).prod * (↑u : α) = a
hs : ∀ b ∈ p ::ₘ s, Prime b
hs0 : ¬s = 0
q : α
hq : q ∈ s
⊢ False
have apply : IsUnit q
Tactic: apply (hs q (by simp [hq])).2.1
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
a : α
f : Multiset α
ha : Irreducible a
pfa : (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
this : DecidableEq α
p : α
s : Multiset α
h : s.prod ~ᵤ a → (∀ b ∈ s, Prime b) → ∃ (p : α), a ~ᵤ p ∧ s = {p}
u : αˣ
hu : (p ::ₘ s).prod * (↑u : α) = a
hs : ∀ b ∈ p ::ₘ s, Prime b
hs0 : ¬s = 0
q : α
hq : q ∈ s
⊢ IsUnit q
have refine_1 : a = p * (↑u : α) * (s.erase q).prod * q
Tactic: refine (ha.isUnit_or_isUnit (?_ : _ = p * ↑u * (s.erase q).prod * _)).resolve_left ?_
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
a : α
f : Multiset α
ha : Irreducible a
pfa : (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
this : DecidableEq α
p : α
s : Multiset α
h : s.prod ~ᵤ a → (∀ b ∈ s, Prime b) → ∃ (p : α), a ~ᵤ p ∧ s = {p}
u : αˣ
hu : (p ::ₘ s).prod * (↑u : α) = a
hs : ∀ b ∈ p ::ₘ s, Prime b
hs0 : ¬s = 0
q : α
hq : q ∈ s
refine_1 : a = p * (↑u : α) * (s.erase q).prod * q
⊢ IsUnit q
have refine_2 : ¬IsUnit (p * (↑u : α) * (s.erase q).prod)
Tactic: refine (ha.isUnit_or_isUnit (?_ : _ = p * ↑u * (s.erase q).prod * _)).resolve_left ?_
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
a : α
f : Multiset α
ha : Irreducible a
pfa : (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
this : DecidableEq α
p : α
s : Multiset α
h : s.prod ~ᵤ a → (∀ b ∈ s, Prime b) → ∃ (p : α), a ~ᵤ p ∧ s = {p}
u : αˣ
hu : (p ::ₘ s).prod * (↑u : α) = a
hs : ∀ b ∈ p ::ₘ s, Prime b
hs0 : ¬s = 0
q : α
hq : q ∈ s
⊢ a = p * (↑u : α) * (s.erase q).prod * q
have refine_1 : (↑u : α) * (p ::ₘ s).prod = (↑u : α) * (p * s.prod)
Tactic: rw [mul_right_comm _ _ q, mul_assoc, ← Multiset.prod_cons, Multiset.cons_erase hq, ← hu,
          mul_comm, mul_comm p _, mul_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
a : α
f : Multiset α
ha : Irreducible a
pfa : (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
this : DecidableEq α
p : α
s : Multiset α
h : s.prod ~ᵤ a → (∀ b ∈ s, Prime b) → ∃ (p : α), a ~ᵤ p ∧ s = {p}
u : αˣ
hu : (p ::ₘ s).prod * (↑u : α) = a
hs : ∀ b ∈ p ::ₘ s, Prime b
hs0 : ¬s = 0
q : α
hq : q ∈ s
⊢ ¬IsUnit (p * (↑u : α) * (s.erase q).prod)
have apply : ¬IsUnit p
Tactic: apply mt isUnit_of_mul_isUnit_left (mt isUnit_of_mul_isUnit_left _)
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Basic (hypothesis)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
a : α
f : Multiset α
ha : Irreducible a
pfa : (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
this : DecidableEq α
p : α
s : Multiset α
h : s.prod ~ᵤ a → (∀ b ∈ s, Prime b) → ∃ (p : α), a ~ᵤ p ∧ s = {p}
u : αˣ
hu : (p ::ₘ s).prod * (↑u : α) = a
hs : ∀ b ∈ p ::ₘ s, Prime b
⊢ a ~ᵤ p ∧ p ::ₘ s = {p}
have hs0 : s = 0
Tactic: have hs0 : s = 0 := by
      by_contra hs0
      obtain ⟨q, hq⟩ := Multiset.exists_mem_of_ne_zero hs0
      apply (hs q (by simp [hq])).2.1
      refine (ha.isUnit_or_isUnit (?_ : _ = p * ↑u * (s.erase q).prod * _)).resolve_left ?_
      · rw [mul_right_comm _ _ q, mul_assoc, ← Multiset.prod_cons, Multiset.cons_erase hq, ← hu,
          mul_comm, mul_comm p _, mul_assoc]
        simp
      apply mt isUnit_of_mul_isUnit_left (mt isUnit_of_mul_isUnit_left _)
      apply (hs p (Multiset.mem_cons_self _ _)).2.1
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
a : α
f : Multiset α
ha : Irreducible a
pfa : (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
this : DecidableEq α
p : α
s : Multiset α
h : s.prod ~ᵤ a → (∀ b ∈ s, Prime b) → ∃ (p : α), a ~ᵤ p ∧ s = {p}
u : αˣ
hu : (p ::ₘ s).prod * (↑u : α) = a
hs : ∀ b ∈ p ::ₘ s, Prime b
hs0 : s = 0
⊢ a ~ᵤ p ∧ p ::ₘ s = {p}
have h : (1 ~ᵤ a →
    (∀ (b : α), Membership.mem (γ := Multiset α) 0 b → Prime b) → ∃ (p : α), a ~ᵤ p ∧ Eq (α := Multiset α) 0 {p}) →
  ∀ (hu : p * (↑u : α) = a) (hs : ∀ b ∈ p ::ₘ 0, Prime b) (hs0 : True), a ~ᵤ p ∧ p ::ₘ 0 = {p}
Tactic: simp only [mul_one, Multiset.prod_cons, Multiset.prod_zero, hs0] at *
Cleared hypotheses: h, hu, hs, hs0
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Basic (hypothesis)
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
⊢ p ∣ a ∨ p ∣ b
have hx0 : x ≠ 0
Tactic: have hx0 : x ≠ 0 := fun hx0 => by simp_all
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Basic (hypothesis)
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
⊢ p ∣ a ∨ p ∣ b
have ha0 : a ≠ 0
Tactic: have ha0 : a ≠ 0 := left_ne_zero_of_mul hab0
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Basic (hypothesis)
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
⊢ p ∣ a ∨ p ∣ b
have hb0 : b ≠ 0
Tactic: have hb0 : b ≠ 0 := right_ne_zero_of_mul hab0
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Basic (goal)
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
⊢ p ∣ a ∨ p ∣ b
have obtain : ∀ (fx : Multiset α) (hfx : (∀ b ∈ fx, Irreducible b) ∧ fx.prod ~ᵤ x), p ∣ a ∨ p ∣ b
Tactic: obtain ⟨fx, hfx⟩ := eif x hx0
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Basic (goal)
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
⊢ p ∣ a ∨ p ∣ b
have obtain : ∀ (fa : Multiset α) (hfa : (∀ b ∈ fa, Irreducible b) ∧ fa.prod ~ᵤ a), p ∣ a ∨ p ∣ b
Tactic: obtain ⟨fa, hfa⟩ := eif a ha0
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Basic (goal)
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
⊢ p ∣ a ∨ p ∣ b
have obtain : ∀ (fb : Multiset α) (hfb : (∀ b ∈ fb, Irreducible b) ∧ fb.prod ~ᵤ b), p ∣ a ∨ p ∣ b
Tactic: obtain ⟨fb, hfb⟩ := eif b hb0
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Basic (goal)
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)
have a₁ : ∀ x ∈ p ::ₘ fx, Irreducible x
Tactic: apply uif
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Basic (goal)
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
⊢ Multiset.Rel Associated (p ::ₘ fx) (fa + fb)
have a₂ : ∀ x ∈ fa + fb, Irreducible x
Tactic: apply uif
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Basic (goal)
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
⊢ Multiset.Rel Associated (p ::ₘ fx) (fa + fb)
have a₃ : (p ::ₘ fx).prod ~ᵤ (fa + fb).prod
Tactic: apply uif
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Basic (goal)
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 ~ᵤ a * b
have rw : p * fx.prod ~ᵤ p * x
Tactic: rw [hx, Multiset.prod_cons]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Basic (goal)
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
⊢ fa.prod * fb.prod = (fa + fb).prod
have rw : fa.prod * fb.prod = fa.prod * fb.prod
Tactic: rw [Multiset.prod_add]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Basic (goal)
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 ~ᵤ (fa + fb).prod
have a₁ : (p ::ₘ fx).prod ~ᵤ a * b
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]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Basic (goal)
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
⊢ (p ::ₘ fx).prod ~ᵤ (fa + fb).prod
have a₂ : fa.prod * fb.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]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Basic (hypothesis)
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 ∣ a ∨ p ∣ b
have h : 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]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Basic (hypothesis)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
⊢ Eq.{u_1 + 1} (α := Multiset α) (factors 1) 0
have a : Nontrivial α
Tactic: nontriviality α using factors
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
h : Nontrivial α
⊢ Eq.{u_1 + 1} (α := Multiset α) (factors 1) 0
have rw : Rel.{u_1, u_1} (α := α) Associated (factors 1) 0
Tactic: rw [← rel_zero_right]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Basic (goal)
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
⊢ Eq.{u_1 + 1} (α := Multiset α) (factors 1) 0
have rw₂ : α → α → Prop
Tactic: rw [← rel_zero_right]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
h : Nontrivial α
⊢ Associated.{u_1} (M := α) (prod (factors 1)) (prod 0)
have rw : Associated.{u_1} (M := α) (prod (factors 1)) 1
Tactic: rw [prod_zero]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Basic (goal)
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
have rw : p * b ~ᵤ p * (factors b).prod
Tactic: rw [prod_cons]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
x : α
hx : x ≠ 0
h : ¬IsUnit x
⊢ ∃ (p : α), p ∈ factors x
have obtain : ∀ (p' : α) (hp' : Irreducible p') (hp'x : p' ∣ x), ∃ (p : α), p ∈ factors x
Tactic: obtain ⟨p', hp', hp'x⟩ := WfDvdMonoid.exists_irreducible_factor h hx
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Basic (goal)
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 : α), p ∈ factors x
have obtain : ∀ (p : α) (hp : p ∈ factors x), p' ~ᵤ p → ∃ (p : α), p ∈ factors x
Tactic: obtain ⟨p, hp, _⟩ := exists_mem_factors_of_dvd hx hp' hp'x
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a : α
ha : Irreducible a
⊢ ∃ (b : α), a ~ᵤ b ∧ factors a = {b}
have obtain : ∀ (b : α) (hbmem : b ∈ factors a) (hab : a ~ᵤ b), ∃ (b : α), a ~ᵤ b ∧ factors a = {b}
Tactic: obtain ⟨b, hbmem, hab⟩ := exists_mem_factors_of_dvd ha.ne_zero ha dvd_rfl
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a : α
ha : Irreducible a
b : α
hbmem : b ∈ factors a
hab : a ~ᵤ b
⊢ (factors a).card ≤ card (α := α) {b}
have rw : 1 ≤ card (α := α) {b}
Tactic: rw [card_factors_of_irreducible ha, Multiset.card_singleton]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Basic (goal)
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}
⊢ (factors a).card ≤ card (α := α) {b}
have rw₁ : LE.le (α := ℕ) 1 1
Tactic: rw [card_factors_of_irreducible ha, Multiset.card_singleton]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Basic (goal)
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)
have factors_unique : x * y ~ᵤ (factors x + factors y).prod
Tactic: refine
    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 ?_)
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
⊢ x * y ~ᵤ (factors x + factors y).prod
have rw : x * y ~ᵤ (factors x).prod * (factors y).prod
Tactic: rw [prod_add]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
x : α
n : ℕ
⊢ Rel Associated (factors (HPow.hPow (β := ℕ) x 0)) (HSMul.hSMul (α := ℕ) 0 (factors x))
have rw : Rel Associated (factors (HPow.hPow (β := ℕ) x 0)) 0
Tactic: rw [zero_nsmul, pow_zero, factors_one, rel_zero_right]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
x : α
n : ℕ
rw : Rel Associated (factors (HPow.hPow (β := ℕ) x 0)) 0
⊢ Rel Associated (factors (HPow.hPow (β := ℕ) x 0)) (HSMul.hSMul (α := ℕ) 0 (factors x))
have rw₁ : Rel.{u_1, u_1} (α := α) Associated (factors 1) 0
Tactic: rw [zero_nsmul, pow_zero, factors_one, rel_zero_right]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
x : α
n : ℕ
rw : Rel Associated (factors (HPow.hPow (β := ℕ) x 0)) 0
rw₁ : Rel.{u_1, u_1} (α := α) Associated (factors 1) 0
⊢ Rel Associated (factors (HPow.hPow (β := ℕ) x 0)) (HSMul.hSMul (α := ℕ) 0 (factors x))
have rw₂ : Rel.{u_1, u_1} (α := α) Associated 0 0
Tactic: rw [zero_nsmul, pow_zero, factors_one, rel_zero_right]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
x : α
n : ℕ
rw : Rel Associated (factors (HPow.hPow (β := ℕ) x 0)) 0
rw₁ : Rel.{u_1, u_1} (α := α) Associated (factors 1) 0
rw₂ : Rel.{u_1, u_1} (α := α) Associated 0 0
⊢ Rel Associated (factors (HPow.hPow (β := ℕ) x 0)) (HSMul.hSMul (α := ℕ) 0 (factors x))
have rw₃ : Eq.{u_1 + 1} (α := Multiset α) 0 0
Tactic: rw [zero_nsmul, pow_zero, factors_one, rel_zero_right]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
x : α
n_1 n : ℕ
⊢ Rel Associated (factors (x ^ (n + 1))) ((n + 1) • factors x)
have pos : ∀ (h0 : x = 0), Rel Associated (factors (x ^ (n + 1))) ((n + 1) • factors x)
Tactic: by_cases h0 : x = 0
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
x : α
n_1 n : ℕ
pos : ∀ (h0 : x = 0), Rel Associated (factors (x ^ (n + 1))) ((n + 1) • factors x)
⊢ Rel Associated (factors (x ^ (n + 1))) ((n + 1) • factors x)
have neg : ∀ (h0 : ¬x = 0), Rel Associated (factors (x ^ (n + 1))) ((n + 1) • factors x)
Tactic: by_cases h0 : x = 0
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
x : α
n_1 n : ℕ
h0 : ¬x = 0
⊢ Rel Associated (factors (x ^ (n + 1))) ((n + 1) • factors x)
have neg : Rel Associated (factors (x * x ^ n)) (factors x + n • factors x)
Tactic: rw [pow_succ', succ_nsmul']