replace hy := congr_arg (b.basis.coord ((Fin.castOrderIso hdim.symm) ⟨j, hj⟩)) hy
case neg.intro
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 : ℤ
ζ' : 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
y : 𝓞 L
hy :
  ∑ x : Fin b.dim, f ((Fin.castOrderIso ⋯) ((Fin.castOrderIso hdim) x).castSucc) • b.basis x -
      ∑ x : Fin b.dim, f ⟨(↑p).pred, ⋯⟩ • b.basis x =
    ↑m * y
⊢ m ∣ f j
case neg.intro
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 : ℤ
ζ' : 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
y : 𝓞 L
hy :
  (b.basis.coord ((Fin.castOrderIso ⋯) ⟨↑j, hj⟩))
      (∑ x : Fin b.dim, f ((Fin.castOrderIso ⋯) ((Fin.castOrderIso hdim) x).castSucc) • b.basis x -
        ∑ x : Fin b.dim, f ⟨(↑p).pred, ⋯⟩ • b.basis x) =
    (b.basis.coord ((Fin.castOrderIso ⋯) ⟨↑j, hj⟩)) (↑m * y)
⊢ m ∣ f j