Theorem: dvd_coeff_cycl_integer (FltRegular/NumberTheory/Cyclotomic/CyclRat.lean)

State before:
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
⊢ ∀ (j : Fin ↑p), m ∣ f j
Tactic:
let ζ' := (ζ : L)
State after:
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 := ↑ζ
⊢ ∀ (j : Fin ↑p), m ∣ f j

State before:
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 := ↑ζ
⊢ ∀ (j : Fin ↑p), m ∣ f j
Tactic:
have : Fact (p : ℕ).Prime := ⟨hp⟩
State after:
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
⊢ ∀ (j : Fin ↑p), m ∣ f j

State before:
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
⊢ ∀ (j : Fin ↑p), m ∣ f j
Tactic:
have hζ' : IsPrimitiveRoot ζ' p := IsPrimitiveRoot.coe_submonoidClass_iff.2 hζ
State after:
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
⊢ ∀ (j : Fin ↑p), m ∣ f j

State before:
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
⊢ ∀ (j : Fin ↑p), m ∣ f j
Tactic:
have hcoe : ζ = ⟨ζ', hζ'.isIntegral p.pos⟩ := by rfl
State after:
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 : ζ = ⟨ζ', ⋯⟩
⊢ ∀ (j : Fin ↑p), m ∣ f j

State before:
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 : ζ = ⟨ζ', ⋯⟩
⊢ ∀ (j : Fin ↑p), m ∣ f j
Tactic:
have hlast : (Fin.castOrderIso (succ_pred_prime hp)) (Fin.last (p : ℕ).pred) =
    ⟨(p : ℕ).pred, pred_lt hp.ne_zero⟩ := Fin.ext rfl
State after:
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, ⋯⟩
⊢ ∀ (j : Fin ↑p), m ∣ f j

State before:
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, ⋯⟩
⊢ ∀ (j : Fin ↑p), m ∣ f j
Tactic:
have h : ∀ x, (Fin.castOrderIso (succ_pred_prime hp)) (Fin.castSuccEmb x) =
  ⟨x, lt_trans x.2 (pred_lt hp.ne_zero)⟩ := fun x => Fin.ext rfl
State after:
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, ⋯⟩
⊢ ∀ (j : Fin ↑p), m ∣ f j

State before:
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, ⋯⟩
⊢ ∀ (j : Fin ↑p), m ∣ f j
Tactic:
set b := hζ'.integralPowerBasis' with hb
State after:
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'
⊢ ∀ (j : Fin ↑p), m ∣ f j

State before:
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'
⊢ ∀ (j : Fin ↑p), m ∣ f j
Tactic:
have hdim : b.dim = (p : ℕ).pred := by rw [hζ'.power_basis_int'_dim, totient_prime hp,
  pred_eq_sub_one]
State after:
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
⊢ ∀ (j : Fin ↑p), m ∣ f j

State before:
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
⊢ ∀ (j : Fin ↑p), m ∣ f j
Tactic:
have last_dvd := dvd_last_coeff_cycl_integer hζ hf hdiv
State after:
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), m ∣ f j

State before:
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), m ∣ f j
Tactic:
intro j
State after:
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
⊢ m ∣ f j

State before:
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
⊢ m ∣ f j
Tactic:
by_cases H : j = ⟨(p : ℕ) - 1, pred_lt hp.ne_zero⟩
State after:
case pos
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, ⋯⟩
⊢ m ∣ f j

State before:
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
Tactic:
have hj : ↑j < (p : ℕ) - 1 := by
  by_contra! habs
  simp [le_antisymm habs (le_pred_of_lt (Fin.is_lt j))] at H
State after:
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

State before:
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
Tactic:
obtain ⟨y, hy⟩ := hdiv
State after:
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 : ∑ j : Fin ↑p, f j • ζ ^ ↑j = ↑m * y
⊢ m ∣ f j

State before:
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 : ∑ j : Fin ↑p, f j • ζ ^ ↑j = ↑m * y
⊢ m ∣ f j
Tactic:
rw [← Equiv.sum_comp (Fin.castOrderIso (succ_pred_prime hp)).toEquiv, Fin.sum_univ_castSucc] at hy
State after:
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 :
  ∑ i : Fin (↑p).pred, f ((Fin.castOrderIso ⋯).toEquiv i.castSucc) • ζ ^ ↑((Fin.castOrderIso ⋯).toEquiv i.castSucc) +
      f ((Fin.castOrderIso ⋯).toEquiv (Fin.last (↑p).pred)) • ζ ^ ↑((Fin.castOrderIso ⋯).toEquiv (Fin.last (↑p).pred)) =
    ↑m * y
