awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
h : Nontrivial α
x : α
hx : Membership.mem (γ := Multiset α) 0 x
⊢ False

Tactic:
apply Multiset.notMem_zero x hx

Premises used: Multiset.notMem_zero
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
h : Nontrivial α
⊢ Associated.{u_1} (M := α) (Multiset.prod (normalizedFactors 1)) (Multiset.prod 0)

Tactic:
apply prod_normalizedFactors one_ne_zero

Premises used: UniqueFactorizationMonoid.prod_normalizedFactors, one_ne_zero
-- 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 : ∀ (x : α), (normalize : (a : α) → α) x = Function.comp (β := Associates α) Associates.out Associates.mk x
⊢ Eq.{u_1 + 1} (α := (a : α) → α) (⇑normalize : (a : α) → α)
    (Function.comp (β := Associates α) Associates.out Associates.mk)

Tactic:
ext
-- 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
x_1 : α
h : (normalize : (a : α) → α) x_1 = Associates.out (Associates.mk x_1)
h₁ h₂ : Eq (α := α) ((normalize : (a : α) → α) x_1 : α) ((normalize : (a : α) → α) x_1 : α)
⊢ (normalize : (a : α) → α) x_1 = Function.comp (β := Associates α) Associates.out Associates.mk x_1

Tactic:
rw [Function.comp_apply, Associates.out_mk]

Premises used: Associates.out_mk, Function.comp_apply
-- 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
⊢ Eq.{u_1 + 1} (α := (a : α) → α) (⇑normalize : (a : α) → α)
    (Function.comp (β := Associates α) Associates.out Associates.mk)

Tactic:
have h : (normalize : α → α) = Associates.out ∘ Associates.mk := by
    ext
    rw [Function.comp_apply, Associates.out_mk]
-- 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 :
  Eq.{u_1 + 1} (α := (a : α) → α) (⇑normalize : (a : α) → α)
    (Function.comp (β := Associates α) Associates.out Associates.mk)
rw :
  Multiset.map (α := Associates α) Associates.out
      (Multiset.map Associates.mk (normalizedFactors x + normalizedFactors y)) =
    Multiset.map (α := Associates α) Associates.out (Multiset.map Associates.mk (normalizedFactors (x * y)))
⊢ normalizedFactors (x * y) = normalizedFactors x + normalizedFactors y

Tactic:
rw [← Multiset.map_id' (normalizedFactors (x * y)), ← Multiset.map_id' (normalizedFactors x), ←
    Multiset.map_id' (normalizedFactors y), ← Multiset.map_congr rfl normalize_normalized_factor, ←
    Multiset.map_congr rfl normalize_normalized_factor, ←
    Multiset.map_congr rfl normalize_normalized_factor, ← Multiset.map_add, h, ←
    Multiset.map_map Associates.out, eq_comm, ← Multiset.map_map Associates.out]

Premises used: UniqueFactorizationMonoid.normalizedFactors, HMul.hMul, UniqueFactorizationMonoid.normalize_normalized_factor, eq_comm, Multiset.map_congr, Associates.out, Multiset.map_map, Multiset.map_id', Multiset.map_add, rfl
-- 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 :
  Eq.{u_1 + 1} (α := (a : α) → α) (⇑normalize : (a : α) → α)
    (Function.comp (β := Associates α) Associates.out Associates.mk)
⊢ Multiset.map (α := Associates α) Associates.out
      (Multiset.map Associates.mk (normalizedFactors x + normalizedFactors y)) =
    Multiset.map (α := Associates α) Associates.out (Multiset.map Associates.mk (normalizedFactors (x * y)))

Tactic:
congr rfl ?_

Premises used: congr, rfl
-- 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 :
  Eq.{u_1 + 1} (α := (a : α) → α) (⇑normalize : (a : α) → α)
    (Function.comp (β := Associates α) Associates.out Associates.mk)
refine :
  Eq (α := Multiset (Associates α)) (Multiset.map Associates.mk (normalizedFactors x + normalizedFactors y))
    (Multiset.map Associates.mk (normalizedFactors (x * y)))
