awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
u : (𝓞 K)ˣ
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
hrank : rank K = 0
x : ↥(torsion K)
e : Fin (rank K) → ℤ
hxu : u = (↑x : (𝓞 K)ˣ)
n : ℕ
hnpos : 0 < n
hn :
  HPow.hPow (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K)
      (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n hnpos) : ℕ) =
    1
r : ℕ
hr3 : r < 3
hru : (algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) = ζ ^ r ∨ (algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) = -ζ ^ r
⊢ 0 ≤ r

Tactic:
simp
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
u : (𝓞 K)ˣ
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
hrank : rank K = 0
x : ↥(torsion K)
e : Fin (rank K) → ℤ
hxu : u = (↑x : (𝓞 K)ˣ)
n : ℕ
hnpos : 0 < n
hn :
  HPow.hPow (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K)
      (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n hnpos) : ℕ) =
    1
r : ℕ
hr3 : r < 3
hru : (algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) = ζ ^ r ∨ (algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) = -ζ ^ r
⊢ Membership.mem (γ := Finset ℕ) (Finset.Ico 0 3) r

Tactic:
replace hr : r ∈ Finset.Ico 0 3 := Finset.mem_Ico.2 ⟨by simp, hr3⟩
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
u : (𝓞 K)ˣ
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
hrank : rank K = 0
x : ↥(torsion K)
e : Fin (rank K) → ℤ
hxu : u = (↑x : (𝓞 K)ˣ)
n : ℕ
hnpos : 0 < n
hn :
  HPow.hPow (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K)
      (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n hnpos) : ℕ) =
    1
r : ℕ
hr3 : r < 3
hru : (algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) = ζ ^ r ∨ (algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) = -ζ ^ r
hr : Membership.mem (γ := Finset ℕ) (Finset.Ico 0 3) r
inl : ∀ (h : (algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) = ζ ^ r), u = η ^ r ∨ u = -η ^ r
inr : ∀ (h : (algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) = -ζ ^ r), u = η ^ r ∨ u = -η ^ r
⊢ u = η ^ r ∨ u = -η ^ r

Tactic:
rcases hru with h | h
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
u : (𝓞 K)ˣ
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
hrank : rank K = 0
x : ↥(torsion K)
e : Fin (rank K) → ℤ
hxu : u = (↑x : (𝓞 K)ˣ)
n : ℕ
hnpos : 0 < n
hn :
  HPow.hPow (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K)
      (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n hnpos) : ℕ) =
    1
r : ℕ
hr3 : r < 3
hr : Membership.mem (γ := Finset ℕ) (Finset.Ico 0 3) r
h : (algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) = ζ ^ r
inl : u = η ^ r
⊢ u = η ^ r ∨ u = -η ^ r

Tactic:
left
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
u : (𝓞 K)ˣ
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
hrank : rank K = 0
x : ↥(torsion K)
e : Fin (rank K) → ℤ
hxu : u = (↑x : (𝓞 K)ˣ)
n : ℕ
hnpos : 0 < n
hn :
  HPow.hPow (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K)
      (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n hnpos) : ℕ) =
    1
r : ℕ
hr3 : r < 3
hr : Membership.mem (γ := Finset ℕ) (Finset.Ico 0 3) r
h : (algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) = ζ ^ r
inl : (↑(↑u : 𝓞 K) : K) = (↑(↑(η ^ r) : 𝓞 K) : K)
⊢ u = η ^ r

Tactic:
ext
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
u : (𝓞 K)ˣ
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
hrank : rank K = 0
x : ↥(torsion K)
e : Fin (rank K) → ℤ
hxu : u = (↑x : (𝓞 K)ˣ)
n : ℕ
hnpos : 0 < n
hn :
  HPow.hPow (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K)
      (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n hnpos) : ℕ) =
    1
r : ℕ
hr3 : r < 3
hr : Membership.mem (γ := Finset ℕ) (Finset.Ico 0 3) r
h : (algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) = ζ ^ r
⊢ (↑(↑u : 𝓞 K) : K) = (↑(↑(η ^ r) : 𝓞 K) : K)

