awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
x : α
hx : x ≠ 0
mp : 0 < normalizedFactors x → ¬IsUnit x
mpr : ¬IsUnit x → 0 < normalizedFactors x
⊢ 0 < normalizedFactors x ↔ ¬IsUnit x

Tactic:
constructor
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
x : α
hx_1 : x ≠ 0
h : 0 < normalizedFactors x
hx : IsUnit x
mp : ∀ (p : α) (hp : p ∈ normalizedFactors x), False
⊢ False

Tactic:
obtain ⟨p, hp⟩ := Multiset.exists_mem_of_ne_zero h.ne'

Premises used: LT.lt.ne', Multiset.exists_mem_of_ne_zero
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
x : α
hx_1 : x ≠ 0
h : 0 < normalizedFactors x
hx : IsUnit x
p : α
hp : p ∈ normalizedFactors x
⊢ False

Tactic:
(prime_of_normalized_factor _ hp).not_unit
        (isUnit_of_dvd_unit (dvd_of_mem_normalizedFactors hp) hx)

Premises used: UniqueFactorizationMonoid.dvd_of_mem_normalizedFactors, isUnit_of_dvd_unit, Prime.not_unit, UniqueFactorizationMonoid.prime_of_normalized_factor
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
x : α
hx_1 : x ≠ 0
h : 0 < normalizedFactors x
hx : IsUnit x
p : α
hp : p ∈ normalizedFactors x
⊢ False

Tactic:
exact
      (prime_of_normalized_factor _ hp).not_unit
        (isUnit_of_dvd_unit (dvd_of_mem_normalizedFactors hp) hx)

Premises used: UniqueFactorizationMonoid.dvd_of_mem_normalizedFactors, isUnit_of_dvd_unit, Prime.not_unit, UniqueFactorizationMonoid.prime_of_normalized_factor
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
x : α
hx : x ≠ 0
h : ¬IsUnit x
mpr : ∀ (p : α) (hp : p ∈ normalizedFactors x), 0 < normalizedFactors x
⊢ 0 < normalizedFactors x

Tactic:
obtain ⟨p, hp⟩ := exists_mem_normalizedFactors hx h

Premises used: UniqueFactorizationMonoid.exists_mem_normalizedFactors
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
x : α
hx : x ≠ 0
h : ¬IsUnit x
p : α
hp : p ∈ normalizedFactors x
⊢ 0 < normalizedFactors x

Tactic:
bot_lt_iff_ne_bot.mpr
        (mt Multiset.eq_zero_iff_forall_notMem.mp (not_forall.mpr ⟨p, not_not.mpr hp⟩))

Premises used: Iff.mpr, Classical.not_not, Multiset.eq_zero_iff_forall_notMem, mt, bot_lt_iff_ne_bot, Exists.intro, Iff.mp, Classical.not_forall
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
x : α
hx : x ≠ 0
h : ¬IsUnit x
p : α
hp : p ∈ normalizedFactors x
⊢ 0 < normalizedFactors x

Tactic:
exact
      bot_lt_iff_ne_bot.mpr
        (mt Multiset.eq_zero_iff_forall_notMem.mp (not_forall.mpr ⟨p, not_not.mpr hp⟩))

Premises used: Iff.mpr, Classical.not_not, Multiset.eq_zero_iff_forall_notMem, mt, bot_lt_iff_ne_bot, Exists.intro, Iff.mp, Classical.not_forall
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
x : α
hx : x ≠ 0
rw : ¬normalizedFactors x = 0 ↔ ¬IsUnit x
rw₁ : ¬normalizedFactors x = 0 ↔ 0 < normalizedFactors x
rw₂ rw₃ : ¬normalizedFactors x = 0 ↔ normalizedFactors x ≠ 0
⊢ normalizedFactors x = 0 ↔ IsUnit x

Tactic:
rw [← not_iff_not, ← normalizedFactors_pos _ hx, pos_iff_ne_zero]