⊢ Multiset.map (α := Associates α) Associates.out
      (Multiset.map Associates.mk (normalizedFactors x + normalizedFactors y)) =
    Multiset.map (α := Associates α) Associates.out (Multiset.map Associates.mk (normalizedFactors (x * y)))

Tactic:
refine congr rfl ?_

Premises used: congr, rfl
-- 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 :
  Eq.{u_1 + 1} (α := (a : α) → α) (⇑normalize : (a : α) → α)
    (Function.comp (β := Associates α) Associates.out Associates.mk)
hst :
  Multiset.Rel (⇑(Associated.setoid α) : α → α → Prop) (normalizedFactors x + normalizedFactors y)
    (normalizedFactors (x * y))
⊢ Eq (α := Multiset (Associates α)) (Multiset.map Associates.mk (normalizedFactors x + normalizedFactors y))
    (Multiset.map Associates.mk (normalizedFactors (x * y)))

Tactic:
apply Multiset.map_mk_eq_map_mk_of_rel

Premises used: Multiset.map_mk_eq_map_mk_of_rel
-- 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 :
  Eq.{u_1 + 1} (α := (a : α) → α) (⇑normalize : (a : α) → α)
    (Function.comp (β := Associates α) Associates.out Associates.mk)
hst : ∀ x_1 ∈ normalizedFactors x + normalizedFactors y, Irreducible x_1
hst₁ : ∀ x_1 ∈ normalizedFactors (x * y), Irreducible x_1
hst₂ : (normalizedFactors x + normalizedFactors y).prod ~ᵤ (normalizedFactors (x * y)).prod
⊢ Multiset.Rel (⇑(Associated.setoid α) : α → α → Prop) (normalizedFactors x + normalizedFactors y)
    (normalizedFactors (x * y))

Tactic:
apply factors_unique

Premises used: UniqueFactorizationMonoid.factors_unique
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
x_1 y : α
hx_1 : x_1 ≠ 0
hy : y ≠ 0
h :
  Eq.{u_1 + 1} (α := (a : α) → α) (⇑normalize : (a : α) → α)
    (Function.comp (β := Associates α) Associates.out Associates.mk)
x : α
hx : x ∈ normalizedFactors x_1 + normalizedFactors y
hst : ∀ (hx : x ∈ normalizedFactors x_1), Irreducible x
hst₁ : ∀ (hx : x ∈ normalizedFactors y), Irreducible x
⊢ Irreducible x

Tactic:
rcases Multiset.mem_add.1 hx with (hx | hx)

Premises used: Multiset.mem_add, Iff.mp
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
x_1 y : α
hx_1 : x_1 ≠ 0
hy : y ≠ 0
h :
  Eq.{u_1 + 1} (α := (a : α) → α) (⇑normalize : (a : α) → α)
    (Function.comp (β := Associates α) Associates.out Associates.mk)
x : α
hx_2 : x ∈ normalizedFactors x_1 + normalizedFactors y
hx : x ∈ normalizedFactors x_1
⊢ Irreducible x

Tactic:
irreducible_of_normalized_factor x hx

Premises used: UniqueFactorizationMonoid.irreducible_of_normalized_factor
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
x_1 y : α
hx_1 : x_1 ≠ 0
hy : y ≠ 0
h :
  Eq.{u_1 + 1} (α := (a : α) → α) (⇑normalize : (a : α) → α)
    (Function.comp (β := Associates α) Associates.out Associates.mk)
x : α
hx_2 : x ∈ normalizedFactors x_1 + normalizedFactors y
hx : x ∈ normalizedFactors x_1
⊢ Irreducible x

Tactic:
exact irreducible_of_normalized_factor x hx

Premises used: UniqueFactorizationMonoid.irreducible_of_normalized_factor
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
x_1 y : α
hx_1 : x_1 ≠ 0
hy : y ≠ 0
h :
  Eq.{u_1 + 1} (α := (a : α) → α) (⇑normalize : (a : α) → α)
    (Function.comp (β := Associates α) Associates.out Associates.mk)
