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
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
h3 : Fintype.card.{u_1} (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ})) = 3
h :
  Eq (α := HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ}))
    ((Ideal.Quotient.mk (Ideal.span {λ}) : (a : 𝓞 K) → 𝓞 K ⧸ Ideal.span {λ}) x :
      HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ}))
    (-1 : HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ}))
inr :
  HAdd.hAdd (α := HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ})) (β :=
      HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ}))
      ((Ideal.Quotient.mk (Ideal.span {λ}) : (a : 𝓞 K) → 𝓞 K ⧸ Ideal.span {λ}) x :
        HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ}))
      ((Ideal.Quotient.mk (Ideal.span {λ}) : (a : 𝓞 K) → 𝓞 K ⧸ Ideal.span {λ}) 1 :
        HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ})) =
    0
inr₁ :
  HAdd.hAdd (α := HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ})) (-1)
      ((Ideal.Quotient.mk (Ideal.span {λ}) : (a : 𝓞 K) → 𝓞 K ⧸ Ideal.span {λ}) 1) =
    0
inr₂ : HAdd.hAdd (α := HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ})) (-1) 1 = 0
inr₃ inr₄ : Eq.{u_1 + 1} (α := HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ})) 0 0
⊢ Eq (α := HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ}))
    ((Ideal.Quotient.mk (Ideal.span {λ}) : (a : 𝓞 K) → 𝓞 K ⧸ Ideal.span {λ}) (x + 1) :
      HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ}))
    (0 : HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ}))

Tactic:
rw [RingHom.map_add, h, RingHom.map_one, neg_add_cancel]

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

Tactic:
rw [eta_sq]

Premises used: IsCyclotomicExtension.Rat.Three.eta_sq
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
⊢ -(↑(IsUnit.unit (a := hζ.toInteger) ⋯) : 𝓞 K) - 1 + (↑(IsUnit.unit (a := hζ.toInteger) ⋯) : 𝓞 K) + 1 = 0

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

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

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

Tactic:
simp [hζ.toInteger_cube_eq_one]

Premises used: IsPrimitiveRoot.toInteger_cube_eq_one
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
x : 𝓞 K
rw : HPow.hPow (β := ℕ) x 3 - HPow.hPow (β := ℕ) x 2 * 0 + x * 0 - 1 = HPow.hPow (β := ℕ) x 3 - 1
⊢ HPow.hPow (β := ℕ) x 3 - HPow.hPow (β := ℕ) x 2 * (HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 + (↑η : 𝓞 K) + 1) +
        x * (HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 + (↑η : 𝓞 K) + 1) -
      1 =
    HPow.hPow (β := ℕ) x 3 - 1

Tactic:
rw [eta_sq_add_eta_add_one hζ]

Premises used: IsCyclotomicExtension.Rat.Three.eta_sq_add_eta_add_one
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
x : 𝓞 K
⊢ HPow.hPow (β := ℕ) x 3 - HPow.hPow (β := ℕ) x 2 * 0 + x * 0 - 1 = HPow.hPow (β := ℕ) x 3 - 1

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

Tactic:
calc _ = x ^ 3 - x ^ 2 * (η ^ 2 + η + 1) + x * (η ^ 2 + η + η ^ 3) - η ^ 3 := by ring
  _ = x ^ 3 - x ^ 2 * (η ^ 2 + η + 1) + x * (η ^ 2 + η + 1) - 1 := by
    simp [hζ.toInteger_cube_eq_one]
  _ = x ^ 3 - 1 := by rw [eta_sq_add_eta_add_one hζ]; ring
-- 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
inl : ∀ (h : λ ∣ x), λ ∣ x * (x - 1) * (x - ((↑(IsUnit.unit (a := hζ.toInteger) ⋯) : 𝓞 K) + 1))
inr : ∀ (h : λ ∣ x - 1), λ ∣ x * (x - 1) * (x - ((↑(IsUnit.unit (a := hζ.toInteger) ⋯) : 𝓞 K) + 1))
inr₁ : ∀ (h : λ ∣ x + 1), λ ∣ x * (x - 1) * (x - ((↑(IsUnit.unit (a := hζ.toInteger) ⋯) : 𝓞 K) + 1))
⊢ λ ∣ x * (x - 1) * (x - ((↑(IsUnit.unit (a := hζ.toInteger) ⋯) : 𝓞 K) + 1))

