awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
p : α
hp : Irreducible p
k : ℕ
⊢ normalizedFactors (p ^ k) = Multiset.replicate k ((normalize : (a : α) → α) p)
have rw : k • normalizedFactors p = Multiset.replicate k ((normalize : (a : α) → α) p)
Tactic: rw [UniqueFactorizationMonoid.normalizedFactors_pow, normalizedFactors_irreducible hp,
    Multiset.nsmul_singleton]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors (goal)
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)
⊢ normalizedFactors (p ^ k) = Multiset.replicate k ((normalize : (a : α) → α) p)
have rw₁ : HSMul.hSMul (β := Multiset α) k (singleton (α := α) ((normalize : (a : α) → α) p : α)) =
  Multiset.replicate k ((normalize : (a : α) → α) p)
Tactic: rw [UniqueFactorizationMonoid.normalizedFactors_pow, normalizedFactors_irreducible hp,
    Multiset.nsmul_singleton]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors (goal)
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)
⊢ normalizedFactors (p ^ k) = Multiset.replicate k ((normalize : (a : α) → α) p)
have rw₂ : Eq (α := Multiset α) (Multiset.replicate k ((normalize : (a : α) → α) p) : Multiset α)
  (Multiset.replicate k ((normalize : (a : α) → α) p) : Multiset α)
Tactic: rw [UniqueFactorizationMonoid.normalizedFactors_pow, normalizedFactors_irreducible hp,
    Multiset.nsmul_singleton]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
hs : ∀ (a : α), Membership.mem (γ := Multiset α) 0 a → Irreducible a
⊢ Eq.{u_1 + 1} (α := Multiset α) (normalizedFactors (Multiset.prod 0))
    (Multiset.map (α := α) (⇑normalize : (a : α) → α) 0)
have empty : Eq.{u_1 + 1} (α := Multiset α) (normalizedFactors 1) (Multiset.map (α := α) (⇑normalize : (a : α) → α) 0)
Tactic: rw [Multiset.prod_zero, normalizedFactors_one, Multiset.map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors (goal)
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)
⊢ Eq.{u_1 + 1} (α := Multiset α) (normalizedFactors (Multiset.prod 0))
    (Multiset.map (α := α) (⇑normalize : (a : α) → α) 0)
have empty₁ : Eq.{u_1 + 1} (α := Multiset α) 0 (Multiset.map (α := α) (⇑normalize : (a : α) → α) 0)
Tactic: rw [Multiset.prod_zero, normalizedFactors_one, Multiset.map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors (goal)
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)
⊢ Eq.{u_1 + 1} (α := Multiset α) (normalizedFactors (Multiset.prod 0))
    (Multiset.map (α := α) (⇑normalize : (a : α) → α) 0)