Tactic:
h
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
u : (𝓞 K)ˣ
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
hrank : rank K = 0
x : ↥(torsion K)
e : Fin (rank K) → ℤ
hxu : u = (↑x : (𝓞 K)ˣ)
n : ℕ
hnpos : 0 < n
hn :
  HPow.hPow (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K)
      (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n hnpos) : ℕ) =
    1
r : ℕ
hr3 : r < 3
hr : Membership.mem (γ := Finset ℕ) (Finset.Ico 0 3) r
h : (algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) = ζ ^ r
⊢ (↑(↑u : 𝓞 K) : K) = (↑(↑(η ^ r) : 𝓞 K) : K)

Tactic:
exact h
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
u : (𝓞 K)ˣ
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
hrank : rank K = 0
x : ↥(torsion K)
e : Fin (rank K) → ℤ
hxu : u = (↑x : (𝓞 K)ˣ)
n : ℕ
hnpos : 0 < n
hn :
  HPow.hPow (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K)
      (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n hnpos) : ℕ) =
    1
r : ℕ
hr3 : r < 3
hr : Membership.mem (γ := Finset ℕ) (Finset.Ico 0 3) r
h : (algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) = -ζ ^ r
inr : u = -η ^ r
⊢ u = η ^ r ∨ u = -η ^ r

Tactic:
right
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
u : (𝓞 K)ˣ
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
hrank : rank K = 0
x : ↥(torsion K)
e : Fin (rank K) → ℤ
hxu : u = (↑x : (𝓞 K)ˣ)
n : ℕ
hnpos : 0 < n
hn :
  HPow.hPow (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K)
      (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n hnpos) : ℕ) =
    1
r : ℕ
hr3 : r < 3
hr : Membership.mem (γ := Finset ℕ) (Finset.Ico 0 3) r
h : (algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) = -ζ ^ r
inr : (↑(↑u : 𝓞 K) : K) = (↑(↑(-η ^ r) : 𝓞 K) : K)
⊢ u = -η ^ r

Tactic:
ext
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
u : (𝓞 K)ˣ
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
hrank : rank K = 0
x : ↥(torsion K)
e : Fin (rank K) → ℤ
hxu : u = (↑x : (𝓞 K)ˣ)
n : ℕ
hnpos : 0 < n
hn :
  HPow.hPow (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K)
      (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n hnpos) : ℕ) =
    1
r : ℕ
hr3 : r < 3
hr : Membership.mem (γ := Finset ℕ) (Finset.Ico 0 3) r
h : (algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) = -ζ ^ r
⊢ (↑(↑u : 𝓞 K) : K) = (↑(↑(-η ^ r) : 𝓞 K) : K)

Tactic:
h
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
u : (𝓞 K)ˣ
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
hrank : rank K = 0
x : ↥(torsion K)
e : Fin (rank K) → ℤ
hxu : u = (↑x : (𝓞 K)ˣ)
n : ℕ
hnpos : 0 < n
hn :
  HPow.hPow (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K)
      (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n hnpos) : ℕ) =
    1
r : ℕ
hr3 : r < 3
hr : Membership.mem (γ := Finset ℕ) (Finset.Ico 0 3) r
h : (algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) = -ζ ^ r
⊢ (↑(↑u : 𝓞 K) : K) = (↑(↑(-η ^ r) : 𝓞 K) : K)

Tactic:
exact h
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
u : (𝓞 K)ˣ
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
hrank : rank K = 0
x : ↥(torsion K)
e : Fin (rank K) → ℤ
hxu : u = (↑x : (𝓞 K)ˣ)
n : ℕ
hnpos : 0 < n
hn :
  HPow.hPow (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K)
      (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n hnpos) : ℕ) =
    1
r : ℕ
hr3 : r < 3
hru : (algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) = ζ ^ r ∨ (algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) = -ζ ^ r
hr : Membership.mem (γ := Finset ℕ) (Finset.Ico 0 3) r
⊢ u = η ^ r ∨ u = -η ^ r