Tactic:
rcases lambda_dvd_or_dvd_sub_one_or_dvd_add_one hζ x with h | h | h

Premises used: IsCyclotomicExtension.Rat.Three.lambda_dvd_or_dvd_sub_one_or_dvd_add_one
-- 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
h : λ ∣ x
⊢ λ ∣ x * (x - 1) * (x - ((↑(IsUnit.unit (a := hζ.toInteger) ⋯) : 𝓞 K) + 1))

Tactic:
dvd_mul_of_dvd_left (dvd_mul_of_dvd_left h _) _

Premises used: dvd_mul_of_dvd_left
-- 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
h : λ ∣ x
⊢ λ ∣ x * (x - 1) * (x - ((↑(IsUnit.unit (a := hζ.toInteger) ⋯) : 𝓞 K) + 1))

Tactic:
exact dvd_mul_of_dvd_left (dvd_mul_of_dvd_left h _) _

Premises used: dvd_mul_of_dvd_left
-- 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
h : λ ∣ x - 1
⊢ λ ∣ x * (x - 1) * (x - ((↑(IsUnit.unit (a := hζ.toInteger) ⋯) : 𝓞 K) + 1))

Tactic:
dvd_mul_of_dvd_left (dvd_mul_of_dvd_right h _) _

Premises used: dvd_mul_of_dvd_left, dvd_mul_of_dvd_right
-- 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
h : λ ∣ x - 1
⊢ λ ∣ x * (x - 1) * (x - ((↑(IsUnit.unit (a := hζ.toInteger) ⋯) : 𝓞 K) + 1))

Tactic:
exact dvd_mul_of_dvd_left (dvd_mul_of_dvd_right h _) _

Premises used: dvd_mul_of_dvd_left, dvd_mul_of_dvd_right
-- 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
h : λ ∣ x + 1
⊢ λ ∣ x * (x - 1) * (x - ((↑(IsUnit.unit (a := hζ.toInteger) ⋯) : 𝓞 K) + 1))

Tactic:
dvd_mul_of_dvd_right ?_ _

Premises used: dvd_mul_of_dvd_right
-- 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
h : λ ∣ x + 1
inr : λ ∣ x - ((↑(IsUnit.unit (a := hζ.toInteger) ⋯) : 𝓞 K) + 1)
⊢ λ ∣ x * (x - 1) * (x - ((↑(IsUnit.unit (a := hζ.toInteger) ⋯) : 𝓞 K) + 1))

Tactic:
refine dvd_mul_of_dvd_right ?_ _

Premises used: dvd_mul_of_dvd_right
-- 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
h : λ ∣ x + 1
⊢ x - ((↑η : 𝓞 K) + 1) = x + 1 - ((↑η : 𝓞 K) - 1 + 3)

Tactic:
ring
-- 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
h : λ ∣ x + 1
inr : λ ∣ x + 1 - ((↑η : 𝓞 K) - 1 + 3)
⊢ λ ∣ x - ((↑(IsUnit.unit (a := hζ.toInteger) ⋯) : 𝓞 K) + 1)

Tactic:
rw [show x - (η + 1) = x + 1 - (η - 1 + 3) by ring]
-- 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
h : λ ∣ x + 1
⊢ λ ∣ x + 1 - ((↑η : 𝓞 K) - 1 + 3)

Tactic:
dvd_sub h <| dvd_add dvd_rfl hζ.toInteger_sub_one_dvd_prime'

Premises used: dvd_sub, IsPrimitiveRoot.toInteger_sub_one_dvd_prime', dvd_rfl, dvd_add
-- 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
h : λ ∣ x + 1
⊢ λ ∣ x + 1 - ((↑η : 𝓞 K) - 1 + 3)

Tactic:
exact dvd_sub h <| dvd_add dvd_rfl hζ.toInteger_sub_one_dvd_prime'

Premises used: dvd_sub, IsPrimitiveRoot.toInteger_sub_one_dvd_prime', dvd_rfl, dvd_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
x : 𝓞 K
h : λ ∣ x - 1
obtain : ∀ (y : 𝓞 K) (hy : x - 1 = λ * y), HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) x 3 - 1
⊢ HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) x 3 - 1

