awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
P : α → Prop
a : α
h0 : P 0
h1 : ∀ {x : α}, IsUnit x → P x
hpr : ∀ {p : α} (i : ℕ), Prime p → P (p ^ i)
hcp : ∀ {x y : α}, IsRelPrime x y → P x → P y → P (x * y)
this : DecidableEq α := Classical.decEq α
P_of_associated : ∀ {x y : α}, Associated x y → P x → P y
ha0 : ¬a = 0
⊢ Nontrivial α

Tactic:
haveI : Nontrivial α := ⟨⟨_, _, ha0⟩⟩
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
P : α → Prop
a : α
h0 : P 0
h1 : ∀ {x : α}, IsUnit x → P x
hpr : ∀ {p : α} (i : ℕ), Prime p → P (p ^ i)
hcp : ∀ {x y : α}, IsRelPrime x y → P x → P y → P (x * y)
this_1 : DecidableEq α := Classical.decEq α
P_of_associated : ∀ {x y : α}, Associated x y → P x → P y
ha0 : ¬a = 0
this_2 : Nontrivial α
this : NormalizationMonoid α := UniqueFactorizationMonoid.normalizationMonoid
⊢ P a

Tactic:
P_of_associated (prod_normalizedFactors ha0) ?_

Premises used: UniqueFactorizationMonoid.prod_normalizedFactors
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
P : α → Prop
a : α
h0 : P 0
h1 : ∀ {x : α}, IsUnit x → P x
hpr : ∀ {p : α} (i : ℕ), Prime p → P (p ^ i)
hcp : ∀ {x y : α}, IsRelPrime x y → P x → P y → P (x * y)
this_1 : DecidableEq α := Classical.decEq α
P_of_associated : ∀ {x y : α}, Associated x y → P x → P y
ha0 : ¬a = 0
this_2 : Nontrivial α
this : NormalizationMonoid α := UniqueFactorizationMonoid.normalizationMonoid
neg : P (normalizedFactors a).prod
⊢ P a

Tactic:
refine P_of_associated (prod_normalizedFactors ha0) ?_

Premises used: UniqueFactorizationMonoid.prod_normalizedFactors
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
P : α → Prop
a : α
h0 : P 0
h1 : ∀ {x : α}, IsUnit x → P x
hpr : ∀ {p : α} (i : ℕ), Prime p → P (p ^ i)
hcp : ∀ {x y : α}, IsRelPrime x y → P x → P y → P (x * y)
this_1 : DecidableEq α := Classical.decEq α
P_of_associated : ∀ {x y : α}, Associated x y → P x → P y
ha0 : ¬a = 0
this_2 : Nontrivial α
this : NormalizationMonoid α := UniqueFactorizationMonoid.normalizationMonoid
neg : P (∏ m ∈ (normalizedFactors a).toFinset, id m ^ Multiset.count m (normalizedFactors a))
⊢ P (normalizedFactors a).prod

Tactic:
rw [← (normalizedFactors a).map_id, Finset.prod_multiset_map_count]

Premises used: UniqueFactorizationMonoid.normalizedFactors, Multiset.map_id, Finset.prod_multiset_map_count
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
P : α → Prop
a : α
h0 : P 0
h1 : ∀ {x : α}, IsUnit x → P x
hpr : ∀ {p : α} (i : ℕ), Prime p → P (p ^ i)
hcp : ∀ {x y : α}, IsRelPrime x y → P x → P y → P (x * y)
this_1 : DecidableEq α := Classical.decEq α
P_of_associated : ∀ {x y : α}, Associated x y → P x → P y
ha0 : ¬a = 0
this_2 : Nontrivial α
this : NormalizationMonoid α := UniqueFactorizationMonoid.normalizationMonoid
⊢ P (∏ m ∈ (normalizedFactors a).toFinset, id m ^ Multiset.count m (normalizedFactors a))

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

