no goals
M : Type ?u.20156
inst✝⁵ : CancelMonoidWithZero M
inst✝⁴ : Finite M
ι : Type u_1
R : Type u_2
inst✝³ : CommSemiring R
inst✝² : IsDomain R
inst✝¹ : GCDMonoid R
inst✝ : Unique Rˣ
n : ℕ
c : R
s : Finset ι
f : ι → R
h : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → IsCoprime (f i) (f j)
hprod : ∏ i in s, f i = c ^ n
⊢ ∀ (i : ι), i ∈ s → ∃ d, f i = d ^ n
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
M : Type ?u.20156
inst✝⁵ : CancelMonoidWithZero M
inst✝⁴ : Finite M
ι : Type u_1
R : Type u_2
inst✝³ : CommSemiring R
inst✝² : IsDomain R
inst✝¹ : GCDMonoid R
inst✝ : Unique Rˣ
n : ℕ
c : R
s : Finset ι
f : ι → R
h : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → IsCoprime (f i) (f j)
hprod : ∏ i in s, f i = c ^ n
i : ι
hi : i ∈ s
⊢ ∃ d, f i = d ^ n
M : Type ?u.20156
inst✝⁵ : CancelMonoidWithZero M
inst✝⁴ : Finite M
ι : Type u_1
R : Type u_2
inst✝³ : CommSemiring R
inst✝² : IsDomain R
inst✝¹ : GCDMonoid R
inst✝ : Unique Rˣ
n : ℕ
c : R
s : Finset ι
f : ι → R
h : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → IsCoprime (f i) (f j)
hprod : ∏ i in s, f i = c ^ n
⊢ ∀ (i : ι), i ∈ s → ∃ d, f i = d ^ n
intro i hi
M : Type ?u.20156
inst✝⁵ : CancelMonoidWithZero M
inst✝⁴ : Finite M
ι : Type u_1
R : Type u_2
inst✝³ : CommSemiring R
inst✝² : IsDomain R
inst✝¹ : GCDMonoid R
inst✝ : Unique Rˣ
n : ℕ
c : R
s : Finset ι
f : ι → R
h : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → IsCoprime (f i) (f j)
i : ι
hprod : f i * ∏ x in erase s i, f x = c ^ n
hi : i ∈ s
⊢ ∃ d, f i = d ^ n
M : Type ?u.20156
inst✝⁵ : CancelMonoidWithZero M
inst✝⁴ : Finite M
ι : Type u_1
R : Type u_2
inst✝³ : CommSemiring R
inst✝² : IsDomain R
inst✝¹ : GCDMonoid R
inst✝ : Unique Rˣ
n : ℕ
c : R
s : Finset ι
f : ι → R
h : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → IsCoprime (f i) (f j)
hprod : ∏ i in s, f i = c ^ n
i : ι
hi : i ∈ s
⊢ ∃ d, f i = d ^ n
rw [← insert_erase hi, prod_insert (not_mem_erase i s)] at hprod
M : Type ?u.20156
inst✝⁵ : CancelMonoidWithZero M
inst✝⁴ : Finite M
ι : Type u_1
R : Type u_2
inst✝³ : CommSemiring R
inst✝² : IsDomain R
inst✝¹ : GCDMonoid R
inst✝ : Unique Rˣ
n : ℕ
c : R
s : Finset ι
f : ι → R
h : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → IsCoprime (f i) (f j)
i : ι
hprod : f i * ∏ x in erase s i, f x = c ^ n
hi : i ∈ s
j : ι
hj : j ∈ erase s i
hij : i = j
⊢ False
M : Type ?u.20156
inst✝⁵ : CancelMonoidWithZero M
inst✝⁴ : Finite M
ι : Type u_1
R : Type u_2
inst✝³ : CommSemiring R
inst✝² : IsDomain R
inst✝¹ : GCDMonoid R
inst✝ : Unique Rˣ
n : ℕ
c : R
s : Finset ι
f : ι → R
h : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → IsCoprime (f i) (f j)
i : ι
hprod : f i * ∏ x in erase s i, f x = c ^ n
hi : i ∈ s
⊢ ∃ d, f i = d ^ n
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
M : Type ?u.20156
inst✝⁵ : CancelMonoidWithZero M
inst✝⁴ : Finite M
ι : Type u_1
R : Type u_2
inst✝³ : CommSemiring R
inst✝² : IsDomain R
inst✝¹ : GCDMonoid R
inst✝ : Unique Rˣ
n : ℕ
c : R
s : Finset ι
f : ι → R
h : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → IsCoprime (f i) (f j)
i : ι
hprod : f i * ∏ x in erase s i, f x = c ^ n
hi : i ∈ s
j : ι
hj : j ∈ erase s j
hij : i = j
⊢ False
M : Type ?u.20156
inst✝⁵ : CancelMonoidWithZero M
inst✝⁴ : Finite M
ι : Type u_1
R : Type u_2
inst✝³ : CommSemiring R
inst✝² : IsDomain R
inst✝¹ : GCDMonoid R
inst✝ : Unique Rˣ
n : ℕ
c : R
s : Finset ι
f : ι → R
h : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → IsCoprime (f i) (f j)
i : ι
hprod : f i * ∏ x in erase s i, f x = c ^ n
hi : i ∈ s
j : ι
hj : j ∈ erase s i
hij : i = j
⊢ False
rw [hij] at hj
no goals
M : Type ?u.20156
inst✝⁵ : CancelMonoidWithZero M
inst✝⁴ : Finite M
ι : Type u_1
R : Type u_2
inst✝³ : CommSemiring R
inst✝² : IsDomain R
inst✝¹ : GCDMonoid R
inst✝ : Unique Rˣ
n : ℕ
c : R
s : Finset ι
f : ι → R
h : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → IsCoprime (f i) (f j)
i : ι
hprod : f i * ∏ x in erase s i, f x = c ^ n
hi : i ∈ s
j : ι
hj : j ∈ erase s j
hij : i = j
⊢ False
exact (s.not_mem_erase _) hj