Tactic:
obtain ⟨y, hy⟩ := h
-- 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
x y : 𝓞 K
hy : x - 1 = λ * y
simp :
  (x - 1) * (x - hζ.toInteger) * (x - HPow.hPow (β := ℕ) hζ.toInteger 2) =
    (x - 1) * (x - 1 - λ) * (x - 1 - λ * (hζ.toInteger + 1))
⊢ HPow.hPow (β := ℕ) x 3 - 1 = (x - 1) * (x - 1 - λ) * (x - 1 - λ * ((↑η : 𝓞 K) + 1))

Tactic:
simp only [coe_eta, cube_sub_one_eq_mul hζ x]

Premises used: IsCyclotomicExtension.Rat.Three.coe_eta, IsCyclotomicExtension.Rat.Three.cube_sub_one_eq_mul
-- 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
x y : 𝓞 K
hy : x - 1 = λ * y
⊢ (x - 1) * (x - hζ.toInteger) * (x - HPow.hPow (β := ℕ) hζ.toInteger 2) =
    (x - 1) * (x - 1 - λ) * (x - 1 - λ * (hζ.toInteger + 1))

Tactic:
ring
-- 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
x y : 𝓞 K
hy : x - 1 = λ * y
rw :
  λ * y * (λ * y - λ) * (λ * y - λ * ((↑η : 𝓞 K) + 1)) = HPow.hPow (β := ℕ) λ 3 * (y * (y - 1) * (y - ((↑η : 𝓞 K) + 1)))
⊢ (x - 1) * (x - 1 - λ) * (x - 1 - λ * ((↑η : 𝓞 K) + 1)) =
    HPow.hPow (β := ℕ) λ 3 * (y * (y - 1) * (y - ((↑η : 𝓞 K) + 1)))

Tactic:
rw [hy]
-- 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
x y : 𝓞 K
hy : x - 1 = λ * y
⊢ λ * y * (λ * y - λ) * (λ * y - λ * ((↑η : 𝓞 K) + 1)) = HPow.hPow (β := ℕ) λ 3 * (y * (y - 1) * (y - ((↑η : 𝓞 K) + 1)))

Tactic:
ring
-- 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
x y : 𝓞 K
hy : x - 1 = λ * y
calc : HPow.hPow (β := ℕ) x 3 - 1 = (x - 1) * (x - 1 - λ) * (x - 1 - λ * ((↑η : 𝓞 K) + 1))
calc₁ :
  (x - 1) * (x - 1 - λ) * (x - 1 - λ * ((↑η : 𝓞 K) + 1)) =
    HPow.hPow (β := ℕ) λ 3 * (y * (y - 1) * (y - ((↑η : 𝓞 K) + 1)))
⊢ HPow.hPow (β := ℕ) x 3 - 1 = HPow.hPow (β := ℕ) λ 3 * (y * (y - 1) * (y - ((↑η : 𝓞 K) + 1)))

Tactic:
calc _ = (x - 1) * (x - 1 - λ) * (x - 1 - λ * (η + 1)) := by
          simp only [coe_eta, cube_sub_one_eq_mul hζ x]; ring
    _ = _ := by rw [hy]; ring

Premises used: HSub.hSub, 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
x y : 𝓞 K
hy : x - 1 = λ * y
⊢ HPow.hPow (β := ℕ) x 3 - 1 = HPow.hPow (β := ℕ) λ 3 * (y * (y - 1) * (y - ((↑η : 𝓞 K) + 1)))

Tactic:
have : x ^ 3 - 1 = λ ^ 3 * (y * (y - 1) * (y - (η + 1))) := by
    calc _ = (x - 1) * (x - 1 - λ) * (x - 1 - λ * (η + 1)) := by
          simp only [coe_eta, cube_sub_one_eq_mul hζ x]; ring
    _ = _ := by rw [hy]; ring
-- 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
x y : 𝓞 K
hy : x - 1 = λ * y
this : HPow.hPow (β := ℕ) x 3 - 1 = HPow.hPow (β := ℕ) λ 3 * (y * (y - 1) * (y - ((↑η : 𝓞 K) + 1)))
rw : HPow.hPow (β := ℕ) λ 3 * λ ∣ HPow.hPow (β := ℕ) λ 3 * (y * (y - 1) * (y - ((↑η : 𝓞 K) + 1)))
⊢ HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) x 3 - 1

