awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
β : Type u_3
inst_2 : CommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, IsRelPrime x y → f (x * y) = f x * f y
this_1 : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : ¬f 1 = 0
this_2 : Nontrivial α
this_3 : NormalizationMonoid α := UniqueFactorizationMonoid.normalizationMonoid
this :
  f
      (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
        p ^ (Multiset.count p (normalizedFactors a) + Multiset.count p (normalizedFactors b))) =
    f
        (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
          p ^ Multiset.count p (normalizedFactors a)) *
      f
        (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
          p ^ Multiset.count p (normalizedFactors b))
ua : αˣ
a_eq : (normalizedFactors a).prod * (↑ua : α) = a
ub : αˣ
b_eq : (normalizedFactors b).prod * (↑ub : α) = b
rw :
  f ((normalizedFactors a).prod * (normalizedFactors b).prod) * f (↑ub : α) * f (↑ua : α) =
    f (normalizedFactors a).prod * f (normalizedFactors b).prod * f (↑ub : α) * f (↑ua : α)
⊢ f (a * b) = f a * f b

Tactic:
rw [← a_eq, ← b_eq, mul_right_comm (Multiset.prod (normalizedFactors a)) ua
        (Multiset.prod (normalizedFactors b) * ub), h1 ua.isUnit, h1 ub.isUnit, h1 ua.isUnit, ←
      mul_assoc, h1 ub.isUnit, mul_right_comm _ (f ua), ← mul_assoc]

Premises used: UniqueFactorizationMonoid.normalizedFactors, Units.val, HMul.hMul, Multiset.prod, mul_assoc, mul_right_comm, Units.isUnit
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
β : Type u_3
inst_2 : CommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, IsRelPrime x y → f (x * y) = f x * f y
this_1 : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : ¬f 1 = 0
this_2 : Nontrivial α
this_3 : NormalizationMonoid α := UniqueFactorizationMonoid.normalizationMonoid
this :
  f
      (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
        p ^ (Multiset.count p (normalizedFactors a) + Multiset.count p (normalizedFactors b))) =
    f
        (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
          p ^ Multiset.count p (normalizedFactors a)) *
      f
        (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
          p ^ Multiset.count p (normalizedFactors b))
ua : αˣ
a_eq : (normalizedFactors a).prod * (↑ua : α) = a
ub : αˣ
b_eq : (normalizedFactors b).prod * (↑ub : α) = b
e_a :
  f ((normalizedFactors a).prod * (normalizedFactors b).prod) =
    f (normalizedFactors a).prod * f (normalizedFactors b).prod
⊢ f ((normalizedFactors a).prod * (normalizedFactors b).prod) * f (↑ub : α) * f (↑ua : α) =
    f (normalizedFactors a).prod * f (normalizedFactors b).prod * f (↑ub : α) * f (↑ua : α)

Tactic:
congr
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
β : Type u_3
inst_2 : CommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, IsRelPrime x y → f (x * y) = f x * f y
this_1 : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : ¬f 1 = 0
this_2 : Nontrivial α
this_3 : NormalizationMonoid α := UniqueFactorizationMonoid.normalizationMonoid
this :
  f
      (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
        p ^ (Multiset.count p (normalizedFactors a) + Multiset.count p (normalizedFactors b))) =
    f
        (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
          p ^ Multiset.count p (normalizedFactors a)) *
      f
        (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
          p ^ Multiset.count p (normalizedFactors b))
ua : αˣ
a_eq : (normalizedFactors a).prod * (↑ua : α) = a
ub : αˣ
b_eq : (normalizedFactors b).prod * (↑ub : α) = b
e_a :
  f
      (∏ x ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
        id x ^ Multiset.count x (normalizedFactors a) * id x ^ Multiset.count x (normalizedFactors b)) =
    f
        (∏ x ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
          id x ^ Multiset.count x (normalizedFactors a)) *
      f
        (∏ x ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
          id x ^ Multiset.count x (normalizedFactors b))
e_a₁ :
  ∀ x ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
    x ∉ (normalizedFactors b).toFinset → id x ^ Multiset.count x (normalizedFactors b) = 1
e_a₂ :
  ∀ x ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
    x ∉ (normalizedFactors a).toFinset → id x ^ Multiset.count x (normalizedFactors a) = 1
⊢ f ((normalizedFactors a).prod * (normalizedFactors b).prod) =
    f (normalizedFactors a).prod * f (normalizedFactors b).prod

