Theorem: norm_add_one_smul_of_isUnit (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
K : Type u_2
inst✝¹ : Field K
inst✝ : NumberField K
p : ℕ
hpri : p.Prime
hp : p ≠ 2
x : 𝓞 K
hx : IsUnit (1 + p • x)
⊢ (Algebra.norm ℤ) (1 + p • x) = 1
Tactic:
have H : Algebra.norm ℤ (1 + (p : ℕ) • x) = 1 ∨ Algebra.norm ℤ (1 + (p : ℕ) • x) = -1 := by
  apply Int.natAbs_eq_iff.mp
  apply (Int.cast_injective (α := ℚ)).comp Nat.cast_injective
  simp only [Int.cast_abs, Function.comp_apply, Nat.cast_one, Int.cast_one, ← Int.abs_eq_natAbs,
    Algebra.coe_norm_int, ← NumberField.isUnit_iff_norm.mp hx, RingOfIntegers.coe_norm]
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
K : Type u_2
inst✝¹ : Field K
inst✝ : NumberField K
p : ℕ
hpri : p.Prime
hp : p ≠ 2
x : 𝓞 K
hx : IsUnit (1 + p • x)
H : (Algebra.norm ℤ) (1 + p • x) = 1 ∨ (Algebra.norm ℤ) (1 + p • x) = -1
⊢ (Algebra.norm ℤ) (1 + p • x) = 1

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
K : Type u_2
inst✝¹ : Field K
inst✝ : NumberField K
p : ℕ
hpri : p.Prime
hp : p ≠ 2
x : 𝓞 K
hx : IsUnit (1 + p • x)
H : (Algebra.norm ℤ) (1 + p • x) = 1 ∨ (Algebra.norm ℤ) (1 + p • x) = -1
⊢ (Algebra.norm ℤ) (1 + p • x) = 1
Tactic:
have : Algebra.norm ℤ (1 + (p : ℕ) • x) ≠ -1 := by
  intro e; apply hp
  obtain ⟨r, hr⟩ := Algebra.norm_one_add_smul (p : ℤ) x
  have : (p : ℤ) * (- Algebra.trace ℤ _ x - r * p) = 2 := by
    rw [zsmul_eq_mul, Int.cast_natCast, ← nsmul_eq_mul, e, eq_comm, ← sub_eq_zero] at hr
    rw [eq_comm, ← sub_eq_zero, ← hr]
    ring
  exact (Nat.prime_two.eq_one_or_self_of_dvd _
    (Int.natCast_dvd_natCast.mp ⟨_, this.symm⟩)).resolve_left hpri.ne_one
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
K : Type u_2
inst✝¹ : Field K
inst✝ : NumberField K
p : ℕ
hpri : p.Prime
hp : p ≠ 2
x : 𝓞 K
hx : IsUnit (1 + p • x)
H : (Algebra.norm ℤ) (1 + p • x) = 1 ∨ (Algebra.norm ℤ) (1 + p • x) = -1
this : (Algebra.norm ℤ) (1 + p • x) ≠ -1
⊢ (Algebra.norm ℤ) (1 + p • x) = 1

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
K : Type u_2
inst✝¹ : Field K
inst✝ : NumberField K
p : ℕ
hpri : p.Prime
hp : p ≠ 2
x : 𝓞 K
hx : IsUnit (1 + p • x)
H : (Algebra.norm ℤ) (1 + p • x) = 1 ∨ (Algebra.norm ℤ) (1 + p • x) = -1
this : (Algebra.norm ℤ) (1 + p • x) ≠ -1
⊢ (Algebra.norm ℤ) (1 + p • x) = 1
Tactic:
exact H.resolve_right this
State after:
no goals

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
K : Type u_2
inst✝¹ : Field K
inst✝ : NumberField K
p : ℕ
hpri : p.Prime
hp : p ≠ 2
x : 𝓞 K
hx : IsUnit (1 + p • x)
⊢ (Algebra.norm ℤ) (1 + p • x) = 1 ∨ (Algebra.norm ℤ) (1 + p • x) = -1
Tactic:
apply Int.natAbs_eq_iff.mp
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
K : Type u_2
inst✝¹ : Field K
inst✝ : NumberField K
p : ℕ
hpri : p.Prime
hp : p ≠ 2
x : 𝓞 K
hx : IsUnit (1 + p • x)
⊢ ((Algebra.norm ℤ) (1 + p • x)).natAbs = 1

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
K : Type u_2
inst✝¹ : Field K
inst✝ : NumberField K
p : ℕ
hpri : p.Prime
hp : p ≠ 2
x : 𝓞 K
hx : IsUnit (1 + p • x)
⊢ ((Algebra.norm ℤ) (1 + p • x)).natAbs = 1
Tactic:
apply (Int.cast_injective (α := ℚ)).comp Nat.cast_injective
State after:
case a
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
K : Type u_2
inst✝¹ : Field K
inst✝ : NumberField K
p : ℕ
hpri : p.Prime
hp : p ≠ 2
x : 𝓞 K
hx : IsUnit (1 + p • x)
⊢ (Int.cast ∘ Nat.cast) ((Algebra.norm ℤ) (1 + p • x)).natAbs = (Int.cast ∘ Nat.cast) 1

State before:
case a
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
K : Type u_2
inst✝¹ : Field K
inst✝ : NumberField K
p : ℕ
hpri : p.Prime
hp : p ≠ 2
x : 𝓞 K
hx : IsUnit (1 + p • x)
⊢ (Int.cast ∘ Nat.cast) ((Algebra.norm ℤ) (1 + p • x)).natAbs = (Int.cast ∘ Nat.cast) 1
Tactic:
simp only [Int.cast_abs, Function.comp_apply, Nat.cast_one, Int.cast_one, ← Int.abs_eq_natAbs,
  Algebra.coe_norm_int, ← NumberField.isUnit_iff_norm.mp hx, RingOfIntegers.coe_norm]
State after:
no goals

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
K : Type u_2
inst✝¹ : Field K
inst✝ : NumberField K
p : ℕ
hpri : p.Prime
hp : p ≠ 2
x : 𝓞 K
hx : IsUnit (1 + p • x)
H : (Algebra.norm ℤ) (1 + p • x) = 1 ∨ (Algebra.norm ℤ) (1 + p • x) = -1
⊢ (Algebra.norm ℤ) (1 + p • x) ≠ -1
Tactic:
intro e
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
K : Type u_2
inst✝¹ : Field K
inst✝ : NumberField K
p : ℕ
hpri : p.Prime
hp : p ≠ 2
x : 𝓞 K
hx : IsUnit (1 + p • x)
H : (Algebra.norm ℤ) (1 + p • x) = 1 ∨ (Algebra.norm ℤ) (1 + p • x) = -1
e : (Algebra.norm ℤ) (1 + p • x) = -1
⊢ False

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
K : Type u_2
inst✝¹ : Field K
inst✝ : NumberField K
p : ℕ
hpri : p.Prime
hp : p ≠ 2
x : 𝓞 K
hx : IsUnit (1 + p • x)
H : (Algebra.norm ℤ) (1 + p • x) = 1 ∨ (Algebra.norm ℤ) (1 + p • x) = -1
e : (Algebra.norm ℤ) (1 + p • x) = -1
⊢ False
Tactic:
apply hp
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
K : Type u_2
inst✝¹ : Field K
inst✝ : NumberField K
p : ℕ
hpri : p.Prime
hp : p ≠ 2
x : 𝓞 K
hx : IsUnit (1 + p • x)
H : (Algebra.norm ℤ) (1 + p • x) = 1 ∨ (Algebra.norm ℤ) (1 + p • x) = -1
e : (Algebra.norm ℤ) (1 + p • x) = -1
⊢ p = 2

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
K : Type u_2
inst✝¹ : Field K
inst✝ : NumberField K
p : ℕ
hpri : p.Prime
hp : p ≠ 2
x : 𝓞 K
hx : IsUnit (1 + p • x)
H : (Algebra.norm ℤ) (1 + p • x) = 1 ∨ (Algebra.norm ℤ) (1 + p • x) = -1
e : (Algebra.norm ℤ) (1 + p • x) = -1
⊢ p = 2
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
K : Type u_2
inst✝¹ : Field K
inst✝ : NumberField K
p : ℕ
hpri : p.Prime
hp : p ≠ 2
x : 𝓞 K
hx : IsUnit (1 + p • x)
H : (Algebra.norm ℤ) (1 + p • x) = 1 ∨ (Algebra.norm ℤ) (1 + p • x) = -1
e : (Algebra.norm ℤ) (1 + p • x) = -1
r : ℤ
hr : (Algebra.norm ℤ) (1 + ↑p • x) = 1 + (Algebra.trace ℤ (𝓞 K)) x * ↑p + r * ↑p ^ 2
⊢ p = 2

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
K : Type u_2
inst✝¹ : Field K
inst✝ : NumberField K
p : ℕ
hpri : p.Prime
hp : p ≠ 2
x : 𝓞 K
hx : IsUnit (1 + p • x)
H : (Algebra.norm ℤ) (1 + p • x) = 1 ∨ (Algebra.norm ℤ) (1 + p • x) = -1
e : (Algebra.norm ℤ) (1 + p • x) = -1
r : ℤ
hr : (Algebra.norm ℤ) (1 + ↑p • x) = 1 + (Algebra.trace ℤ (𝓞 K)) x * ↑p + r * ↑p ^ 2
⊢ p = 2
Tactic:
have : (p : ℤ) * (- Algebra.trace ℤ _ x - r * p) = 2 := by
  rw [zsmul_eq_mul, Int.cast_natCast, ← nsmul_eq_mul, e, eq_comm, ← sub_eq_zero] at hr
  rw [eq_comm, ← sub_eq_zero, ← hr]
  ring
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
K : Type u_2
inst✝¹ : Field K
inst✝ : NumberField K
p : ℕ
hpri : p.Prime
hp : p ≠ 2
x : 𝓞 K
hx : IsUnit (1 + p • x)
H : (Algebra.norm ℤ) (1 + p • x) = 1 ∨ (Algebra.norm ℤ) (1 + p • x) = -1
e : (Algebra.norm ℤ) (1 + p • x) = -1
r : ℤ
hr : (Algebra.norm ℤ) (1 + ↑p • x) = 1 + (Algebra.trace ℤ (𝓞 K)) x * ↑p + r * ↑p ^ 2
this : ↑p * (-(Algebra.trace ℤ (𝓞 K)) x - r * ↑p) = 2
⊢ p = 2

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
K : Type u_2
inst✝¹ : Field K
inst✝ : NumberField K
p : ℕ
hpri : p.Prime
hp : p ≠ 2
x : 𝓞 K
hx : IsUnit (1 + p • x)
H : (Algebra.norm ℤ) (1 + p • x) = 1 ∨ (Algebra.norm ℤ) (1 + p • x) = -1
e : (Algebra.norm ℤ) (1 + p • x) = -1
r : ℤ
hr : (Algebra.norm ℤ) (1 + ↑p • x) = 1 + (Algebra.trace ℤ (𝓞 K)) x * ↑p + r * ↑p ^ 2
this : ↑p * (-(Algebra.trace ℤ (𝓞 K)) x - r * ↑p) = 2
⊢ p = 2
Tactic:
exact (Nat.prime_two.eq_one_or_self_of_dvd _
  (Int.natCast_dvd_natCast.mp ⟨_, this.symm⟩)).resolve_left hpri.ne_one
State after:
no goals

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
K : Type u_2
inst✝¹ : Field K
inst✝ : NumberField K
p : ℕ
hpri : p.Prime
hp : p ≠ 2
x : 𝓞 K
hx : IsUnit (1 + p • x)
H : (Algebra.norm ℤ) (1 + p • x) = 1 ∨ (Algebra.norm ℤ) (1 + p • x) = -1
e : (Algebra.norm ℤ) (1 + p • x) = -1
r : ℤ
hr : (Algebra.norm ℤ) (1 + ↑p • x) = 1 + (Algebra.trace ℤ (𝓞 K)) x * ↑p + r * ↑p ^ 2
⊢ ↑p * (-(Algebra.trace ℤ (𝓞 K)) x - r * ↑p) = 2
Tactic:
rw [zsmul_eq_mul, Int.cast_natCast, ← nsmul_eq_mul, e, eq_comm, ← sub_eq_zero] at hr
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
K : Type u_2
inst✝¹ : Field K
inst✝ : NumberField K
p : ℕ
hpri : p.Prime
hp : p ≠ 2
x : 𝓞 K
hx : IsUnit (1 + p • x)
H : (Algebra.norm ℤ) (1 + p • x) = 1 ∨ (Algebra.norm ℤ) (1 + p • x) = -1
e : (Algebra.norm ℤ) (1 + p • x) = -1
r : ℤ
hr : 1 + (Algebra.trace ℤ (𝓞 K)) x * ↑p + r * ↑p ^ 2 - -1 = 0
⊢ ↑p * (-(Algebra.trace ℤ (𝓞 K)) x - r * ↑p) = 2

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
K : Type u_2
inst✝¹ : Field K
inst✝ : NumberField K
p : ℕ
hpri : p.Prime
hp : p ≠ 2
x : 𝓞 K
hx : IsUnit (1 + p • x)
H : (Algebra.norm ℤ) (1 + p • x) = 1 ∨ (Algebra.norm ℤ) (1 + p • x) = -1
e : (Algebra.norm ℤ) (1 + p • x) = -1
r : ℤ
hr : 1 + (Algebra.trace ℤ (𝓞 K)) x * ↑p + r * ↑p ^ 2 - -1 = 0
⊢ ↑p * (-(Algebra.trace ℤ (𝓞 K)) x - r * ↑p) = 2
Tactic:
rw [eq_comm, ← sub_eq_zero, ← hr]
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
K : Type u_2
inst✝¹ : Field K
inst✝ : NumberField K
p : ℕ
hpri : p.Prime
hp : p ≠ 2
x : 𝓞 K
hx : IsUnit (1 + p • x)
H : (Algebra.norm ℤ) (1 + p • x) = 1 ∨ (Algebra.norm ℤ) (1 + p • x) = -1
e : (Algebra.norm ℤ) (1 + p • x) = -1
r : ℤ
hr : 1 + (Algebra.trace ℤ (𝓞 K)) x * ↑p + r * ↑p ^ 2 - -1 = 0
⊢ 2 - ↑p * (-(Algebra.trace ℤ (𝓞 K)) x - r * ↑p) = 1 + (Algebra.trace ℤ (𝓞 K)) x * ↑p + r * ↑p ^ 2 - -1

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
K : Type u_2
inst✝¹ : Field K
inst✝ : NumberField K
p : ℕ
hpri : p.Prime
hp : p ≠ 2
x : 𝓞 K
hx : IsUnit (1 + p • x)
H : (Algebra.norm ℤ) (1 + p • x) = 1 ∨ (Algebra.norm ℤ) (1 + p • x) = -1
e : (Algebra.norm ℤ) (1 + p • x) = -1
r : ℤ
hr : 1 + (Algebra.trace ℤ (𝓞 K)) x * ↑p + r * ↑p ^ 2 - -1 = 0
⊢ 2 - ↑p * (-(Algebra.trace ℤ (𝓞 K)) x - r * ↑p) = 1 + (Algebra.trace ℤ (𝓞 K)) x * ↑p + r * ↑p ^ 2 - -1
Tactic:
ring
State after:
no goals