-- Mathlib/RingTheory/Polynomial/Cyclotomic/Basic.lean
theorem _root_.IsPrimitiveRoot.pow_sub_pow_eq_prod_sub_mul (hpos : 0 < n)
    (h : IsPrimitiveRoot ζ n) : x ^ n - y ^ n = ∏ ζ ∈ nthRootsFinset n R, (x - ζ * y)

Proof state:
case a
R : Type u_1
inst✝¹ : CommRing R
ζ : R
n : ℕ
x y : R
inst✝ : IsDomain R
hpos : 0 < n
h : IsPrimitiveRoot ζ n
K : Type u_1 := FractionRing R
h' : IsPrimitiveRoot ((algebraMap R K) ζ) n
⊢ (algebraMap R K) x ^ n - (algebraMap R K) y ^ n =
    ∏ x_1 ∈ nthRootsFinset n R, ((algebraMap R K) x - (algebraMap R K) x_1 * (algebraMap R K) y)

Tactic:
rw [h'.pow_sub_pow_eq_prod_sub_mul_field _ _ hpos]

Result:
case a
R : Type u_1
inst✝¹ : CommRing R
ζ : R
n : ℕ
x y : R
inst✝ : IsDomain R
hpos : 0 < n
h : IsPrimitiveRoot ζ n
K : Type u_1 := FractionRing R
h' : IsPrimitiveRoot ((algebraMap R K) ζ) n
⊢ ∏ ζ ∈ nthRootsFinset n K, ((algebraMap R K) x - ζ * (algebraMap R K) y) =
    ∏ x_1 ∈ nthRootsFinset n R, ((algebraMap R K) x - (algebraMap R K) x_1 * (algebraMap R K) y)

Proof state:
case a
R : Type u_1
inst✝¹ : CommRing R
ζ : R
n : ℕ
x y : R
inst✝ : IsDomain R
hpos : 0 < n
h : IsPrimitiveRoot ζ n
K : Type u_1 := FractionRing R
h' : IsPrimitiveRoot ((algebraMap R K) ζ) n
⊢ ∏ ζ ∈ nthRootsFinset n K, ((algebraMap R K) x - ζ * (algebraMap R K) y) =
    ∏ x_1 ∈ nthRootsFinset n R, ((algebraMap R K) x - (algebraMap R K) x_1 * (algebraMap R K) y)

Tactic:
refine (prod_nbij (algebraMap R K) (fun a ha ↦ map_mem_nthRootsFinset ha _) (fun a _ b _ H ↦
  FaithfulSMul.algebraMap_injective R K H) (fun a ha ↦ ?_) (fun _ _ ↦ rfl)).symm

Result:
case a
R : Type u_1
inst✝¹ : CommRing R
ζ : R
n : ℕ
x y : R
inst✝ : IsDomain R
hpos : 0 < n
h : IsPrimitiveRoot ζ n
K : Type u_1 := FractionRing R
h' : IsPrimitiveRoot ((algebraMap R K) ζ) n
a : K
ha : a ∈ ↑(nthRootsFinset n K)
⊢ a ∈ ⇑(algebraMap R K) '' ↑(nthRootsFinset n R)

Proof state:
case a
R : Type u_1
inst✝¹ : CommRing R
ζ : R
n : ℕ
x y : R
inst✝ : IsDomain R
hpos : 0 < n
h : IsPrimitiveRoot ζ n
K : Type u_1 := FractionRing R
⊢ (algebraMap R K) (x ^ n - y ^ n) = (algebraMap R K) (∏ ζ ∈ nthRootsFinset n R, (x - ζ * y))

Tactic:
rw [map_sub, map_pow, map_pow, map_prod]

Result:
case a
R : Type u_1
inst✝¹ : CommRing R
ζ : R
n : ℕ
x y : R
inst✝ : IsDomain R
hpos : 0 < n
h : IsPrimitiveRoot ζ n
K : Type u_1 := FractionRing R
⊢ (algebraMap R K) x ^ n - (algebraMap R K) y ^ n = ∏ x_1 ∈ nthRootsFinset n R, (algebraMap R K) (x - x_1 * y)

Proof state:
R : Type u_1
inst✝¹ : CommRing R
ζ : R
n : ℕ
x y : R
inst✝ : IsDomain R
hpos : 0 < n
h : IsPrimitiveRoot ζ n
⊢ x ^ n - y ^ n = ∏ ζ ∈ nthRootsFinset n R, (x - ζ * y)

Tactic:
let K := FractionRing R

Result:
R : Type u_1
inst✝¹ : CommRing R
ζ : R
n : ℕ
x y : R
inst✝ : IsDomain R
hpos : 0 < n
h : IsPrimitiveRoot ζ n
K : Type u_1 := FractionRing R
⊢ x ^ n - y ^ n = ∏ ζ ∈ nthRootsFinset n R, (x - ζ * y)

Proof state:
R : Type u_1
inst✝¹ : CommRing R
ζ : R
n : ℕ
x y : R
inst✝ : IsDomain R
hpos : 0 < n
h : IsPrimitiveRoot ζ n
K : Type u_1 := FractionRing R
⊢ x ^ n - y ^ n = ∏ ζ ∈ nthRootsFinset n R, (x - ζ * y)

Tactic:
apply FaithfulSMul.algebraMap_injective R K

Result:
case a
R : Type u_1
inst✝¹ : CommRing R
ζ : R
n : ℕ
x y : R
inst✝ : IsDomain R
hpos : 0 < n
h : IsPrimitiveRoot ζ n
K : Type u_1 := FractionRing R
⊢ (algebraMap R K) (x ^ n - y ^ n) = (algebraMap R K) (∏ ζ ∈ nthRootsFinset n R, (x - ζ * y))

Proof state:
case a
R : Type u_1
inst✝¹ : CommRing R
ζ : R
n : ℕ
x y : R
inst✝ : IsDomain R
hpos : 0 < n
h : IsPrimitiveRoot ζ n
K : Type u_1 := FractionRing R
h' : IsPrimitiveRoot ((algebraMap R K) ζ) n
a : K
ha : a ∈ ↑(nthRootsFinset n K)
this : ∀ b ∈ ↑(nthRootsFinset n K), ∃ a, ∃ (_ : a ∈ ↑(nthRootsFinset n R)), b = (algebraMap R K) a
⊢ a ∈ ⇑(algebraMap R K) '' ↑(nthRootsFinset n R)

Tactic:
obtain ⟨x, hx, hx1⟩ := this _ ha

Result:
case a.intro.intro
R : Type u_1
inst✝¹ : CommRing R
ζ : R
n : ℕ
x✝ y : R
inst✝ : IsDomain R
hpos : 0 < n
h : IsPrimitiveRoot ζ n
K : Type u_1 := FractionRing R
h' : IsPrimitiveRoot ((algebraMap R K) ζ) n
a : K
ha : a ∈ ↑(nthRootsFinset n K)
this : ∀ b ∈ ↑(nthRootsFinset n K), ∃ a, ∃ (_ : a ∈ ↑(nthRootsFinset n R)), b = (algebraMap R K) a
x : R
hx : x ∈ ↑(nthRootsFinset n R)
hx1 : a = (algebraMap R K) x
⊢ a ∈ ⇑(algebraMap R K) '' ↑(nthRootsFinset n R)

Proof state:
case a
R : Type u_1
inst✝¹ : CommRing R
ζ : R
n : ℕ
x y : R
inst✝ : IsDomain R
hpos : 0 < n
h : IsPrimitiveRoot ζ n
K : Type u_1 := FractionRing R
⊢ (algebraMap R K) x ^ n - (algebraMap R K) y ^ n = ∏ x_1 ∈ nthRootsFinset n R, (algebraMap R K) (x - x_1 * y)

Tactic:
simp_rw [map_sub, map_mul]

Result:
case a
R : Type u_1
inst✝¹ : CommRing R
ζ : R
n : ℕ
x y : R
inst✝ : IsDomain R
hpos : 0 < n
h : IsPrimitiveRoot ζ n
K : Type u_1 := FractionRing R
⊢ (algebraMap R K) x ^ n - (algebraMap R K) y ^ n =
    ∏ x_1 ∈ nthRootsFinset n R, ((algebraMap R K) x - (algebraMap R K) x_1 * (algebraMap R K) y)

Proof state:
case a
R : Type u_1
inst✝¹ : CommRing R
ζ : R
n : ℕ
x y : R
inst✝ : IsDomain R
hpos : 0 < n
h : IsPrimitiveRoot ζ n
K : Type u_1 := FractionRing R
⊢ (algebraMap R K) x ^ n - (algebraMap R K) y ^ n =
    ∏ x_1 ∈ nthRootsFinset n R, ((algebraMap R K) x - (algebraMap R K) x_1 * (algebraMap R K) y)

Tactic:
have h' : IsPrimitiveRoot (algebraMap R K ζ) n :=
  h.map_of_injective <| FaithfulSMul.algebraMap_injective R K

Result:
case a
R : Type u_1
inst✝¹ : CommRing R
ζ : R
n : ℕ
x y : R
inst✝ : IsDomain R
hpos : 0 < n
h : IsPrimitiveRoot ζ n
K : Type u_1 := FractionRing R
h' : IsPrimitiveRoot ((algebraMap R K) ζ) n
⊢ (algebraMap R K) x ^ n - (algebraMap R K) y ^ n =
    ∏ x_1 ∈ nthRootsFinset n R, ((algebraMap R K) x - (algebraMap R K) x_1 * (algebraMap R K) y)

Proof state:
R : Type u_1
inst✝¹ : CommRing R
ζ : R
n : ℕ
x y : R
inst✝ : IsDomain R
hpos : 0 < n
h : IsPrimitiveRoot ζ n
K : Type u_1 := FractionRing R
h' : IsPrimitiveRoot ((algebraMap R K) ζ) n
a : K
ha : a ∈ ↑(nthRootsFinset n K)
⊢ (↑(nthRootsFinset n K)).ncard ≤ (↑(nthRootsFinset n R)).ncard

Tactic:
simp [h.card_nthRootsFinset, h'.card_nthRootsFinset]

Result:
no goals

Proof state:
case a.intro.intro
R : Type u_1
inst✝¹ : CommRing R
ζ : R
n : ℕ
x✝ y : R
inst✝ : IsDomain R
hpos : 0 < n
h : IsPrimitiveRoot ζ n
K : Type u_1 := FractionRing R
h' : IsPrimitiveRoot ((algebraMap R K) ζ) n
a : K
ha : a ∈ ↑(nthRootsFinset n K)
this : ∀ b ∈ ↑(nthRootsFinset n K), ∃ a, ∃ (_ : a ∈ ↑(nthRootsFinset n R)), b = (algebraMap R K) a
x : R
hx : x ∈ ↑(nthRootsFinset n R)
hx1 : a = (algebraMap R K) x
⊢ a ∈ ⇑(algebraMap R K) '' ↑(nthRootsFinset n R)

Tactic:
exact ⟨x, hx, hx1.symm⟩

Result:
no goals

Proof state:
case a
R : Type u_1
inst✝¹ : CommRing R
ζ : R
n : ℕ
x y : R
inst✝ : IsDomain R
hpos : 0 < n
h : IsPrimitiveRoot ζ n
K : Type u_1 := FractionRing R
h' : IsPrimitiveRoot ((algebraMap R K) ζ) n
a : K
ha : a ∈ ↑(nthRootsFinset n K)
⊢ a ∈ ⇑(algebraMap R K) '' ↑(nthRootsFinset n R)

Tactic:
have := Set.surj_on_of_inj_on_of_ncard_le (s := nthRootsFinset n R)
  (t := nthRootsFinset n K) _ (fun _ hr ↦ map_mem_nthRootsFinset hr _)
  (fun a _ b _ H ↦ FaithfulSMul.algebraMap_injective R K H)
  (by simp [h.card_nthRootsFinset, h'.card_nthRootsFinset])

Result:
case a
R : Type u_1
inst✝¹ : CommRing R
ζ : R
n : ℕ
x y : R
inst✝ : IsDomain R
hpos : 0 < n
h : IsPrimitiveRoot ζ n
K : Type u_1 := FractionRing R
h' : IsPrimitiveRoot ((algebraMap R K) ζ) n
a : K
ha : a ∈ ↑(nthRootsFinset n K)
this : ∀ b ∈ ↑(nthRootsFinset n K), ∃ a, ∃ (_ : a ∈ ↑(nthRootsFinset n R)), b = (algebraMap R K) a
⊢ a ∈ ⇑(algebraMap R K) '' ↑(nthRootsFinset n R)