-- Mathlib/NumberTheory/Cyclotomic/Three.lean
theorem eq_one_or_neg_one_of_unit_of_congruent
    [NumberField K] [IsCyclotomicExtension {3} ℚ K] (hcong : ∃ n : ℤ, λ ^ 2 ∣ (u - n : 𝓞 K)) :
    u = 1 ∨ u = -1

Proof state:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
u : (𝓞 K)ˣ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hcong : ∃ n, 3 ∣ ↑u - ↑n
⊢ u = 1 ∨ u = -1

Tactic:
have hζ := IsCyclotomicExtension.zeta_spec 3 ℚ K

Result:
K : Type u_1
inst✝² : Field K
ζ : K
hζ✝ : IsPrimitiveRoot ζ ↑3
u : (𝓞 K)ˣ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hcong : ∃ n, 3 ∣ ↑u - ↑n
hζ : IsPrimitiveRoot (zeta 3 ℚ K) ↑3
⊢ u = 1 ∨ u = -1

Proof state:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
u : (𝓞 K)ˣ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hcong : ∃ n, λ ^ 2 ∣ ↑u - ↑n
⊢ ∃ n, 3 ∣ ↑u - ↑n

Tactic:
obtain ⟨n, x, hx⟩ := hcong

Result:
case intro.intro
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
u : (𝓞 K)ˣ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
n : ℤ
x : 𝓞 K
hx : ↑u - ↑n = λ ^ 2 * x
⊢ ∃ n, 3 ∣ ↑u - ↑n

Proof state:
K : Type u_1
inst✝² : Field K
ζ : K
hζ✝ : IsPrimitiveRoot ζ ↑3
u : (𝓞 K)ˣ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hcong : ∃ n, 3 ∣ ↑u - ↑n
hζ : IsPrimitiveRoot (zeta 3 ℚ K) ↑3
this : u ∈ [1, -1, ⋯.unit, -⋯.unit, ⋯.unit ^ 2, -⋯.unit ^ 2]
⊢ u = 1 ∨ u = -1

Tactic:
fin_cases this

Result:
case «0»
K : Type u_1
inst✝² : Field K
ζ : K
hζ✝ : IsPrimitiveRoot ζ ↑3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hζ : IsPrimitiveRoot (zeta 3 ℚ K) ↑3
hcong : ∃ n, 3 ∣ ↑1 - ↑n
⊢ 1 = 1 ∨ 1 = -1

case «1»
K : Type u_1
inst✝² : Field K
ζ : K
hζ✝ : IsPrimitiveRoot ζ ↑3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hζ : IsPrimitiveRoot (zeta 3 ℚ K) ↑3
hcong : ∃ n, 3 ∣ ↑(-1) - ↑n
⊢ -1 = 1 ∨ -1 = -1

case «2»
K : Type u_1
inst✝² : Field K
ζ : K
hζ✝ : IsPrimitiveRoot ζ ↑3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hζ : IsPrimitiveRoot (zeta 3 ℚ K) ↑3
hcong : ∃ n, 3 ∣ ↑⋯.unit - ↑n
⊢ ⋯.unit = 1 ∨ ⋯.unit = -1

case «3»
K : Type u_1
inst✝² : Field K
ζ : K
hζ✝ : IsPrimitiveRoot ζ ↑3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hζ : IsPrimitiveRoot (zeta 3 ℚ K) ↑3
hcong : ∃ n, 3 ∣ ↑(-⋯.unit) - ↑n
⊢ -⋯.unit = 1 ∨ -⋯.unit = -1

case «4»
K : Type u_1
inst✝² : Field K
ζ : K
hζ✝ : IsPrimitiveRoot ζ ↑3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hζ : IsPrimitiveRoot (zeta 3 ℚ K) ↑3
hcong : ∃ n, 3 ∣ ↑(⋯.unit ^ 2) - ↑n
⊢ ⋯.unit ^ 2 = 1 ∨ ⋯.unit ^ 2 = -1

