-- Mathlib/RingTheory/Prime.lean
theorem mul_eq_mul_prime_prod {α : Type*} [DecidableEq α] {x y a : R} {s : Finset α} {p : α → R}
    (hp : ∀ i ∈ s, Prime (p i)) (hx : x * y = a * ∏ i ∈ s, p i) :
    ∃ (t u : Finset α) (b c : R),
      t ∪ u = s ∧ Disjoint t u ∧ a = b * c ∧ (x = b * ∏ i ∈ t, p i) ∧ y = c * ∏ i ∈ u, p i

Proof state:
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
α : Type u_2
inst✝ : DecidableEq α
p : α → R
i : α
s : Finset α
his : i ∉ s
ih :
  ∀ {x y a : R},
    (∀ i ∈ s, Prime (p i)) →
      x * y = a * ∏ i ∈ s, p i →
        ∃ t u b c, t ∪ u = s ∧ Disjoint t u ∧ a = b * c ∧ x = b * ∏ i ∈ t, p i ∧ y = c * ∏ i ∈ u, p i
a : R
hp : ∀ i_1 ∈ insert i s, Prime (p i_1)
hpi : Prime (p i)
t u : Finset α
b c : R
htus : t ∪ u = s
htu : Disjoint t u
hbc : a * p i = b * c
hx : (b * ∏ i ∈ t, p i) * (c * ∏ i ∈ u, p i) = a * p i * ∏ x ∈ s, p x
hit : i ∉ t
hiu : i ∉ u
⊢ b * c = p i * a

Tactic:
rw [← hbc, mul_comm]

Result:
no goals

Proof state:
case insert.intro.intro.intro.intro.intro.intro.intro.intro
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
α : Type u_2
inst✝ : DecidableEq α
p : α → R
i : α
s : Finset α
his : i ∉ s
ih :
  ∀ {x y a : R},
    (∀ i ∈ s, Prime (p i)) →
      x * y = a * ∏ i ∈ s, p i →
        ∃ t u b c, t ∪ u = s ∧ Disjoint t u ∧ a = b * c ∧ x = b * ∏ i ∈ t, p i ∧ y = c * ∏ i ∈ u, p i
a : R
hp : ∀ i_1 ∈ insert i s, Prime (p i_1)
hpi : Prime (p i)
t u : Finset α
b c : R
htus : t ∪ u = s
htu : Disjoint t u
hbc : a * p i = b * c
hx : (b * ∏ i ∈ t, p i) * (c * ∏ i ∈ u, p i) = a * p i * ∏ x ∈ s, p x
⊢ ∃ t_1 u_1 b_1 c_1,
    t_1 ∪ u_1 = insert i s ∧
      Disjoint t_1 u_1 ∧
        a = b_1 * c_1 ∧ b * ∏ i ∈ t, p i = b_1 * ∏ i ∈ t_1, p i ∧ c * ∏ i ∈ u, p i = c_1 * ∏ i ∈ u_1, p i

Tactic:
have hit : i ∉ t := fun hit ↦ his (htus ▸ mem_union_left _ hit)

Result:
case insert.intro.intro.intro.intro.intro.intro.intro.intro
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
α : Type u_2
inst✝ : DecidableEq α
p : α → R
i : α
s : Finset α
his : i ∉ s
ih :
  ∀ {x y a : R},
    (∀ i ∈ s, Prime (p i)) →
      x * y = a * ∏ i ∈ s, p i →
        ∃ t u b c, t ∪ u = s ∧ Disjoint t u ∧ a = b * c ∧ x = b * ∏ i ∈ t, p i ∧ y = c * ∏ i ∈ u, p i
a : R
hp : ∀ i_1 ∈ insert i s, Prime (p i_1)
hpi : Prime (p i)
t u : Finset α
b c : R
htus : t ∪ u = s
htu : Disjoint t u
hbc : a * p i = b * c
hx : (b * ∏ i ∈ t, p i) * (c * ∏ i ∈ u, p i) = a * p i * ∏ x ∈ s, p x
hit : i ∉ t
⊢ ∃ t_1 u_1 b_1 c_1,
    t_1 ∪ u_1 = insert i s ∧
      Disjoint t_1 u_1 ∧
        a = b_1 * c_1 ∧ b * ∏ i ∈ t, p i = b_1 * ∏ i ∈ t_1, p i ∧ c * ∏ i ∈ u, p i = c_1 * ∏ i ∈ u_1, p i

