Theorem: zeta_sub_one_pow_dvd_norm_sub_pow (FltRegular/NumberTheory/Cyclotomic/MoreLemmas.lean)

State before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
x : 𝓞 K
⊢ (↑hζ.unit' - 1) ^ ↑p ∣ ↑((Algebra.norm ℤ) (1 + ↑p • x)) - 1 + ↑p • x
Tactic:
letI := IsCyclotomicExtension.numberField {p} ℚ K
State after:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
x : 𝓞 K
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
⊢ (↑hζ.unit' - 1) ^ ↑p ∣ ↑((Algebra.norm ℤ) (1 + ↑p • x)) - 1 + ↑p • x

State before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
x : 𝓞 K
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
⊢ (↑hζ.unit' - 1) ^ ↑p ∣ ↑((Algebra.norm ℤ) (1 + ↑p • x)) - 1 + ↑p • x
Tactic:
obtain ⟨r, hr⟩ := Algebra.norm_one_add_smul (p : ℤ) x
State after:
case intro
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
x : 𝓞 K
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
r : ℤ
hr : (Algebra.norm ℤ) (1 + ↑↑p • x) = 1 + (Algebra.trace ℤ (𝓞 K)) x * ↑↑p + r * ↑↑p ^ 2
⊢ (↑hζ.unit' - 1) ^ ↑p ∣ ↑((Algebra.norm ℤ) (1 + ↑p • x)) - 1 + ↑p • x

State before:
case intro
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
x : 𝓞 K
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
r : ℤ
hr : (Algebra.norm ℤ) (1 + ↑↑p • x) = 1 + (Algebra.trace ℤ (𝓞 K)) x * ↑↑p + r * ↑↑p ^ 2
⊢ (↑hζ.unit' - 1) ^ ↑p ∣ ↑((Algebra.norm ℤ) (1 + ↑p • x)) - 1 + ↑p • x
Tactic:
obtain ⟨s, hs⟩ := zeta_sub_one_dvd_trace_sub_smul hζ x
State after:
case intro.intro
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
x : 𝓞 K
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
r : ℤ
hr : (Algebra.norm ℤ) (1 + ↑↑p • x) = 1 + (Algebra.trace ℤ (𝓞 K)) x * ↑↑p + r * ↑↑p ^ 2
s : 𝓞 K
hs : ↑((Algebra.trace ℤ (𝓞 K)) x) - (↑p - 1) • x = (↑hζ.unit' - 1) * s
⊢ (↑hζ.unit' - 1) ^ ↑p ∣ ↑((Algebra.norm ℤ) (1 + ↑p • x)) - 1 + ↑p • x

State before:
case intro.intro
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
x : 𝓞 K
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
r : ℤ
hr : (Algebra.norm ℤ) (1 + ↑↑p • x) = 1 + (Algebra.trace ℤ (𝓞 K)) x * ↑↑p + r * ↑↑p ^ 2
s : 𝓞 K
hs : ↑((Algebra.trace ℤ (𝓞 K)) x) - (↑p - 1) • x = (↑hζ.unit' - 1) * s
⊢ (↑hζ.unit' - 1) ^ ↑p ∣ ↑((Algebra.norm ℤ) (1 + ↑p • x)) - 1 + ↑p • x
Tactic:
obtain ⟨t, ht⟩ := (associated_zeta_sub_one_pow_prime hζ).dvd
State after:
case intro.intro.intro
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
x : 𝓞 K
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
r : ℤ
hr : (Algebra.norm ℤ) (1 + ↑↑p • x) = 1 + (Algebra.trace ℤ (𝓞 K)) x * ↑↑p + r * ↑↑p ^ 2
s : 𝓞 K
hs : ↑((Algebra.trace ℤ (𝓞 K)) x) - (↑p - 1) • x = (↑hζ.unit' - 1) * s
t : 𝓞 K
ht : ↑↑p = (↑hζ.unit' - 1) ^ (↑p - 1) * t
⊢ (↑hζ.unit' - 1) ^ ↑p ∣ ↑((Algebra.norm ℤ) (1 + ↑p • x)) - 1 + ↑p • x

State before:
case intro.intro.intro
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
x : 𝓞 K
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
r : ℤ
hr : (Algebra.norm ℤ) (1 + ↑↑p • x) = 1 + (Algebra.trace ℤ (𝓞 K)) x * ↑↑p + r * ↑↑p ^ 2
s : 𝓞 K
hs : ↑((Algebra.trace ℤ (𝓞 K)) x) - (↑p - 1) • x = (↑hζ.unit' - 1) * s
t : 𝓞 K
ht : ↑↑p = (↑hζ.unit' - 1) ^ (↑p - 1) * t
⊢ (↑hζ.unit' - 1) ^ ↑p ∣ ↑((Algebra.norm ℤ) (1 + ↑p • x)) - 1 + ↑p • x
Tactic:
rw [sub_eq_iff_eq_add] at hs
State after:
case intro.intro.intro
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
x : 𝓞 K
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
r : ℤ
hr : (Algebra.norm ℤ) (1 + ↑↑p • x) = 1 + (Algebra.trace ℤ (𝓞 K)) x * ↑↑p + r * ↑↑p ^ 2
s : 𝓞 K
hs : ↑((Algebra.trace ℤ (𝓞 K)) x) = (↑hζ.unit' - 1) * s + (↑p - 1) • x
t : 𝓞 K
ht : ↑↑p = (↑hζ.unit' - 1) ^ (↑p - 1) * t
⊢ (↑hζ.unit' - 1) ^ ↑p ∣ ↑((Algebra.norm ℤ) (1 + ↑p • x)) - 1 + ↑p • x

State before:
case intro.intro.intro
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
x : 𝓞 K
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
r : ℤ
hr : (Algebra.norm ℤ) (1 + ↑↑p • x) = 1 + (Algebra.trace ℤ (𝓞 K)) x * ↑↑p + r * ↑↑p ^ 2
s : 𝓞 K
hs : ↑((Algebra.trace ℤ (𝓞 K)) x) = (↑hζ.unit' - 1) * s + (↑p - 1) • x
t : 𝓞 K
ht : ↑↑p = (↑hζ.unit' - 1) ^ (↑p - 1) * t
⊢ (↑hζ.unit' - 1) ^ ↑p ∣ ↑((Algebra.norm ℤ) (1 + ↑p • x)) - 1 + ↑p • x
Tactic:
simp only [zsmul_eq_mul, Int.cast_natCast] at hr
State after:
case intro.intro.intro
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
x : 𝓞 K
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
r : ℤ
s : 𝓞 K
hs : ↑((Algebra.trace ℤ (𝓞 K)) x) = (↑hζ.unit' - 1) * s + (↑p - 1) • x
t : 𝓞 K
ht : ↑↑p = (↑hζ.unit' - 1) ^ (↑p - 1) * t
hr : (Algebra.norm ℤ) (1 + ↑↑p * x) = 1 + (Algebra.trace ℤ (𝓞 K)) x * ↑↑p + r * ↑↑p ^ 2
⊢ (↑hζ.unit' - 1) ^ ↑p ∣ ↑((Algebra.norm ℤ) (1 + ↑p • x)) - 1 + ↑p • x

State before:
case intro.intro.intro
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
x : 𝓞 K
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
r : ℤ
s : 𝓞 K
hs : ↑((Algebra.trace ℤ (𝓞 K)) x) = (↑hζ.unit' - 1) * s + (↑p - 1) • x
t : 𝓞 K
ht : ↑↑p = (↑hζ.unit' - 1) ^ (↑p - 1) * t
hr : (Algebra.norm ℤ) (1 + ↑↑p * x) = 1 + (Algebra.trace ℤ (𝓞 K)) x * ↑↑p + r * ↑↑p ^ 2
⊢ (↑hζ.unit' - 1) ^ ↑p ∣ ↑((Algebra.norm ℤ) (1 + ↑p • x)) - 1 + ↑p • x
Tactic:
simp only [nsmul_eq_mul, hr, Int.cast_add, Int.cast_one, Int.cast_mul, hs, ge_iff_le, PNat.pos,
  Nat.cast_pred, Int.cast_pow, Nat.cast_mul, ne_eq, PNat.ne_zero, Int.cast_natCast,
  not_false_eq_true, isUnit_pow_iff]
State after:
case intro.intro.intro
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
x : 𝓞 K
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
r : ℤ
s : 𝓞 K
hs : ↑((Algebra.trace ℤ (𝓞 K)) x) = (↑hζ.unit' - 1) * s + (↑p - 1) • x
t : 𝓞 K
ht : ↑↑p = (↑hζ.unit' - 1) ^ (↑p - 1) * t
hr : (Algebra.norm ℤ) (1 + ↑↑p * x) = 1 + (Algebra.trace ℤ (𝓞 K)) x * ↑↑p + r * ↑↑p ^ 2
⊢ (↑hζ.unit' - 1) ^ ↑p ∣ 1 + ((↑hζ.unit' - 1) * s + (↑↑p - 1) * x) * ↑↑p + ↑r * ↑↑p ^ 2 - 1 + ↑↑p * x

State before:
case intro.intro.intro
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
x : 𝓞 K
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
r : ℤ
s : 𝓞 K
hs : ↑((Algebra.trace ℤ (𝓞 K)) x) = (↑hζ.unit' - 1) * s + (↑p - 1) • x
t : 𝓞 K
ht : ↑↑p = (↑hζ.unit' - 1) ^ (↑p - 1) * t
hr : (Algebra.norm ℤ) (1 + ↑↑p * x) = 1 + (Algebra.trace ℤ (𝓞 K)) x * ↑↑p + r * ↑↑p ^ 2
⊢ (↑hζ.unit' - 1) ^ ↑p ∣ 1 + ((↑hζ.unit' - 1) * s + (↑↑p - 1) * x) * ↑↑p + ↑r * ↑↑p ^ 2 - 1 + ↑↑p * x
Tactic:
suffices (hζ.unit' - 1 : 𝓞 K) ^ (p : ℕ) ∣ (hζ.unit' - 1) * p * s + (p : 𝓞 K) ^ 2 * (r + x) by
  convert this using 1; ring
State after:
case intro.intro.intro
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
x : 𝓞 K
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
r : ℤ
s : 𝓞 K
hs : ↑((Algebra.trace ℤ (𝓞 K)) x) = (↑hζ.unit' - 1) * s + (↑p - 1) • x
t : 𝓞 K
ht : ↑↑p = (↑hζ.unit' - 1) ^ (↑p - 1) * t
hr : (Algebra.norm ℤ) (1 + ↑↑p * x) = 1 + (Algebra.trace ℤ (𝓞 K)) x * ↑↑p + r * ↑↑p ^ 2
⊢ (↑hζ.unit' - 1) ^ ↑p ∣ (↑hζ.unit' - 1) * ↑↑p * s + ↑↑p ^ 2 * (↑r + x)

State before:
case intro.intro.intro
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
x : 𝓞 K
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
r : ℤ
s : 𝓞 K
hs : ↑((Algebra.trace ℤ (𝓞 K)) x) = (↑hζ.unit' - 1) * s + (↑p - 1) • x
t : 𝓞 K
ht : ↑↑p = (↑hζ.unit' - 1) ^ (↑p - 1) * t
hr : (Algebra.norm ℤ) (1 + ↑↑p * x) = 1 + (Algebra.trace ℤ (𝓞 K)) x * ↑↑p + r * ↑↑p ^ 2
⊢ (↑hζ.unit' - 1) ^ ↑p ∣ (↑hζ.unit' - 1) * ↑↑p * s + ↑↑p ^ 2 * (↑r + x)
Tactic:
apply dvd_add
State after:
case intro.intro.intro.h₁
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
x : 𝓞 K
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
r : ℤ
s : 𝓞 K
hs : ↑((Algebra.trace ℤ (𝓞 K)) x) = (↑hζ.unit' - 1) * s + (↑p - 1) • x
t : 𝓞 K
ht : ↑↑p = (↑hζ.unit' - 1) ^ (↑p - 1) * t
hr : (Algebra.norm ℤ) (1 + ↑↑p * x) = 1 + (Algebra.trace ℤ (𝓞 K)) x * ↑↑p + r * ↑↑p ^ 2
⊢ (↑hζ.unit' - 1) ^ ↑p ∣ (↑hζ.unit' - 1) * ↑↑p * s

case intro.intro.intro.h₂
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
x : 𝓞 K
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
r : ℤ
s : 𝓞 K
hs : ↑((Algebra.trace ℤ (𝓞 K)) x) = (↑hζ.unit' - 1) * s + (↑p - 1) • x
t : 𝓞 K
ht : ↑↑p = (↑hζ.unit' - 1) ^ (↑p - 1) * t
hr : (Algebra.norm ℤ) (1 + ↑↑p * x) = 1 + (Algebra.trace ℤ (𝓞 K)) x * ↑↑p + r * ↑↑p ^ 2
⊢ (↑hζ.unit' - 1) ^ ↑p ∣ ↑↑p ^ 2 * (↑r + x)

State before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
x : 𝓞 K
this✝ : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
r : ℤ
s : 𝓞 K
hs : ↑((Algebra.trace ℤ (𝓞 K)) x) = (↑hζ.unit' - 1) * s + (↑p - 1) • x
t : 𝓞 K
ht : ↑↑p = (↑hζ.unit' - 1) ^ (↑p - 1) * t
hr : (Algebra.norm ℤ) (1 + ↑↑p * x) = 1 + (Algebra.trace ℤ (𝓞 K)) x * ↑↑p + r * ↑↑p ^ 2
this : (↑hζ.unit' - 1) ^ ↑p ∣ (↑hζ.unit' - 1) * ↑↑p * s + ↑↑p ^ 2 * (↑r + x)
⊢ (↑hζ.unit' - 1) ^ ↑p ∣ 1 + ((↑hζ.unit' - 1) * s + (↑↑p - 1) * x) * ↑↑p + ↑r * ↑↑p ^ 2 - 1 + ↑↑p * x
Tactic:
convert this using 1
State after:
case h.e'_4
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
x : 𝓞 K
this✝ : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
r : ℤ
s : 𝓞 K
hs : ↑((Algebra.trace ℤ (𝓞 K)) x) = (↑hζ.unit' - 1) * s + (↑p - 1) • x
t : 𝓞 K
ht : ↑↑p = (↑hζ.unit' - 1) ^ (↑p - 1) * t
hr : (Algebra.norm ℤ) (1 + ↑↑p * x) = 1 + (Algebra.trace ℤ (𝓞 K)) x * ↑↑p + r * ↑↑p ^ 2
this : (↑hζ.unit' - 1) ^ ↑p ∣ (↑hζ.unit' - 1) * ↑↑p * s + ↑↑p ^ 2 * (↑r + x)
⊢ 1 + ((↑hζ.unit' - 1) * s + (↑↑p - 1) * x) * ↑↑p + ↑r * ↑↑p ^ 2 - 1 + ↑↑p * x =
    (↑hζ.unit' - 1) * ↑↑p * s + ↑↑p ^ 2 * (↑r + x)

State before:
case h.e'_4
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
x : 𝓞 K
this✝ : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
r : ℤ
s : 𝓞 K
hs : ↑((Algebra.trace ℤ (𝓞 K)) x) = (↑hζ.unit' - 1) * s + (↑p - 1) • x
t : 𝓞 K
ht : ↑↑p = (↑hζ.unit' - 1) ^ (↑p - 1) * t
hr : (Algebra.norm ℤ) (1 + ↑↑p * x) = 1 + (Algebra.trace ℤ (𝓞 K)) x * ↑↑p + r * ↑↑p ^ 2
this : (↑hζ.unit' - 1) ^ ↑p ∣ (↑hζ.unit' - 1) * ↑↑p * s + ↑↑p ^ 2 * (↑r + x)
⊢ 1 + ((↑hζ.unit' - 1) * s + (↑↑p - 1) * x) * ↑↑p + ↑r * ↑↑p ^ 2 - 1 + ↑↑p * x =
    (↑hζ.unit' - 1) * ↑↑p * s + ↑↑p ^ 2 * (↑r + x)
Tactic:
ring
State after:
no goals

State before:
case intro.intro.intro.h₁
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
x : 𝓞 K
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
r : ℤ
s : 𝓞 K
hs : ↑((Algebra.trace ℤ (𝓞 K)) x) = (↑hζ.unit' - 1) * s + (↑p - 1) • x
t : 𝓞 K
ht : ↑↑p = (↑hζ.unit' - 1) ^ (↑p - 1) * t
hr : (Algebra.norm ℤ) (1 + ↑↑p * x) = 1 + (Algebra.trace ℤ (𝓞 K)) x * ↑↑p + r * ↑↑p ^ 2
⊢ (↑hζ.unit' - 1) ^ ↑p ∣ (↑hζ.unit' - 1) * ↑↑p * s
Tactic:
apply dvd_mul_of_dvd_left
State after:
case intro.intro.intro.h₁.h
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
x : 𝓞 K
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
r : ℤ
s : 𝓞 K
hs : ↑((Algebra.trace ℤ (𝓞 K)) x) = (↑hζ.unit' - 1) * s + (↑p - 1) • x
t : 𝓞 K
ht : ↑↑p = (↑hζ.unit' - 1) ^ (↑p - 1) * t
hr : (Algebra.norm ℤ) (1 + ↑↑p * x) = 1 + (Algebra.trace ℤ (𝓞 K)) x * ↑↑p + r * ↑↑p ^ 2
⊢ (↑hζ.unit' - 1) ^ ↑p ∣ (↑hζ.unit' - 1) * ↑↑p

State before:
case intro.intro.intro.h₁.h
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
x : 𝓞 K
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
r : ℤ
s : 𝓞 K
hs : ↑((Algebra.trace ℤ (𝓞 K)) x) = (↑hζ.unit' - 1) * s + (↑p - 1) • x
t : 𝓞 K
ht : ↑↑p = (↑hζ.unit' - 1) ^ (↑p - 1) * t
hr : (Algebra.norm ℤ) (1 + ↑↑p * x) = 1 + (Algebra.trace ℤ (𝓞 K)) x * ↑↑p + r * ↑↑p ^ 2
⊢ (↑hζ.unit' - 1) ^ ↑p ∣ (↑hζ.unit' - 1) * ↑↑p
Tactic:
rw [ht, ← mul_assoc, ← pow_succ', tsub_add_cancel_of_le (Nat.Prime.one_lt hpri.out).le]
State after:
case intro.intro.intro.h₁.h
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
x : 𝓞 K
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
r : ℤ
s : 𝓞 K
hs : ↑((Algebra.trace ℤ (𝓞 K)) x) = (↑hζ.unit' - 1) * s + (↑p - 1) • x
t : 𝓞 K
ht : ↑↑p = (↑hζ.unit' - 1) ^ (↑p - 1) * t
hr : (Algebra.norm ℤ) (1 + ↑↑p * x) = 1 + (Algebra.trace ℤ (𝓞 K)) x * ↑↑p + r * ↑↑p ^ 2
⊢ (↑hζ.unit' - 1) ^ ↑p ∣ (↑hζ.unit' - 1) ^ ↑p * t

State before:
case intro.intro.intro.h₁.h
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
x : 𝓞 K
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
r : ℤ
s : 𝓞 K
hs : ↑((Algebra.trace ℤ (𝓞 K)) x) = (↑hζ.unit' - 1) * s + (↑p - 1) • x
t : 𝓞 K
ht : ↑↑p = (↑hζ.unit' - 1) ^ (↑p - 1) * t
hr : (Algebra.norm ℤ) (1 + ↑↑p * x) = 1 + (Algebra.trace ℤ (𝓞 K)) x * ↑↑p + r * ↑↑p ^ 2
⊢ (↑hζ.unit' - 1) ^ ↑p ∣ (↑hζ.unit' - 1) ^ ↑p * t
Tactic:
exact dvd_mul_right _ _
State after:
no goals

State before:
case intro.intro.intro.h₂
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
x : 𝓞 K
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
r : ℤ
s : 𝓞 K
hs : ↑((Algebra.trace ℤ (𝓞 K)) x) = (↑hζ.unit' - 1) * s + (↑p - 1) • x
t : 𝓞 K
ht : ↑↑p = (↑hζ.unit' - 1) ^ (↑p - 1) * t
hr : (Algebra.norm ℤ) (1 + ↑↑p * x) = 1 + (Algebra.trace ℤ (𝓞 K)) x * ↑↑p + r * ↑↑p ^ 2
⊢ (↑hζ.unit' - 1) ^ ↑p ∣ ↑↑p ^ 2 * (↑r + x)
Tactic:
rw [ht, mul_pow, ← pow_mul, mul_assoc]
State after:
case intro.intro.intro.h₂
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
x : 𝓞 K
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
r : ℤ
s : 𝓞 K
hs : ↑((Algebra.trace ℤ (𝓞 K)) x) = (↑hζ.unit' - 1) * s + (↑p - 1) • x
t : 𝓞 K
ht : ↑↑p = (↑hζ.unit' - 1) ^ (↑p - 1) * t
hr : (Algebra.norm ℤ) (1 + ↑↑p * x) = 1 + (Algebra.trace ℤ (𝓞 K)) x * ↑↑p + r * ↑↑p ^ 2
⊢ (↑hζ.unit' - 1) ^ ↑p ∣ (↑hζ.unit' - 1) ^ ((↑p - 1) * 2) * (t ^ 2 * (↑r + x))

State before:
case intro.intro.intro.h₂
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
x : 𝓞 K
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
r : ℤ
s : 𝓞 K
hs : ↑((Algebra.trace ℤ (𝓞 K)) x) = (↑hζ.unit' - 1) * s + (↑p - 1) • x
t : 𝓞 K
ht : ↑↑p = (↑hζ.unit' - 1) ^ (↑p - 1) * t
hr : (Algebra.norm ℤ) (1 + ↑↑p * x) = 1 + (Algebra.trace ℤ (𝓞 K)) x * ↑↑p + r * ↑↑p ^ 2
⊢ (↑hζ.unit' - 1) ^ ↑p ∣ (↑hζ.unit' - 1) ^ ((↑p - 1) * 2) * (t ^ 2 * (↑r + x))
Tactic:
apply dvd_mul_of_dvd_left
State after:
case intro.intro.intro.h₂.h
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
x : 𝓞 K
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
r : ℤ
s : 𝓞 K
hs : ↑((Algebra.trace ℤ (𝓞 K)) x) = (↑hζ.unit' - 1) * s + (↑p - 1) • x
t : 𝓞 K
ht : ↑↑p = (↑hζ.unit' - 1) ^ (↑p - 1) * t
hr : (Algebra.norm ℤ) (1 + ↑↑p * x) = 1 + (Algebra.trace ℤ (𝓞 K)) x * ↑↑p + r * ↑↑p ^ 2
⊢ (↑hζ.unit' - 1) ^ ↑p ∣ (↑hζ.unit' - 1) ^ ((↑p - 1) * 2)

State before:
case intro.intro.intro.h₂.h
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
x : 𝓞 K
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
r : ℤ
s : 𝓞 K
hs : ↑((Algebra.trace ℤ (𝓞 K)) x) = (↑hζ.unit' - 1) * s + (↑p - 1) • x
t : 𝓞 K
ht : ↑↑p = (↑hζ.unit' - 1) ^ (↑p - 1) * t
hr : (Algebra.norm ℤ) (1 + ↑↑p * x) = 1 + (Algebra.trace ℤ (𝓞 K)) x * ↑↑p + r * ↑↑p ^ 2
⊢ (↑hζ.unit' - 1) ^ ↑p ∣ (↑hζ.unit' - 1) ^ ((↑p - 1) * 2)
Tactic:
apply pow_dvd_pow
State after:
case intro.intro.intro.h₂.h.h
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
x : 𝓞 K
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
r : ℤ
s : 𝓞 K
hs : ↑((Algebra.trace ℤ (𝓞 K)) x) = (↑hζ.unit' - 1) * s + (↑p - 1) • x
t : 𝓞 K
ht : ↑↑p = (↑hζ.unit' - 1) ^ (↑p - 1) * t
hr : (Algebra.norm ℤ) (1 + ↑↑p * x) = 1 + (Algebra.trace ℤ (𝓞 K)) x * ↑↑p + r * ↑↑p ^ 2
⊢ ↑p ≤ (↑p - 1) * 2

State before:
case intro.intro.intro.h₂.h.h
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
x : 𝓞 K
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
r : ℤ
s : 𝓞 K
hs : ↑((Algebra.trace ℤ (𝓞 K)) x) = (↑hζ.unit' - 1) * s + (↑p - 1) • x
t : 𝓞 K
ht : ↑↑p = (↑hζ.unit' - 1) ^ (↑p - 1) * t
hr : (Algebra.norm ℤ) (1 + ↑↑p * x) = 1 + (Algebra.trace ℤ (𝓞 K)) x * ↑↑p + r * ↑↑p ^ 2
⊢ ↑p ≤ (↑p - 1) * 2
Tactic:
zify [(Nat.Prime.one_lt hpri.out).le]
State after:
case intro.intro.intro.h₂.h.h
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
x : 𝓞 K
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
r : ℤ
s : 𝓞 K
hs : ↑((Algebra.trace ℤ (𝓞 K)) x) = (↑hζ.unit' - 1) * s + (↑p - 1) • x
t : 𝓞 K
ht : ↑↑p = (↑hζ.unit' - 1) ^ (↑p - 1) * t
hr : (Algebra.norm ℤ) (1 + ↑↑p * x) = 1 + (Algebra.trace ℤ (𝓞 K)) x * ↑↑p + r * ↑↑p ^ 2
⊢ ↑↑p ≤ (↑↑p - 1) * 2

State before:
case intro.intro.intro.h₂.h.h
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
x : 𝓞 K
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
r : ℤ
s : 𝓞 K
hs : ↑((Algebra.trace ℤ (𝓞 K)) x) = (↑hζ.unit' - 1) * s + (↑p - 1) • x
t : 𝓞 K
ht : ↑↑p = (↑hζ.unit' - 1) ^ (↑p - 1) * t
hr : (Algebra.norm ℤ) (1 + ↑↑p * x) = 1 + (Algebra.trace ℤ (𝓞 K)) x * ↑↑p + r * ↑↑p ^ 2
⊢ ↑↑p ≤ (↑↑p - 1) * 2
Tactic:
linarith only [Nat.Prime.two_le hpri.out]
State after:
no goals