Premises used: UniqueFactorizationMonoid.normalizedFactors, Multiset.toFinset, UniqueFactorizationMonoid.induction_on_prime_power, Multiset.count
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
P : α → Prop
a : α
h0 : P 0
h1 : ∀ {x : α}, IsUnit x → P x
hpr : ∀ {p : α} (i : ℕ), Prime p → P (p ^ i)
hcp : ∀ {x y : α}, IsRelPrime x y → P x → P y → P (x * y)
this_1 : DecidableEq α := Classical.decEq α
P_of_associated : ∀ {x y : α}, Associated x y → P x → P y
ha0 : ¬a = 0
this_2 : Nontrivial α
this : NormalizationMonoid α := UniqueFactorizationMonoid.normalizationMonoid
neg : ∀ p ∈ (normalizedFactors a).toFinset, Prime p
neg₁ : ∀ p ∈ (normalizedFactors a).toFinset, ∀ q ∈ (normalizedFactors a).toFinset, p ∣ q → p = q
⊢ P (∏ m ∈ (normalizedFactors a).toFinset, id m ^ Multiset.count m (normalizedFactors a))

Tactic:
refine induction_on_prime_power _ _ ?_ ?_ @h1 @hpr @hcp
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
P : α → Prop
a : α
h0 : P 0
h1 : ∀ {x : α}, IsUnit x → P x
hpr : ∀ {p : α} (i : ℕ), Prime p → P (p ^ i)
hcp : ∀ {x y : α}, IsRelPrime x y → P x → P y → P (x * y)
this_1 : DecidableEq α := Classical.decEq α
P_of_associated : ∀ {x y : α}, Associated x y → P x → P y
ha0 : ¬a = 0
this_2 : Nontrivial α
this : NormalizationMonoid α := UniqueFactorizationMonoid.normalizationMonoid
neg : ∀ p ∈ normalizedFactors a, Prime p
⊢ ∀ p ∈ (normalizedFactors a).toFinset, Prime p

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 α
P : α → Prop
a : α
h0 : P 0
h1 : ∀ {x : α}, IsUnit x → P x
hpr : ∀ {p : α} (i : ℕ), Prime p → P (p ^ i)
hcp : ∀ {x y : α}, IsRelPrime x y → P x → P y → P (x * y)
this_1 : DecidableEq α := Classical.decEq α
P_of_associated : ∀ {x y : α}, Associated x y → P x → P y
ha0 : ¬a = 0
this_2 : Nontrivial α
this : NormalizationMonoid α := UniqueFactorizationMonoid.normalizationMonoid
neg : ∀ p ∈ normalizedFactors a, ∀ q ∈ normalizedFactors a, p ∣ q → p = q
⊢ ∀ p ∈ (normalizedFactors a).toFinset, ∀ q ∈ (normalizedFactors a).toFinset, p ∣ q → p = q

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 α
P : α → Prop
a : α
h0 : P 0
h1 : ∀ {x : α}, IsUnit x → P x
hpr : ∀ {p : α} (i : ℕ), Prime p → P (p ^ i)
hcp : ∀ {x y : α}, IsRelPrime x y → P x → P y → P (x * y)
this_1 : DecidableEq α := Classical.decEq α
P_of_associated : ∀ {x y : α}, Associated x y → P x → P y
ha0 : ¬a = 0
this_2 : Nontrivial α
this : NormalizationMonoid α := UniqueFactorizationMonoid.normalizationMonoid
⊢ ∀ p ∈ normalizedFactors a, Prime p

Tactic:
apply prime_of_normalized_factor

Premises used: UniqueFactorizationMonoid.prime_of_normalized_factor
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
P : α → Prop
a : α
h0 : P 0
h1 : ∀ {x : α}, IsUnit x → P x
hpr : ∀ {p : α} (i : ℕ), Prime p → P (p ^ i)
hcp : ∀ {x y : α}, IsRelPrime x y → P x → P y → P (x * y)
this_1 : DecidableEq α := Classical.decEq α
P_of_associated : ∀ {x y : α}, Associated x y → P x → P y
ha0 : ¬a = 0
this_2 : Nontrivial α
this : NormalizationMonoid α := UniqueFactorizationMonoid.normalizationMonoid
⊢ ∀ p ∈ normalizedFactors a, ∀ q ∈ normalizedFactors a, p ∣ q → p = q

Tactic:
apply normalizedFactors_eq_of_dvd