x : α
hx_2 : x ∈ normalizedFactors x_1 + normalizedFactors y
hx : x ∈ normalizedFactors y
⊢ Irreducible x

Tactic:
irreducible_of_normalized_factor x hx

Premises used: UniqueFactorizationMonoid.irreducible_of_normalized_factor
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
x_1 y : α
hx_1 : x_1 ≠ 0
hy : y ≠ 0
h :
  Eq.{u_1 + 1} (α := (a : α) → α) (⇑normalize : (a : α) → α)
    (Function.comp (β := Associates α) Associates.out Associates.mk)
x : α
hx_2 : x ∈ normalizedFactors x_1 + normalizedFactors y
hx : x ∈ normalizedFactors y
⊢ Irreducible x

Tactic:
exact irreducible_of_normalized_factor x hx

Premises used: UniqueFactorizationMonoid.irreducible_of_normalized_factor
-- 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 :
  Eq.{u_1 + 1} (α := (a : α) → α) (⇑normalize : (a : α) → α)
    (Function.comp (β := Associates α) Associates.out Associates.mk)
⊢ ∀ x_1 ∈ normalizedFactors (x * y), Irreducible x_1

Tactic:
irreducible_of_normalized_factor

Premises used: UniqueFactorizationMonoid.irreducible_of_normalized_factor
-- 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 :
  Eq.{u_1 + 1} (α := (a : α) → α) (⇑normalize : (a : α) → α)
    (Function.comp (β := Associates α) Associates.out Associates.mk)
⊢ ∀ x_1 ∈ normalizedFactors (x * y), Irreducible x_1

Tactic:
exact irreducible_of_normalized_factor

Premises used: UniqueFactorizationMonoid.irreducible_of_normalized_factor
-- 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 :
  Eq.{u_1 + 1} (α := (a : α) → α) (⇑normalize : (a : α) → α)
    (Function.comp (β := Associates α) Associates.out Associates.mk)
hst : (normalizedFactors x).prod * (normalizedFactors y).prod ~ᵤ (normalizedFactors (x * y)).prod
⊢ (normalizedFactors x + normalizedFactors y).prod ~ᵤ (normalizedFactors (x * y)).prod

Tactic:
rw [Multiset.prod_add]

Premises used: Multiset.prod_add
-- 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 :
  Eq.{u_1 + 1} (α := (a : α) → α) (⇑normalize : (a : α) → α)
    (Function.comp (β := Associates α) Associates.out Associates.mk)
⊢ (normalizedFactors x).prod * (normalizedFactors y).prod ~ᵤ (normalizedFactors (x * y)).prod

Tactic:
((prod_normalizedFactors hx).mul_mul (prod_normalizedFactors hy)).trans
        (prod_normalizedFactors (mul_ne_zero hx hy)).symm

Premises used: Associated.trans, Associated.symm, UniqueFactorizationMonoid.prod_normalizedFactors, mul_ne_zero, Associated.mul_mul
-- 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 :
  Eq.{u_1 + 1} (α := (a : α) → α) (⇑normalize : (a : α) → α)
    (Function.comp (β := Associates α) Associates.out Associates.mk)
⊢ (normalizedFactors x).prod * (normalizedFactors y).prod ~ᵤ (normalizedFactors (x * y)).prod

Tactic:
exact
      ((prod_normalizedFactors hx).mul_mul (prod_normalizedFactors hy)).trans
        (prod_normalizedFactors (mul_ne_zero hx hy)).symm

Premises used: Associated.trans, Associated.symm, UniqueFactorizationMonoid.prod_normalizedFactors, mul_ne_zero, Associated.mul_mul
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
x : α
⊢ normalizedFactors (HPow.hPow (β := ℕ) x 0) = HSMul.hSMul (α := ℕ) 0 (normalizedFactors x)

Tactic:
simp [zero_nsmul]