Proof state:
case insert.intro.intro.intro.intro.intro.intro.intro.intro
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
α : Type u_2
inst✝ : DecidableEq α
p : α → R
i : α
s : Finset α
his : i ∉ s
ih :
  ∀ {x y a : R},
    (∀ i ∈ s, Prime (p i)) →
      x * y = a * ∏ i ∈ s, p i →
        ∃ t u b c, t ∪ u = s ∧ Disjoint t u ∧ a = b * c ∧ x = b * ∏ i ∈ t, p i ∧ y = c * ∏ i ∈ u, p i
a : R
hp : ∀ i_1 ∈ insert i s, Prime (p i_1)
hpi : Prime (p i)
t u : Finset α
b c : R
htus : t ∪ u = s
htu : Disjoint t u
hbc : a * p i = b * c
hx : (b * ∏ i ∈ t, p i) * (c * ∏ i ∈ u, p i) = a * p i * ∏ x ∈ s, p x
hit : i ∉ t
hiu : i ∉ u
⊢ ∃ t_1 u_1 b_1 c_1,
    t_1 ∪ u_1 = insert i s ∧
      Disjoint t_1 u_1 ∧
        a = b_1 * c_1 ∧ b * ∏ i ∈ t, p i = b_1 * ∏ i ∈ t_1, p i ∧ c * ∏ i ∈ u, p i = c_1 * ∏ i ∈ u_1, p i

Tactic:
obtain ⟨d, rfl⟩ | ⟨d, rfl⟩ : p i ∣ b ∨ p i ∣ c := hpi.dvd_or_dvd ⟨a, by rw [← hbc, mul_comm]⟩

Result:
case insert.intro.intro.intro.intro.intro.intro.intro.intro.inl.intro
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
α : Type u_2
inst✝ : DecidableEq α
p : α → R
i : α
s : Finset α
his : i ∉ s
ih :
  ∀ {x y a : R},
    (∀ i ∈ s, Prime (p i)) →
      x * y = a * ∏ i ∈ s, p i →
        ∃ t u b c, t ∪ u = s ∧ Disjoint t u ∧ a = b * c ∧ x = b * ∏ i ∈ t, p i ∧ y = c * ∏ i ∈ u, p i
a : R
hp : ∀ i_1 ∈ insert i s, Prime (p i_1)
hpi : Prime (p i)
t u : Finset α
c : R
htus : t ∪ u = s
htu : Disjoint t u
hit : i ∉ t
hiu : i ∉ u
d : R
hbc : a * p i = p i * d * c
hx : (p i * d * ∏ i ∈ t, p i) * (c * ∏ i ∈ u, p i) = a * p i * ∏ x ∈ s, p x
⊢ ∃ t_1 u_1 b c_1,
    t_1 ∪ u_1 = insert i s ∧
      Disjoint t_1 u_1 ∧
        a = b * c_1 ∧ p i * d * ∏ i ∈ t, p i = b * ∏ i ∈ t_1, p i ∧ c * ∏ i ∈ u, p i = c_1 * ∏ i ∈ u_1, p i

case insert.intro.intro.intro.intro.intro.intro.intro.intro.inr.intro
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
α : Type u_2
inst✝ : DecidableEq α
p : α → R
i : α
s : Finset α
his : i ∉ s
ih :
  ∀ {x y a : R},
    (∀ i ∈ s, Prime (p i)) →
      x * y = a * ∏ i ∈ s, p i →
        ∃ t u b c, t ∪ u = s ∧ Disjoint t u ∧ a = b * c ∧ x = b * ∏ i ∈ t, p i ∧ y = c * ∏ i ∈ u, p i