Premises used: UniqueFactorizationMonoid.normalizedFactors_eq_of_dvd
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
β : Type u_3
inst_2 : CommMonoidWithZero β
f : α → β
i j : α → ℕ
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 : DecidableEq α := Classical.decEq α
is_prime : ∀ (p : α), Membership.mem (γ := Finset α) ∅ p → Prime p
is_coprime :
  ∀ (p : α), Membership.mem (γ := Finset α) ∅ p → ∀ (q : α), Membership.mem (γ := Finset α) ∅ q → p ∣ q → p = q
⊢ f (∏ p ∈ ∅, p ^ (i p + j p)) = f (∏ p ∈ ∅, p ^ i p) * f (∏ p ∈ ∅, p ^ j p)

Tactic:
simpa using h1 isUnit_one

Premises used: isUnit_one
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
β : Type u_3
inst_2 : CommMonoidWithZero β
f : α → β
i j : α → ℕ
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 : DecidableEq α := Classical.decEq α
p : α
s : Finset α
hps : p ∉ s
ih :
  ∀ (is_prime : ∀ p ∈ s, Prime p) (is_coprime : ∀ p ∈ s, ∀ q ∈ s, p ∣ q → p = q),
    f (∏ p ∈ s, p ^ (i p + j p)) = f (∏ p ∈ s, p ^ i p) * f (∏ p ∈ s, p ^ j p)
is_prime : ∀ p_1 ∈ insert p s, Prime p_1
is_coprime : ∀ p_1 ∈ insert p s, ∀ q ∈ insert p s, p_1 ∣ q → p_1 = q
⊢ Prime p

Tactic:
have hpr_p := is_prime _ (Finset.mem_insert_self _ _)
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
β : Type u_3
inst_2 : CommMonoidWithZero β
f : α → β
i j : α → ℕ
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 : DecidableEq α := Classical.decEq α
p : α
s : Finset α
hps : p ∉ s
ih :
  ∀ (is_prime : ∀ p ∈ s, Prime p) (is_coprime : ∀ p ∈ s, ∀ q ∈ s, p ∣ q → p = q),
    f (∏ p ∈ s, p ^ (i p + j p)) = f (∏ p ∈ s, p ^ i p) * f (∏ p ∈ s, p ^ j p)
is_prime : ∀ p_1 ∈ insert p s, Prime p_1
is_coprime : ∀ p_1 ∈ insert p s, ∀ q ∈ insert p s, p_1 ∣ q → p_1 = q
hpr_p : Prime p
⊢ ∀ p ∈ s, Prime p

Tactic:
have hpr_s : ∀ p ∈ s, Prime p := fun p hp => is_prime _ (Finset.mem_insert_of_mem hp)
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
β : Type u_3
inst_2 : CommMonoidWithZero β
f : α → β
i j : α → ℕ
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 : DecidableEq α := Classical.decEq α
p : α
s : Finset α
hps : p ∉ s
ih :
  ∀ (is_prime : ∀ p ∈ s, Prime p) (is_coprime : ∀ p ∈ s, ∀ q ∈ s, p ∣ q → p = q),
    f (∏ p ∈ s, p ^ (i p + j p)) = f (∏ p ∈ s, p ^ i p) * f (∏ p ∈ s, p ^ j p)