Tactic:
rw [← (normalizedFactors a).map_id, ← (normalizedFactors b).map_id,
      Finset.prod_multiset_map_count, Finset.prod_multiset_map_count,
      Finset.prod_subset (Finset.subset_union_left (s₂ := (normalizedFactors b).toFinset)),
      Finset.prod_subset (Finset.subset_union_right (s₂ := (normalizedFactors b).toFinset)), ←
      Finset.prod_mul_distrib]

Premises used: UniqueFactorizationMonoid.normalizedFactors, Multiset.map_id, Finset.prod_multiset_map_count, Finset.prod_mul_distrib, Finset.subset_union_left, Finset.prod_subset, Finset.subset_union_right
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
β : Type u_3
inst_2 : CommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, IsRelPrime x y → f (x * y) = f x * f y
this_1 : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : ¬f 1 = 0
this_2 : Nontrivial α
this_3 : NormalizationMonoid α := UniqueFactorizationMonoid.normalizationMonoid
this :
  f
      (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
        p ^ (Multiset.count p (normalizedFactors a) + Multiset.count p (normalizedFactors b))) =
    f
        (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
          p ^ Multiset.count p (normalizedFactors a)) *
      f
        (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
          p ^ Multiset.count p (normalizedFactors b))
ua : αˣ
a_eq : (normalizedFactors a).prod * (↑ua : α) = a
ub : αˣ
b_eq : (normalizedFactors b).prod * (↑ub : α) = b
e_a :
  f
      (∏ x ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
        x ^ Multiset.count x (normalizedFactors a) * x ^ Multiset.count x (normalizedFactors b)) =
    f
        (∏ x ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
          x ^ Multiset.count x (normalizedFactors a)) *
      f
        (∏ x ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
          x ^ Multiset.count x (normalizedFactors b))
e_a₁ :
  f
      (∏ x ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
        x ^ (Multiset.count x (normalizedFactors a) + Multiset.count x (normalizedFactors b))) =
    f
        (∏ x ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
          x ^ Multiset.count x (normalizedFactors a)) *
      f
        (∏ x ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
          x ^ Multiset.count x (normalizedFactors b))
⊢ f
      (∏ x ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
        id x ^ Multiset.count x (normalizedFactors a) * id x ^ Multiset.count x (normalizedFactors b)) =
    f
        (∏ x ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
          id x ^ Multiset.count x (normalizedFactors a)) *
      f
        (∏ x ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
          id x ^ Multiset.count x (normalizedFactors b))

Tactic:
simp_rw [id, ← pow_add, this]

Premises used: pow_add, id
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
β : Type u_3
inst_2 : CommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, IsRelPrime x y → f (x * y) = f x * f y
this_1 : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : ¬f 1 = 0
this_2 : Nontrivial α
this_3 : NormalizationMonoid α := UniqueFactorizationMonoid.normalizationMonoid
this :
  f
      (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
        p ^ (Multiset.count p (normalizedFactors a) + Multiset.count p (normalizedFactors b))) =
    f
        (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
          p ^ Multiset.count p (normalizedFactors a)) *
      f
        (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
          p ^ Multiset.count p (normalizedFactors b))
ua : αˣ
a_eq : (normalizedFactors a).prod * (↑ua : α) = a
ub : αˣ
b_eq : (normalizedFactors b).prod * (↑ub : α) = b
e_a :
  ∀ x ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
    x ∉ normalizedFactors b → id x ^ Multiset.count x (normalizedFactors b) = 1
⊢ ∀ x ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
    x ∉ (normalizedFactors b).toFinset → id x ^ Multiset.count x (normalizedFactors b) = 1

Tactic:
simp only [Multiset.mem_toFinset]

Premises used: Multiset.mem_toFinset
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
β : Type u_3
inst_2 : CommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, IsRelPrime x y → f (x * y) = f x * f y
this_1 : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : ¬f 1 = 0
this_2 : Nontrivial α
this_3 : NormalizationMonoid α := UniqueFactorizationMonoid.normalizationMonoid
this :
  f
      (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
        p ^ (Multiset.count p (normalizedFactors a) + Multiset.count p (normalizedFactors b))) =
    f
        (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
          p ^ Multiset.count p (normalizedFactors a)) *
      f
        (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
          p ^ Multiset.count p (normalizedFactors b))
ua : αˣ
a_eq : (normalizedFactors a).prod * (↑ua : α) = a
ub : αˣ
b_eq : (normalizedFactors b).prod * (↑ub : α) = b
e_a :
  ∀ x ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
    x ∉ normalizedFactors a → id x ^ Multiset.count x (normalizedFactors a) = 1
⊢ ∀ x ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
    x ∉ (normalizedFactors a).toFinset → id x ^ Multiset.count x (normalizedFactors a) = 1

