rw [h, associated_isUnit_mul_right_iff u.isUnit, ← associated_isUnit_mul_right_iff isUnit_one.neg,
  neg_one_mul, neg_sub]
case intro.intro.intro.intro.intro
n : ℕ+
K : Type u
L : Type v
A✝ : Type w
B : Type z
inst✝⁷ : CommRing A✝
inst✝⁶ : CommRing B
inst✝⁵ : Algebra A✝ B
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsDomain A
p : ℕ
hp : p.Prime
ζ : A
hζ : IsPrimitiveRoot ζ p
i : ℕ
hi : i < p
hη₁ : ζ ^ i ∈ nthRootsFinset p A
j : ℕ
hj : j < p
hη₂ : ζ ^ j ∈ nthRootsFinset p A
e : ζ ^ i ≠ ζ ^ j
this : i ≠ j
u : Aˣ
h : ζ ^ i - ζ ^ j = ↑u * (1 - ζ)
⊢ Associated (ζ - 1) (ζ ^ i - ζ ^ j)
case intro.intro.intro.intro.intro
n : ℕ+
K : Type u
L : Type v
A✝ : Type w
B : Type z
inst✝⁷ : CommRing A✝
inst✝⁶ : CommRing B
inst✝⁵ : Algebra A✝ B
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsDomain A
p : ℕ
hp : p.Prime
ζ : A
hζ : IsPrimitiveRoot ζ p
i : ℕ
hi : i < p
hη₁ : ζ ^ i ∈ nthRootsFinset p A
j : ℕ
hj : j < p
hη₂ : ζ ^ j ∈ nthRootsFinset p A
e : ζ ^ i ≠ ζ ^ j
this : i ≠ j
u : Aˣ
h : ζ ^ i - ζ ^ j = ↑u * (1 - ζ)
⊢ Associated (ζ - 1) (ζ - 1)