a : R
hp : ∀ i_1 ∈ insert i s, Prime (p i_1)
hpi : Prime (p i)
t u : Finset α
b : R
htus : t ∪ u = s
htu : Disjoint t u
hit : i ∉ t
hiu : i ∉ u
d : R
hbc : a * p i = b * (p i * d)
hx : (b * ∏ i ∈ t, p i) * (p i * d * ∏ i ∈ u, p i) = a * p i * ∏ x ∈ s, p x
⊢ ∃ t_1 u_1 b_1 c,
    t_1 ∪ u_1 = insert i s ∧
      Disjoint t_1 u_1 ∧
        a = b_1 * c ∧ b * ∏ i ∈ t, p i = b_1 * ∏ i ∈ t_1, p i ∧ p i * d * ∏ i ∈ u, p i = c * ∏ i ∈ u_1, p i

Proof state:
case insert.intro.intro.intro.intro.intro.intro.intro.intro.inr.intro
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
α : Type u_2
inst✝ : DecidableEq α
p : α → R
i : α
s : Finset α
his : i ∉ s
ih :
  ∀ {x y a : R},
    (∀ i ∈ s, Prime (p i)) →
      x * y = a * ∏ i ∈ s, p i →
        ∃ t u b c, t ∪ u = s ∧ Disjoint t u ∧ a = b * c ∧ x = b * ∏ i ∈ t, p i ∧ y = c * ∏ i ∈ u, p i
a : R
hp : ∀ i_1 ∈ insert i s, Prime (p i_1)
hpi : Prime (p i)
t u : Finset α
b : R
htus : t ∪ u = s
htu : Disjoint t u
hit : i ∉ t
hiu : i ∉ u
d : R
hbc : a = b * d
hx : (b * ∏ i ∈ t, p i) * (p i * d * ∏ i ∈ u, p i) = a * p i * ∏ x ∈ s, p x
⊢ ∃ t_1 u_1 b_1 c,
    t_1 ∪ u_1 = insert i s ∧
      Disjoint t_1 u_1 ∧
        a = b_1 * c ∧ b * ∏ i ∈ t, p i = b_1 * ∏ i ∈ t_1, p i ∧ p i * d * ∏ i ∈ u, p i = c * ∏ i ∈ u_1, p i

Tactic:
exact ⟨t, insert i u, b, d, by rw [union_insert, htus], disjoint_insert_right.2 ⟨hit, htu⟩, by
    simp [← hbc, prod_insert hiu, mul_assoc, mul_comm, mul_left_comm]⟩

Result:
no goals

Proof state:
case insert
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
α : Type u_2
inst✝ : DecidableEq α
p : α → R
i : α
s : Finset α
his : i ∉ s
ih :
  ∀ {x y a : R},
    (∀ i ∈ s, Prime (p i)) →
      x * y = a * ∏ i ∈ s, p i →
        ∃ t u b c, t ∪ u = s ∧ Disjoint t u ∧ a = b * c ∧ x = b * ∏ i ∈ t, p i ∧ y = c * ∏ i ∈ u, p i
x y a : R
hp : ∀ i_1 ∈ insert i s, Prime (p i_1)
hx : x * y = a * ∏ i ∈ insert i s, p i
⊢ ∃ t u b c, t ∪ u = insert i s ∧ Disjoint t u ∧ a = b * c ∧ x = b * ∏ i ∈ t, p i ∧ y = c * ∏ i ∈ u, p i

Tactic:
rw [prod_insert his, ← mul_assoc] at hx

Result:
case insert
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
α : Type u_2
inst✝ : DecidableEq α
p : α → R
i : α
s : Finset α
his : i ∉ s
ih :
  ∀ {x y a : R},
    (∀ i ∈ s, Prime (p i)) →
      x * y = a * ∏ i ∈ s, p i →
        ∃ t u b c, t ∪ u = s ∧ Disjoint t u ∧ a = b * c ∧ x = b * ∏ i ∈ t, p i ∧ y = c * ∏ i ∈ u, p i
x y a : R
hp : ∀ i_1 ∈ insert i s, Prime (p i_1)
hx : x * y = a * p i * ∏ x ∈ s, p x
⊢ ∃ t u b c, t ∪ u = insert i s ∧ Disjoint t u ∧ a = b * c ∧ x = b * ∏ i ∈ t, p i ∧ y = c * ∏ i ∈ u, p i