Premises used: zero_nsmul
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
x : α
n : ℕ
ih : normalizedFactors (x ^ n) = n • normalizedFactors x
pos : ∀ (h0 : x = 0), normalizedFactors (x ^ (n + 1)) = (n + 1) • normalizedFactors x
neg : ∀ (h0 : ¬x = 0), normalizedFactors (x ^ (n + 1)) = (n + 1) • normalizedFactors x
⊢ normalizedFactors (x ^ (n + 1)) = (n + 1) • normalizedFactors x

Tactic:
by_cases h0 : x = 0
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
x : α
n : ℕ
ih : normalizedFactors (x ^ n) = n • normalizedFactors x
h0 : x = 0
⊢ normalizedFactors (x ^ (n + 1)) = (n + 1) • normalizedFactors x

Tactic:
simp [h0, zero_pow n.succ_ne_zero, nsmul_zero]

Premises used: nsmul_zero, Nat.succ_ne_zero, zero_pow
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
x : α
n : ℕ
ih : normalizedFactors (x ^ n) = n • normalizedFactors x
h0 : ¬x = 0
neg : normalizedFactors (x * x ^ n) = (n + 1) • normalizedFactors x
neg₁ : normalizedFactors (x * x ^ n) = normalizedFactors x + n • normalizedFactors x
neg₂ : normalizedFactors x + normalizedFactors (x ^ n) = normalizedFactors x + n • normalizedFactors x
neg₃ neg₄ : normalizedFactors x + n • normalizedFactors x = normalizedFactors x + n • normalizedFactors x
⊢ normalizedFactors (x ^ (n + 1)) = (n + 1) • normalizedFactors x

Tactic:
rw [pow_succ', succ_nsmul', normalizedFactors_mul h0 (pow_ne_zero _ h0), ih]

Premises used: UniqueFactorizationMonoid.normalizedFactors_mul, pow_ne_zero, succ_nsmul', pow_succ'
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
x : α
n : ℕ
zero : normalizedFactors (HPow.hPow (β := ℕ) x 0) = HSMul.hSMul (α := ℕ) 0 (normalizedFactors x)
succ :
  ∀ (n : ℕ) (ih : normalizedFactors (x ^ n) = n • normalizedFactors x),
    normalizedFactors (x ^ (n + 1)) = (n + 1) • normalizedFactors x
⊢ normalizedFactors (x ^ n) = n • normalizedFactors x

Tactic:
induction n with
  | zero => simp [zero_nsmul]
  | succ n ih =>
    by_cases h0 : x = 0
    · simp [h0, zero_pow n.succ_ne_zero, nsmul_zero]
    rw [pow_succ', succ_nsmul', normalizedFactors_mul h0 (pow_ne_zero _ h0), ih]

Premises used: nsmul_zero, zero_nsmul, Nat.succ_ne_zero, succ_nsmul', pow_succ', zero_pow
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
p : α
hp : Irreducible p
k : ℕ
rw : k • normalizedFactors p = Multiset.replicate k ((normalize : (a : α) → α) p)
rw₁ :
  HSMul.hSMul (β := Multiset α) k (singleton (α := α) ((normalize : (a : α) → α) p : α)) =
    Multiset.replicate k ((normalize : (a : α) → α) p)
rw₂ rw₃ :
  Eq (α := Multiset α) (Multiset.replicate k ((normalize : (a : α) → α) p) : Multiset α)
    (Multiset.replicate k ((normalize : (a : α) → α) p) : Multiset α)
⊢ normalizedFactors (p ^ k) = Multiset.replicate k ((normalize : (a : α) → α) p)

Tactic:
rw [UniqueFactorizationMonoid.normalizedFactors_pow, normalizedFactors_irreducible hp,
    Multiset.nsmul_singleton]