⊢ m ∣ f j

State before:
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 :
  ∑ i : Fin (↑p).pred, f ((Fin.castOrderIso ⋯).toEquiv i.castSucc) • ζ ^ ↑((Fin.castOrderIso ⋯).toEquiv i.castSucc) +
      f ((Fin.castOrderIso ⋯).toEquiv (Fin.last (↑p).pred)) • ζ ^ ↑((Fin.castOrderIso ⋯).toEquiv (Fin.last (↑p).pred)) =
    ↑m * y
⊢ m ∣ f j
Tactic:
simp only [hlast, h, RelIso.coe_fn_toEquiv, Fin.val_mk] at hy
State after:
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 (↑p).pred, f ((Fin.castOrderIso ⋯) x.castSucc) • ζ ^ ↑((Fin.castOrderIso ⋯) x.castSucc) +
      f ⟨(↑p).pred, ⋯⟩ • ζ ^ (↑p).pred =
    ↑m * y
⊢ m ∣ f j

State before:
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 (↑p).pred, f ((Fin.castOrderIso ⋯) x.castSucc) • ζ ^ ↑((Fin.castOrderIso ⋯) x.castSucc) +
      f ⟨(↑p).pred, ⋯⟩ • ζ ^ (↑p).pred =
    ↑m * y
⊢ m ∣ f j
Tactic:
rw [hζ.pow_sub_one_eq hp.one_lt, ← sum_neg_distrib, smul_sum, sum_range, ← sum_add_distrib,
  ← (Fin.castOrderIso hdim).toEquiv.sum_comp] at hy
State after:
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 :
  ∑ i : Fin b.dim,
      (f ((Fin.castOrderIso ⋯) ((Fin.castOrderIso hdim).toEquiv i).castSucc) •
          ζ ^ ↑((Fin.castOrderIso ⋯) ((Fin.castOrderIso hdim).toEquiv i).castSucc) +
        f ⟨(↑p).pred, ⋯⟩ • -ζ ^ ↑((Fin.castOrderIso hdim).toEquiv i)) =
    ↑m * y
⊢ m ∣ f j

State before:
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 :
  ∑ i : Fin b.dim,
      (f ((Fin.castOrderIso ⋯) ((Fin.castOrderIso hdim).toEquiv i).castSucc) •
          ζ ^ ↑((Fin.castOrderIso ⋯) ((Fin.castOrderIso hdim).toEquiv i).castSucc) +
        f ⟨(↑p).pred, ⋯⟩ • -ζ ^ ↑((Fin.castOrderIso hdim).toEquiv i)) =
    ↑m * y
⊢ m ∣ f j
Tactic:
simp only [RelIso.coe_fn_toEquiv, Fin.coe_cast, mul_neg, ← Subtype.coe_inj, Fin.coe_castSucc,
  Fin.coe_orderIso_apply] at hy
State after:
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) • ζ ^ ↑x + f ⟨(↑p).pred, ⋯⟩ • -ζ ^ ↑x) =
    ↑m * y
⊢ m ∣ f j

State before:
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) • ζ ^ ↑x + f ⟨(↑p).pred, ⋯⟩ • -ζ ^ ↑x) =
    ↑m * y
⊢ m ∣ f j
Tactic:
conv_lhs at hy =>
  congr; rfl; ext x
  rw [smul_neg]
  congr; congr; rfl; congr
  rw [hcoe, ← IsPrimitiveRoot.toInteger, ← hζ'.integralPowerBasis'_gen, ← hb]
  rfl; rfl; congr; congr; rfl; congr
  rw [hcoe, ← IsPrimitiveRoot.toInteger, ← hζ'.integralPowerBasis'_gen, ← hb]
State after:
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.gen ^ ↑x + -(f ⟨(↑p).pred, ⋯⟩ • b.gen ^ ↑x)) =
    ↑m * y
⊢ m ∣ f j

State before:
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.gen ^ ↑x + -(f ⟨(↑p).pred, ⋯⟩ • b.gen ^ ↑x)) =
    ↑m * y
⊢ m ∣ f j
Tactic:
conv_lhs at hy =>
  congr; rfl; ext x
  rw [← show ∀ y, _ = _ from fun y => congr_fun b.coe_basis y, ← sub_eq_add_neg]
State after:
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 - f ⟨(↑p).pred, ⋯⟩ • b.basis x) =
    ↑m * y
⊢ m ∣ f j

State before:
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 - f ⟨(↑p).pred, ⋯⟩ • b.basis x) =
    ↑m * y
⊢ m ∣ f j
Tactic:
rw [sum_sub_distrib] at hy
State after:
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