case «5»
K : Type u_1
inst✝² : Field K
ζ : K
hζ✝ : IsPrimitiveRoot ζ ↑3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hζ : IsPrimitiveRoot (zeta 3 ℚ K) ↑3
hcong : ∃ n, 3 ∣ ↑(-⋯.unit ^ 2) - ↑n
⊢ -⋯.unit ^ 2 = 1 ∨ -⋯.unit ^ 2 = -1

Proof state:
case «5»
K : Type u_1
inst✝² : Field K
ζ : K
hζ✝ : IsPrimitiveRoot ζ ↑3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hζ : IsPrimitiveRoot (zeta 3 ℚ K) ↑3
hcong : ∃ n, 3 ∣ ↑(-⋯.unit ^ 2) - ↑n
⊢ ∃ n, ↑↑3 ∣ ⋯.toInteger - ↑n

Tactic:
obtain ⟨n, x, hx⟩ := hcong

Result:
case «5».intro.intro
K : Type u_1
inst✝² : Field K
ζ : K
hζ✝ : IsPrimitiveRoot ζ ↑3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hζ : IsPrimitiveRoot (zeta 3 ℚ K) ↑3
n : ℤ
x : 𝓞 K
hx : ↑(-⋯.unit ^ 2) - ↑n = 3 * x
⊢ ∃ n, ↑↑3 ∣ ⋯.toInteger - ↑n

Proof state:
K : Type u_1
inst✝² : Field K
ζ : K
hζ✝ : IsPrimitiveRoot ζ ↑3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hζ : IsPrimitiveRoot (zeta 3 ℚ K) ↑3
n : ℤ
x : 𝓞 K
hx : ↑(-⋯.unit ^ 2) - ↑n = 3 * x
⊢ ⋯.toInteger = hζ.toInteger ^ 2

Tactic:
ext

Result:
case h
K : Type u_1
inst✝² : Field K
ζ : K
hζ✝ : IsPrimitiveRoot ζ ↑3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hζ : IsPrimitiveRoot (zeta 3 ℚ K) ↑3
n : ℤ
x : 𝓞 K
hx : ↑(-⋯.unit ^ 2) - ↑n = 3 * x
⊢ ↑⋯.toInteger = ↑(hζ.toInteger ^ 2)

Proof state:
K : Type u_1
inst✝² : Field K
ζ : K
hζ✝ : IsPrimitiveRoot ζ ↑3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hζ : IsPrimitiveRoot (zeta 3 ℚ K) ↑3
hcong : ∃ n, 3 ∣ ↑(-⋯.unit ^ 2) - ↑n
⊢ 3 ≠ 2

Tactic:
decide

Result:
no goals

Proof state:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
u : (𝓞 K)ˣ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
n : ℤ
x : 𝓞 K
hx : ↑u - ↑n = λ ^ 2 * x
⊢ ↑u - ↑n = 3 * (-↑η * x)

Tactic:
rw [← mul_assoc, mul_neg, ← neg_mul, ← lambda_sq, hx]

Result:
no goals

Proof state:
case «5»
K : Type u_1
inst✝² : Field K
ζ : K
hζ✝ : IsPrimitiveRoot ζ ↑3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hζ : IsPrimitiveRoot (zeta 3 ℚ K) ↑3
hcong : ∃ n, 3 ∣ ↑(-⋯.unit ^ 2) - ↑n
⊢ False

Tactic:
apply (hζ.pow_of_coprime 2 (by decide)).not_exists_int_prime_dvd_sub_of_prime_ne_two'
  (by decide)

Result:
case «5»
K : Type u_1
inst✝² : Field K
ζ : K
hζ✝ : IsPrimitiveRoot ζ ↑3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hζ : IsPrimitiveRoot (zeta 3 ℚ K) ↑3
hcong : ∃ n, 3 ∣ ↑(-⋯.unit ^ 2) - ↑n
⊢ ∃ n, ↑↑3 ∣ ⋯.toInteger - ↑n

Proof state:
case «0».h
K : Type u_1
inst✝² : Field K
ζ : K
hζ✝ : IsPrimitiveRoot ζ ↑3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hζ : IsPrimitiveRoot (zeta 3 ℚ K) ↑3
hcong : ∃ n, 3 ∣ ↑1 - ↑n
⊢ 1 = 1