Tactic:
replace hru : ↑u = η ^ r ∨ ↑u = -η ^ r := by
    rcases hru with h | h
    · left; ext; exact h
    · right; ext; exact h
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
u : (𝓞 K)ˣ
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
hrank : rank K = 0
x : ↥(torsion K)
e : Fin (rank K) → ℤ
hxu : u = (↑x : (𝓞 K)ˣ)
n : ℕ
hnpos : 0 < n
hn :
  HPow.hPow (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K)
      (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n hnpos) : ℕ) =
    1
r : ℕ
hr3 : r < 3
hr : Membership.mem (γ := Finset ℕ) (Finset.Ico 0 3) r
hru : u = η ^ r ∨ u = -η ^ r
0 :
  ∀ (hr3 : LT.lt (α := ℕ) 0 3) (hru : u = HPow.hPow (β := ℕ) η 0 ∨ u = -HPow.hPow (β := ℕ) η 0),
    u ∈
      [1, -1, IsUnit.unit (a := hζ.toInteger) ⋯, -IsUnit.unit (a := hζ.toInteger) ⋯,
        HPow.hPow (β := ℕ) (IsUnit.unit (a := hζ.toInteger) ⋯) 2,
        -HPow.hPow (β := ℕ) (IsUnit.unit (a := hζ.toInteger) ⋯) 2]
1 :
  ∀ (hr3 : HAdd.hAdd (α := ℕ) 0 1 < 3) (hru : u = η ^ HAdd.hAdd (α := ℕ) 0 1 ∨ u = -η ^ HAdd.hAdd (α := ℕ) 0 1),
    u ∈
      [1, -1, IsUnit.unit (a := hζ.toInteger) ⋯, -IsUnit.unit (a := hζ.toInteger) ⋯,
        HPow.hPow (β := ℕ) (IsUnit.unit (a := hζ.toInteger) ⋯) 2,
        -HPow.hPow (β := ℕ) (IsUnit.unit (a := hζ.toInteger) ⋯) 2]
2 :
  ∀ (hr3 : HAdd.hAdd (α := ℕ) 0 1 + 1 < 3)
    (hru : u = η ^ (HAdd.hAdd (α := ℕ) 0 1 + 1) ∨ u = -η ^ (HAdd.hAdd (α := ℕ) 0 1 + 1)),
    u ∈
      [1, -1, IsUnit.unit (a := hζ.toInteger) ⋯, -IsUnit.unit (a := hζ.toInteger) ⋯,
        HPow.hPow (β := ℕ) (IsUnit.unit (a := hζ.toInteger) ⋯) 2,
        -HPow.hPow (β := ℕ) (IsUnit.unit (a := hζ.toInteger) ⋯) 2]
⊢ u ∈
    [1, -1, IsUnit.unit (a := hζ.toInteger) ⋯, -IsUnit.unit (a := hζ.toInteger) ⋯,
      HPow.hPow (β := ℕ) (IsUnit.unit (a := hζ.toInteger) ⋯) 2,
      -HPow.hPow (β := ℕ) (IsUnit.unit (a := hζ.toInteger) ⋯) 2]

Tactic:
fin_cases hr
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
u : (𝓞 K)ˣ
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
hrank : rank K = 0
x : ↥(torsion K)
e : Fin (rank K) → ℤ
hxu : u = (↑x : (𝓞 K)ˣ)
n : ℕ
hnpos : 0 < n
hn :
  HPow.hPow (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K)
      (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n hnpos) : ℕ) =
    1
hr3 : LT.lt (α := ℕ) 0 3
hru : u = HPow.hPow (β := ℕ) η 0 ∨ u = -HPow.hPow (β := ℕ) η 0
0 :
  ∀ (h : u = HPow.hPow (β := ℕ) η 0),
    u ∈
      [1, -1, IsUnit.unit (a := hζ.toInteger) ⋯, -IsUnit.unit (a := hζ.toInteger) ⋯,
        HPow.hPow (β := ℕ) (IsUnit.unit (a := hζ.toInteger) ⋯) 2,
        -HPow.hPow (β := ℕ) (IsUnit.unit (a := hζ.toInteger) ⋯) 2]
