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
n : ℤ
x : 𝓞 K
hx : (↑u : 𝓞 K) - (↑n : 𝓞 K) = HPow.hPow (β := ℕ) λ 2 * x
rw : (↑u : 𝓞 K) - (↑n : 𝓞 K) = 3 * -(↑η : 𝓞 K) * x
rw₁ : (↑u : 𝓞 K) - (↑n : 𝓞 K) = -(3 * (↑η : 𝓞 K)) * x
rw₂ : (↑u : 𝓞 K) - (↑n : 𝓞 K) = -3 * (↑η : 𝓞 K) * x
rw₃ : (↑u : 𝓞 K) - (↑n : 𝓞 K) = HPow.hPow (β := ℕ) λ 2 * x
rw₄ rw₅ : HPow.hPow (β := ℕ) λ 2 * x = HPow.hPow (β := ℕ) λ 2 * x
⊢ (↑u : 𝓞 K) - (↑n : 𝓞 K) = 3 * (-(↑η : 𝓞 K) * x)

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

Premises used: mul_assoc, neg_mul, _private.0.IsCyclotomicExtension.Rat.Three.lambda_sq, mul_neg
-- 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
n : ℤ
x : 𝓞 K
hx : (↑u : 𝓞 K) - (↑n : 𝓞 K) = HPow.hPow (β := ℕ) λ 2 * x
⊢ ∃ (n : ℤ), 3 ∣ (↑u : 𝓞 K) - (↑n : 𝓞 K)

Tactic:
exact ⟨n, -η * x, by rw [← mul_assoc, mul_neg, ← neg_mul, ← lambda_sq, hx]⟩
-- 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)
⊢ ∃ (n : ℤ), 3 ∣ (↑u : 𝓞 K) - (↑n : 𝓞 K)

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]⟩
-- 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 : ℤ), 3 ∣ (↑u : 𝓞 K) - (↑n : 𝓞 K)
⊢ 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:
have := Units.mem hζ u
-- 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 : ℤ), 3 ∣ (↑u : 𝓞 K) - (↑n : 𝓞 K)
this :
  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]
0 :
  ∀ (hcong : ∃ (n : ℤ), 3 ∣ HSub.hSub (α := 𝓞 K) (↑1 : 𝓞 K) (↑n : 𝓞 K)),
    Eq.{u_1 + 1} (α := (𝓞 K)ˣ) 1 1 ∨ Eq.{u_1 + 1} (α := (𝓞 K)ˣ) 1 (-1)
1 :
  ∀ (hcong : ∃ (n : ℤ), 3 ∣ HSub.hSub (α := 𝓞 K) (↑(-1) : 𝓞 K) (↑n : 𝓞 K)),
    Eq.{u_1 + 1} (α := (𝓞 K)ˣ) (-1) 1 ∨ Eq.{u_1 + 1} (α := (𝓞 K)ˣ) (-1) (-1)
2 :
  ∀ (hcong : ∃ (n : ℤ), 3 ∣ (↑(IsUnit.unit (a := hζ.toInteger) ⋯) : 𝓞 K) - (↑n : 𝓞 K)),
    IsUnit.unit (a := hζ.toInteger) ⋯ = 1 ∨ IsUnit.unit (a := hζ.toInteger) ⋯ = -1
3 :
  ∀ (hcong : ∃ (n : ℤ), 3 ∣ (↑(-IsUnit.unit (a := hζ.toInteger) ⋯) : 𝓞 K) - (↑n : 𝓞 K)),
    -IsUnit.unit (a := hζ.toInteger) ⋯ = 1 ∨ -IsUnit.unit (a := hζ.toInteger) ⋯ = -1
4 :
  ∀ (hcong : ∃ (n : ℤ), 3 ∣ (↑(HPow.hPow (β := ℕ) (IsUnit.unit (a := hζ.toInteger) ⋯) 2) : 𝓞 K) - (↑n : 𝓞 K)),
    HPow.hPow (β := ℕ) (IsUnit.unit (a := hζ.toInteger) ⋯) 2 = 1 ∨
      HPow.hPow (β := ℕ) (IsUnit.unit (a := hζ.toInteger) ⋯) 2 = -1