Premises used: not_iff_not, UniqueFactorizationMonoid.normalizedFactors_pos, pos_iff_ne_zero
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
x : α
hx : IsUnit x
inl : ∀ (hx : IsUnit.{u_1} (M := α) 0), Eq.{u_1 + 1} (α := Multiset α) (normalizedFactors 0) 0
inr : ∀ (hx₀ : x ≠ 0), normalizedFactors x = 0
⊢ normalizedFactors x = 0

Tactic:
obtain rfl | hx₀ := eq_or_ne x 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
hx : IsUnit.{u_1} (M := α) 0
⊢ Eq.{u_1 + 1} (α := Multiset α) (normalizedFactors 0) 0

Tactic:
simp
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
x : α
hx : IsUnit x
hx₀ : x ≠ 0
inr inr₁ inr₂ inr₃ : IsUnit x
⊢ normalizedFactors x = 0

Tactic:
rwa [normalizedFactors_eq_zero_iff hx₀]

Premises used: UniqueFactorizationMonoid.normalizedFactors_eq_zero_iff
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
mp : DvdNotUnit x y → normalizedFactors x < normalizedFactors y
mpr : normalizedFactors x < normalizedFactors y → DvdNotUnit x y
⊢ DvdNotUnit x y ↔ normalizedFactors x < normalizedFactors y

Tactic:
constructor
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
x : α
hx left : x ≠ 0
c : α
hc : ¬IsUnit c
hy : x * c ≠ 0
⊢ normalizedFactors x < normalizedFactors (x * c)

Tactic:
simp only [hx, right_ne_zero_of_mul hy, normalizedFactors_mul, Ne, not_false_iff,
      lt_add_iff_pos_right, normalizedFactors_pos, hc]

Premises used: lt_add_iff_pos_right, UniqueFactorizationMonoid.normalizedFactors_mul, UniqueFactorizationMonoid.normalizedFactors_pos, right_ne_zero_of_mul, Ne, not_false_iff
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
h : normalizedFactors x < normalizedFactors y
⊢ DvdNotUnit x y

Tactic:
dvdNotUnit_of_dvd_of_not_dvd
        ((dvd_iff_normalizedFactors_le_normalizedFactors hx hy).mpr h.le)
        (mt (dvd_iff_normalizedFactors_le_normalizedFactors hy hx).mp h.not_ge)

Premises used: Iff.mpr, mt, LT.lt.le, dvdNotUnit_of_dvd_of_not_dvd, Iff.mp, UniqueFactorizationMonoid.dvd_iff_normalizedFactors_le_normalizedFactors, LT.lt.not_ge
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
h : normalizedFactors x < normalizedFactors y
⊢ DvdNotUnit x y

Tactic:
exact
      dvdNotUnit_of_dvd_of_not_dvd
        ((dvd_iff_normalizedFactors_le_normalizedFactors hx hy).mpr h.le)
        (mt (dvd_iff_normalizedFactors_le_normalizedFactors hy hx).mp h.not_ge)

Premises used: Iff.mpr, mt, LT.lt.le, dvdNotUnit_of_dvd_of_not_dvd, Iff.mp, UniqueFactorizationMonoid.dvd_iff_normalizedFactors_le_normalizedFactors, LT.lt.not_ge
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
s : Multiset α
hs : 0 ∉ s
inl : Subsingleton α → normalizedFactors s.prod = (Multiset.map normalizedFactors s).sum
inr : Nontrivial α → normalizedFactors s.prod = (Multiset.map normalizedFactors s).sum
⊢ normalizedFactors s.prod = (Multiset.map normalizedFactors s).sum

Tactic:
cases subsingleton_or_nontrivial α

Premises used: subsingleton_or_nontrivial
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
s : Multiset α
hs : 0 ∉ s
h : Subsingleton α
a : ∀ (x : α), x ∉ s
⊢ s = 0