h :
  ∀ (h : u = -HPow.hPow (β := ℕ) η 0),
    u ∈
      [1, -1, IsUnit.unit (a := hζ.toInteger) ⋯, -IsUnit.unit (a := hζ.toInteger) ⋯,
        HPow.hPow (β := ℕ) (IsUnit.unit (a := hζ.toInteger) ⋯) 2,
        -HPow.hPow (β := ℕ) (IsUnit.unit (a := hζ.toInteger) ⋯) 2]
⊢ u ∈
    [1, -1, IsUnit.unit (a := hζ.toInteger) ⋯, -IsUnit.unit (a := hζ.toInteger) ⋯,
      HPow.hPow (β := ℕ) (IsUnit.unit (a := hζ.toInteger) ⋯) 2,
      -HPow.hPow (β := ℕ) (IsUnit.unit (a := hζ.toInteger) ⋯) 2]

Tactic:
rcases hru with h | h
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
u : (𝓞 K)ˣ
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
hrank : rank K = 0
x : ↥(torsion K)
e : Fin (rank K) → ℤ
hxu : u = (↑x : (𝓞 K)ˣ)
n : ℕ
hnpos : 0 < n
hn :
  HPow.hPow (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K)
      (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n hnpos) : ℕ) =
    1
hr3 : HAdd.hAdd (α := ℕ) 0 1 < 3
hru : u = η ^ HAdd.hAdd (α := ℕ) 0 1 ∨ u = -η ^ HAdd.hAdd (α := ℕ) 0 1
1 :
  ∀ (h : u = η ^ HAdd.hAdd (α := ℕ) 0 1),
    u ∈
      [1, -1, IsUnit.unit (a := hζ.toInteger) ⋯, -IsUnit.unit (a := hζ.toInteger) ⋯,
        HPow.hPow (β := ℕ) (IsUnit.unit (a := hζ.toInteger) ⋯) 2,
        -HPow.hPow (β := ℕ) (IsUnit.unit (a := hζ.toInteger) ⋯) 2]
h :
  ∀ (h : u = -η ^ HAdd.hAdd (α := ℕ) 0 1),
    u ∈
      [1, -1, IsUnit.unit (a := hζ.toInteger) ⋯, -IsUnit.unit (a := hζ.toInteger) ⋯,
        HPow.hPow (β := ℕ) (IsUnit.unit (a := hζ.toInteger) ⋯) 2,
        -HPow.hPow (β := ℕ) (IsUnit.unit (a := hζ.toInteger) ⋯) 2]
⊢ u ∈
    [1, -1, IsUnit.unit (a := hζ.toInteger) ⋯, -IsUnit.unit (a := hζ.toInteger) ⋯,
      HPow.hPow (β := ℕ) (IsUnit.unit (a := hζ.toInteger) ⋯) 2,
      -HPow.hPow (β := ℕ) (IsUnit.unit (a := hζ.toInteger) ⋯) 2]

Tactic:
rcases hru with h | h
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
u : (𝓞 K)ˣ
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
hrank : rank K = 0
x : ↥(torsion K)
e : Fin (rank K) → ℤ
hxu : u = (↑x : (𝓞 K)ˣ)
n : ℕ
hnpos : 0 < n
hn :
  HPow.hPow (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K)
      (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n hnpos) : ℕ) =
    1
hr3 : HAdd.hAdd (α := ℕ) 0 1 + 1 < 3
hru : u = η ^ (HAdd.hAdd (α := ℕ) 0 1 + 1) ∨ u = -η ^ (HAdd.hAdd (α := ℕ) 0 1 + 1)
2 :
  ∀ (h : u = η ^ (HAdd.hAdd (α := ℕ) 0 1 + 1)),
    u ∈
      [1, -1, IsUnit.unit (a := hζ.toInteger) ⋯, -IsUnit.unit (a := hζ.toInteger) ⋯,
        HPow.hPow (β := ℕ) (IsUnit.unit (a := hζ.toInteger) ⋯) 2,
        -HPow.hPow (β := ℕ) (IsUnit.unit (a := hζ.toInteger) ⋯) 2]