5 :
  ∀ (hcong : ∃ (n : ℤ), 3 ∣ (↑(-HPow.hPow (β := ℕ) (IsUnit.unit (a := hζ.toInteger) ⋯) 2) : 𝓞 K) - (↑n : 𝓞 K)),
    -HPow.hPow (β := ℕ) (IsUnit.unit (a := hζ.toInteger) ⋯) 2 = 1 ∨
      -HPow.hPow (β := ℕ) (IsUnit.unit (a := hζ.toInteger) ⋯) 2 = -1
⊢ u = 1 ∨ u = -1

Tactic:
fin_cases this
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
hcong : ∃ (n : ℤ), 3 ∣ HSub.hSub (α := 𝓞 K) (↑1 : 𝓞 K) (↑n : 𝓞 K)
0 : Eq.{u_1 + 1} (α := (𝓞 K)ˣ) 1 1
⊢ Eq.{u_1 + 1} (α := (𝓞 K)ˣ) 1 1 ∨ Eq.{u_1 + 1} (α := (𝓞 K)ˣ) 1 (-1)

Tactic:
left
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
hcong : ∃ (n : ℤ), 3 ∣ HSub.hSub (α := 𝓞 K) (↑1 : 𝓞 K) (↑n : 𝓞 K)
⊢ Eq.{u_1 + 1} (α := (𝓞 K)ˣ) 1 1

Tactic:
rfl
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
hcong : ∃ (n : ℤ), 3 ∣ HSub.hSub (α := 𝓞 K) (↑(-1) : 𝓞 K) (↑n : 𝓞 K)
1 : Eq.{u_1 + 1} (α := (𝓞 K)ˣ) (-1) (-1)
⊢ Eq.{u_1 + 1} (α := (𝓞 K)ˣ) (-1) 1 ∨ Eq.{u_1 + 1} (α := (𝓞 K)ˣ) (-1) (-1)

Tactic:
right
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
hcong : ∃ (n : ℤ), 3 ∣ HSub.hSub (α := 𝓞 K) (↑(-1) : 𝓞 K) (↑n : 𝓞 K)
⊢ Eq.{u_1 + 1} (α := (𝓞 K)ˣ) (-1) (-1)

Tactic:
rfl
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
hcong : ∃ (n : ℤ), 3 ∣ (↑(IsUnit.unit (a := hζ.toInteger) ⋯) : 𝓞 K) - (↑n : 𝓞 K)
2 : False
⊢ IsUnit.unit (a := hζ.toInteger) ⋯ = 1 ∨ IsUnit.unit (a := hζ.toInteger) ⋯ = -1

Tactic:
exfalso
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
hcong : ∃ (n : ℤ), 3 ∣ (↑(-IsUnit.unit (a := hζ.toInteger) ⋯) : 𝓞 K) - (↑n : 𝓞 K)
3 : False
⊢ -IsUnit.unit (a := hζ.toInteger) ⋯ = 1 ∨ -IsUnit.unit (a := hζ.toInteger) ⋯ = -1

Tactic:
exfalso
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
hcong : ∃ (n : ℤ), 3 ∣ (↑(HPow.hPow (β := ℕ) (IsUnit.unit (a := hζ.toInteger) ⋯) 2) : 𝓞 K) - (↑n : 𝓞 K)
4 : False
⊢ HPow.hPow (β := ℕ) (IsUnit.unit (a := hζ.toInteger) ⋯) 2 = 1 ∨
    HPow.hPow (β := ℕ) (IsUnit.unit (a := hζ.toInteger) ⋯) 2 = -1

Tactic:
exfalso
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
hcong : ∃ (n : ℤ), 3 ∣ (↑(-HPow.hPow (β := ℕ) (IsUnit.unit (a := hζ.toInteger) ⋯) 2) : 𝓞 K) - (↑n : 𝓞 K)
5 : False
⊢ -HPow.hPow (β := ℕ) (IsUnit.unit (a := hζ.toInteger) ⋯) 2 = 1 ∨
    -HPow.hPow (β := ℕ) (IsUnit.unit (a := hζ.toInteger) ⋯) 2 = -1