Tactic:
apply Multiset.eq_zero_of_forall_notMem

Premises used: Multiset.eq_zero_of_forall_notMem
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
s : Multiset α
hs : 0 ∉ s
h : Subsingleton α
x : α
⊢ 0 ∉ s

Tactic:
hs
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
s : Multiset α
hs : 0 ∉ s
h : Subsingleton α
x : α
⊢ x ∉ s

Tactic:
convert! hs
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
s : Multiset α
hs : 0 ∉ s
h : Subsingleton α
inl :
  ∀ (hs : 0 ∉ 0),
    Eq.{u_1 + 1} (α := Multiset α) (normalizedFactors (Multiset.prod 0))
      (Multiset.sum (Multiset.map normalizedFactors 0))
⊢ normalizedFactors s.prod = (Multiset.map normalizedFactors s).sum

Tactic:
obtain rfl : s = 0 := by
      apply Multiset.eq_zero_of_forall_notMem
      intro _
      convert! hs

Premises used: rfl
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
h : Subsingleton α
hs : 0 ∉ 0
⊢ Eq.{u_1 + 1} (α := Multiset α) (normalizedFactors (Multiset.prod 0)) (Multiset.sum (Multiset.map normalizedFactors 0))

Tactic:
simp
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
h : Nontrivial α
hs : 0 ∉ 0
⊢ Eq.{u_1 + 1} (α := Multiset α) (normalizedFactors (Multiset.prod 0)) (Multiset.sum (Multiset.map normalizedFactors 0))

Tactic:
simp
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
h : Nontrivial α
a : α
s : Multiset α
IH : ∀ (hs : 0 ∉ s), normalizedFactors s.prod = (Multiset.map normalizedFactors s).sum
hs : 0 ∉ a ::ₘ s
inr : 0 ∉ s
inr₁ : a ≠ 0
inr₂ : s.prod ≠ 0
⊢ normalizedFactors (a ::ₘ s).prod = (Multiset.map normalizedFactors (a ::ₘ s)).sum

Tactic:
rw [Multiset.prod_cons, Multiset.map_cons, Multiset.sum_cons, normalizedFactors_mul, IH]

Premises used: Multiset.map_cons, Multiset.prod_cons, UniqueFactorizationMonoid.normalizedFactors_mul, Multiset.sum_cons
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
h : Nontrivial α
a : α
s : Multiset α
IH : ∀ (hs : 0 ∉ s), normalizedFactors s.prod = (Multiset.map normalizedFactors s).sum
hs : 0 ∉ a ::ₘ s
⊢ 0 ∉ s

Tactic:
fun h ↦ hs (Multiset.mem_cons_of_mem h)

Premises used: Multiset.mem_cons_of_mem, Not
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
h : Nontrivial α
a : α
s : Multiset α
IH : ∀ (hs : 0 ∉ s), normalizedFactors s.prod = (Multiset.map normalizedFactors s).sum
hs : 0 ∉ a ::ₘ s
⊢ 0 ∉ s

Tactic:
exact fun h ↦ hs (Multiset.mem_cons_of_mem h)

Premises used: Multiset.mem_cons_of_mem
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
h : Nontrivial α
a : α
s : Multiset α
IH : ∀ (hs : 0 ∉ s), normalizedFactors s.prod = (Multiset.map normalizedFactors s).sum
hs : 0 ∉ a ::ₘ s
⊢ a ≠ 0

Tactic:
fun h ↦ hs (h ▸ Multiset.mem_cons_self _ _)

Premises used: Eq.rec, Multiset.mem_cons_self, Not
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
h : Nontrivial α
a : α
s : Multiset α
IH : ∀ (hs : 0 ∉ s), normalizedFactors s.prod = (Multiset.map normalizedFactors s).sum
hs : 0 ∉ a ::ₘ s
⊢ a ≠ 0