h :
  ∀ (h : u = -η ^ (HAdd.hAdd (α := ℕ) 0 1 + 1)),
    u ∈
      [1, -1, IsUnit.unit (a := hζ.toInteger) ⋯, -IsUnit.unit (a := hζ.toInteger) ⋯,
        HPow.hPow (β := ℕ) (IsUnit.unit (a := hζ.toInteger) ⋯) 2,
        -HPow.hPow (β := ℕ) (IsUnit.unit (a := hζ.toInteger) ⋯) 2]
⊢ u ∈
    [1, -1, IsUnit.unit (a := hζ.toInteger) ⋯, -IsUnit.unit (a := hζ.toInteger) ⋯,
      HPow.hPow (β := ℕ) (IsUnit.unit (a := hζ.toInteger) ⋯) 2,
      -HPow.hPow (β := ℕ) (IsUnit.unit (a := hζ.toInteger) ⋯) 2]

Tactic:
rcases hru with h | h
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
u : (𝓞 K)ˣ
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
hrank : rank K = 0
x : ↥(torsion K)
e : Fin (rank K) → ℤ
hxu : u = (↑x : (𝓞 K)ˣ)
n : ℕ
hnpos : 0 < n
hn :
  HPow.hPow (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K)
      (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n hnpos) : ℕ) =
    1
hr3 : LT.lt (α := ℕ) 0 3
h : u = HPow.hPow (β := ℕ) η 0
⊢ u ∈
    [1, -1, IsUnit.unit (a := hζ.toInteger) ⋯, -IsUnit.unit (a := hζ.toInteger) ⋯,
      HPow.hPow (β := ℕ) (IsUnit.unit (a := hζ.toInteger) ⋯) 2,
      -HPow.hPow (β := ℕ) (IsUnit.unit (a := hζ.toInteger) ⋯) 2]

Tactic:
simp [h]
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
u : (𝓞 K)ˣ
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
hrank : rank K = 0
x : ↥(torsion K)
e : Fin (rank K) → ℤ
hxu : u = (↑x : (𝓞 K)ˣ)
n : ℕ
hnpos : 0 < n
hn :
  HPow.hPow (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K)
      (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n hnpos) : ℕ) =
    1
hr3 : LT.lt (α := ℕ) 0 3
h : u = -HPow.hPow (β := ℕ) η 0
⊢ u ∈
    [1, -1, IsUnit.unit (a := hζ.toInteger) ⋯, -IsUnit.unit (a := hζ.toInteger) ⋯,
      HPow.hPow (β := ℕ) (IsUnit.unit (a := hζ.toInteger) ⋯) 2,
      -HPow.hPow (β := ℕ) (IsUnit.unit (a := hζ.toInteger) ⋯) 2]

Tactic:
simp [h]
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
u : (𝓞 K)ˣ
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
hrank : rank K = 0
x : ↥(torsion K)
e : Fin (rank K) → ℤ
hxu : u = (↑x : (𝓞 K)ˣ)
n : ℕ
hnpos : 0 < n
hn :
  HPow.hPow (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K)
      (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n hnpos) : ℕ) =
    1
hr3 : HAdd.hAdd (α := ℕ) 0 1 < 3
h : u = η ^ HAdd.hAdd (α := ℕ) 0 1
⊢ u ∈
    [1, -1, IsUnit.unit (a := hζ.toInteger) ⋯, -IsUnit.unit (a := hζ.toInteger) ⋯,
      HPow.hPow (β := ℕ) (IsUnit.unit (a := hζ.toInteger) ⋯) 2,
      -HPow.hPow (β := ℕ) (IsUnit.unit (a := hζ.toInteger) ⋯) 2]

Tactic:
simp [h]
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
u : (𝓞 K)ˣ
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
hrank : rank K = 0
x : ↥(torsion K)
e : Fin (rank K) → ℤ
hxu : u = (↑x : (𝓞 K)ˣ)
n : ℕ
hnpos : 0 < n
hn :
  HPow.hPow (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K)
      (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n hnpos) : ℕ) =
    1
hr3 : HAdd.hAdd (α := ℕ) 0 1 < 3
h : u = -η ^ HAdd.hAdd (α := ℕ) 0 1
⊢ u ∈
    [1, -1, IsUnit.unit (a := hζ.toInteger) ⋯, -IsUnit.unit (a := hζ.toInteger) ⋯,
      HPow.hPow (β := ℕ) (IsUnit.unit (a := hζ.toInteger) ⋯) 2,
      -HPow.hPow (β := ℕ) (IsUnit.unit (a := hζ.toInteger) ⋯) 2]

