have hlast :
  (Fin.castOrderIso (succ_pred_prime hp.out)) (Fin.last (p : ℕ).pred) =
  ⟨(p : ℕ).pred, pred_lt hp.out.ne_zero⟩ := Fin.ext rfl
case intro
p : ℕ+
L : Type u
inst✝² : Field L
inst✝¹ : CharZero L
inst✝ : IsCyclotomicExtension {p} ℚ L
hp : Fact (↑p).Prime
ζ : 𝓞 L
hζ : IsPrimitiveRoot ζ ↑p
f : Fin ↑p → ℤ
m : ℤ
hdiv : ↑m ∣ ∑ j : Fin ↑p, f j • ζ ^ ↑j
i : Fin ↑p
Hi : f i = 0
⊢ m ∣ f ⟨(↑p).pred, ⋯⟩
case intro
p : ℕ+
L : Type u
inst✝² : Field L
inst✝¹ : CharZero L
inst✝ : IsCyclotomicExtension {p} ℚ L
hp : Fact (↑p).Prime
ζ : 𝓞 L
hζ : IsPrimitiveRoot ζ ↑p
f : Fin ↑p → ℤ
m : ℤ
hdiv : ↑m ∣ ∑ j : Fin ↑p, f j • ζ ^ ↑j
i : Fin ↑p
Hi : f i = 0
hlast : (Fin.castOrderIso ⋯) (Fin.last (↑p).pred) = ⟨(↑p).pred, ⋯⟩
⊢ m ∣ f ⟨(↑p).pred, ⋯⟩