dsimp only at e
case neg.h
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁴ : Field K
inst✝³ : NumberField K
inst✝² : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
L : Type u_2
inst✝¹ : Field L
inst✝ : Algebra K L
α : L
e✝ : α ^ ↑p = (algebraMap K L) ((algebraMap (𝓞 K) K) ↑u)
hα : ¬α = 0
hζ' : (algebraMap K L) ζ - 1 ≠ 0
i : ℕ
hi : i ∈ ↑(Finset.range ↑p)
j : ℕ
hj : j ∈ ↑(Finset.range ↑p)
e :
  1 - (fun i => (1 - ζ ^ i • α) / (algebraMap K L) (ζ - 1)) i * ((algebraMap K L) ζ - 1) =
    1 - (fun i => (1 - ζ ^ i • α) / (algebraMap K L) (ζ - 1)) j * ((algebraMap K L) ζ - 1)
⊢ (fun x => (algebraMap K L) ζ ^ x * α) i = (fun x => (algebraMap K L) ζ ^ x * α) j
case neg.h
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁴ : Field K
inst✝³ : NumberField K
inst✝² : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
L : Type u_2
inst✝¹ : Field L
inst✝ : Algebra K L
α : L
e✝ : α ^ ↑p = (algebraMap K L) ((algebraMap (𝓞 K) K) ↑u)
hα : ¬α = 0
hζ' : (algebraMap K L) ζ - 1 ≠ 0
i : ℕ
hi : i ∈ ↑(Finset.range ↑p)
j : ℕ
hj : j ∈ ↑(Finset.range ↑p)
e :
  1 - (1 - ζ ^ i • α) / (algebraMap K L) (ζ - 1) * ((algebraMap K L) ζ - 1) =
    1 - (1 - ζ ^ j • α) / (algebraMap K L) (ζ - 1) * ((algebraMap K L) ζ - 1)
⊢ (fun x => (algebraMap K L) ζ ^ x * α) i = (fun x => (algebraMap K L) ζ ^ x * α) j