Tactic:
simp [h]
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
u : (𝓞 K)ˣ
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
hrank : rank K = 0
x : ↥(torsion K)
e : Fin (rank K) → ℤ
hxu : u = (↑x : (𝓞 K)ˣ)
n : ℕ
hnpos : 0 < n
hn :
  HPow.hPow (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K)
      (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n hnpos) : ℕ) =
    1
hr3 : HAdd.hAdd (α := ℕ) 0 1 + 1 < 3
h : u = η ^ (HAdd.hAdd (α := ℕ) 0 1 + 1)
⊢ u ∈
    [1, -1, IsUnit.unit (a := hζ.toInteger) ⋯, -IsUnit.unit (a := hζ.toInteger) ⋯,
      HPow.hPow (β := ℕ) (IsUnit.unit (a := hζ.toInteger) ⋯) 2,
      -HPow.hPow (β := ℕ) (IsUnit.unit (a := hζ.toInteger) ⋯) 2]

Tactic:
simp [h]
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
u : (𝓞 K)ˣ
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
hrank : rank K = 0
x : ↥(torsion K)
e : Fin (rank K) → ℤ
hxu : u = (↑x : (𝓞 K)ˣ)
n : ℕ
hnpos : 0 < n
hn :
  HPow.hPow (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K)
      (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n hnpos) : ℕ) =
    1
hr3 : HAdd.hAdd (α := ℕ) 0 1 + 1 < 3
h : u = -η ^ (HAdd.hAdd (α := ℕ) 0 1 + 1)
⊢ u ∈
    [1, -1, IsUnit.unit (a := hζ.toInteger) ⋯, -IsUnit.unit (a := hζ.toInteger) ⋯,
      HPow.hPow (β := ℕ) (IsUnit.unit (a := hζ.toInteger) ⋯) 2,
      -HPow.hPow (β := ℕ) (IsUnit.unit (a := hζ.toInteger) ⋯) 2]

Tactic:
simp [h]
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
h : (↑(HPow.hPow (β := ℕ) λ 2) : K) = (↑(-3 * (↑η : 𝓞 K)) : K)
⊢ HPow.hPow (β := ℕ) λ 2 = -3 * (↑η : 𝓞 K)

Tactic:
ext
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
simp : HPow.hPow (β := ℕ) (ζ - 1) 2 = HPow.hPow (β := ℕ) ζ 2 + ζ + 1 - 3 * ζ
⊢ HPow.hPow (β := ℕ) ((↑hζ.toInteger : K) - 1) 2 =
    HAdd.hAdd (β := K) (HPow.hPow (α := K) (β := ℕ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑η : 𝓞 K) : K) 2)
          ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑η : 𝓞 K) : K) +
        1 -
      HMul.hMul (α := K) (β := K) (3 : K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑η : 𝓞 K) : K)

Tactic:
simp only [RingOfIntegers.map_mk, IsUnit.unit_spec]

Premises used: NumberField.RingOfIntegers.map_mk, IsUnit.unit_spec
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
⊢ HPow.hPow (β := ℕ) (ζ - 1) 2 = HPow.hPow (β := ℕ) ζ 2 + ζ + 1 - 3 * ζ

Tactic:
ring
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
⊢ LT.lt (α := ℕ) 0 3

Tactic:
decide
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
⊢ HAdd.hAdd (β := K) (HPow.hPow (α := K) (β := ℕ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑η : 𝓞 K) : K) 2)
          ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑η : 𝓞 K) : K) +
        1 -
      HMul.hMul (α := K) (β := K) (3 : K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑η : 𝓞 K) : K) =
    0 - HMul.hMul (α := K) (β := K) (3 : K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑η : 𝓞 K) : K)

Tactic:
simpa using hζ.isRoot_cyclotomic (by decide)

Premises used: IsPrimitiveRoot.isRoot_cyclotomic
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
⊢ 0 - HMul.hMul (α := K) (β := K) (3 : K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑η : 𝓞 K) : K) =
    HMul.hMul (α := K) (β := K) (-3 : K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑η : 𝓞 K) : K)