is_prime : ∀ p_1 ∈ insert p s, Prime p_1
is_coprime : ∀ p_1 ∈ insert p s, ∀ q ∈ insert p s, p_1 ∣ q → p_1 = q
hpr_p : Prime p
hpr_s : ∀ p ∈ s, Prime p
⊢ ∀ (i : α → ℕ), IsRelPrime (p ^ i p) (∏ p' ∈ s, p' ^ i p')

Tactic:
have hcp_p := fun i => prime_pow_coprime_prod_of_coprime_insert i p hps is_prime is_coprime
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
β : Type u_3
inst_2 : CommMonoidWithZero β
f : α → β
i j : α → ℕ
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 : DecidableEq α := Classical.decEq α
p : α
s : Finset α
hps : p ∉ s
ih :
  ∀ (is_prime : ∀ p ∈ s, Prime p) (is_coprime : ∀ p ∈ s, ∀ q ∈ s, p ∣ q → p = q),
    f (∏ p ∈ s, p ^ (i p + j p)) = f (∏ p ∈ s, p ^ i p) * f (∏ p ∈ s, p ^ j p)
is_prime : ∀ p_1 ∈ insert p s, Prime p_1
is_coprime : ∀ p_1 ∈ insert p s, ∀ q ∈ insert p s, p_1 ∣ q → p_1 = q
hpr_p : Prime p
hpr_s : ∀ p ∈ s, Prime p
hcp_p : ∀ (i : α → ℕ), IsRelPrime (p ^ i p) (∏ p' ∈ s, p' ^ i p')
⊢ ∀ p ∈ s, ∀ q ∈ s, p ∣ q → p = q

Tactic:
have hcp_s : ∀ᵉ (p ∈ s) (q ∈ s), p ∣ q → p = q := fun p hp q hq =>
      is_coprime p (Finset.mem_insert_of_mem hp) q (Finset.mem_insert_of_mem hq)
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
β : Type u_3
inst_2 : CommMonoidWithZero β
f : α → β
s : Finset α
i j : α → ℕ
is_prime : ∀ p ∈ s, Prime p
is_coprime : ∀ p ∈ s, ∀ q ∈ s, p ∣ q → p = q
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 : DecidableEq α := Classical.decEq α
empty :
  ∀ (is_prime : ∀ (p : α), Membership.mem (γ := Finset α) ∅ p → Prime p)
    (is_coprime :
      ∀ (p : α), Membership.mem (γ := Finset α) ∅ p → ∀ (q : α), Membership.mem (γ := Finset α) ∅ q → p ∣ q → p = q),
    f (∏ p ∈ ∅, p ^ (i p + j p)) = f (∏ p ∈ ∅, p ^ i p) * f (∏ p ∈ ∅, p ^ j p)
insert :
  ∀ (p : α) (s : Finset α) (hps : p ∉ s)
    (ih :
      ∀ (is_prime : ∀ p ∈ s, Prime p) (is_coprime : ∀ p ∈ s, ∀ q ∈ s, p ∣ q → p = q),
        f (∏ p ∈ s, p ^ (i p + j p)) = f (∏ p ∈ s, p ^ i p) * f (∏ p ∈ s, p ^ j p))
    (is_prime : ∀ p_1 ∈ Insert.insert p s, Prime p_1)
    (is_coprime : ∀ p_1 ∈ Insert.insert p s, ∀ q ∈ Insert.insert p s, p_1 ∣ q → p_1 = q),
    f (∏ p ∈ Insert.insert p s, p ^ (i p + j p)) =
      f (∏ p ∈ Insert.insert p s, p ^ i p) * f (∏ p ∈ Insert.insert p s, p ^ j p)
⊢ f (∏ p ∈ s, p ^ (i p + j p)) = f (∏ p ∈ s, p ^ i p) * f (∏ p ∈ s, p ^ j p)

Tactic:
induction s using Finset.induction_on with
  | empty => simpa using h1 isUnit_one
  | insert p s hps ih =>
    have hpr_p := is_prime _ (Finset.mem_insert_self _ _)
    have hpr_s : ∀ p ∈ s, Prime p := fun p hp => is_prime _ (Finset.mem_insert_of_mem hp)
    have hcp_p := fun i => prime_pow_coprime_prod_of_coprime_insert i p hps is_prime is_coprime
    have hcp_s : ∀ᵉ (p ∈ s) (q ∈ s), p ∣ q → p = q := fun p hp q hq =>
      is_coprime p (Finset.mem_insert_of_mem hp) q (Finset.mem_insert_of_mem hq)
    rw [Finset.prod_insert hps, Finset.prod_insert hps, Finset.prod_insert hps, hcp (hcp_p _),
      hpr _ hpr_p, hcp (hcp_p _), hpr _ hpr_p, hcp (hcp_p (fun p => i p + j p)), hpr _ hpr_p,
      ih hpr_s hcp_s, pow_add, mul_assoc, mul_left_comm (f p ^ j p), mul_assoc]

Premises used: mul_assoc, pow_add, Insert.insert, isUnit_one
-- 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 : DecidableEq α := Classical.decEq α
pos : ∀ (ha0 : a = 0), f (a * b) = f a * f b
neg : ∀ (ha0 : ¬a = 0), f (a * b) = f a * f b
⊢ f (a * b) = f a * f b

Tactic:
by_cases ha0 : a = 0
-- 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 : DecidableEq α := Classical.decEq α
ha0 : a = 0
pos : f (0 * b) = f 0 * f b
pos₁ : f 0 = f 0 * f b
pos₂ : 0 = 0 * f b
pos₃ pos₄ : Eq.{u_3 + 1} (α := β) 0 0
⊢ f (a * b) = f a * f b

Tactic:
rw [ha0, zero_mul, h0, zero_mul]

Premises used: MulZeroClass.zero_mul
-- 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 : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
pos : ∀ (hb0 : b = 0), f (a * b) = f a * f b
neg : ∀ (hb0 : ¬b = 0), f (a * b) = f a * f b
⊢ f (a * b) = f a * f b

Tactic:
by_cases hb0 : b = 0
-- 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 : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : b = 0
pos : f (a * 0) = f a * f 0
pos₁ : f 0 = f a * f 0
pos₂ : 0 = f a * 0
pos₃ pos₄ : Eq.{u_3 + 1} (α := β) 0 0
⊢ f (a * b) = f a * f b

Tactic:
rw [hb0, mul_zero, h0, mul_zero]

Premises used: MulZeroClass.mul_zero
-- 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 : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
pos : ∀ (hf1 : f 1 = 0), f (a * b) = f a * f b
neg : ∀ (hf1 : ¬f 1 = 0), f (a * b) = f a * f b
⊢ f (a * b) = f a * f b

Tactic:
by_cases hf1 : f 1 = 0

Premises used: OfNat.ofNat
-- 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 : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : f 1 = 0
rw rw₁ : f (a * b) = f (a * b)
⊢ f (a * b) = f (a * b * 1)

Tactic:
rw [mul_one]

Premises used: mul_one
-- 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 : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : f 1 = 0
⊢ f (a * b * 1) = 0

Tactic:
simp only [h1 isUnit_one, hf1, mul_zero]

Premises used: MulZeroClass.mul_zero, isUnit_one
-- 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 : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : f 1 = 0
⊢ 0 = f a * f (b * 1)

Tactic:
simp only [h1 isUnit_one, hf1, mul_zero]

Premises used: MulZeroClass.mul_zero, isUnit_one
-- 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 : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : f 1 = 0
rw rw₁ : f a * f b = f a * f b
⊢ f a * f (b * 1) = f a * f b

Tactic:
rw [mul_one]

Premises used: mul_one
-- 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 : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : f 1 = 0
f₁ : f (a * b) = f (a * b * 1)
f₂ : f (a * b * 1) = 0
f₃ : 0 = f a * f (b * 1)
f₄ : f a * f (b * 1) = f a * f b
⊢ f (a * b) = f a * f b

Tactic:
calc
      f (a * b) = f (a * b * 1) := by rw [mul_one]
      _ = 0 := by simp only [h1 isUnit_one, hf1, mul_zero]
      _ = f a * f (b * 1) := by simp only [h1 isUnit_one, hf1, mul_zero]
      _ = f a * f b := by rw [mul_one]

Premises used: HMul.hMul, OfNat.ofNat
-- 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 : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : ¬f 1 = 0
⊢ Nontrivial α

Tactic:
haveI : Nontrivial α := ⟨⟨_, _, ha0⟩⟩
-- 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))
obtain : ∀ (ua : αˣ) (a_eq : (normalizedFactors a).prod * (↑ua : α) = a), f (a * b) = f a * f b
⊢ f (a * b) = f a * f b

Tactic:
obtain ⟨ua, a_eq⟩ := prod_normalizedFactors ha0

Premises used: UniqueFactorizationMonoid.prod_normalizedFactors
-- 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
obtain : ∀ (ub : αˣ) (b_eq : (normalizedFactors b).prod * (↑ub : α) = b), f (a * b) = f a * f b
⊢ f (a * b) = f a * f b

Tactic:
obtain ⟨ub, b_eq⟩ := prod_normalizedFactors hb0

Premises used: UniqueFactorizationMonoid.prod_normalizedFactors