Premises used: UniqueFactorizationMonoid.normalizedFactors_irreducible, UniqueFactorizationMonoid.normalizedFactors_pow, Multiset.nsmul_singleton
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
hs : ∀ (a : α), Membership.mem (γ := Multiset α) 0 a → Irreducible a
empty : Eq.{u_1 + 1} (α := Multiset α) (normalizedFactors 1) (Multiset.map (α := α) (⇑normalize : (a : α) → α) 0)
empty₁ : Eq.{u_1 + 1} (α := Multiset α) 0 (Multiset.map (α := α) (⇑normalize : (a : α) → α) 0)
empty₂ empty₃ : Eq.{u_1 + 1} (α := Multiset α) 0 0
⊢ Eq.{u_1 + 1} (α := Multiset α) (normalizedFactors (Multiset.prod 0))
    (Multiset.map (α := α) (⇑normalize : (a : α) → α) 0)

Tactic:
rw [Multiset.prod_zero, normalizedFactors_one, Multiset.map_zero]

Premises used: Multiset.prod_zero, Multiset.map_zero, UniqueFactorizationMonoid.normalizedFactors_one
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
a : α
s : Multiset α
ih : ∀ (hs : ∀ a ∈ s, Irreducible a), normalizedFactors s.prod = Multiset.map (⇑normalize : (a : α) → α) s
hs : ∀ a_1 ∈ a ::ₘ s, Irreducible a_1
⊢ Irreducible a

Tactic:
have ia := hs a (Multiset.mem_cons_self a _)
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
a : α
s : Multiset α
ih : ∀ (hs : ∀ a ∈ s, Irreducible a), normalizedFactors s.prod = Multiset.map (⇑normalize : (a : α) → α) s
hs : ∀ a_1 ∈ a ::ₘ s, Irreducible a_1
ia : Irreducible a
⊢ ∀ (b : α) (h : b ∈ s), Irreducible b

Tactic:
have ib := fun b h => hs b (Multiset.mem_cons_of_mem h)
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
a : α
s : Multiset α
ih : ∀ (hs : ∀ a ∈ s, Irreducible a), normalizedFactors s.prod = Multiset.map (⇑normalize : (a : α) → α) s
hs : ∀ a_1 ∈ a ::ₘ s, Irreducible a_1
ia : Irreducible a
ib : ∀ (b : α) (h : b ∈ s), Irreducible b
cons :
  ∀
    (ih :
      ∀ (hs : ∀ (a : α), Membership.mem (γ := Multiset α) 0 a → Irreducible a),
        Eq.{u_1 + 1} (α := Multiset α) (normalizedFactors (Multiset.prod 0))
          (Multiset.map (α := α) (⇑normalize : (a : α) → α) 0))
    (hs : ∀ a_1 ∈ a ::ₘ 0, Irreducible a_1) (ib : ∀ (b : α) (h : Membership.mem (γ := Multiset α) 0 b), Irreducible b),
    normalizedFactors (a ::ₘ 0).prod = Multiset.map (⇑normalize : (a : α) → α) (a ::ₘ 0)
cons₁ : ∀ (b : α) (hb : b ∈ s), normalizedFactors (a ::ₘ s).prod = Multiset.map (⇑normalize : (a : α) → α) (a ::ₘ s)
⊢ normalizedFactors (a ::ₘ s).prod = Multiset.map (⇑normalize : (a : α) → α) (a ::ₘ s)

Tactic:
obtain rfl | ⟨b, hb⟩ := s.empty_or_exists_mem

Premises used: Multiset.empty_or_exists_mem, rfl
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
a : α
ia : Irreducible a
ih :
  ∀ (hs : ∀ (a : α), Membership.mem (γ := Multiset α) 0 a → Irreducible a),
    Eq.{u_1 + 1} (α := Multiset α) (normalizedFactors (Multiset.prod 0))
      (Multiset.map (α := α) (⇑normalize : (a : α) → α) 0)
hs : ∀ a_1 ∈ a ::ₘ 0, Irreducible a_1
ib : ∀ (b : α) (h : Membership.mem (γ := Multiset α) 0 b), Irreducible b
cons :
  Eq (α := Multiset α) (normalizedFactors (Multiset.prod {a})) (Multiset.map (α := α) (⇑normalize : (a : α) → α) {a})