Tactic:
exact fun h ↦ hs (h ▸ Multiset.mem_cons_self _ _)
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
h : Nontrivial α
a : α
s : Multiset α
IH : ∀ (hs : 0 ∉ s), normalizedFactors s.prod = (Multiset.map normalizedFactors s).sum
hs : 0 ∉ a ::ₘ s
inr : 0 ∉ s
⊢ s.prod ≠ 0

Tactic:
apply Multiset.prod_ne_zero

Premises used: Multiset.prod_ne_zero
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
s : Multiset α
hs : 0 ∉ s
h : Nontrivial α
inr :
  ∀ (hs : 0 ∉ 0),
    Eq.{u_1 + 1} (α := Multiset α) (normalizedFactors (Multiset.prod 0))
      (Multiset.sum (Multiset.map normalizedFactors 0))
inr₁ :
  ∀ (a : α) (s : Multiset α) (IH : ∀ (hs : 0 ∉ s), normalizedFactors s.prod = (Multiset.map normalizedFactors s).sum)
    (hs : 0 ∉ a ::ₘ s), normalizedFactors (a ::ₘ s).prod = (Multiset.map normalizedFactors (a ::ₘ s)).sum
⊢ normalizedFactors s.prod = (Multiset.map normalizedFactors s).sum

Tactic:
induction s using Multiset.induction with
  | empty => simp
  | cons _ _ IH =>
    rw [Multiset.prod_cons, Multiset.map_cons, Multiset.sum_cons, normalizedFactors_mul, IH]
    · exact fun h ↦ hs (Multiset.mem_cons_of_mem h)
    · exact fun h ↦ hs (h ▸ Multiset.mem_cons_self _ _)
    · apply Multiset.prod_ne_zero
      exact fun h ↦ hs (Multiset.mem_cons_of_mem h)

Premises used: Multiset.map_cons, Multiset.prod_cons, Multiset.prod_ne_zero, UniqueFactorizationMonoid.normalizedFactors_mul, Multiset.sum_cons
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
β : Type u_2
inst_3 : CommMonoidWithZero β
inst_4 : NormalizationMonoid β
inst_5 : UniqueFactorizationMonoid β
F : Type u_3
inst_6 : EquivLike F α β
inst_7 : MulEquivClass F α β
f : F
he :
  ∀ (x : α),
    Eq (α := β) ((normalize : (a : β) → β) ((f : (a : α) → β) x : β) : β)
      ((f : (a : α) → β) ((normalize : (a : α) → α) x : α) : β)
a x : α
inl :
  Membership.mem (γ := Multiset α) (normalizedFactors 0) x ↔
    Membership.mem.{u_2, u_2} (α := β) (γ := Multiset β) (normalizedFactors ((f : (a : α) → β) 0) : Multiset β)
      (((↑f : α ≃ β) : (a : α) → β) x : β)
inr :
  ∀ (ha : a ≠ 0),
    x ∈ normalizedFactors a ↔
      Membership.mem.{u_2, u_2} (α := β) (γ := Multiset β) (normalizedFactors ((f : (a : α) → β) a) : Multiset β)
        (((↑f : α ≃ β) : (a : α) → β) x : β)
⊢ x ∈ normalizedFactors a ↔
    Membership.mem.{u_2, u_2} (α := β) (γ := Multiset β) (normalizedFactors ((f : (a : α) → β) a) : Multiset β)
      (((↑f : α ≃ β) : (a : α) → β) x : β)

Tactic:
rcases eq_or_ne a 0 with rfl | ha

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
β : Type u_2
inst_3 : CommMonoidWithZero β
inst_4 : NormalizationMonoid β
inst_5 : UniqueFactorizationMonoid β
F : Type u_3
inst_6 : EquivLike F α β
inst_7 : MulEquivClass F α β
f : F
he :
  ∀ (x : α),
    Eq (α := β) ((normalize : (a : β) → β) ((f : (a : α) → β) x : β) : β)
      ((f : (a : α) → β) ((normalize : (a : α) → α) x : α) : β)