Tactic:
rfl

Result:
no goals

Proof state:
case «3».intro.intro
K : Type u_1
inst✝² : Field K
ζ : K
hζ✝ : IsPrimitiveRoot ζ ↑3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hζ : IsPrimitiveRoot (zeta 3 ℚ K) ↑3
n : ℤ
x : 𝓞 K
hx : ↑(-⋯.unit) = 3 * x + ↑n
⊢ ∃ n, ↑↑3 ∣ hζ.toInteger - ↑n

Tactic:
refine ⟨-n, -x, sub_eq_iff_eq_add.2 ?_⟩

Result:
case «3».intro.intro
K : Type u_1
inst✝² : Field K
ζ : K
hζ✝ : IsPrimitiveRoot ζ ↑3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hζ : IsPrimitiveRoot (zeta 3 ℚ K) ↑3
n : ℤ
x : 𝓞 K
hx : ↑(-⋯.unit) = 3 * x + ↑n
⊢ hζ.toInteger = ↑↑3 * -x + ↑(-n)

Proof state:
case «5».intro.intro
K : Type u_1
inst✝² : Field K
ζ : K
hζ✝ : IsPrimitiveRoot ζ ↑3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hζ : IsPrimitiveRoot (zeta 3 ℚ K) ↑3
n : ℤ
x : 𝓞 K
hx : ↑(-⋯.unit ^ 2) - ↑n = 3 * x
⊢ ∃ n, ↑↑3 ∣ ⋯.toInteger - ↑n

Tactic:
refine ⟨-n, -x, sub_eq_iff_eq_add.2 ?_⟩

Result:
case «5».intro.intro
K : Type u_1
inst✝² : Field K
ζ : K
hζ✝ : IsPrimitiveRoot ζ ↑3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hζ : IsPrimitiveRoot (zeta 3 ℚ K) ↑3
n : ℤ
x : 𝓞 K
hx : ↑(-⋯.unit ^ 2) - ↑n = 3 * x
⊢ ⋯.toInteger = ↑↑3 * -x + ↑(-n)

Proof state:
case «5».intro.intro
K : Type u_1
inst✝² : Field K
ζ : K
hζ✝ : IsPrimitiveRoot ζ ↑3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hζ : IsPrimitiveRoot (zeta 3 ℚ K) ↑3
n : ℤ
x : 𝓞 K
hx : ↑(-⋯.unit ^ 2) - ↑n = 3 * x
this : ⋯.toInteger = hζ.toInteger ^ 2
⊢ ⋯.toInteger = ↑↑3 * -x + ↑(-n)

Tactic:
simp only [this, PNat.val_ofNat, Nat.cast_ofNat, mul_neg, Int.cast_neg, ← neg_add, ←
  sub_eq_iff_eq_add.1 hx, Units.val_neg, val_pow_eq_pow_val, IsUnit.unit_spec, neg_neg]

Result:
no goals

Proof state:
K : Type u_1
inst✝² : Field K
ζ : K
hζ✝ : IsPrimitiveRoot ζ ↑3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hζ : IsPrimitiveRoot (zeta 3 ℚ K) ↑3
hcong : ∃ n, 3 ∣ ↑(⋯.unit ^ 2) - ↑n
⊢ 3 ≠ 2

Tactic:
decide

Result:
no goals

Proof state:
K : Type u_1
inst✝² : Field K
ζ : K
hζ✝ : IsPrimitiveRoot ζ ↑3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hζ : IsPrimitiveRoot (zeta 3 ℚ K) ↑3
hcong : ∃ n, 3 ∣ ↑(-⋯.unit) - ↑n
⊢ 3 ≠ 2

Tactic:
decide

Result:
no goals

Proof state:
K : Type u_1
inst✝² : Field K
ζ : K
hζ✝ : IsPrimitiveRoot ζ ↑3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hζ : IsPrimitiveRoot (zeta 3 ℚ K) ↑3
hcong : ∃ n, 3 ∣ ↑⋯.unit - ↑n
⊢ 3 ≠ 2

Tactic:
decide

Result:
no goals