Tactic:
exfalso
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
hcong : ∃ (n : ℤ), 3 ∣ (↑(IsUnit.unit (a := hζ.toInteger) ⋯) : 𝓞 K) - (↑n : 𝓞 K)
⊢ Ne (α := ℕ) 3 2

Tactic:
decide
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
hcong : ∃ (n : ℤ), 3 ∣ (↑(IsUnit.unit (a := hζ.toInteger) ⋯) : 𝓞 K) - (↑n : 𝓞 K)
⊢ False

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

Premises used: IsPrimitiveRoot.not_exists_int_prime_dvd_sub_of_prime_ne_two'
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
hcong : ∃ (n : ℤ), 3 ∣ (↑(-IsUnit.unit (a := hζ.toInteger) ⋯) : 𝓞 K) - (↑n : 𝓞 K)
⊢ Ne (α := ℕ) 3 2

Tactic:
decide
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
hcong : ∃ (n : ℤ), 3 ∣ (↑(-IsUnit.unit (a := hζ.toInteger) ⋯) : 𝓞 K) - (↑n : 𝓞 K)
3 : ∃ (n : ℤ), (↑3 : 𝓞 K) ∣ hζ.toInteger - (↑n : 𝓞 K)
⊢ False

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

Premises used: IsPrimitiveRoot.not_exists_int_prime_dvd_sub_of_prime_ne_two'
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
hcong : ∃ (n : ℤ), 3 ∣ (↑(-IsUnit.unit (a := hζ.toInteger) ⋯) : 𝓞 K) - (↑n : 𝓞 K)
3 :
  ∀ (n : ℤ) (x : 𝓞 K) (hx : (↑(-IsUnit.unit (a := hζ.toInteger) ⋯) : 𝓞 K) - (↑n : 𝓞 K) = 3 * x),
    ∃ (n : ℤ), (↑3 : 𝓞 K) ∣ hζ.toInteger - (↑n : 𝓞 K)
⊢ ∃ (n : ℤ), (↑3 : 𝓞 K) ∣ hζ.toInteger - (↑n : 𝓞 K)

Tactic:
obtain ⟨n, x, hx⟩ := hcong
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
n : ℤ
x : 𝓞 K
hx : (↑(-IsUnit.unit (a := hζ.toInteger) ⋯) : 𝓞 K) - (↑n : 𝓞 K) = 3 * x
⊢ (↑(-IsUnit.unit (a := hζ.toInteger) ⋯) : 𝓞 K) = 3 * x + (↑n : 𝓞 K)

Tactic:
rw [sub_eq_iff_eq_add] at hx

Premises used: sub_eq_iff_eq_add
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
n : ℤ
x : 𝓞 K
hx : (↑(-IsUnit.unit (a := hζ.toInteger) ⋯) : 𝓞 K) = 3 * x + (↑n : 𝓞 K)
⊢ ∃ (n : ℤ), (↑3 : 𝓞 K) ∣ hζ.toInteger - (↑n : 𝓞 K)

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

Premises used: Iff.mpr, sub_eq_iff_eq_add, Exists.intro, Neg.neg
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
n : ℤ
x : 𝓞 K
hx : (↑(-IsUnit.unit (a := hζ.toInteger) ⋯) : 𝓞 K) = 3 * x + (↑n : 𝓞 K)
3 : hζ.toInteger = (↑3 : 𝓞 K) * -x + (↑(-n) : 𝓞 K)
⊢ ∃ (n : ℤ), (↑3 : 𝓞 K) ∣ hζ.toInteger - (↑n : 𝓞 K)

Tactic:
refine ⟨-n, -x, sub_eq_iff_eq_add.2 ?_⟩
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
n : ℤ
x : 𝓞 K
hx : (↑(-IsUnit.unit (a := hζ.toInteger) ⋯) : 𝓞 K) = 3 * x + (↑n : 𝓞 K)
⊢ hζ.toInteger = (↑3 : 𝓞 K) * -x + (↑(-n) : 𝓞 K)