Tactic:
rw [this, pow_succ]

Premises used: pow_succ
-- 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
x y : 𝓞 K
hy : x - 1 = λ * y
this : HPow.hPow (β := ℕ) x 3 - 1 = HPow.hPow (β := ℕ) λ 3 * (y * (y - 1) * (y - ((↑η : 𝓞 K) + 1)))
⊢ HPow.hPow (β := ℕ) λ 3 * λ ∣ HPow.hPow (β := ℕ) λ 3 * (y * (y - 1) * (y - ((↑η : 𝓞 K) + 1)))

Tactic:
mul_dvd_mul_left _ (lambda_dvd_mul_sub_one_mul_sub_eta_add_one hζ y)

Premises used: mul_dvd_mul_left, IsCyclotomicExtension.Rat.Three.lambda_dvd_mul_sub_one_mul_sub_eta_add_one
-- 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
x y : 𝓞 K
hy : x - 1 = λ * y
this : HPow.hPow (β := ℕ) x 3 - 1 = HPow.hPow (β := ℕ) λ 3 * (y * (y - 1) * (y - ((↑η : 𝓞 K) + 1)))
⊢ HPow.hPow (β := ℕ) λ 3 * λ ∣ HPow.hPow (β := ℕ) λ 3 * (y * (y - 1) * (y - ((↑η : 𝓞 K) + 1)))

Tactic:
exact mul_dvd_mul_left _ (lambda_dvd_mul_sub_one_mul_sub_eta_add_one hζ y)

Premises used: mul_dvd_mul_left, IsCyclotomicExtension.Rat.Three.lambda_dvd_mul_sub_one_mul_sub_eta_add_one
-- 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
x : 𝓞 K
h : λ ∣ x + 1
⊢ λ ∣ -(x + 1)

Tactic:
h.neg_right

Premises used: Dvd.dvd.neg_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
x : 𝓞 K
h : λ ∣ x + 1
h₁ : -x - 1 = -(x + 1)
⊢ λ ∣ -x - 1

Tactic:
convert! h.neg_right using 1

Premises used: Dvd.dvd.neg_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
x : 𝓞 K
h : λ ∣ x + 1
⊢ -x - 1 = -(x + 1)

Tactic:
(neg_add' x 1).symm

Premises used: neg_add', OfNat.ofNat, Eq.symm
-- 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
x : 𝓞 K
h : λ ∣ x + 1
⊢ -x - 1 = -(x + 1)

Tactic:
exact (neg_add' x 1).symm

Premises used: neg_add', OfNat.ofNat, Eq.symm
-- 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
x : 𝓞 K
h : λ ∣ x + 1
⊢ λ ∣ -x - 1

Tactic:
replace h : λ ∣ -x - 1 := by
    convert! h.neg_right using 1
    exact (neg_add' x 1).symm
-- 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
x : 𝓞 K
h : λ ∣ -x - 1
⊢ HPow.hPow (β := ℕ) λ 4 ∣ -(HPow.hPow (β := ℕ) (-x) 3 - 1)

Tactic:
(lambda_pow_four_dvd_cube_sub_one_of_dvd_sub_one hζ h).neg_right

Premises used: IsCyclotomicExtension.Rat.Three.lambda_pow_four_dvd_cube_sub_one_of_dvd_sub_one, Dvd.dvd.neg_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
x : 𝓞 K
h : λ ∣ -x - 1
h₁ : HPow.hPow (β := ℕ) x 3 + 1 = -(HPow.hPow (β := ℕ) (-x) 3 - 1)
⊢ HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) x 3 + 1

Tactic:
convert! (lambda_pow_four_dvd_cube_sub_one_of_dvd_sub_one hζ h).neg_right using 1

Premises used: IsCyclotomicExtension.Rat.Three.lambda_pow_four_dvd_cube_sub_one_of_dvd_sub_one, Dvd.dvd.neg_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
x : 𝓞 K
h : λ ∣ -x - 1
⊢ HPow.hPow (β := ℕ) x 3 + 1 = -(HPow.hPow (β := ℕ) (-x) 3 - 1)

Tactic:
ring
-- 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
x : 𝓞 K
h : ¬λ ∣ x
inl :
  ∀ (H : λ ∣ x),
    HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) x 3 - 1 ∨ HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) x 3 + 1