cons₁ : normalizedFactors a = Multiset.map (α := α) (⇑normalize : (a : α) → α) {a}
cons₂ : normalizedFactors a = singleton (α := α) ((normalize : (a : α) → α) a : α)
cons₃ cons₄ :
  Eq (α := Multiset α) (singleton (α := α) ((normalize : (a : α) → α) a : α))
    (singleton (α := α) ((normalize : (a : α) → α) a : α))
⊢ normalizedFactors (a ::ₘ 0).prod = Multiset.map (⇑normalize : (a : α) → α) (a ::ₘ 0)

Tactic:
rw [Multiset.cons_zero, Multiset.prod_singleton, Multiset.map_singleton,
        normalizedFactors_irreducible ia]

Premises used: Multiset.map_singleton, Multiset.prod_singleton, UniqueFactorizationMonoid.normalizedFactors_irreducible, Multiset.cons_zero
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
a : α
s : Multiset α
ih : ∀ (hs : ∀ a ∈ s, Irreducible a), normalizedFactors s.prod = Multiset.map (⇑normalize : (a : α) → α) s
hs : ∀ a_1 ∈ a ::ₘ s, Irreducible a_1
ia : Irreducible a
ib : ∀ (b : α) (h : b ∈ s), Irreducible b
b : α
hb : b ∈ s
⊢ Nontrivial α

Tactic:
haveI := nontrivial_of_ne b 0 (ib b hb).ne_zero
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
a : α
s : Multiset α
ih : ∀ (hs : ∀ a ∈ s, Irreducible a), normalizedFactors s.prod = Multiset.map (⇑normalize : (a : α) → α) s
hs : ∀ a_1 ∈ a ::ₘ s, Irreducible a_1
ia : Irreducible a
ib : ∀ (b : α) (h : b ∈ s), Irreducible b
b : α
hb : b ∈ s
this : Nontrivial α
cons : normalizedFactors (a * s.prod) = Multiset.map (⇑normalize : (a : α) → α) (a ::ₘ s)
cons₁ : normalizedFactors (a * s.prod) = (normalize : (a : α) → α) a ::ₘ Multiset.map (⇑normalize : (a : α) → α) s
cons₂ :
  normalizedFactors a + normalizedFactors s.prod =
    (normalize : (a : α) → α) a ::ₘ Multiset.map (⇑normalize : (a : α) → α) s
cons₃ :
  singleton (α := α) ((normalize : (a : α) → α) a : α) + normalizedFactors s.prod =
    (normalize : (a : α) → α) a ::ₘ Multiset.map (⇑normalize : (a : α) → α) s
cons₄ :
  HAdd.hAdd (α := Multiset α) (singleton (α := α) ((normalize : (a : α) → α) a : α))
      (Multiset.map (⇑normalize : (a : α) → α) s) =
    (normalize : (a : α) → α) a ::ₘ Multiset.map (⇑normalize : (a : α) → α) s
cons₅ cons₆ :
  Eq (α := Multiset α) ((normalize : (a : α) → α) a ::ₘ Multiset.map (⇑normalize : (a : α) → α) s : Multiset α)
    ((normalize : (a : α) → α) a ::ₘ Multiset.map (⇑normalize : (a : α) → α) s : Multiset α)
⊢ normalizedFactors (a ::ₘ s).prod = Multiset.map (⇑normalize : (a : α) → α) (a ::ₘ s)

Tactic:
rw [Multiset.prod_cons, Multiset.map_cons,
      normalizedFactors_mul ia.ne_zero (Multiset.prod_ne_zero fun h => (ib 0 h).ne_zero rfl),
      normalizedFactors_irreducible ia, ih ib, Multiset.singleton_add]

Premises used: Multiset.singleton_add, Multiset.map_cons, Multiset.prod_cons, Multiset.prod_ne_zero, UniqueFactorizationMonoid.normalizedFactors_mul, UniqueFactorizationMonoid.normalizedFactors_irreducible, Irreducible.ne_zero, OfNat.ofNat, rfl