awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative (goal)
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))
have neg : ∀ p ∈ (normalizedFactors a).toFinset, Prime p
Tactic: refine induction_on_prime_power _ _ ?_ ?_ @h1 @hpr @hcp
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative (goal)
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
⊢ P (∏ m ∈ (normalizedFactors a).toFinset, id m ^ Multiset.count m (normalizedFactors a))
have neg₁ : ∀ p ∈ (normalizedFactors a).toFinset, ∀ q ∈ (normalizedFactors a).toFinset, p ∣ q → p = q
Tactic: refine induction_on_prime_power _ _ ?_ ?_ @h1 @hpr @hcp
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative (goal)
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).toFinset, Prime p
have neg : ∀ p ∈ normalizedFactors a, Prime p
Tactic: simp only [Multiset.mem_toFinset]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative (goal)
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).toFinset, ∀ q ∈ (normalizedFactors a).toFinset, p ∣ q → p = q
have neg : ∀ p ∈ normalizedFactors a, ∀ q ∈ normalizedFactors a, p ∣ q → p = q
Tactic: simp only [Multiset.mem_toFinset]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative (hypothesis)
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
⊢ f (∏ p ∈ insert p s, p ^ (i p + j p)) = f (∏ p ∈ insert p s, p ^ i p) * f (∏ p ∈ insert p s, p ^ j p)
have hpr_p : Prime p
Tactic: have hpr_p := is_prime _ (Finset.mem_insert_self _ _)
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative (hypothesis)
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
⊢ f (∏ p ∈ insert p s, p ^ (i p + j p)) = f (∏ p ∈ insert p s, p ^ i p) * f (∏ p ∈ insert p s, p ^ j p)
have hpr_s : ∀ p ∈ s, Prime p
Tactic: have hpr_s : ∀ p ∈ s, Prime p := fun p hp => is_prime _ (Finset.mem_insert_of_mem hp)
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative (hypothesis)
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
⊢ f (∏ p ∈ insert p s, p ^ (i p + j p)) = f (∏ p ∈ insert p s, p ^ i p) * f (∏ p ∈ insert p s, p ^ j p)
have hcp_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
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative (hypothesis)
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')
⊢ f (∏ p ∈ insert p s, p ^ (i p + j p)) = f (∏ p ∈ insert p s, p ^ i p) * f (∏ p ∈ insert p s, p ^ j p)
have hcp_s : ∀ 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)
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative (goal)
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')
hcp_s : ∀ p ∈ s, ∀ q ∈ s, p ∣ q → p = q
⊢ f (∏ p ∈ insert p s, p ^ (i p + j p)) = f (∏ p ∈ insert p s, p ^ i p) * f (∏ p ∈ insert p s, p ^ j p)
have insert : f (p ^ (i p + j p) * ∏ x ∈ s, x ^ (i x + j x)) = f (∏ p ∈ insert p s, p ^ i p) * f (∏ p ∈ insert p s, p ^ j p)
Tactic: 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]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative (goal)
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.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
hpr_p : Prime p
hpr_s : ∀ p ∈ s, Prime p
hcp_p : ∀ (i : α → ℕ), IsRelPrime (p ^ i p) (∏ p' ∈ s, p' ^ i p')
hcp_s : ∀ p ∈ s, ∀ q ∈ s, p ∣ q → p = q
insert :
  f (p ^ (i p + j p) * ∏ x ∈ s, x ^ (i x + j x)) =
    f (∏ p ∈ Insert.insert p s, p ^ i p) * f (∏ p ∈ Insert.insert p s, p ^ j p)
⊢ 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)
have insert₁ : f (p ^ (i p + j p) * ∏ x ∈ s, x ^ (i x + j x)) = f (p ^ i p * ∏ x ∈ s, x ^ i x) * f (∏ p ∈ Insert.insert p s, p ^ j p)
Tactic: 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]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative (goal)
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.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
hpr_p : Prime p
hpr_s : ∀ p ∈ s, Prime p
hcp_p : ∀ (i : α → ℕ), IsRelPrime (p ^ i p) (∏ p' ∈ s, p' ^ i p')
hcp_s : ∀ p ∈ s, ∀ q ∈ s, p ∣ q → p = q
insert :
  f (p ^ (i p + j p) * ∏ x ∈ s, x ^ (i x + j x)) =
    f (∏ p ∈ Insert.insert p s, p ^ i p) * f (∏ p ∈ Insert.insert p s, p ^ j p)
insert₁ :
  f (p ^ (i p + j p) * ∏ x ∈ s, x ^ (i x + j x)) = f (p ^ i p * ∏ x ∈ s, x ^ i x) * f (∏ p ∈ Insert.insert p s, p ^ j p)
⊢ 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)
have insert₂ : f (p ^ (i p + j p) * ∏ x ∈ s, x ^ (i x + j x)) = f (p ^ i p * ∏ x ∈ s, x ^ i x) * f (p ^ j p * ∏ x ∈ s, x ^ j x)
Tactic: 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]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative (goal)
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.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
hpr_p : Prime p
hpr_s : ∀ p ∈ s, Prime p
hcp_p : ∀ (i : α → ℕ), IsRelPrime (p ^ i p) (∏ p' ∈ s, p' ^ i p')
hcp_s : ∀ p ∈ s, ∀ q ∈ s, p ∣ q → p = q
insert :
  f (p ^ (i p + j p) * ∏ x ∈ s, x ^ (i x + j x)) =
    f (∏ p ∈ Insert.insert p s, p ^ i p) * f (∏ p ∈ Insert.insert p s, p ^ j p)
insert₁ :
  f (p ^ (i p + j p) * ∏ x ∈ s, x ^ (i x + j x)) = f (p ^ i p * ∏ x ∈ s, x ^ i x) * f (∏ p ∈ Insert.insert p s, p ^ j p)
insert₂ :
  f (p ^ (i p + j p) * ∏ x ∈ s, x ^ (i x + j x)) = f (p ^ i p * ∏ x ∈ s, x ^ i x) * f (p ^ j p * ∏ x ∈ s, x ^ j x)
⊢ 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)
have insert₃ : f (p ^ (i p + j p) * ∏ x ∈ s, x ^ (i x + j x)) = f (p ^ i p) * f (∏ p' ∈ s, p' ^ i p') * f (p ^ j p * ∏ x ∈ s, x ^ j x)
Tactic: 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]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative (goal)
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.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
hpr_p : Prime p
hpr_s : ∀ p ∈ s, Prime p
hcp_p : ∀ (i : α → ℕ), IsRelPrime (p ^ i p) (∏ p' ∈ s, p' ^ i p')
hcp_s : ∀ p ∈ s, ∀ q ∈ s, p ∣ q → p = q
insert :
  f (p ^ (i p + j p) * ∏ x ∈ s, x ^ (i x + j x)) =
    f (∏ p ∈ Insert.insert p s, p ^ i p) * f (∏ p ∈ Insert.insert p s, p ^ j p)
insert₁ :
  f (p ^ (i p + j p) * ∏ x ∈ s, x ^ (i x + j x)) = f (p ^ i p * ∏ x ∈ s, x ^ i x) * f (∏ p ∈ Insert.insert p s, p ^ j p)
insert₂ :
  f (p ^ (i p + j p) * ∏ x ∈ s, x ^ (i x + j x)) = f (p ^ i p * ∏ x ∈ s, x ^ i x) * f (p ^ j p * ∏ x ∈ s, x ^ j x)
insert₃ :
  f (p ^ (i p + j p) * ∏ x ∈ s, x ^ (i x + j x)) =
    f (p ^ i p) * f (∏ p' ∈ s, p' ^ i p') * f (p ^ j p * ∏ x ∈ s, x ^ j x)
⊢ 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)
have insert₄ : f (p ^ (i p + j p) * ∏ x ∈ s, x ^ (i x + j x)) = f p ^ i p * f (∏ p' ∈ s, p' ^ i p') * f (p ^ j p * ∏ x ∈ s, x ^ j x)
Tactic: 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]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative (goal)
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.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
hpr_p : Prime p
hpr_s : ∀ p ∈ s, Prime p
hcp_p : ∀ (i : α → ℕ), IsRelPrime (p ^ i p) (∏ p' ∈ s, p' ^ i p')
hcp_s : ∀ p ∈ s, ∀ q ∈ s, p ∣ q → p = q
insert :
  f (p ^ (i p + j p) * ∏ x ∈ s, x ^ (i x + j x)) =
    f (∏ p ∈ Insert.insert p s, p ^ i p) * f (∏ p ∈ Insert.insert p s, p ^ j p)
insert₁ :
  f (p ^ (i p + j p) * ∏ x ∈ s, x ^ (i x + j x)) = f (p ^ i p * ∏ x ∈ s, x ^ i x) * f (∏ p ∈ Insert.insert p s, p ^ j p)
insert₂ :
  f (p ^ (i p + j p) * ∏ x ∈ s, x ^ (i x + j x)) = f (p ^ i p * ∏ x ∈ s, x ^ i x) * f (p ^ j p * ∏ x ∈ s, x ^ j x)
insert₃ :
  f (p ^ (i p + j p) * ∏ x ∈ s, x ^ (i x + j x)) =
    f (p ^ i p) * f (∏ p' ∈ s, p' ^ i p') * f (p ^ j p * ∏ x ∈ s, x ^ j x)
insert₄ :
  f (p ^ (i p + j p) * ∏ x ∈ s, x ^ (i x + j x)) = f p ^ i p * f (∏ p' ∈ s, p' ^ i p') * f (p ^ j p * ∏ x ∈ s, x ^ j x)
⊢ 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)
have insert₅ : f (p ^ (i p + j p) * ∏ x ∈ s, x ^ (i x + j x)) =
  f p ^ i p * f (∏ p' ∈ s, p' ^ i p') * (f (p ^ j p) * f (∏ p' ∈ s, p' ^ j p'))
Tactic: 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]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative (goal)
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.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
hpr_p : Prime p
hpr_s : ∀ p ∈ s, Prime p
hcp_p : ∀ (i : α → ℕ), IsRelPrime (p ^ i p) (∏ p' ∈ s, p' ^ i p')
hcp_s : ∀ p ∈ s, ∀ q ∈ s, p ∣ q → p = q
insert :
  f (p ^ (i p + j p) * ∏ x ∈ s, x ^ (i x + j x)) =
    f (∏ p ∈ Insert.insert p s, p ^ i p) * f (∏ p ∈ Insert.insert p s, p ^ j p)
insert₁ :
  f (p ^ (i p + j p) * ∏ x ∈ s, x ^ (i x + j x)) = f (p ^ i p * ∏ x ∈ s, x ^ i x) * f (∏ p ∈ Insert.insert p s, p ^ j p)
insert₂ :
  f (p ^ (i p + j p) * ∏ x ∈ s, x ^ (i x + j x)) = f (p ^ i p * ∏ x ∈ s, x ^ i x) * f (p ^ j p * ∏ x ∈ s, x ^ j x)
insert₃ :
  f (p ^ (i p + j p) * ∏ x ∈ s, x ^ (i x + j x)) =
    f (p ^ i p) * f (∏ p' ∈ s, p' ^ i p') * f (p ^ j p * ∏ x ∈ s, x ^ j x)
insert₄ :
  f (p ^ (i p + j p) * ∏ x ∈ s, x ^ (i x + j x)) = f p ^ i p * f (∏ p' ∈ s, p' ^ i p') * f (p ^ j p * ∏ x ∈ s, x ^ j x)
insert₅ :
  f (p ^ (i p + j p) * ∏ x ∈ s, x ^ (i x + j x)) =
    f p ^ i p * f (∏ p' ∈ s, p' ^ i p') * (f (p ^ j p) * f (∏ p' ∈ s, p' ^ j p'))
⊢ 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)
have insert₆ : f (p ^ (i p + j p) * ∏ x ∈ s, x ^ (i x + j x)) =
  f p ^ i p * f (∏ p' ∈ s, p' ^ i p') * (f p ^ j p * f (∏ p' ∈ s, p' ^ j p'))
Tactic: 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]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative (goal)
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.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
hpr_p : Prime p
hpr_s : ∀ p ∈ s, Prime p
hcp_p : ∀ (i : α → ℕ), IsRelPrime (p ^ i p) (∏ p' ∈ s, p' ^ i p')
hcp_s : ∀ p ∈ s, ∀ q ∈ s, p ∣ q → p = q
insert :
  f (p ^ (i p + j p) * ∏ x ∈ s, x ^ (i x + j x)) =
    f (∏ p ∈ Insert.insert p s, p ^ i p) * f (∏ p ∈ Insert.insert p s, p ^ j p)
insert₁ :
  f (p ^ (i p + j p) * ∏ x ∈ s, x ^ (i x + j x)) = f (p ^ i p * ∏ x ∈ s, x ^ i x) * f (∏ p ∈ Insert.insert p s, p ^ j p)
insert₂ :
  f (p ^ (i p + j p) * ∏ x ∈ s, x ^ (i x + j x)) = f (p ^ i p * ∏ x ∈ s, x ^ i x) * f (p ^ j p * ∏ x ∈ s, x ^ j x)
insert₃ :
  f (p ^ (i p + j p) * ∏ x ∈ s, x ^ (i x + j x)) =
    f (p ^ i p) * f (∏ p' ∈ s, p' ^ i p') * f (p ^ j p * ∏ x ∈ s, x ^ j x)
insert₄ :
  f (p ^ (i p + j p) * ∏ x ∈ s, x ^ (i x + j x)) = f p ^ i p * f (∏ p' ∈ s, p' ^ i p') * f (p ^ j p * ∏ x ∈ s, x ^ j x)
insert₅ :
  f (p ^ (i p + j p) * ∏ x ∈ s, x ^ (i x + j x)) =
    f p ^ i p * f (∏ p' ∈ s, p' ^ i p') * (f (p ^ j p) * f (∏ p' ∈ s, p' ^ j p'))
insert₆ :
  f (p ^ (i p + j p) * ∏ x ∈ s, x ^ (i x + j x)) =
    f p ^ i p * f (∏ p' ∈ s, p' ^ i p') * (f p ^ j p * f (∏ p' ∈ s, p' ^ j p'))
⊢ 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)
have insert₇ : f (p ^ (i p + j p)) * f (∏ p' ∈ s, p' ^ (i p' + j p')) =
  f p ^ i p * f (∏ p' ∈ s, p' ^ i p') * (f p ^ j p * f (∏ p' ∈ s, p' ^ j p'))
Tactic: 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]