have hj : ↑j < (p : ℕ) - 1 := by
  by_contra! habs
  simp [le_antisymm habs (le_pred_of_lt (Fin.is_lt j))] at H
case neg
p : ℕ+
L : Type u
inst✝² : Field L
inst✝¹ : CharZero L
inst✝ : IsCyclotomicExtension {p} ℚ L
hp : (↑p).Prime
ζ : 𝓞 L
hζ : IsPrimitiveRoot ζ ↑p
f : Fin ↑p → ℤ
hf : ∃ i, f i = 0
m : ℤ
hdiv : ↑m ∣ ∑ j : Fin ↑p, f j • ζ ^ ↑j
ζ' : L := ↑ζ
this : Fact (↑p).Prime
hζ' : IsPrimitiveRoot ζ' ↑p
hcoe : ζ = ⟨ζ', ⋯⟩
hlast : (Fin.castOrderIso ⋯) (Fin.last (↑p).pred) = ⟨(↑p).pred, ⋯⟩
h : ∀ (x : Fin (↑p).pred), (Fin.castOrderIso ⋯) (Fin.castSuccEmb x) = ⟨↑x, ⋯⟩
b : PowerBasis ℤ (𝓞 L) := hζ'.integralPowerBasis'
hb : b = hζ'.integralPowerBasis'
hdim : b.dim = (↑p).pred
last_dvd : m ∣ f ⟨(↑p).pred, ⋯⟩
j : Fin ↑p
H : ¬j = ⟨↑p - 1, ⋯⟩
⊢ m ∣ f j
case neg
p : ℕ+
L : Type u
inst✝² : Field L
inst✝¹ : CharZero L
inst✝ : IsCyclotomicExtension {p} ℚ L
hp : (↑p).Prime
ζ : 𝓞 L
hζ : IsPrimitiveRoot ζ ↑p
f : Fin ↑p → ℤ
hf : ∃ i, f i = 0
m : ℤ
hdiv : ↑m ∣ ∑ j : Fin ↑p, f j • ζ ^ ↑j
ζ' : L := ↑ζ
this : Fact (↑p).Prime
hζ' : IsPrimitiveRoot ζ' ↑p
hcoe : ζ = ⟨ζ', ⋯⟩
hlast : (Fin.castOrderIso ⋯) (Fin.last (↑p).pred) = ⟨(↑p).pred, ⋯⟩
h : ∀ (x : Fin (↑p).pred), (Fin.castOrderIso ⋯) (Fin.castSuccEmb x) = ⟨↑x, ⋯⟩
b : PowerBasis ℤ (𝓞 L) := hζ'.integralPowerBasis'
hb : b = hζ'.integralPowerBasis'
hdim : b.dim = (↑p).pred
last_dvd : m ∣ f ⟨(↑p).pred, ⋯⟩
j : Fin ↑p
H : ¬j = ⟨↑p - 1, ⋯⟩
hj : ↑j < ↑p - 1
⊢ m ∣ f j