State before:
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
Tactic:
replace hy := congr_arg (b.basis.coord ((Fin.castOrderIso hdim.symm) ⟨j, hj⟩)) hy
State after:
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

State before:
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
Tactic:
rw [← b.basis.equivFun_symm_apply, ← b.basis.equivFun_symm_apply, LinearMap.map_sub,
  b.basis.coord_equivFun_symm, b.basis.coord_equivFun_symm] at hy
State after:
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 :
  f ((Fin.castOrderIso ⋯) ((Fin.castOrderIso hdim) ((Fin.castOrderIso ⋯) ⟨↑j, hj⟩)).castSucc) - f ⟨(↑p).pred, ⋯⟩ =
    (b.basis.coord ((Fin.castOrderIso ⋯) ⟨↑j, hj⟩)) (↑m * y)
⊢ m ∣ f j

State before:
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 :
  f ((Fin.castOrderIso ⋯) ((Fin.castOrderIso hdim) ((Fin.castOrderIso ⋯) ⟨↑j, hj⟩)).castSucc) - f ⟨(↑p).pred, ⋯⟩ =
    (b.basis.coord ((Fin.castOrderIso ⋯) ⟨↑j, hj⟩)) (↑m * y)
⊢ m ∣ f j
Tactic:
simp only [Fin.castOrderIso_apply, Fin.cast_mk, Fin.castSucc_mk, Fin.eta, Basis.coord_apply,
  sub_eq_iff_eq_add] at hy
State after:
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 : f j = (b.basis.repr (↑m * y)) ⟨↑j, ⋯⟩ + f ⟨(↑p).pred, ⋯⟩
⊢ m ∣ f j

State before:
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 : f j = (b.basis.repr (↑m * y)) ⟨↑j, ⋯⟩ + f ⟨(↑p).pred, ⋯⟩
⊢ m ∣ f j
Tactic:
obtain ⟨n, hn⟩ := b.basis.dvd_coord_smul ((Fin.cast hdim.symm) ⟨j, hj⟩) y m
State after:
case neg.intro.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 : f j = (b.basis.repr (↑m * y)) ⟨↑j, ⋯⟩ + f ⟨(↑p).pred, ⋯⟩
n : ℤ
hn : (b.basis.coord (Fin.cast ⋯ ⟨↑j, hj⟩)) (m • y) = m * n
⊢ m ∣ f j

State before:
case neg.intro.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 : f j = (b.basis.repr (↑m * y)) ⟨↑j, ⋯⟩ + f ⟨(↑p).pred, ⋯⟩
n : ℤ
hn : (b.basis.coord (Fin.cast ⋯ ⟨↑j, hj⟩)) (m • y) = m * n
⊢ m ∣ f j
Tactic:
rw [hy, ← smul_eq_mul, ← zsmul_eq_smul_cast, ← b.basis.coord_apply, ← Fin.cast_mk, hn]
State after:
case neg.intro.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 : f j = (b.basis.repr (↑m * y)) ⟨↑j, ⋯⟩ + f ⟨(↑p).pred, ⋯⟩
n : ℤ
hn : (b.basis.coord (Fin.cast ⋯ ⟨↑j, hj⟩)) (m • y) = m * n
⊢ m ∣ m * n + f ⟨(↑p).pred, ⋯⟩

State before:
case neg.intro.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 : f j = (b.basis.repr (↑m * y)) ⟨↑j, ⋯⟩ + f ⟨(↑p).pred, ⋯⟩
n : ℤ
hn : (b.basis.coord (Fin.cast ⋯ ⟨↑j, hj⟩)) (m • y) = m * n
⊢ m ∣ m * n + f ⟨(↑p).pred, ⋯⟩
Tactic:
exact dvd_add (dvd_mul_right _ _) last_dvd
State after:
no goals

State before:
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
⊢ ζ = ⟨ζ', ⋯⟩
Tactic:
rfl
State after:
no goals

State before:
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'
⊢ b.dim = (↑p).pred
Tactic:
rw [hζ'.power_basis_int'_dim, totient_prime hp,
pred_eq_sub_one]
State after:
no goals

State before:
case pos
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
Tactic:
simpa [H] using last_dvd
State after:
no goals

State before:
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, ⋯⟩
⊢ ↑j < ↑p - 1
Tactic:
by_contra! habs
State after:
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, ⋯⟩
habs : ↑p - 1 ≤ ↑j
⊢ False

State before:
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, ⋯⟩
habs : ↑p - 1 ≤ ↑j
⊢ False
Tactic:
simp [le_antisymm habs (le_pred_of_lt (Fin.is_lt j))] at H
State after:
no goals