-- Mathlib/NumberTheory/Cyclotomic/Three.lean
/-- If `λ` divides `x - 1`, then `λ ^ 4` divides `x ^ 3 - 1`. -/
lemma lambda_pow_four_dvd_cube_sub_one_of_dvd_sub_one {x : 𝓞 K} (h : λ ∣ x - 1) :
    λ ^ 4 ∣ x ^ 3 - 1

Proof state:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
x y : 𝓞 K
hy : x - 1 = λ * y
⊢ (x - 1) * (x - hζ.toInteger) * (x - hζ.toInteger ^ 2) = (x - 1) * (x - 1 - λ) * (x - 1 - λ * (hζ.toInteger + 1))

Tactic:
ring

Result:
no goals

Proof state:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
x y : 𝓞 K
hy : x - 1 = λ * y
⊢ (x - 1) * (x - 1 - λ) * (x - 1 - λ * (↑η + 1)) = λ ^ 3 * (y * (y - 1) * (y - (↑η + 1)))

Tactic:
rw [hy]

Result:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
x y : 𝓞 K
hy : x - 1 = λ * y
⊢ λ * y * (λ * y - λ) * (λ * y - λ * (↑η + 1)) = λ ^ 3 * (y * (y - 1) * (y - (↑η + 1)))

Proof state:
case intro
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
x y : 𝓞 K
hy : x - 1 = λ * y
this : x ^ 3 - 1 = λ ^ 3 * (y * (y - 1) * (y - (↑η + 1)))
⊢ λ ^ 3 * λ ∣ λ ^ 3 * (y * (y - 1) * (y - (↑η + 1)))

Tactic:
exact mul_dvd_mul_left _ (lambda_dvd_mul_sub_one_mul_sub_eta_add_one hζ y)

Result:
no goals

Proof state:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
x y : 𝓞 K
hy : x - 1 = λ * y
⊢ λ * y * (λ * y - λ) * (λ * y - λ * (↑η + 1)) = λ ^ 3 * (y * (y - 1) * (y - (↑η + 1)))

Tactic:
ring

Result:
no goals

Proof state:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
x : 𝓞 K
h : λ ∣ x - 1
⊢ λ ^ 4 ∣ x ^ 3 - 1

Tactic:
obtain ⟨y, hy⟩ := h

Result:
case intro
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
x y : 𝓞 K
hy : x - 1 = λ * y
⊢ λ ^ 4 ∣ x ^ 3 - 1

Proof state:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
x y : 𝓞 K
hy : x - 1 = λ * y
⊢ x ^ 3 - 1 = λ ^ 3 * (y * (y - 1) * (y - (↑η + 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

Result:
no goals

Proof state:
case intro
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
x y : 𝓞 K
hy : x - 1 = λ * y
⊢ λ ^ 4 ∣ x ^ 3 - 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

Result:
case intro
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
x y : 𝓞 K
hy : x - 1 = λ * y
this : x ^ 3 - 1 = λ ^ 3 * (y * (y - 1) * (y - (↑η + 1)))
⊢ λ ^ 4 ∣ x ^ 3 - 1

Proof state:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
x y : 𝓞 K
hy : x - 1 = λ * y
⊢ x ^ 3 - 1 = (x - 1) * (x - 1 - λ) * (x - 1 - λ * (↑η + 1))

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

Result:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
x y : 𝓞 K
hy : x - 1 = λ * y
⊢ (x - 1) * (x - hζ.toInteger) * (x - hζ.toInteger ^ 2) = (x - 1) * (x - 1 - λ) * (x - 1 - λ * (hζ.toInteger + 1))

Proof state:
case intro
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
x y : 𝓞 K
hy : x - 1 = λ * y
this : x ^ 3 - 1 = λ ^ 3 * (y * (y - 1) * (y - (↑η + 1)))
⊢ λ ^ 4 ∣ x ^ 3 - 1

Tactic:
rw [this, pow_succ]

Result:
case intro
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
x y : 𝓞 K
hy : x - 1 = λ * y
this : x ^ 3 - 1 = λ ^ 3 * (y * (y - 1) * (y - (↑η + 1)))
⊢ λ ^ 3 * λ ∣ λ ^ 3 * (y * (y - 1) * (y - (↑η + 1)))