x : α
⊢ Membership.mem (γ := Multiset α) (normalizedFactors 0) x ↔
    Membership.mem.{u_2, u_2} (α := β) (γ := Multiset β) (normalizedFactors ((f : (a : α) → β) 0) : Multiset β)
      (((↑f : α ≃ β) : (a : α) → β) x : β)

Tactic:
simp
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
β : Type u_2
inst_3 : CommMonoidWithZero β
inst_4 : NormalizationMonoid β
inst_5 : UniqueFactorizationMonoid β
F : Type u_3
inst_6 : EquivLike F α β
inst_7 : MulEquivClass F α β
f : F
he :
  ∀ (x : α),
    Eq (α := β) ((normalize : (a : β) → β) ((f : (a : α) → β) x : β) : β)
      ((f : (a : α) → β) ((normalize : (a : α) → α) x : α) : β)
a x : α
ha : a ≠ 0
⊢ x ∈ normalizedFactors a ↔
    Membership.mem.{u_2, u_2} (α := β) (γ := Multiset β) (normalizedFactors ((f : (a : α) → β) a) : Multiset β)
      (((↑f : α ≃ β) : (a : α) → β) x : β)

Tactic:
simp [mem_normalizedFactors_iff' ha,
        mem_normalizedFactors_iff' (EmbeddingLike.map_ne_zero_iff.mpr ha), map_dvd_iff_dvd_symm,
        MulEquiv.irreducible_iff, he]

Premises used: Iff.mpr, map_dvd_iff_dvd_symm, MulEquiv.irreducible_iff, EmbeddingLike.map_ne_zero_iff, UniqueFactorizationMonoid.mem_normalizedFactors_iff'
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
β : Type u_2
inst_3 : CommMonoidWithZero β
inst_4 : NormalizationMonoid β
inst_5 : UniqueFactorizationMonoid β
F : Type u_3
inst_6 : EquivLike F α β
inst_7 : MulEquivClass F α β
f : F
he :
  ∀ (x : α),
    Eq (α := β) ((normalize : (a : β) → β) ((f : (a : α) → β) x : β) : β)
      ((f : (a : α) → β) ((normalize : (a : α) → α) x : α) : β)