Tactic:
ring
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
calc :
  HPow.hPow (β := ℕ) ((↑hζ.toInteger : K) - 1) 2 =
    HAdd.hAdd (β := K) (HPow.hPow (α := K) (β := ℕ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑η : 𝓞 K) : K) 2)
          ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑η : 𝓞 K) : K) +
        1 -
      HMul.hMul (α := K) (β := K) (3 : K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑η : 𝓞 K) : K)
calc₁ :
  HAdd.hAdd (β := K) (HPow.hPow (α := K) (β := ℕ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑η : 𝓞 K) : K) 2)
          ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑η : 𝓞 K) : K) +
        1 -
      HMul.hMul (α := K) (β := K) (3 : K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑η : 𝓞 K) : K) =
    0 - HMul.hMul (α := K) (β := K) (3 : K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑η : 𝓞 K) : K)
calc₂ :
  0 - HMul.hMul (α := K) (β := K) (3 : K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑η : 𝓞 K) : K) =
    HMul.hMul (α := K) (β := K) (-3 : K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑η : 𝓞 K) : K)
⊢ (↑(HPow.hPow (β := ℕ) λ 2) : K) = (↑(-3 * (↑η : 𝓞 K)) : K)

Tactic:
calc (λ ^ 2 : K) = η ^ 2 + η + 1 - 3 * η := by
        simp only [RingOfIntegers.map_mk, IsUnit.unit_spec]; ring
  _ = 0 - 3 * η := by simpa using hζ.isRoot_cyclotomic (by decide)
  _ = -3 * η := by ring
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
rw :
  HPow.hPow (β := ℕ) (↑(IsUnit.unit (a := hζ.toInteger) ⋯) : 𝓞 K) 2 + (↑(IsUnit.unit (a := hζ.toInteger) ⋯) : 𝓞 K) + 1 =
    0
⊢ HPow.hPow (β := ℕ) (↑(IsUnit.unit (a := hζ.toInteger) ⋯) : 𝓞 K) 2 = -(↑(IsUnit.unit (a := hζ.toInteger) ⋯) : 𝓞 K) - 1

Tactic:
rw [← neg_add', ← add_eq_zero_iff_eq_neg, ← add_assoc]

Premises used: add_assoc, add_eq_zero_iff_eq_neg, neg_add'
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
h :
  (↑(HPow.hPow (β := ℕ) (↑(IsUnit.unit (a := hζ.toInteger) ⋯) : 𝓞 K) 2 + (↑(IsUnit.unit (a := hζ.toInteger) ⋯) : 𝓞 K) +
          1) :
      K) =
    (↑0 : K)
⊢ HPow.hPow (β := ℕ) (↑(IsUnit.unit (a := hζ.toInteger) ⋯) : 𝓞 K) 2 + (↑(IsUnit.unit (a := hζ.toInteger) ⋯) : 𝓞 K) + 1 =
    0

Tactic:
ext
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
⊢ (↑(HPow.hPow (β := ℕ) (↑(IsUnit.unit (a := hζ.toInteger) ⋯) : 𝓞 K) 2 + (↑(IsUnit.unit (a := hζ.toInteger) ⋯) : 𝓞 K) +
          1) :
      K) =
    (↑0 : K)

Tactic:
simpa using hζ.isRoot_cyclotomic (by decide)

Premises used: IsPrimitiveRoot.isRoot_cyclotomic
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
u : (𝓞 K)ˣ
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
hcong : ∃ (n : ℤ), HPow.hPow (β := ℕ) λ 2 ∣ (↑u : 𝓞 K) - (↑n : 𝓞 K)
obtain :
  ∀ (n : ℤ) (x : 𝓞 K) (hx : (↑u : 𝓞 K) - (↑n : 𝓞 K) = HPow.hPow (β := ℕ) λ 2 * x),
    ∃ (n : ℤ), 3 ∣ (↑u : 𝓞 K) - (↑n : 𝓞 K)
⊢ ∃ (n : ℤ), 3 ∣ (↑u : 𝓞 K) - (↑n : 𝓞 K)

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