-- Mathlib/RingTheory/IntegralDomain.lean
theorem Finset.exists_eq_pow_of_mul_eq_pow_of_coprime {ι R : Type*} [CommSemiring R] [IsDomain R]
    [GCDMonoid R] [Subsingleton Rˣ] {n : ℕ} {c : R} {s : Finset ι} {f : ι → R}
    (h : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → IsCoprime (f i) (f j))
    (hprod : ∏ i ∈ s, f i = c ^ n) : ∀ i ∈ s, ∃ d : R, f i = d ^ n

Proof state:
ι : Type u_2
R : Type u_3
inst✝³ : CommSemiring R
inst✝² : IsDomain R
inst✝¹ : GCDMonoid R
inst✝ : Subsingleton Rˣ
n : ℕ
c : R
s : Finset ι
f : ι → R
h : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → IsCoprime (f i) (f j)
hprod : ∏ i ∈ s, f i = c ^ n
⊢ ∀ i ∈ s, ∃ d, f i = d ^ n

Tactic:
classical
  intro i hi
  rw [← insert_erase hi, prod_insert (not_mem_erase i s)] at hprod
  refine
    exists_eq_pow_of_mul_eq_pow_of_coprime
      (IsCoprime.prod_right fun j hj => h i hi j (erase_subset i s hj) fun hij => ?_) hprod
  rw [hij] at hj
  exact (s.not_mem_erase _) hj

Result:
no goals

Proof state:
ι : Type u_2
R : Type u_3
inst✝³ : CommSemiring R
inst✝² : IsDomain R
inst✝¹ : GCDMonoid R
inst✝ : Subsingleton Rˣ
n : ℕ
c : R
s : Finset ι
f : ι → R
h : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → IsCoprime (f i) (f j)
i : ι
hprod : f i * ∏ x ∈ s.erase i, f x = c ^ n
hi : i ∈ s
j : ι
hj : j ∈ s.erase i
hij : i = j
⊢ False

Tactic:
rw [hij] at hj

Result:
ι : Type u_2
R : Type u_3
inst✝³ : CommSemiring R
inst✝² : IsDomain R
inst✝¹ : GCDMonoid R
inst✝ : Subsingleton Rˣ
n : ℕ
c : R
s : Finset ι
f : ι → R
h : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → IsCoprime (f i) (f j)
i : ι
hprod : f i * ∏ x ∈ s.erase i, f x = c ^ n
hi : i ∈ s
j : ι
hj : j ∈ s.erase j
hij : i = j
⊢ False

Proof state:
ι : Type u_2
R : Type u_3
inst✝³ : CommSemiring R
inst✝² : IsDomain R
inst✝¹ : GCDMonoid R
inst✝ : Subsingleton Rˣ
n : ℕ
c : R
s : Finset ι
f : ι → R
h : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → IsCoprime (f i) (f j)
hprod : ∏ i ∈ s, f i = c ^ n
i : ι
hi : i ∈ s
⊢ ∃ d, f i = d ^ n

Tactic:
rw [← insert_erase hi, prod_insert (not_mem_erase i s)] at hprod

Result:
ι : Type u_2
R : Type u_3
inst✝³ : CommSemiring R
inst✝² : IsDomain R
inst✝¹ : GCDMonoid R
inst✝ : Subsingleton Rˣ
n : ℕ
c : R
s : Finset ι
f : ι → R
h : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → IsCoprime (f i) (f j)
i : ι
hprod : f i * ∏ x ∈ s.erase i, f x = c ^ n
hi : i ∈ s
⊢ ∃ d, f i = d ^ n

Proof state:
ι : Type u_2
R : Type u_3
inst✝³ : CommSemiring R
inst✝² : IsDomain R
inst✝¹ : GCDMonoid R
inst✝ : Subsingleton Rˣ
n : ℕ
c : R
s : Finset ι
f : ι → R
h : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → IsCoprime (f i) (f j)
i : ι
hprod : f i * ∏ x ∈ s.erase i, f x = c ^ n
hi : i ∈ s
⊢ ∃ d, f i = d ^ n

Tactic:
refine
  exists_eq_pow_of_mul_eq_pow_of_coprime
    (IsCoprime.prod_right fun j hj => h i hi j (erase_subset i s hj) fun hij => ?_) hprod

Result:
ι : Type u_2
R : Type u_3
inst✝³ : CommSemiring R
inst✝² : IsDomain R
inst✝¹ : GCDMonoid R
inst✝ : Subsingleton Rˣ
n : ℕ
c : R
s : Finset ι
f : ι → R
h : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → IsCoprime (f i) (f j)
i : ι
hprod : f i * ∏ x ∈ s.erase i, f x = c ^ n
hi : i ∈ s
j : ι
hj : j ∈ s.erase i
hij : i = j
⊢ False

Proof state:
ι : Type u_2
R : Type u_3
inst✝³ : CommSemiring R
inst✝² : IsDomain R
inst✝¹ : GCDMonoid R
inst✝ : Subsingleton Rˣ
n : ℕ
c : R
s : Finset ι
f : ι → R
h : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → IsCoprime (f i) (f j)
i : ι
hprod : f i * ∏ x ∈ s.erase i, f x = c ^ n
hi : i ∈ s
j : ι
hj : j ∈ s.erase j
hij : i = j
⊢ False

Tactic:
exact (s.not_mem_erase _) hj

Result:
no goals

Proof state:
ι : Type u_2
R : Type u_3
inst✝³ : CommSemiring R
inst✝² : IsDomain R
inst✝¹ : GCDMonoid R
inst✝ : Subsingleton Rˣ
n : ℕ
c : R
s : Finset ι
f : ι → R
h : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → IsCoprime (f i) (f j)
hprod : ∏ i ∈ s, f i = c ^ n
⊢ ∀ i ∈ s, ∃ d, f i = d ^ n

Tactic:
intro i hi

Result:
ι : Type u_2
R : Type u_3
inst✝³ : CommSemiring R
inst✝² : IsDomain R
inst✝¹ : GCDMonoid R
inst✝ : Subsingleton Rˣ
n : ℕ
c : R
s : Finset ι
f : ι → R
h : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → IsCoprime (f i) (f j)
hprod : ∏ i ∈ s, f i = c ^ n
i : ι
hi : i ∈ s
⊢ ∃ d, f i = d ^ n