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

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
⊢ Odd ↑3

Tactic:
decide

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
hru : (algebraMap (𝓞 K) K) ↑u = ζ ^ r ∨ (algebraMap (𝓞 K) K) ↑u = -ζ ^ r
⊢ u ∈ [1, -1, η, -η, η ^ 2, -η ^ 2]

Tactic:
replace hr : r ∈ Finset.Ico 0 3 := Finset.mem_Ico.2 ⟨by simp, hr3⟩

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
hr : r ∈ Finset.Ico 0 3
⊢ 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 : ↑x ^ n = 1
⊢ u ∈ [1, -1, η, -η, η ^ 2, -η ^ 2]

Tactic:
replace hn : (↑u : K) ^ ((⟨n, hnpos⟩ : ℕ+) : ℕ) = 1 := by
  rw [← map_pow]
  convert map_one (algebraMap (𝓞 K) K)
  rw_mod_cast [hxu, hn]
  simp

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 : (algebraMap (𝓞 K) K) ↑u ^ ↑⟨n, hnpos⟩ = 1
⊢ u ∈ [1, -1, η, -η, η ^ 2, -η ^ 2]

Proof state:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
u : (𝓞 K)ˣ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
⊢ u ∈ [1, -1, η, -η, η ^ 2, -η ^ 2]

Tactic:
have hrank : rank K = 0 := by
  dsimp only [rank]
  rw [card_eq_nrRealPlaces_add_nrComplexPlaces, nrRealPlaces_eq_zero (n := 3) K (by decide),
    zero_add, nrComplexPlaces_eq_totient_div_two (n := 3)]
  rfl

Result:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
u : (𝓞 K)ˣ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hrank : rank K = 0
⊢ u ∈ [1, -1, η, -η, η ^ 2, -η ^ 2]

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 : ↑x ^ n = 1
⊢ (algebraMap (𝓞 K) K) ↑u ^ ↑⟨n, hnpos⟩ = 1

Tactic:
rw [← map_pow]

Result:
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
⊢ (algebraMap (𝓞 K) K) (↑u ^ ↑⟨n, hnpos⟩) = 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, e).1 * ∏ i : Fin (rank K), fundSystem K i ^ (x, e).2 i
⊢ ↑(x, e).1 * ∏ i : Fin (rank K), fundSystem K i ^ (x, e).2 i = ↑x * 1

Tactic:
apply congr_arg

Result:
case 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, e).1 * ∏ i : Fin (rank K), fundSystem K i ^ (x, e).2 i
⊢ ∏ i : Fin (rank K), fundSystem K i ^ (x, e).2 i = 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
⊢ u ∈ [1, -1, η, -η, η ^ 2, -η ^ 2]

Tactic:
obtain ⟨⟨x, e⟩, hxu, -⟩ := exist_unique_eq_mul_prod _ u

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, e).1 * ∏ i : Fin (rank K), fundSystem K i ^ (x, e).2 i
⊢ u ∈ [1, -1, η, -η, η ^ 2, -η ^ 2]

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
hr : r ∈ Finset.Ico 0 3
⊢ u = η ^ r ∨ u = -η ^ r

Tactic:
rcases hru with h | h

Result:
case inl
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 ∨ u = -η ^ r

case inr
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 ∨ u = -η ^ r

Proof state:
case inl.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:
ext

Result:
case inl.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)

Proof state:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
u : (𝓞 K)ˣ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
⊢ Fintype.card (InfinitePlace K) - 1 = 0

Tactic:
rw [card_eq_nrRealPlaces_add_nrComplexPlaces, nrRealPlaces_eq_zero (n := 3) K (by decide),
  zero_add, nrComplexPlaces_eq_totient_div_two (n := 3)]

Result:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
u : (𝓞 K)ˣ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
⊢ (↑3).totient / 2 - 1 = 0

Proof state:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
u : (𝓞 K)ˣ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
⊢ (↑3).totient / 2 - 1 = 0

Tactic:
rfl

Result:
no goals