-- 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'))
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 ∈ s, p ^ i p) * (f p ^ j 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]