a p : α
hp : p ∈ normalizedFactors a
⊢ Eq.{u_2 + 1} (α := β)
    ((↑(((normalizedFactorsEquiv he a :
                Equiv.{u_1 + 1, u_2 + 1} { x : α // x ∈ normalizedFactors a }
                  { y : β //
                    Membership.mem (γ := Multiset β) (normalizedFactors ((f : (a : α) → β) a) : Multiset β) y }) :
              (a_1 : { x : α // x ∈ normalizedFactors a }) → { y : β // y ∈ normalizedFactors ((f : (a : α) → β) a) })
            (Subtype.mk (p := fun (x : α) ↦ x ∈ normalizedFactors a) p hp)) :
        β) :
      β)
    ((f : (a : α) → β) p : β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
β : Type u_2
inst_3 : CommMonoidWithZero β
inst_4 : NormalizationMonoid β
inst_5 : UniqueFactorizationMonoid β
F : Type u_3
inst_6 : EquivLike F α β
inst_7 : MulEquivClass F α β
f : F
he :
  ∀ (x : α),
    Eq (α := β) ((normalize : (a : β) → β) ((f : (a : α) → β) x : β) : β)
      ((f : (a : α) → β) ((normalize : (a : α) → α) x : α) : β)
a : α
q : β
hq : Membership.mem (γ := Multiset β) (normalizedFactors ((f : (a : α) → β) a) : Multiset β) q
⊢ Eq.{u_1 + 1} (α := α)
    ((↑(((Equiv.symm (normalizedFactorsEquiv he a) :
                Equiv.{u_2 + 1, u_1 + 1}
                  { y : β // Membership.mem (γ := Multiset β) (normalizedFactors ((f : (a : α) → β) a) : Multiset β) y }
                  { x : α // x ∈ normalizedFactors a }) :
              (a_1 : { y : β // y ∈ normalizedFactors ((f : (a : α) → β) a) }) → { x : α // x ∈ normalizedFactors a })
            (Subtype.mk (p := fun (y : β) ↦
              Membership.mem (γ := Multiset β) (normalizedFactors ((f : (a : α) → β) a) : Multiset β) y) q hq)) :
        α) :
      α)
    ((MulEquiv.symm (↑f : α ≃* β) : (a : β) → α) q : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
⊢ Nontrivial α

Tactic:
nontriviality α
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
h : Nontrivial α
⊢ Eq.{u_1 + 1} (α := α)
    (if Eq.{u_1 + 1} (α := Associates α) 1 0 then 0
    else
      prod
        (map (α := Associates α)
          (Classical.choose (p := fun (x : Associates α → α) ↦ Function.RightInverse x Associates.mk) ⋯)
          (normalizedFactors 1)))
    1

Tactic:
simp
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
x y : Associates α
pos :
  ∀ (hx : x = 0),
    (if x * y = 0 then 0
      else
        (map (Classical.choose (p := fun (x : Associates α → α) ↦ Function.RightInverse x Associates.mk) ⋯)
            (normalizedFactors (x * y))).prod) =
      (if x = 0 then 0
        else
          (map (Classical.choose (p := fun (x : Associates α → α) ↦ Function.RightInverse x Associates.mk) ⋯)
              (normalizedFactors x)).prod) *
        if y = 0 then 0
        else
          (map (Classical.choose (p := fun (x : Associates α → α) ↦ Function.RightInverse x Associates.mk) ⋯)
              (normalizedFactors y)).prod
neg :
  ∀ (hx : ¬x = 0),
    (if x * y = 0 then 0
      else
        (map (Classical.choose (p := fun (x : Associates α → α) ↦ Function.RightInverse x Associates.mk) ⋯)
            (normalizedFactors (x * y))).prod) =
      (if x = 0 then 0
        else
          (map (Classical.choose (p := fun (x : Associates α → α) ↦ Function.RightInverse x Associates.mk) ⋯)
              (normalizedFactors x)).prod) *
        if y = 0 then 0
        else
          (map (Classical.choose (p := fun (x : Associates α → α) ↦ Function.RightInverse x Associates.mk) ⋯)
              (normalizedFactors y)).prod
⊢ (if x * y = 0 then 0
    else
      (map (Classical.choose (p := fun (x : Associates α → α) ↦ Function.RightInverse x Associates.mk) ⋯)
          (normalizedFactors (x * y))).prod) =
    (if x = 0 then 0
      else
        (map (Classical.choose (p := fun (x : Associates α → α) ↦ Function.RightInverse x Associates.mk) ⋯)
            (normalizedFactors x)).prod) *
      if y = 0 then 0
      else
        (map (Classical.choose (p := fun (x : Associates α → α) ↦ Function.RightInverse x Associates.mk) ⋯)
            (normalizedFactors y)).prod

Tactic:
by_cases hx : x = 0
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
x y : Associates α
hx : x = 0
⊢ (if x * y = 0 then 0
    else
      (map (Classical.choose (p := fun (x : Associates α → α) ↦ Function.RightInverse x Associates.mk) ⋯)
          (normalizedFactors (x * y))).prod) =
    (if x = 0 then 0
      else
        (map (Classical.choose (p := fun (x : Associates α → α) ↦ Function.RightInverse x Associates.mk) ⋯)
            (normalizedFactors x)).prod) *
      if y = 0 then 0
      else
        (map (Classical.choose (p := fun (x : Associates α → α) ↦ Function.RightInverse x Associates.mk) ⋯)
            (normalizedFactors y)).prod

Tactic:
simp [hx]