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 α
β : 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'))
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'))
⊢ 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]
-- 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'))
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'))
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'))
⊢ 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) * f (∏ p ∈ s, 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]
-- 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'))
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'))
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'))
insert₉ :
  f p ^ (i p + j p) * (f (∏ p ∈ s, p ^ i p) * f (∏ p ∈ s, p ^ j p)) =
    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 * f p ^ j p * (f (∏ p ∈ s, p ^ i p) * f (∏ p ∈ s, 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]
-- 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'))
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'))
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'))
insert₉ :
  f p ^ (i p + j p) * (f (∏ p ∈ s, p ^ i p) * f (∏ p ∈ s, p ^ j p)) =
    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 * f p ^ j p * (f (∏ p ∈ s, p ^ i p) * f (∏ p ∈ s, p ^ j p)) =
    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 * (f p ^ j p * (f (∏ p ∈ s, p ^ i p) * f (∏ p ∈ s, 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]
-- 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 : α → β
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 α
⊢ f (∏ p ∈ s, p ^ (i p + j p)) = f (∏ p ∈ s, p ^ i p) * f (∏ p ∈ s, p ^ j p)
have 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)
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]
Cleared hypotheses: s, is_prime, is_coprime
-- 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 : α → β
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)
⊢ f (∏ p ∈ s, p ^ (i p + j p)) = f (∏ p ∈ s, p ^ i p) * f (∏ p ∈ s, p ^ j p)
have 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 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)
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]
Cleared hypotheses: s, is_prime, is_coprime
-- 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 : α → β
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 α
⊢ f (a * b) = f a * f b
have pos : ∀ (ha0 : a = 0), f (a * b) = f a * f b
Tactic: by_cases ha0 : a = 0
-- 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 : α → β
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
⊢ f (a * b) = f a * f b
have neg : ∀ (ha0 : ¬a = 0), f (a * b) = f a * f b
Tactic: by_cases ha0 : a = 0
-- 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 : α → β
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
⊢ f (a * b) = f a * f b
have pos : f (0 * b) = f 0 * f b
Tactic: rw [ha0, zero_mul, h0, zero_mul]
-- 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 : α → β
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
⊢ f (a * b) = f a * f b
have pos₁ : f 0 = f 0 * f b
Tactic: rw [ha0, zero_mul, h0, zero_mul]
-- 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 : α → β
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
⊢ f (a * b) = f a * f b
have pos₂ : 0 = 0 * f b
Tactic: rw [ha0, zero_mul, h0, zero_mul]
-- 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 : α → β
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
⊢ f (a * b) = f a * f b
have pos₃ : Eq.{u_3 + 1} (α := β) 0 0
Tactic: rw [ha0, zero_mul, h0, zero_mul]
-- 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 : α → β
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
⊢ f (a * b) = f a * f b
have pos : ∀ (hb0 : b = 0), f (a * b) = f a * f b
Tactic: by_cases hb0 : b = 0
-- 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 : α → β
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
⊢ f (a * b) = f a * f b
have neg : ∀ (hb0 : ¬b = 0), f (a * b) = f a * f b
Tactic: by_cases hb0 : b = 0
-- 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 : α → β
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
⊢ f (a * b) = f a * f b
have pos : f (a * 0) = f a * f 0
Tactic: rw [hb0, mul_zero, h0, mul_zero]
-- 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 : α → β
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
⊢ f (a * b) = f a * f b
have pos₁ : f 0 = f a * f 0
Tactic: rw [hb0, mul_zero, h0, mul_zero]
-- 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 : α → β
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
⊢ f (a * b) = f a * f b
have pos₂ : 0 = f a * 0
Tactic: rw [hb0, mul_zero, h0, mul_zero]
-- 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 : α → β
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
⊢ f (a * b) = f a * f b
have pos₃ : Eq.{u_3 + 1} (α := β) 0 0
Tactic: rw [hb0, mul_zero, h0, mul_zero]
-- 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 : α → β
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
⊢ f (a * b) = f a * f b
have pos : ∀ (hf1 : f 1 = 0), f (a * b) = f a * f b
Tactic: by_cases hf1 : f 1 = 0
-- 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 : α → β
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
⊢ f (a * b) = f a * f b
have neg : ∀ (hf1 : ¬f 1 = 0), f (a * b) = f a * f b
Tactic: by_cases hf1 : f 1 = 0
-- 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 : α → β
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) = f (a * b * 1)
have rw : f (a * b) = f (a * b)
Tactic: rw [mul_one]