have empty₂ : Eq.{u_1 + 1} (α := Multiset α) 0 0
Tactic: rw [Multiset.prod_zero, normalizedFactors_one, Multiset.map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors (hypothesis)
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
⊢ normalizedFactors (a ::ₘ s).prod = Multiset.map (⇑normalize : (a : α) → α) (a ::ₘ s)
have ia : Irreducible a
Tactic: have ia := hs a (Multiset.mem_cons_self a _)
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors (hypothesis)
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
⊢ normalizedFactors (a ::ₘ s).prod = Multiset.map (⇑normalize : (a : α) → α) (a ::ₘ s)
have ib : ∀ (b : α) (h : b ∈ s), Irreducible b
Tactic: have ib := fun b h => hs b (Multiset.mem_cons_of_mem h)
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors (goal)
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
⊢ normalizedFactors (a ::ₘ s).prod = Multiset.map (⇑normalize : (a : α) → α) (a ::ₘ s)
have 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)
Tactic: obtain rfl | ⟨b, hb⟩ := s.empty_or_exists_mem
Cleared hypotheses: s, ih, hs, ib
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors (goal)
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)
⊢ normalizedFactors (a ::ₘ s).prod = Multiset.map (⇑normalize : (a : α) → α) (a ::ₘ s)
have cons₁ : ∀ (b : α) (hb : b ∈ s), normalizedFactors (a ::ₘ s).prod = Multiset.map (⇑normalize : (a : α) → α) (a ::ₘ s)
Tactic: obtain rfl | ⟨b, hb⟩ := s.empty_or_exists_mem
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors (goal)
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
⊢ normalizedFactors (a ::ₘ 0).prod = Multiset.map (⇑normalize : (a : α) → α) (a ::ₘ 0)
have cons : Eq (α := Multiset α) (normalizedFactors (Multiset.prod {a})) (Multiset.map (α := α) (⇑normalize : (a : α) → α) {a})
Tactic: rw [Multiset.cons_zero, Multiset.prod_singleton, Multiset.map_singleton,
        normalizedFactors_irreducible ia]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors (goal)
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})
⊢ normalizedFactors (a ::ₘ 0).prod = Multiset.map (⇑normalize : (a : α) → α) (a ::ₘ 0)
have cons₁ : normalizedFactors a = Multiset.map (α := α) (⇑normalize : (a : α) → α) {a}
Tactic: rw [Multiset.cons_zero, Multiset.prod_singleton, Multiset.map_singleton,
        normalizedFactors_irreducible ia]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors (goal)
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}
⊢ normalizedFactors (a ::ₘ 0).prod = Multiset.map (⇑normalize : (a : α) → α) (a ::ₘ 0)
have cons₂ : normalizedFactors a = singleton (α := α) ((normalize : (a : α) → α) a : α)
Tactic: rw [Multiset.cons_zero, Multiset.prod_singleton, Multiset.map_singleton,
        normalizedFactors_irreducible ia]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors (goal)
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 : α)
⊢ normalizedFactors (a ::ₘ 0).prod = Multiset.map (⇑normalize : (a : α) → α) (a ::ₘ 0)
have cons₃ : Eq (α := Multiset α) (singleton (α := α) ((normalize : (a : α) → α) a : α))
  (singleton (α := α) ((normalize : (a : α) → α) a : α))
