-- 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:
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

Tactic:
right

Result:
case «1».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

Proof state:
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)

Tactic:
simp

Result:
no goals

Proof state:
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
⊢ False

Tactic:
exact hζ.not_exists_int_prime_dvd_sub_of_prime_ne_two' (by decide) hcong

Result:
no goals

Proof state:
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
⊢ False

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

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
hcong : ∃ n, 3 ∣ ↑u - ↑n
hζ : IsPrimitiveRoot (zeta 3 ℚ K) ↑3
⊢ u = 1 ∨ u = -1

Tactic:
have := Units.mem hζ u

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
this : u ∈ [1, -1, ⋯.unit, -⋯.unit, ⋯.unit ^ 2, -⋯.unit ^ 2]
⊢ u = 1 ∨ u = -1

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
⊢ hζ.toInteger = ↑↑3 * -x + ↑(-n)

Tactic:
simp only [PNat.val_ofNat, Nat.cast_ofNat, mul_neg, Int.cast_neg, ← neg_add, ← hx,
  Units.val_neg, IsUnit.unit_spec, RingOfIntegers.neg_mk, 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
⊢ Nat.Coprime 2 ↑3

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
n : ℤ
x : 𝓞 K
hx : ↑(-⋯.unit ^ 2) - ↑n = 3 * x
⊢ Nat.Coprime 2 ↑3

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
hcong : ∃ n, λ ^ 2 ∣ ↑u - ↑n
⊢ u = 1 ∨ u = -1

Tactic:
replace hcong : ∃ n : ℤ, (3 : 𝓞 K) ∣ (↑u - n : 𝓞 K) := by
  obtain ⟨n, x, hx⟩ := hcong
  exact ⟨n, -η * x, by rw [← mul_assoc, mul_neg, ← neg_mul, ← lambda_sq, hx]⟩

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
⊢ u = 1 ∨ u = -1

Proof state:
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

Tactic:
all_goals exfalso

Result:
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
⊢ False

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
⊢ False

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
⊢ False

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

Proof state:
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
⊢ ∃ n, ↑↑3 ∣ hζ.toInteger - ↑n

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

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) - ↑n = 3 * x
⊢ ∃ n, ↑↑3 ∣ hζ.toInteger - ↑n

Proof state:
case «1».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 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

Tactic:
exact ⟨n, -η * x, by rw [← mul_assoc, mul_neg, ← neg_mul, ← lambda_sq, hx]⟩

Result:
no goals

Proof state:
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

Tactic:
left

Result:
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

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
⊢ -⋯.unit ^ 2 = 1 ∨ -⋯.unit ^ 2 = -1

Tactic:
exfalso

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
⊢ False