Tactic:
simp only [Nat.cast_ofNat, mul_neg, Int.cast_neg, ← neg_add, ← hx, Units.val_neg,
      IsUnit.unit_spec, RingOfIntegers.neg_mk, neg_neg]

Premises used: Int.cast_neg, Nat.cast_ofNat, neg_add, neg_neg, Units.val_neg, NumberField.RingOfIntegers.neg_mk, IsUnit.unit_spec, mul_neg
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
hcong : ∃ (n : ℤ), 3 ∣ (↑(HPow.hPow (β := ℕ) (IsUnit.unit (a := hζ.toInteger) ⋯) 2) : 𝓞 K) - (↑n : 𝓞 K)
⊢ Nat.Coprime 2 3

Tactic:
decide
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
hcong : ∃ (n : ℤ), 3 ∣ (↑(HPow.hPow (β := ℕ) (IsUnit.unit (a := hζ.toInteger) ⋯) 2) : 𝓞 K) - (↑n : 𝓞 K)
⊢ Ne (α := ℕ) 3 2

Tactic:
decide
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
hcong : ∃ (n : ℤ), 3 ∣ (↑(HPow.hPow (β := ℕ) (IsUnit.unit (a := hζ.toInteger) ⋯) 2) : 𝓞 K) - (↑n : 𝓞 K)
⊢ False

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

Premises used: IsPrimitiveRoot.not_exists_int_prime_dvd_sub_of_prime_ne_two', IsPrimitiveRoot.pow_of_coprime, OfNat.ofNat
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
hcong : ∃ (n : ℤ), 3 ∣ (↑(-HPow.hPow (β := ℕ) (IsUnit.unit (a := hζ.toInteger) ⋯) 2) : 𝓞 K) - (↑n : 𝓞 K)
⊢ Nat.Coprime 2 3

Tactic:
decide
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
hcong : ∃ (n : ℤ), 3 ∣ (↑(-HPow.hPow (β := ℕ) (IsUnit.unit (a := hζ.toInteger) ⋯) 2) : 𝓞 K) - (↑n : 𝓞 K)
⊢ Ne (α := ℕ) 3 2

Tactic:
decide
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
hcong : ∃ (n : ℤ), 3 ∣ (↑(-HPow.hPow (β := ℕ) (IsUnit.unit (a := hζ.toInteger) ⋯) 2) : 𝓞 K) - (↑n : 𝓞 K)
5 : ∃ (n : ℤ), (↑3 : 𝓞 K) ∣ ⋯.toInteger - (↑n : 𝓞 K)
⊢ False

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

Premises used: IsPrimitiveRoot.not_exists_int_prime_dvd_sub_of_prime_ne_two', IsPrimitiveRoot.pow_of_coprime, OfNat.ofNat
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
hcong : ∃ (n : ℤ), 3 ∣ (↑(-HPow.hPow (β := ℕ) (IsUnit.unit (a := hζ.toInteger) ⋯) 2) : 𝓞 K) - (↑n : 𝓞 K)
5 :
  ∀ (n : ℤ) (x : 𝓞 K) (hx : (↑(-HPow.hPow (β := ℕ) (IsUnit.unit (a := hζ.toInteger) ⋯) 2) : 𝓞 K) - (↑n : 𝓞 K) = 3 * x),
    ∃ (n : ℤ), (↑3 : 𝓞 K) ∣ ⋯.toInteger - (↑n : 𝓞 K)
⊢ ∃ (n : ℤ), (↑3 : 𝓞 K) ∣ ⋯.toInteger - (↑n : 𝓞 K)

Tactic:
obtain ⟨n, x, hx⟩ := hcong
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
n : ℤ
x : 𝓞 K
hx : (↑(-HPow.hPow (β := ℕ) (IsUnit.unit (a := hζ.toInteger) ⋯) 2) : 𝓞 K) - (↑n : 𝓞 K) = 3 * x
⊢ ∃ (n : ℤ), (↑3 : 𝓞 K) ∣ ⋯.toInteger - (↑n : 𝓞 K)

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