Tactic:
simp only [Multiset.mem_toFinset]

Premises used: Multiset.mem_toFinset
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
β : Type u_3
inst_2 : CommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, IsRelPrime x y → f (x * y) = f x * f y
this_1 : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : ¬f 1 = 0
this_2 : Nontrivial α
this_3 : NormalizationMonoid α := UniqueFactorizationMonoid.normalizationMonoid
this :
  f
      (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
        p ^ (Multiset.count p (normalizedFactors a) + Multiset.count p (normalizedFactors b))) =
    f
        (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
          p ^ Multiset.count p (normalizedFactors a)) *
      f
        (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
          p ^ Multiset.count p (normalizedFactors b))
ua : αˣ
a_eq : (normalizedFactors a).prod * (↑ua : α) = a
ub : αˣ
b_eq : (normalizedFactors b).prod * (↑ub : α) = b
p : α
e_a :
  p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset →
    p ∉ normalizedFactors b → id p ^ Multiset.count p (normalizedFactors b) = 1
⊢ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset →
    p ∉ normalizedFactors b → id p ^ Multiset.count p (normalizedFactors b) = 1

Tactic:
_
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
β : Type u_3
inst_2 : CommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, IsRelPrime x y → f (x * y) = f x * f y
this_1 : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : ¬f 1 = 0
this_2 : Nontrivial α
this_3 : NormalizationMonoid α := UniqueFactorizationMonoid.normalizationMonoid
this :
  f
      (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
        p ^ (Multiset.count p (normalizedFactors a) + Multiset.count p (normalizedFactors b))) =
    f
        (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
          p ^ Multiset.count p (normalizedFactors a)) *
      f
        (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
          p ^ Multiset.count p (normalizedFactors b))
ua : αˣ
a_eq : (normalizedFactors a).prod * (↑ua : α) = a
ub : αˣ
b_eq : (normalizedFactors b).prod * (↑ub : α) = b
p : α
h : p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset
hpb : p ∉ normalizedFactors b
⊢ id p ^ Multiset.count p (normalizedFactors b) = 1

Tactic:
simp [hpb]
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
β : Type u_3
inst_2 : CommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, IsRelPrime x y → f (x * y) = f x * f y
this_1 : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : ¬f 1 = 0
this_2 : Nontrivial α
this_3 : NormalizationMonoid α := UniqueFactorizationMonoid.normalizationMonoid
this :
  f
      (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
        p ^ (Multiset.count p (normalizedFactors a) + Multiset.count p (normalizedFactors b))) =
    f
        (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
          p ^ Multiset.count p (normalizedFactors a)) *
      f
        (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
          p ^ Multiset.count p (normalizedFactors b))
ua : αˣ
a_eq : (normalizedFactors a).prod * (↑ua : α) = a
ub : αˣ
b_eq : (normalizedFactors b).prod * (↑ub : α) = b
p : α
e_a :
  p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset →
    p ∉ normalizedFactors a → id p ^ Multiset.count p (normalizedFactors a) = 1
⊢ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset →
    p ∉ normalizedFactors a → id p ^ Multiset.count p (normalizedFactors a) = 1

Tactic:
_
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
β : Type u_3
inst_2 : CommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, IsRelPrime x y → f (x * y) = f x * f y
this_1 : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : ¬f 1 = 0
this_2 : Nontrivial α
this_3 : NormalizationMonoid α := UniqueFactorizationMonoid.normalizationMonoid
this :
  f
      (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
        p ^ (Multiset.count p (normalizedFactors a) + Multiset.count p (normalizedFactors b))) =
    f
        (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
          p ^ Multiset.count p (normalizedFactors a)) *
      f
        (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
          p ^ Multiset.count p (normalizedFactors b))
ua : αˣ
a_eq : (normalizedFactors a).prod * (↑ua : α) = a
ub : αˣ
b_eq : (normalizedFactors b).prod * (↑ub : α) = b
p : α
h : p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset
hpa : p ∉ normalizedFactors a
⊢ id p ^ Multiset.count p (normalizedFactors a) = 1

Tactic:
simp [hpa]
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
β : Type u_3
inst_2 : CommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, IsRelPrime x y → f (x * y) = f x * f y
this_1 : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : ¬f 1 = 0
this_2 : Nontrivial α
this : NormalizationMonoid α := UniqueFactorizationMonoid.normalizationMonoid
neg :
  f
      (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
        p ^ (Multiset.count p (normalizedFactors a) + Multiset.count p (normalizedFactors b))) =
    f
        (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
          p ^ Multiset.count p (normalizedFactors a)) *
      f
        (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
          p ^ Multiset.count p (normalizedFactors b))
