awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.ClassGroup
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Nonempty.{u_1 + 1} (NormalizedGCDMonoid R)
refine : ∀ (y : ClassGroup R), y = 1
⊢ Subsingleton.{u_1 + 1} (ClassGroup R)

Tactic:
refine subsingleton_of_forall_eq 1 ?_

Premises used: subsingleton_of_forall_eq, OfNat.ofNat
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.ClassGroup
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Nonempty.{u_1 + 1} (NormalizedGCDMonoid R)
x : ClassGroup R
⊢ x = 1

Tactic:
ClassGroup.induction (FractionRing R) ?_ x

Premises used: ClassGroup.induction
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.ClassGroup
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Nonempty.{u_1 + 1} (NormalizedGCDMonoid R)
x : ClassGroup R
refine :
  ∀ (I : (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ),
    Eq (α := ClassGroup R)
      ((ClassGroup.mk (FractionRing R) : (a : (FractionalIdeal R⁰ (FractionRing R))ˣ) → ClassGroup R) I : ClassGroup R)
      (1 : ClassGroup R)
⊢ x = 1

Tactic:
refine ClassGroup.induction (FractionRing R) ?_ x
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.ClassGroup
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Nonempty.{u_1 + 1} (NormalizedGCDMonoid R)
x : ClassGroup R
I : (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ
⊢ Eq (α := ClassGroup R)
    ((ClassGroup.mk (FractionRing R) : (a : (FractionalIdeal R⁰ (FractionRing R))ˣ) → ClassGroup R) I : ClassGroup R)
    (1 : ClassGroup R)

Tactic:
ClassGroup.mk_eq_one_iff.mpr
    (isPrincipal_fractionalIdeal_of_isUnit I)

Premises used: Iff.mpr, ClassGroup.mk_eq_one_iff, _private.0.NormalizedGCDMonoid.isPrincipal_fractionalIdeal_of_isUnit
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.ClassGroup
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Nonempty.{u_1 + 1} (NormalizedGCDMonoid R)
x : ClassGroup R
I : (FractionalIdeal (R := R) R⁰ (FractionRing R))ˣ
⊢ Eq (α := ClassGroup R)
    ((ClassGroup.mk (FractionRing R) : (a : (FractionalIdeal R⁰ (FractionRing R))ˣ) → ClassGroup R) I : ClassGroup R)
    (1 : ClassGroup R)

Tactic:
exact ClassGroup.mk_eq_one_iff.mpr
    (isPrincipal_fractionalIdeal_of_isUnit I)

Premises used: Iff.mpr, ClassGroup.mk_eq_one_iff, _private.0.NormalizedGCDMonoid.isPrincipal_fractionalIdeal_of_isUnit
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Defs
Goal:
α : Type u_2
inst : CommMonoidWithZero α
h : WfDvdMonoid α
⊢ WellFounded.{u_2 + 1} (α := α) DvdNotUnit

Tactic:
h.wf

Premises used: IsWellFounded.wf
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Defs
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : WfDvdMonoid α
a : α
ha : ¬IsUnit a
ha0 : a ≠ 0
⊢ ∃ (i : α), Irreducible i ∧ i ∣ a

Tactic:
let ⟨b, hs, hr⟩ := wellFounded_dvdNotUnit.has_min { b | b ∣ a ∧ ¬IsUnit b } ⟨a, dvd_rfl, ha⟩
  ⟨b,
    ⟨hs.2, fun c d he =>
      let h := dvd_trans ⟨d, he⟩ hs.1
      or_iff_not_imp_left.2 fun hc =>
        of_not_not fun hd => hr c ⟨h, hc⟩ ⟨ne_zero_of_dvd_ne_zero ha0 h, d, hd, he⟩⟩,
    hs.1⟩

Premises used: Iff.mpr, Dvd.dvd, setOf, wellFounded_dvdNotUnit, IsUnit, Exists, Irreducible.mk, Irreducible, dvd_trans, _private.0.WfDvdMonoid.exists_irreducible_factor.match_1, And, And.right, And.left, Classical.or_iff_not_imp_left, And.intro, Exists.intro, of_not_not, dvd_rfl, WellFounded.has_min, ne_zero_of_dvd_ne_zero, Not
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Defs
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : WfDvdMonoid α
motive : α → Prop
a : α
zero : motive 0
unit : ∀ (u : α), IsUnit u → motive u
mul : ∀ (a i : α), a ≠ 0 → Irreducible i → motive a → motive (i * a)
⊢ motive a

Tactic:
haveI := Classical.dec
  wellFounded_dvdNotUnit.fix
    (fun a ih =>
      if ha0 : a = 0 then ha0.substr zero
      else
        if hau : IsUnit a then unit a hau
        else
          let ⟨i, i_irred, b, hb⟩ := exists_irreducible_factor hau ha0
          let hb0 : b ≠ 0 := ne_zero_of_dvd_ne_zero ha0 ⟨i, mul_comm i b ▸ hb⟩
          hb.symm ▸ mul b i hb0 i_irred <| ih b ⟨hb0, i, i_irred.1, mul_comm i b ▸ hb⟩)
    a

Premises used: _private.0.WfDvdMonoid.induction_on_irreducible.match_1, wellFounded_dvdNotUnit, IsUnit, Eq.rec, WfDvdMonoid.exists_irreducible_factor, dite, Classical.dec, Exists.intro, Eq.substr, mul_comm, ne_zero_of_dvd_ne_zero, OfNat.ofNat, Eq, WellFounded.fix
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Defs
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : WfDvdMonoid α
a_1 a i : α
ha0 : a ≠ 0
hi : Irreducible i
ih : a ≠ 0 → ∃ (f : Multiset α), (∀ b ∈ f, Irreducible b) ∧ f.prod ~ᵤ a
h : i * a ≠ 0
s : Multiset α
hs : (∀ b ∈ s, Irreducible b) ∧ s.prod ~ᵤ a
rw : i * s.prod ~ᵤ i * a
⊢ (i ::ₘ s).prod ~ᵤ i * a

Tactic:
rw [s.prod_cons i]

Premises used: Multiset.prod_cons
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Defs
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : WfDvdMonoid α
a_1 a i : α
ha0 : a ≠ 0
hi : Irreducible i
ih : a ≠ 0 → ∃ (f : Multiset α), (∀ b ∈ f, Irreducible b) ∧ f.prod ~ᵤ a
h : i * a ≠ 0
s : Multiset α
hs : (∀ b ∈ s, Irreducible b) ∧ s.prod ~ᵤ a
⊢ i * s.prod ~ᵤ i * a

Tactic:
hs.2.mul_left i

Premises used: And.right, Associated.mul_left
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Defs
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : WfDvdMonoid α
a_1 a i : α
ha0 : a ≠ 0
hi : Irreducible i
ih : a ≠ 0 → ∃ (f : Multiset α), (∀ b ∈ f, Irreducible b) ∧ f.prod ~ᵤ a
h : i * a ≠ 0
s : Multiset α
hs : (∀ b ∈ s, Irreducible b) ∧ s.prod ~ᵤ a
⊢ i * s.prod ~ᵤ i * a

Tactic:
exact hs.2.mul_left i

Premises used: And.right, Associated.mul_left
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Defs
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : WfDvdMonoid α
a : α
hn0 : a ≠ 0
hnu : ¬IsUnit a
obtain :
  ∀ (f : Multiset α) (hi : ∀ b ∈ f, Irreducible b) (u : αˣ) (hn0 : f.prod * (↑u : α) ≠ 0)
    (hnu : ¬IsUnit (f.prod * (↑u : α))),
    ∃ (f_1 : Multiset α), (∀ b ∈ f_1, Irreducible b) ∧ f_1.prod = f.prod * (↑u : α) ∧ f_1 ≠ ∅
⊢ ∃ (f : Multiset α), (∀ b ∈ f, Irreducible b) ∧ f.prod = a ∧ f ≠ ∅

Tactic:
obtain ⟨f, hi, u, rfl⟩ := exists_factors a hn0

Premises used: WfDvdMonoid.exists_factors, rfl
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Defs
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : WfDvdMonoid α
f : Multiset α
hi : ∀ b ∈ f, Irreducible b
u : αˣ
hn0 : f.prod * (↑u : α) ≠ 0
hnu : ¬IsUnit (f.prod * (↑u : α))
h : f = 0
⊢ IsUnit (f.prod * (↑u : α))

Tactic:
simp [h]
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Defs
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : WfDvdMonoid α
f : Multiset α
hi : ∀ b ∈ f, Irreducible b
u : αˣ
hn0 : f.prod * (↑u : α) ≠ 0
hnu : ¬IsUnit (f.prod * (↑u : α))
obtain :
  ∀ (b : α) (h : b ∈ f), ∃ (f_1 : Multiset α), (∀ b ∈ f_1, Irreducible b) ∧ f_1.prod = f.prod * (↑u : α) ∧ f_1 ≠ ∅
⊢ ∃ (f_1 : Multiset α), (∀ b ∈ f_1, Irreducible b) ∧ f_1.prod = f.prod * (↑u : α) ∧ f_1 ≠ ∅

Tactic:
obtain ⟨b, h⟩ := Multiset.exists_mem_of_ne_zero fun h : f = 0 => hnu <| by simp [h]

Premises used: Multiset.exists_mem_of_ne_zero
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Defs
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : WfDvdMonoid α
f : Multiset α
hi : ∀ b ∈ f, Irreducible b
u : αˣ
hn0 : f.prod * (↑u : α) ≠ 0
hnu : ¬IsUnit (f.prod * (↑u : α))
b : α
h : b ∈ f
⊢ ∃ (f_1 : Multiset α), (∀ b ∈ f_1, Irreducible b) ∧ f_1.prod = f.prod * (↑u : α) ∧ f_1 ≠ ∅

Tactic:
⟨(f.erase b).cons (b * u), fun a ha => ?_, ?_, Multiset.cons_ne_zero⟩

Premises used: Units.val, HMul.hMul, Multiset.cons, And.intro, Multiset.erase, Exists.intro, Multiset.cons_ne_zero
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Defs
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : WfDvdMonoid α
f : Multiset α
hi : ∀ b ∈ f, Irreducible b
u : αˣ
hn0 : f.prod * (↑u : α) ≠ 0
hnu : ¬IsUnit (f.prod * (↑u : α))
b : α
h : b ∈ f
refine_1 : ∀ (a : α) (ha : a ∈ b * (↑u : α) ::ₘ f.erase b), Irreducible a
refine_2 : (b * (↑u : α) ::ₘ f.erase b).prod = f.prod * (↑u : α)
⊢ ∃ (f_1 : Multiset α), (∀ b ∈ f_1, Irreducible b) ∧ f_1.prod = f.prod * (↑u : α) ∧ f_1 ≠ ∅

Tactic:
refine ⟨(f.erase b).cons (b * u), fun a ha => ?_, ?_, Multiset.cons_ne_zero⟩
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Defs
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : WfDvdMonoid α
f : Multiset α
hi : ∀ b ∈ f, Irreducible b
u : αˣ
hn0 : f.prod * (↑u : α) ≠ 0
hnu : ¬IsUnit (f.prod * (↑u : α))
b : α
h : b ∈ f
a : α
ha : a ∈ b * (↑u : α) ::ₘ f.erase b
refine_1 : ∀ (ha : b * (↑u : α) ∈ b * (↑u : α) ::ₘ f.erase b), Irreducible (b * (↑u : α))
refine_1₁ : ∀ (ha : a ∈ f.erase b), Irreducible a
⊢ Irreducible a

Tactic:
obtain rfl | ha := Multiset.mem_cons.1 ha

Premises used: Multiset.mem_cons, Iff.mp, rfl
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Defs
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : WfDvdMonoid α
f : Multiset α
hi : ∀ b ∈ f, Irreducible b
u : αˣ
hn0 : f.prod * (↑u : α) ≠ 0
hnu : ¬IsUnit (f.prod * (↑u : α))
b : α
h : b ∈ f
ha : b * (↑u : α) ∈ b * (↑u : α) ::ₘ f.erase b
⊢ Irreducible (b * (↑u : α))

Tactic:
Associated.irreducible ⟨u, rfl⟩ (hi b h)

Premises used: Associated.irreducible, Exists.intro, rfl
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Defs
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : WfDvdMonoid α
f : Multiset α
hi : ∀ b ∈ f, Irreducible b
u : αˣ
hn0 : f.prod * (↑u : α) ≠ 0
hnu : ¬IsUnit (f.prod * (↑u : α))
b : α
h : b ∈ f
a : α
ha_1 : a ∈ b * (↑u : α) ::ₘ f.erase b
ha : a ∈ f.erase b
⊢ Irreducible a

Tactic:
hi a (Multiset.mem_of_mem_erase ha)

Premises used: Multiset.mem_of_mem_erase
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Defs
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : WfDvdMonoid α
f : Multiset α
hi : ∀ b ∈ f, Irreducible b
u : αˣ
hn0 : f.prod * (↑u : α) ≠ 0
hnu : ¬IsUnit (f.prod * (↑u : α))
b : α
h : b ∈ f
ha : b * (↑u : α) ∈ b * (↑u : α) ::ₘ f.erase b
⊢ Irreducible (b * (↑u : α))

Tactic:
exacts [Associated.irreducible ⟨u, rfl⟩ (hi b h), hi a (Multiset.mem_of_mem_erase ha)]

Premises used: Associated.irreducible, Exists.intro, rfl
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Defs
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : WfDvdMonoid α
f : Multiset α
hi : ∀ b ∈ f, Irreducible b
u : αˣ
hn0 : f.prod * (↑u : α) ≠ 0
hnu : ¬IsUnit (f.prod * (↑u : α))
b : α
h : b ∈ f
refine_2 : b * (↑u : α) * (f.erase b).prod = f.prod * (↑u : α)
refine_2₁ : (↑u : α) * b * (f.erase b).prod = f.prod * (↑u : α)
refine_2₂ : (↑u : α) * (b * (f.erase b).prod) = f.prod * (↑u : α)
refine_2₃ : (↑u : α) * f.prod = f.prod * (↑u : α)
refine_2₄ refine_2₅ : f.prod * (↑u : α) = f.prod * (↑u : α)
⊢ (b * (↑u : α) ::ₘ f.erase b).prod = f.prod * (↑u : α)

Tactic:
rw [Multiset.prod_cons, mul_comm b, mul_assoc, Multiset.prod_erase h, mul_comm]

Premises used: Multiset.prod_cons, mul_assoc, mul_comm, Multiset.prod_erase
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Defs
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : WfDvdMonoid α
f : Multiset α
hi : ∀ b ∈ f, Irreducible b
u : αˣ
hn0 : f.prod * (↑u : α) ≠ 0
hnu : ¬IsUnit (f.prod * (↑u : α))
b : α
h : b ∈ f
refine_1 : ∀ (a : α) (ha : a ∈ b * (↑u : α) ::ₘ f.erase b), Irreducible a
refine_2 refine_2₁ : (b * (↑u : α) ::ₘ f.erase b).prod = f.prod * (↑u : α)
⊢ ∃ (f_1 : Multiset α), (∀ b ∈ f_1, Irreducible b) ∧ f_1.prod = f.prod * (↑u : α) ∧ f_1 ≠ ∅

Tactic:
classical
      refine ⟨(f.erase b).cons (b * u), fun a ha => ?_, ?_, Multiset.cons_ne_zero⟩
      · obtain rfl | ha := Multiset.mem_cons.1 ha
        exacts [Associated.irreducible ⟨u, rfl⟩ (hi b h), hi a (Multiset.mem_of_mem_erase ha)]
      · rw [Multiset.prod_cons, mul_comm b, mul_assoc, Multiset.prod_erase h, mul_comm]

Premises used: Multiset.prod_cons, mul_assoc, Associated.irreducible, Exists.intro, mul_comm, rfl
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Defs
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : WfDvdMonoid α
x y : α
nonzero : ¬(x = 0 ∧ y = 0)
H : ∀ (z : α), Irreducible z → z ∣ x → ¬z ∣ y
⊢ IsRelPrime x y

Tactic:
isRelPrime_of_no_nonunits_factors nonzero fun _z znu znz zx zy ↦
    have ⟨i, h1, h2⟩ := exists_irreducible_factor znu znz
    H i h1 (h2.trans zx) (h2.trans zy)

Premises used: False, _private.0.WfDvdMonoid.isRelPrime_of_no_irreducible_factors.match_1, WfDvdMonoid.exists_irreducible_factor, isRelPrime_of_no_nonunits_factors, Dvd.dvd.trans
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Defs
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a : α
simp_rw : a ≠ 0 → ∃ (f : Multiset α), (∀ b ∈ f, Irreducible b) ∧ f.prod ~ᵤ a
⊢ a ≠ 0 → ∃ (f : Multiset α), (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a

Tactic:
simp_rw [← UniqueFactorizationMonoid.irreducible_iff_prime]

Premises used: UniqueFactorizationMonoid.irreducible_iff_prime
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Defs
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a : α
⊢ a ≠ 0 → ∃ (f : Multiset α), (∀ b ∈ f, Irreducible b) ∧ f.prod ~ᵤ a

Tactic:
apply WfDvdMonoid.exists_factors a

Premises used: WfDvdMonoid.exists_factors
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Defs
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
⊢ (∃ (p : α), Prime p) ↔ ∃ (x : α), x ≠ 0 ∧ ¬IsUnit x

Tactic:
⟨fun ⟨p, hp⟩ ↦ ⟨p, hp.ne_zero, hp.not_unit⟩, fun ⟨x, hx₀, hxu⟩ ↦ ?_⟩

Premises used: Prime, IsUnit, Exists, _private.0.UniqueFactorizationMonoid.exists_prime_iff.match_1, Ne, Prime.not_unit, And, _private.0.UniqueFactorizationMonoid.exists_prime_iff.match_2, And.intro, Iff.intro, Exists.intro, Prime.ne_zero, OfNat.ofNat, Not
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Defs
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
refine : (∃ (x : α), x ≠ 0 ∧ ¬IsUnit x) → ∀ (x : α) (hx₀ : x ≠ 0) (hxu : ¬IsUnit x), ∃ (p : α), Prime p
⊢ (∃ (p : α), Prime p) ↔ ∃ (x : α), x ≠ 0 ∧ ¬IsUnit x

Tactic:
refine ⟨fun ⟨p, hp⟩ ↦ ⟨p, hp.ne_zero, hp.not_unit⟩, fun ⟨x, hx₀, hxu⟩ ↦ ?_⟩
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Defs
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
h : ∃ (x : α), x ≠ 0 ∧ ¬IsUnit x
x : α
hx₀ : x ≠ 0
hxu : ¬IsUnit x
obtain : ∀ (f : α) (hf : Irreducible f), ∃ (p : α), Prime p
⊢ ∃ (p : α), Prime p

Tactic:
obtain ⟨f, hf, -⟩ := WfDvdMonoid.exists_irreducible_factor hxu hx₀

Premises used: WfDvdMonoid.exists_irreducible_factor
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Defs
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
h : ∃ (x : α), x ≠ 0 ∧ ¬IsUnit x
x : α
hx₀ : x ≠ 0
hxu : ¬IsUnit x
f : α
hf : Irreducible f
⊢ ∃ (p : α), Prime p

Tactic:
⟨f, UniqueFactorizationMonoid.irreducible_iff_prime.mp hf⟩

Premises used: UniqueFactorizationMonoid.irreducible_iff_prime, Exists.intro, Iff.mp
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Defs
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
h : ∃ (x : α), x ≠ 0 ∧ ¬IsUnit x
x : α
hx₀ : x ≠ 0
hxu : ¬IsUnit x
f : α
hf : Irreducible f
⊢ ∃ (p : α), Prime p

Tactic:
exact ⟨f, UniqueFactorizationMonoid.irreducible_iff_prime.mp hf⟩
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Defs
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
P : α → Prop
a : α
h₁ : P 0
h₂ : ∀ (x : α), IsUnit x → P x
h₃ : ∀ (a p : α), a ≠ 0 → Prime p → P a → P (p * a)
⊢ ∀ (a p : α), a ≠ 0 → Irreducible p → P a → P (p * a)

Tactic:
simp_rw [← UniqueFactorizationMonoid.irreducible_iff_prime] at h₃

Premises used: UniqueFactorizationMonoid.irreducible_iff_prime
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Defs
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
P : α → Prop
a : α
h₁ : P 0
h₂ : ∀ (x : α), IsUnit x → P x
h₃ : ∀ (a p : α), a ≠ 0 → Irreducible p → P a → P (p * a)
⊢ P a

Tactic:
WfDvdMonoid.induction_on_irreducible a h₁ h₂ h₃

Premises used: WfDvdMonoid.induction_on_irreducible
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Defs
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
P : α → Prop
a : α
h₁ : P 0
h₂ : ∀ (x : α), IsUnit x → P x
h₃ : ∀ (a p : α), a ≠ 0 → Irreducible p → P a → P (p * a)
⊢ P a

Tactic:
exact WfDvdMonoid.induction_on_irreducible a h₁ h₂ h₃
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Defs
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a : α
inl : IsPrimal.{u_1} (α := α) 0
inr : ∀ (ha : a ≠ 0), IsPrimal a
⊢ IsPrimal a

Tactic:
obtain rfl | ha := eq_or_ne a 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Defs
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
⊢ IsPrimal.{u_1} (α := α) 0

Tactic:
isPrimal_zero

Premises used: isPrimal_zero
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Defs
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
⊢ IsPrimal.{u_1} (α := α) 0

Tactic:
exact isPrimal_zero

Premises used: isPrimal_zero
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Defs
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a : α
ha : a ≠ 0
inr : ∀ (f : Multiset α) (hf : ∀ b ∈ f, Prime b) (u : αˣ) (ha : f.prod * (↑u : α) ≠ 0), IsPrimal (f.prod * (↑u : α))
⊢ IsPrimal a

Tactic:
obtain ⟨f, hf, u, rfl⟩ := exists_prime_factors a ha

Premises used: UniqueFactorizationMonoid.exists_prime_factors, rfl
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Defs
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
f : Multiset α
hf : ∀ b ∈ f, Prime b
u : αˣ
ha : f.prod * (↑u : α) ≠ 0
⊢ IsPrimal (f.prod * (↑u : α))

Tactic:
((Submonoid.isPrimal α).multiset_prod_mem f (hf · · |>.isPrimal)).mul u.isUnit.isPrimal

Premises used: Prime.isPrimal, IsUnit.isPrimal, Submonoid.multiset_prod_mem, Submonoid.isPrimal, IsPrimal.mul, Units.isUnit
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Defs
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
f : Multiset α
hf : ∀ b ∈ f, Prime b
u : αˣ
ha : f.prod * (↑u : α) ≠ 0
⊢ IsPrimal (f.prod * (↑u : α))

Tactic:
exact ((Submonoid.isPrimal α).multiset_prod_mem f (hf · · |>.isPrimal)).mul u.isUnit.isPrimal

Premises used: Prime.isPrimal, IsUnit.isPrimal, Submonoid.multiset_prod_mem, Submonoid.isPrimal, IsPrimal.mul, Units.isUnit
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Defs
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a : α
ane0 : a ≠ 0
rw : (Classical.choose (p := fun (x : Multiset α) ↦ (∀ b ∈ x, Prime b) ∧ x.prod ~ᵤ a) ⋯).prod ~ᵤ a
⊢ (factors a).prod ~ᵤ a

Tactic:
rw [factors, dif_neg ane0]

Premises used: UniqueFactorizationMonoid.factors, dif_neg
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Defs
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a : α
ane0 : a ≠ 0
⊢ (Classical.choose (p := fun (x : Multiset α) ↦ (∀ b ∈ x, Prime b) ∧ x.prod ~ᵤ a) ⋯).prod ~ᵤ a

Tactic:
(Classical.choose_spec (exists_prime_factors a ane0)).2

Premises used: UniqueFactorizationMonoid.exists_prime_factors, Classical.choose_spec, And.right
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Defs
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a : α
ane0 : a ≠ 0
⊢ (Classical.choose (p := fun (x : Multiset α) ↦ (∀ b ∈ x, Prime b) ∧ x.prod ~ᵤ a) ⋯).prod ~ᵤ a

Tactic:
exact (Classical.choose_spec (exists_prime_factors a ane0)).2

Premises used: UniqueFactorizationMonoid.exists_prime_factors, Classical.choose_spec, And.right
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Defs
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
⊢ Eq.{u_1 + 1} (α := Multiset α) (factors 0) 0

Tactic:
simp [factors]

Premises used: UniqueFactorizationMonoid.factors
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Defs
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
p : α
h : Membership.mem (γ := Multiset α) (factors 0) p
⊢ False

Tactic:
simp at h
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Defs
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
p a : α
h : p ∈ factors a
⊢ p ∣ a

Tactic:
dvd_trans (Multiset.dvd_prod h) (Associated.dvd (factors_prod (ne_zero_of_mem_factors h)))

Premises used: Associated.dvd, Multiset.dvd_prod, dvd_trans, UniqueFactorizationMonoid.ne_zero_of_mem_factors, UniqueFactorizationMonoid.factors_prod
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Defs
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a x : α
hx : x ∈ factors a
⊢ a ≠ 0

Tactic:
have ane0 := ne_zero_of_mem_factors hx
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Defs
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a x : α
hx : x ∈ factors a
ane0 : a ≠ 0
⊢ a ≠ 0

Tactic:
rw [factors, dif_neg ane0] at hx

Premises used: UniqueFactorizationMonoid.factors, dif_neg
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Defs
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a x : α
hx : x ∈ factors a
ane0 ane0₁ : a ≠ 0
⊢ x ∈ Classical.choose (p := fun (x : Multiset α) ↦ (∀ b ∈ x, Prime b) ∧ x.prod ~ᵤ a) ⋯

Tactic:
rw [factors, dif_neg ane0] at hx

Premises used: UniqueFactorizationMonoid.factors, dif_neg
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Defs
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a x : α
ane0 : a ≠ 0
hx : x ∈ Classical.choose (p := fun (x : Multiset α) ↦ (∀ b ∈ x, Prime b) ∧ x.prod ~ᵤ a) ⋯
⊢ Prime x

Tactic:
(Classical.choose_spec (UniqueFactorizationMonoid.exists_prime_factors a ane0)).1 x hx

Premises used: UniqueFactorizationMonoid.exists_prime_factors, Classical.choose_spec, And.left
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Defs
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a x : α
ane0 : a ≠ 0
hx : x ∈ Classical.choose (p := fun (x : Multiset α) ↦ (∀ b ∈ x, Prime b) ∧ x.prod ~ᵤ a) ⋯
⊢ Prime x

Tactic:
exact (Classical.choose_spec (UniqueFactorizationMonoid.exists_prime_factors a ane0)).1 x hx

Premises used: UniqueFactorizationMonoid.exists_prime_factors, Classical.choose_spec, And.left
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Defs
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a : α
⊢ ∀ x ∈ factors a, Irreducible x

Tactic:
fun x h =>
  (prime_of_factor x h).irreducible

Premises used: Prime.irreducible, UniqueFactorizationMonoid.prime_of_factor
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Defs
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a : α
ha : Irreducible a
hf : factors a = 0
⊢ False

Tactic:
simpa [hf, Associated.comm, ha.not_isUnit] using factors_prod ha.ne_zero

Premises used: Associated.comm, Irreducible.not_isUnit, UniqueFactorizationMonoid.factors_prod, Irreducible.ne_zero
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Defs
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a : α
ha : Irreducible a
⊢ factors a ≠ 0

Tactic:
have hf : factors a ≠ 0 := by
    intro hf
    simpa [hf, Associated.comm, ha.not_isUnit] using factors_prod ha.ne_zero
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Defs
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a : α
ha : Irreducible a
hf : factors a ≠ 0
obtain : ∀ (b : α) (hb : b ∈ factors a), (factors a).card = 1
⊢ (factors a).card = 1

Tactic:
obtain ⟨b, hb⟩ := exists_mem_of_ne_zero hf

Premises used: Multiset.exists_mem_of_ne_zero
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Defs
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a : α
ha : Irreducible a
hf : factors a ≠ 0
b : α
hb : b ∈ factors a
obtain : ∀ (f : Multiset α) (hf : factors a = b ::ₘ f), (factors a).card = 1
⊢ (factors a).card = 1

Tactic:
obtain ⟨f, hf⟩ := exists_cons_of_mem hb

Premises used: Multiset.exists_cons_of_mem