Premises used: Iff.mpr, sub_eq_iff_eq_add, Exists.intro, Neg.neg
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
n : ℤ
x : 𝓞 K
hx : (↑(-HPow.hPow (β := ℕ) (IsUnit.unit (a := hζ.toInteger) ⋯) 2) : 𝓞 K) - (↑n : 𝓞 K) = 3 * x
5 : ⋯.toInteger = (↑3 : 𝓞 K) * -x + (↑(-n) : 𝓞 K)
⊢ ∃ (n : ℤ), (↑3 : 𝓞 K) ∣ ⋯.toInteger - (↑n : 𝓞 K)

Tactic:
refine ⟨-n, -x, sub_eq_iff_eq_add.2 ?_⟩
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
n : ℤ
x : 𝓞 K
hx : (↑(-HPow.hPow (β := ℕ) (IsUnit.unit (a := hζ.toInteger) ⋯) 2) : 𝓞 K) - (↑n : 𝓞 K) = 3 * x
⊢ Nat.Coprime 2 3

Tactic:
decide
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
n : ℤ
x : 𝓞 K
hx : (↑(-HPow.hPow (β := ℕ) (IsUnit.unit (a := hζ.toInteger) ⋯) 2) : 𝓞 K) - (↑n : 𝓞 K) = 3 * x
h : (↑⋯.toInteger : K) = (↑(HPow.hPow (β := ℕ) hζ.toInteger 2) : K)
⊢ ⋯.toInteger = HPow.hPow (β := ℕ) hζ.toInteger 2

Tactic:
ext
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
n : ℤ
x : 𝓞 K
hx : (↑(-HPow.hPow (β := ℕ) (IsUnit.unit (a := hζ.toInteger) ⋯) 2) : 𝓞 K) - (↑n : 𝓞 K) = 3 * x
⊢ (↑⋯.toInteger : K) = (↑(HPow.hPow (β := ℕ) hζ.toInteger 2) : K)

Tactic:
simp
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
n : ℤ
x : 𝓞 K
hx : (↑(-HPow.hPow (β := ℕ) (IsUnit.unit (a := hζ.toInteger) ⋯) 2) : 𝓞 K) - (↑n : 𝓞 K) = 3 * x
⊢ ⋯.toInteger = HPow.hPow (β := ℕ) hζ.toInteger 2

Tactic:
have : (hζ.pow_of_coprime 2 (by decide)).toInteger = hζ.toInteger ^ 2 := by ext; simp
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
n : ℤ
x : 𝓞 K
hx : (↑(-HPow.hPow (β := ℕ) (IsUnit.unit (a := hζ.toInteger) ⋯) 2) : 𝓞 K) - (↑n : 𝓞 K) = 3 * x
this : ⋯.toInteger = HPow.hPow (β := ℕ) hζ.toInteger 2
⊢ ⋯.toInteger = (↑3 : 𝓞 K) * -x + (↑(-n) : 𝓞 K)

Tactic:
simp only [this, 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]

Premises used: Int.cast_neg, Nat.cast_ofNat, neg_add, neg_neg, Units.val_neg, sub_eq_iff_eq_add, Iff.mp, Units.val_pow_eq_pow_val, IsUnit.unit_spec, mul_neg
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
x : 𝓞 K
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
⊢ LT.lt (α := ℕ) 1 3

Tactic:
decide
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
x : 𝓞 K
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
⊢ Finite.{u_1 + 1} (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ}))

Tactic:
have := hζ.finite_quotient_toInteger_sub_one (by decide)
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
x : 𝓞 K
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
this : Finite.{u_1 + 1} (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ}))
x_1 : Fintype (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ})) :=
  Fintype.ofFinite (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ}))