⊢ f (a * b) = f a * f b

Tactic:
suffices
      f (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
        p ^ ((normalizedFactors a).count p + (normalizedFactors b).count p)) =
      f (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
        p ^ (normalizedFactors a).count p) *
      f (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
        p ^ (normalizedFactors b).count p) by
    obtain ⟨ua, a_eq⟩ := prod_normalizedFactors ha0
    obtain ⟨ub, b_eq⟩ := prod_normalizedFactors hb0
    rw [← a_eq, ← b_eq, mul_right_comm (Multiset.prod (normalizedFactors a)) ua
        (Multiset.prod (normalizedFactors b) * ub), h1 ua.isUnit, h1 ub.isUnit, h1 ua.isUnit, ←
      mul_assoc, h1 ub.isUnit, mul_right_comm _ (f ua), ← mul_assoc]
    congr
    rw [← (normalizedFactors a).map_id, ← (normalizedFactors b).map_id,
      Finset.prod_multiset_map_count, Finset.prod_multiset_map_count,
      Finset.prod_subset (Finset.subset_union_left (s₂ := (normalizedFactors b).toFinset)),
      Finset.prod_subset (Finset.subset_union_right (s₂ := (normalizedFactors b).toFinset)), ←
      Finset.prod_mul_distrib]
    · simp_rw [id, ← pow_add, this]
    all_goals simp only [Multiset.mem_toFinset]
    · intro p _ hpb
      simp [hpb]
    · intro p _ hpa
      simp [hpa]
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
β : Type u_3
inst_2 : CommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, IsRelPrime x y → f (x * y) = f x * f y
this_1 : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : ¬f 1 = 0
this_2 : Nontrivial α
this : NormalizationMonoid α := UniqueFactorizationMonoid.normalizationMonoid
⊢ f
      (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
        p ^ (Multiset.count p (normalizedFactors a) + Multiset.count p (normalizedFactors b))) =
    f
        (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
          p ^ Multiset.count p (normalizedFactors a)) *
      f
        (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
          p ^ Multiset.count p (normalizedFactors b))

Tactic:
multiplicative_prime_power _ _ _ ?_ ?_ @h1 @hpr @hcp

Premises used: UniqueFactorizationMonoid.multiplicative_prime_power
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
β : Type u_3
inst_2 : CommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, IsRelPrime x y → f (x * y) = f x * f y
this_1 : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : ¬f 1 = 0
this_2 : Nontrivial α
this : NormalizationMonoid α := UniqueFactorizationMonoid.normalizationMonoid
neg : ∀ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset, Prime p
neg₁ :
  ∀ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
    ∀ q ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset, p ∣ q → p = q
⊢ f
      (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
        p ^ (Multiset.count p (normalizedFactors a) + Multiset.count p (normalizedFactors b))) =
    f
        (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
          p ^ Multiset.count p (normalizedFactors a)) *
      f
        (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
          p ^ Multiset.count p (normalizedFactors b))

Tactic:
refine multiplicative_prime_power _ _ _ ?_ ?_ @h1 @hpr @hcp

Premises used: UniqueFactorizationMonoid.multiplicative_prime_power
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
β : Type u_3
inst_2 : CommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, IsRelPrime x y → f (x * y) = f x * f y
this_1 : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : ¬f 1 = 0
this_2 : Nontrivial α
this : NormalizationMonoid α := UniqueFactorizationMonoid.normalizationMonoid
neg : ∀ (p : α), p ∈ normalizedFactors a ∨ p ∈ normalizedFactors b → Prime p
⊢ ∀ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset, Prime p

Tactic:
simp only [Multiset.mem_toFinset, Finset.mem_union]

Premises used: Finset.mem_union, Multiset.mem_toFinset
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
β : Type u_3
inst_2 : CommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, IsRelPrime x y → f (x * y) = f x * f y
this_1 : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : ¬f 1 = 0
this_2 : Nontrivial α
this : NormalizationMonoid α := UniqueFactorizationMonoid.normalizationMonoid
neg :
  ∀ (p : α),
    p ∈ normalizedFactors a ∨ p ∈ normalizedFactors b →
      ∀ (q : α), q ∈ normalizedFactors a ∨ q ∈ normalizedFactors b → p ∣ q → p = q
⊢ ∀ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
    ∀ q ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset, p ∣ q → p = q

Tactic:
simp only [Multiset.mem_toFinset, Finset.mem_union]

Premises used: Finset.mem_union, Multiset.mem_toFinset