inr :
  ∀ (H : λ ∣ x - 1),
    HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) x 3 - 1 ∨ HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) x 3 + 1
inr₁ :
  ∀ (H : λ ∣ x + 1),
    HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) x 3 - 1 ∨ HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) x 3 + 1
⊢ HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) x 3 - 1 ∨ HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) x 3 + 1

Tactic:
rcases lambda_dvd_or_dvd_sub_one_or_dvd_add_one hζ x with H | H | H

Premises used: IsCyclotomicExtension.Rat.Three.lambda_dvd_or_dvd_sub_one_or_dvd_add_one
-- 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
x : 𝓞 K
h : ¬λ ∣ x
H : λ ∣ x
⊢ HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) x 3 - 1 ∨ HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) x 3 + 1

Tactic:
contradiction
-- 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
x : 𝓞 K
h : ¬λ ∣ x
H : λ ∣ x - 1
inr : HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) x 3 - 1
⊢ HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) x 3 - 1 ∨ HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) x 3 + 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
x : 𝓞 K
h : ¬λ ∣ x
H : λ ∣ x - 1
⊢ HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) x 3 - 1

Tactic:
lambda_pow_four_dvd_cube_sub_one_of_dvd_sub_one hζ H

Premises used: IsCyclotomicExtension.Rat.Three.lambda_pow_four_dvd_cube_sub_one_of_dvd_sub_one
-- 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
x : 𝓞 K
h : ¬λ ∣ x
H : λ ∣ x - 1
⊢ HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) x 3 - 1

Tactic:
exact lambda_pow_four_dvd_cube_sub_one_of_dvd_sub_one hζ H

Premises used: IsCyclotomicExtension.Rat.Three.lambda_pow_four_dvd_cube_sub_one_of_dvd_sub_one
-- 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
x : 𝓞 K
h : ¬λ ∣ x
H : λ ∣ x + 1
inr : HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) x 3 + 1
⊢ HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) x 3 - 1 ∨ HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) x 3 + 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
x : 𝓞 K
h : ¬λ ∣ x
H : λ ∣ x + 1
⊢ HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) x 3 + 1

Tactic:
lambda_pow_four_dvd_cube_add_one_of_dvd_add_one hζ H

Premises used: IsCyclotomicExtension.Rat.Three.lambda_pow_four_dvd_cube_add_one_of_dvd_add_one
-- 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
x : 𝓞 K
h : ¬λ ∣ x
H : λ ∣ x + 1
⊢ HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) x 3 + 1

Tactic:
exact lambda_pow_four_dvd_cube_add_one_of_dvd_add_one hζ H

Premises used: IsCyclotomicExtension.Rat.Three.lambda_pow_four_dvd_cube_add_one_of_dvd_add_one
-- Module: Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind
Goal:
K : Type u_1
inst : Field K
θ : 𝓞 K
rw :
  Eq (α := ℕ) ((absNorm : (a : Ideal ℤ) → ℕ) (under ℤ (conductor ℤ θ)) : ℕ) (1 : ℕ) ↔
    Eq (α := Subalgebra ℤ (𝓞 K)) ℤ[θ] ⊤
rw₁ : Eq (α := Ideal ℤ) (under ℤ (conductor ℤ θ)) ⊤ ↔ Eq (α := Subalgebra ℤ (𝓞 K)) ℤ[θ] ⊤
rw₂ : Eq (α := Ideal (𝓞 K)) (conductor ℤ θ) ⊤ ↔ Eq (α := Subalgebra ℤ (𝓞 K)) ℤ[θ] ⊤
rw₃ rw₄ : Eq (α := Subalgebra ℤ (𝓞 K)) ℤ[θ] ⊤ ↔ Eq (α := Subalgebra ℤ (𝓞 K)) ℤ[θ] ⊤
⊢ exponent θ = 1 ↔ Eq (α := Subalgebra ℤ (𝓞 K)) ℤ[θ] ⊤

Tactic:
rw [exponent, absNorm_eq_one_iff, comap_eq_top_iff, conductor_eq_top_iff_adjoin_eq_top]

Premises used: Ideal.comap_eq_top_iff, RingOfIntegers.exponent, Ideal.absNorm_eq_one_iff, conductor_eq_top_iff_adjoin_eq_top