x_2 : Ring (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ})) := CommRing.toRing
x_3 : AddGroup (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ})) := AddGroupWithOne.toAddGroup
⊢ Membership.mem (α := HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ})) (γ :=
    Finset (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ}))) Finset.univ
    ((Ideal.Quotient.mk (Ideal.span {λ}) : (a : 𝓞 K) → 𝓞 K ⧸ Ideal.span {λ}) x :
      HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ}))

Tactic:
have := Finset.mem_univ (Ideal.Quotient.mk (Ideal.span {λ}) x)
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
x : 𝓞 K
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
this_1 : Finite.{u_1 + 1} (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ}))
x_1 : Fintype (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ})) :=
  Fintype.ofFinite (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ}))
x_2 : Ring (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ})) := CommRing.toRing
x_3 : AddGroup (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ})) := AddGroupWithOne.toAddGroup
this :
  Membership.mem (α := HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ})) (γ :=
    Finset (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ}))) Finset.univ
    ((Ideal.Quotient.mk (Ideal.span {λ}) : (a : 𝓞 K) → 𝓞 K ⧸ Ideal.span {λ}) x :
      HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ}))
⊢ Ne (α := ℕ) 3 2

Tactic:
decide
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
x : 𝓞 K
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
this_1 : Finite.{u_1 + 1} (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ}))
x_1 : Fintype (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ})) :=
  Fintype.ofFinite (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ}))
x_2 : Ring (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ})) := CommRing.toRing
x_3 : AddGroup (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ})) := AddGroupWithOne.toAddGroup
this :
  Membership.mem (α := HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ})) (γ :=
    Finset (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ}))) Finset.univ
    ((Ideal.Quotient.mk (Ideal.span {λ}) : (a : 𝓞 K) → 𝓞 K ⧸ Ideal.span {λ}) x :
      HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ}))
rw : Int.natAbs (↑3 : ℤ) = 3
⊢ Fintype.card.{u_1} (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ})) = 3

Tactic:
rw [← Nat.card_eq_fintype_card, hζ.card_quotient_toInteger_sub_one,
      hζ.norm_toInteger_sub_one_of_prime_ne_two' (by decide)]

Premises used: IsPrimitiveRoot.card_quotient_toInteger_sub_one, IsPrimitiveRoot.norm_toInteger_sub_one_of_prime_ne_two', Nat.card_eq_fintype_card
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
x : 𝓞 K
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
this_1 : Finite.{u_1 + 1} (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ}))
x_1 : Fintype (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ})) :=
  Fintype.ofFinite (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ}))
x_2 : Ring (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ})) := CommRing.toRing
x_3 : AddGroup (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ})) := AddGroupWithOne.toAddGroup
this :
  Membership.mem (α := HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ})) (γ :=
    Finset (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ}))) Finset.univ
    ((Ideal.Quotient.mk (Ideal.span {λ}) : (a : 𝓞 K) → 𝓞 K ⧸ Ideal.span {λ}) x :
      HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ}))
⊢ Int.natAbs (↑3 : ℤ) = 3

Tactic:
simp only [Nat.cast_ofNat, Int.reduceAbs]

Premises used: Nat.cast_ofNat, Int.reduceAbs
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
x : 𝓞 K
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
this_1 : Finite.{u_1 + 1} (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ}))
x_1 : Fintype (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ})) :=
  Fintype.ofFinite (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ}))
x_2 : Ring (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ})) := CommRing.toRing
x_3 : AddGroup (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ})) := AddGroupWithOne.toAddGroup
this :
  Membership.mem (α := HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ})) (γ :=
    Finset (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ}))) Finset.univ
    ((Ideal.Quotient.mk (Ideal.span {λ}) : (a : 𝓞 K) → 𝓞 K ⧸ Ideal.span {λ}) x :
      HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ}))
⊢ Fintype.card.{u_1} (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ})) = 3

Tactic:
have h3 : Fintype.card (𝓞 K ⧸ Ideal.span {λ}) = 3 := by
    rw [← Nat.card_eq_fintype_card, hζ.card_quotient_toInteger_sub_one,
      hζ.norm_toInteger_sub_one_of_prime_ne_two' (by decide)]
    simp only [Nat.cast_ofNat, Int.reduceAbs]