Tactic: rw [Multiset.cons_zero, Multiset.prod_singleton, Multiset.map_singleton,
        normalizedFactors_irreducible ia]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors (hypothesis)
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
⊢ normalizedFactors (a ::ₘ s).prod = Multiset.map (⇑normalize : (a : α) → α) (a ::ₘ s)
have this : Nontrivial α
Tactic: haveI := nontrivial_of_ne b 0 (ib b hb).ne_zero
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors (goal)
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 α
⊢ normalizedFactors (a ::ₘ s).prod = Multiset.map (⇑normalize : (a : α) → α) (a ::ₘ s)
have cons : 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]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors (goal)
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)
⊢ normalizedFactors (a ::ₘ s).prod = Multiset.map (⇑normalize : (a : α) → α) (a ::ₘ s)
have cons₁ : normalizedFactors (a * s.prod) = (normalize : (a : α) → α) a ::ₘ Multiset.map (⇑normalize : (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]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors (goal)
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
⊢ normalizedFactors (a ::ₘ s).prod = Multiset.map (⇑normalize : (a : α) → α) (a ::ₘ s)
have cons₂ : normalizedFactors a + normalizedFactors s.prod =
  (normalize : (a : α) → α) a ::ₘ Multiset.map (⇑normalize : (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]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors (goal)
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
⊢ normalizedFactors (a ::ₘ s).prod = Multiset.map (⇑normalize : (a : α) → α) (a ::ₘ s)
have cons₃ : singleton (α := α) ((normalize : (a : α) → α) a : α) + normalizedFactors s.prod =
  (normalize : (a : α) → α) a ::ₘ Multiset.map (⇑normalize : (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]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors (goal)
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
⊢ normalizedFactors (a ::ₘ s).prod = Multiset.map (⇑normalize : (a : α) → α) (a ::ₘ s)
have cons₄ : HAdd.hAdd (α := Multiset α) (singleton (α := α) ((normalize : (a : α) → α) a : α))
    (Multiset.map (⇑normalize : (a : α) → α) s) =
  (normalize : (a : α) → α) a ::ₘ Multiset.map (⇑normalize : (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]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors (goal)
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
⊢ normalizedFactors (a ::ₘ s).prod = Multiset.map (⇑normalize : (a : α) → α) (a ::ₘ s)
have cons₅ : Eq (α := Multiset α) ((normalize : (a : α) → α) a ::ₘ Multiset.map (⇑normalize : (a : α) → α) s : Multiset α)
  ((normalize : (a : α) → α) a ::ₘ Multiset.map (⇑normalize : (a : α) → α) s : Multiset α)
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]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
s : Multiset α
hs : ∀ a ∈ s, Irreducible a
⊢ normalizedFactors s.prod = Multiset.map (⇑normalize : (a : α) → α) s
have empty : ∀ (hs : ∀ (a : α), Membership.mem (γ := Multiset α) 0 a → Irreducible a),
  Eq.{u_1 + 1} (α := Multiset α) (normalizedFactors (Multiset.prod 0))
    (Multiset.map (α := α) (⇑normalize : (a : α) → α) 0)
Tactic: induction s using Multiset.induction with
  | empty => rw [Multiset.prod_zero, normalizedFactors_one, Multiset.map_zero]
  | cons a s ih =>
    have ia := hs a (Multiset.mem_cons_self a _)
    have ib := fun b h => hs b (Multiset.mem_cons_of_mem h)
    obtain rfl | ⟨b, hb⟩ := s.empty_or_exists_mem
    · rw [Multiset.cons_zero, Multiset.prod_singleton, Multiset.map_singleton,
        normalizedFactors_irreducible ia]
    haveI := nontrivial_of_ne b 0 (ib b hb).ne_zero
    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]
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
s : Multiset α
hs : ∀ a ∈ s, Irreducible a
empty :
  ∀ (hs : ∀ (a : α), Membership.mem (γ := Multiset α) 0 a → Irreducible a),
    Eq.{u_1 + 1} (α := Multiset α) (normalizedFactors (Multiset.prod 0))
      (Multiset.map (α := α) (⇑normalize : (a : α) → α) 0)
⊢ normalizedFactors s.prod = Multiset.map (⇑normalize : (a : α) → α) s
have cons : ∀ (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),
  normalizedFactors (a ::ₘ s).prod = Multiset.map (⇑normalize : (a : α) → α) (a ::ₘ s)
Tactic: induction s using Multiset.induction with
  | empty => rw [Multiset.prod_zero, normalizedFactors_one, Multiset.map_zero]
  | cons a s ih =>
    have ia := hs a (Multiset.mem_cons_self a _)
    have ib := fun b h => hs b (Multiset.mem_cons_of_mem h)
    obtain rfl | ⟨b, hb⟩ := s.empty_or_exists_mem
    · rw [Multiset.cons_zero, Multiset.prod_singleton, Multiset.map_singleton,
        normalizedFactors_irreducible ia]
    haveI := nontrivial_of_ne b 0 (ib b hb).ne_zero
    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]
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
⊢ x ∣ y ↔ normalizedFactors x ≤ normalizedFactors y
have mp : x ∣ y → normalizedFactors x ≤ normalizedFactors y
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
mp : x ∣ y → normalizedFactors x ≤ normalizedFactors y
⊢ x ∣ y ↔ normalizedFactors x ≤ normalizedFactors y
have mpr : normalizedFactors x ≤ normalizedFactors y → x ∣ y
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
⊢ normalizedFactors x ≤ normalizedFactors y → x ∣ y
have mpr : normalizedFactors x ≤ normalizedFactors y → (normalizedFactors x).prod ∣ (normalizedFactors y).prod
Tactic: rw [← (prod_normalizedFactors hx).dvd_iff_dvd_left, ←
      (prod_normalizedFactors hy).dvd_iff_dvd_right]