-- Mathlib/NumberTheory/Cyclotomic/Three.lean
theorem Units.mem [NumberField K] [IsCyclotomicExtension {3} ℚ K] :
    u ∈ [1, -1, η, -η, η ^ 2, -η ^ 2]

Proof state:
case intro.mk.intro.intro.intro
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
u : (𝓞 K)ˣ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hrank : rank K = 0
x : ↥(torsion K)
e : Fin (rank K) → ℤ
hxu : u = ↑x
n : ℕ
hnpos : 0 < n
hn : (algebraMap (𝓞 K) K) ↑u ^ ↑⟨n, hnpos⟩ = 1
⊢ u ∈ [1, -1, η, -η, η ^ 2, -η ^ 2]

Tactic:
obtain ⟨r, hr3, hru⟩ := hζ.exists_pow_or_neg_mul_pow_of_isOfFinOrder (by decide)
  (isOfFinOrder_iff_pow_eq_one.2 ⟨n, hnpos, hn⟩)

Result:
case intro.mk.intro.intro.intro.intro.intro
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
u : (𝓞 K)ˣ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hrank : rank K = 0
x : ↥(torsion K)
e : Fin (rank K) → ℤ
hxu : u = ↑x
n : ℕ
hnpos : 0 < n
hn : (algebraMap (𝓞 K) K) ↑u ^ ↑⟨n, hnpos⟩ = 1
r : ℕ
hr3 : r < ↑3
hru : (algebraMap (𝓞 K) K) ↑u = ζ ^ r ∨ (algebraMap (𝓞 K) K) ↑u = -ζ ^ r
⊢ u ∈ [1, -1, η, -η, η ^ 2, -η ^ 2]

Proof state:
case h.e'_2.h.e'_6
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
u : (𝓞 K)ˣ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hrank : rank K = 0
x : ↥(torsion K)
e : Fin (rank K) → ℤ
hxu : u = ↑x
n : ℕ
hnpos : 0 < n
hn : ↑x ^ n = 1
⊢ ↑u ^ ↑⟨n, hnpos⟩ = 1

Tactic:
rw_mod_cast [hxu, hn]

Result:
case h.e'_2.h.e'_6
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
u : (𝓞 K)ˣ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hrank : rank K = 0
x : ↥(torsion K)
e : Fin (rank K) → ℤ
hxu : u = ↑x
n : ℕ
hnpos : 0 < n
hn : x ^ n = 1
⊢ ↑↑1 = 1

Proof state:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
u : (𝓞 K)ˣ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hrank : rank K = 0
x : ↥(torsion K)
e : Fin (rank K) → ℤ
hxu : u = ↑x
n : ℕ
hnpos : 0 < n
hn : (algebraMap (𝓞 K) K) ↑u ^ ↑⟨n, hnpos⟩ = 1
r : ℕ
hr3 : r < ↑3
hru : (algebraMap (𝓞 K) K) ↑u = ζ ^ r ∨ (algebraMap (𝓞 K) K) ↑u = -ζ ^ r
⊢ 0 ≤ r

Tactic:
simp

Result:
no goals

Proof state:
case inr.h.a.h
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
u : (𝓞 K)ˣ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hrank : rank K = 0
x : ↥(torsion K)
e : Fin (rank K) → ℤ
hxu : u = ↑x
n : ℕ
hnpos : 0 < n
hn : (algebraMap (𝓞 K) K) ↑u ^ ↑⟨n, hnpos⟩ = 1
r : ℕ
hr3 : r < ↑3
hr : r ∈ Finset.Ico 0 3
h : (algebraMap (𝓞 K) K) ↑u = -ζ ^ r
⊢ ↑↑u = ↑↑(-η ^ r)

Tactic:
exact h

Result:
no goals

Proof state:
case intro.mk.intro.intro.intro.intro.intro
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
u : (𝓞 K)ˣ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hrank : rank K = 0
x : ↥(torsion K)
e : Fin (rank K) → ℤ
hxu : u = ↑x
n : ℕ
hnpos : 0 < n
hn : (algebraMap (𝓞 K) K) ↑u ^ ↑⟨n, hnpos⟩ = 1
r : ℕ
hr3 : r < ↑3
hr : r ∈ Finset.Ico 0 3
hru : u = η ^ r ∨ u = -η ^ r
⊢ u ∈ [1, -1, η, -η, η ^ 2, -η ^ 2]

Tactic:
fin_cases hr <;> rcases hru with h | h <;> simp [h]

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
⊢ 2 < 3

Tactic:
decide

Result:
no goals

Proof state:
case intro.mk.intro
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
u : (𝓞 K)ˣ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hrank : rank K = 0
x : ↥(torsion K)
e : Fin (rank K) → ℤ
hxu : u = ↑(x, e).1 * ∏ i : Fin (rank K), fundSystem K i ^ (x, e).2 i
⊢ u ∈ [1, -1, η, -η, η ^ 2, -η ^ 2]

Tactic:
replace hxu : u = x := by
  rw [← mul_one x.1, hxu]
  apply congr_arg
  rw [← Finset.prod_empty]
  congr
  rw [Finset.univ_eq_empty_iff, hrank]
  infer_instance

Result:
case intro.mk.intro
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
u : (𝓞 K)ˣ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hrank : rank K = 0
x : ↥(torsion K)
e : Fin (rank K) → ℤ
hxu : u = ↑x
⊢ u ∈ [1, -1, η, -η, η ^ 2, -η ^ 2]

Proof state:
case h.e_s
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
u : (𝓞 K)ˣ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hrank : rank K = 0
x : ↥(torsion K)
e : Fin (rank K) → ℤ
hxu : u = ↑(x, e).1 * ∏ i : Fin (rank K), fundSystem K i ^ (x, e).2 i
⊢ Finset.univ = ∅

Tactic:
rw [Finset.univ_eq_empty_iff, hrank]

Result:
case h.e_s
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
u : (𝓞 K)ˣ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hrank : rank K = 0
x : ↥(torsion K)
e : Fin (rank K) → ℤ
hxu : u = ↑(x, e).1 * ∏ i : Fin (rank K), fundSystem K i ^ (x, e).2 i
⊢ IsEmpty (Fin 0)

Proof state:
case intro.mk.intro
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
u : (𝓞 K)ˣ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hrank : rank K = 0
x : ↥(torsion K)
e : Fin (rank K) → ℤ
hxu : u = ↑x
⊢ u ∈ [1, -1, η, -η, η ^ 2, -η ^ 2]

Tactic:
obtain ⟨n, hnpos, hn⟩ := isOfFinOrder_iff_pow_eq_one.1 <| (CommGroup.mem_torsion _ _).1 x.2

Result:
case intro.mk.intro.intro.intro
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
u : (𝓞 K)ˣ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hrank : rank K = 0
x : ↥(torsion K)
e : Fin (rank K) → ℤ
hxu : u = ↑x
n : ℕ
hnpos : 0 < n
hn : ↑x ^ n = 1
⊢ u ∈ [1, -1, η, -η, η ^ 2, -η ^ 2]