awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Three (goal)
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
x : 𝓞 K
⊢ HPow.hPow (β := ℕ) x 3 - 1 =
    (x - 1) * (x - (↑(IsUnit.unit (a := hζ.toInteger) ⋯) : 𝓞 K)) *
      (x - HPow.hPow (β := ℕ) (↑(IsUnit.unit (a := hζ.toInteger) ⋯) : 𝓞 K) 2)
have symm : (x - 1) * (x - (↑(IsUnit.unit (a := hζ.toInteger) sorry) : 𝓞 K)) *
    (x - HPow.hPow (β := ℕ) (↑(IsUnit.unit (a := hζ.toInteger) sorry) : 𝓞 K) 2) =
  HPow.hPow (β := ℕ) x 3 - 1
Tactic: symm
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Three (goal)
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) + 1) -
      1 =
    HPow.hPow (β := ℕ) x 3 - 1
have rw : HPow.hPow (β := ℕ) x 3 - HPow.hPow (β := ℕ) x 2 * 0 + x * 0 - 1 = HPow.hPow (β := ℕ) x 3 - 1
Tactic: rw [eta_sq_add_eta_add_one hζ]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Three (goal)
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 - 1
have calc : (x - 1) * (x - (↑(IsUnit.unit (a := hζ.toInteger) sorry) : 𝓞 K)) *
    (x - HPow.hPow (β := ℕ) (↑(IsUnit.unit (a := hζ.toInteger) sorry) : 𝓞 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: 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
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Three (goal)
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
⊢ (x - 1) * (x - (↑(IsUnit.unit (a := hζ.toInteger) ⋯) : 𝓞 K)) *
      (x - HPow.hPow (β := ℕ) (↑(IsUnit.unit (a := hζ.toInteger) ⋯) : 𝓞 K) 2) =
    HPow.hPow (β := ℕ) x 3 - 1
have 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
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
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Three (goal)
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
⊢ (x - 1) * (x - (↑(IsUnit.unit (a := hζ.toInteger) ⋯) : 𝓞 K)) *
      (x - HPow.hPow (β := ℕ) (↑(IsUnit.unit (a := hζ.toInteger) ⋯) : 𝓞 K) 2) =
    HPow.hPow (β := ℕ) x 3 - 1
have 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
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
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Three (goal)
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
x : 𝓞 K
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
⊢ λ ∣ x * (x - 1) * (x - ((↑(IsUnit.unit (a := hζ.toInteger) ⋯) : 𝓞 K) + 1))
have inl : ∀ (h : λ ∣ x), λ ∣ x * (x - 1) * (x - ((↑(IsUnit.unit (a := hζ.toInteger) sorry) : 𝓞 K) + 1))
Tactic: rcases lambda_dvd_or_dvd_sub_one_or_dvd_add_one hζ x with h | h | h
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Three (goal)
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))
⊢ λ ∣ x * (x - 1) * (x - ((↑(IsUnit.unit (a := hζ.toInteger) ⋯) : 𝓞 K) + 1))
have inr : ∀ (h : λ ∣ x - 1), λ ∣ x * (x - 1) * (x - ((↑(IsUnit.unit (a := hζ.toInteger) sorry) : 𝓞 K) + 1))
Tactic: rcases lambda_dvd_or_dvd_sub_one_or_dvd_add_one hζ x with h | h | h
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Three (goal)
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))
⊢ λ ∣ x * (x - 1) * (x - ((↑(IsUnit.unit (a := hζ.toInteger) ⋯) : 𝓞 K) + 1))
have inr₁ : ∀ (h : λ ∣ x + 1), λ ∣ x * (x - 1) * (x - ((↑(IsUnit.unit (a := hζ.toInteger) sorry) : 𝓞 K) + 1))
Tactic: rcases lambda_dvd_or_dvd_sub_one_or_dvd_add_one hζ x with h | h | h
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Three (goal)
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))
have inr : λ ∣ x - ((↑(IsUnit.unit (a := hζ.toInteger) sorry) : 𝓞 K) + 1)
Tactic: refine dvd_mul_of_dvd_right ?_ _
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Three (goal)
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 - ((↑(IsUnit.unit (a := hζ.toInteger) ⋯) : 𝓞 K) + 1)
have inr : λ ∣ x + 1 - ((↑η : 𝓞 K) - 1 + 3)
Tactic: rw [show x - (η + 1) = x + 1 - (η - 1 + 3) by ring]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Three (goal)
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
have obtain : ∀ (y : 𝓞 K) (hy : x - 1 = λ * y), HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) x 3 - 1
Tactic: obtain ⟨y, hy⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Three (goal)
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 = (x - 1) * (x - 1 - λ) * (x - 1 - λ * ((↑η : 𝓞 K) + 1))
have simp : (x - 1) * (x - hζ.toInteger) * (x - HPow.hPow (β := ℕ) hζ.toInteger 2) =
  (x - 1) * (x - 1 - λ) * (x - 1 - λ * (hζ.toInteger + 1))
Tactic: simp only [coe_eta, cube_sub_one_eq_mul hζ x]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Three (goal)
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 - 1 - λ) * (x - 1 - λ * ((↑η : 𝓞 K) + 1)) =
    HPow.hPow (β := ℕ) λ 3 * (y * (y - 1) * (y - ((↑η : 𝓞 K) + 1)))
have rw : λ * y * (λ * y - λ) * (λ * y - λ * ((↑η : 𝓞 K) + 1)) = HPow.hPow (β := ℕ) λ 3 * (y * (y - 1) * (y - ((↑η : 𝓞 K) + 1)))
Tactic: rw [hy]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Three (goal)
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)))
have calc : HPow.hPow (β := ℕ) x 3 - 1 = (x - 1) * (x - 1 - λ) * (x - 1 - λ * ((↑η : 𝓞 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
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Three (goal)
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))
⊢ HPow.hPow (β := ℕ) x 3 - 1 = HPow.hPow (β := ℕ) λ 3 * (y * (y - 1) * (y - ((↑η : 𝓞 K) + 1)))
have calc₁ : (x - 1) * (x - 1 - λ) * (x - 1 - λ * ((↑η : 𝓞 K) + 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
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Three (hypothesis)
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 (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) x 3 - 1
have this : 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
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Three (goal)
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 (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) x 3 - 1
have rw : HPow.hPow (β := ℕ) λ 3 * λ ∣ HPow.hPow (β := ℕ) λ 3 * (y * (y - 1) * (y - ((↑η : 𝓞 K) + 1)))
Tactic: rw [this, pow_succ]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Three (goal)
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
have h₁ : -x - 1 = -(x + 1)
Tactic: convert! h.neg_right using 1
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Three (hypothesis)
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
have h₁ : λ ∣ -x - 1
Tactic: replace h : λ ∣ -x - 1 := by
    convert! h.neg_right using 1
    exact (neg_add' x 1).symm
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Three (goal)
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
have h₁ : HPow.hPow (β := ℕ) x 3 + 1 = -(HPow.hPow (β := ℕ) (-x) 3 - 1)
Tactic: convert! (lambda_pow_four_dvd_cube_sub_one_of_dvd_sub_one hζ h).neg_right using 1
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Three (goal)
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
⊢ HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) x 3 - 1 ∨ HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) x 3 + 1
have inl : ∀ (H : λ ∣ x), 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
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Three (goal)
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
⊢ HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) x 3 - 1 ∨ HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) x 3 + 1
have inr : ∀ (H : λ ∣ x - 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
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Three (goal)
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
⊢ HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) x 3 - 1 ∨ HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) x 3 + 1
have inr₁ : ∀ (H : λ ∣ x + 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
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Three (goal)
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 ∨ HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) x 3 + 1
have inr : HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) x 3 - 1
Tactic: left
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Three (goal)
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 ∨ HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) x 3 + 1
have inr : HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) x 3 + 1
Tactic: right
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind (goal)
Goal:
K : Type u_1
inst : Field K
θ : 𝓞 K
⊢ exponent θ = 1 ↔ Eq (α := Subalgebra ℤ (𝓞 K)) ℤ[θ] ⊤
have rw : Eq (α := ℕ) ((absNorm : (a : Ideal ℤ) → ℕ) (under ℤ (conductor ℤ θ)) : ℕ) (1 : ℕ) ↔ Eq (α := Subalgebra ℤ (𝓞 K)) ℤ[θ] ⊤
Tactic: rw [exponent, absNorm_eq_one_iff, comap_eq_top_iff, conductor_eq_top_iff_adjoin_eq_top]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind (goal)
Goal:
K : Type u_1
inst : Field K
θ : 𝓞 K
rw :
  Eq (α := ℕ) ((absNorm : (a : Ideal ℤ) → ℕ) (under ℤ (conductor ℤ θ)) : ℕ) (1 : ℕ) ↔
    Eq (α := Subalgebra ℤ (𝓞 K)) ℤ[θ] ⊤
⊢ exponent θ = 1 ↔ Eq (α := Subalgebra ℤ (𝓞 K)) ℤ[θ] ⊤
have rw₁ : Eq (α := Ideal ℤ) (under ℤ (conductor ℤ θ)) ⊤ ↔ Eq (α := Subalgebra ℤ (𝓞 K)) ℤ[θ] ⊤
Tactic: rw [exponent, absNorm_eq_one_iff, comap_eq_top_iff, conductor_eq_top_iff_adjoin_eq_top]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind (goal)
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)) ℤ[θ] ⊤
⊢ exponent θ = 1 ↔ Eq (α := Subalgebra ℤ (𝓞 K)) ℤ[θ] ⊤
have rw₂ : Eq (α := Ideal (𝓞 K)) (conductor ℤ θ) ⊤ ↔ Eq (α := Subalgebra ℤ (𝓞 K)) ℤ[θ] ⊤
Tactic: rw [exponent, absNorm_eq_one_iff, comap_eq_top_iff, conductor_eq_top_iff_adjoin_eq_top]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind (goal)
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)) ℤ[θ] ⊤
⊢ exponent θ = 1 ↔ Eq (α := Subalgebra ℤ (𝓞 K)) ℤ[θ] ⊤
have rw₃ : Eq (α := Subalgebra ℤ (𝓞 K)) ℤ[θ] ⊤ ↔ Eq (α := Subalgebra ℤ (𝓞 K)) ℤ[θ] ⊤
Tactic: rw [exponent, absNorm_eq_one_iff, comap_eq_top_iff, conductor_eq_top_iff_adjoin_eq_top]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind (goal)
Goal:
K : Type u_1
inst : Field K
θ : 𝓞 K
p : ℕ
inst_1 : Fact (Nat.Prime p)
⊢ ¬p ∣ exponent θ ↔
    Codisjoint (α := Ideal ℤ) (comap (F := ℤ →+* 𝓞 K) (algebraMap ℤ (𝓞 K)) (conductor ℤ θ)) (span {(↑p : ℤ)})
have rw : IsCoatom (α := Ideal ℤ) (span {(↑p : ℤ)})
Tactic: rw [codisjoint_comm, ← IsCoatom.not_le_iff_codisjoint, ← under_def, ← Ideal.dvd_iff_le,
    ← Int.ideal_span_absNorm_eq_self (under ℤ (conductor ℤ θ)),
    Ideal.span_singleton_dvd_span_singleton_iff_dvd, Int.natCast_dvd_natCast, exponent]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind (goal)
Goal:
K : Type u_1
inst : Field K
θ : 𝓞 K
⊢ exponent θ = sInf {d : ℕ | 0 < d ∧ Membership.mem (γ := Ideal (𝓞 K)) (conductor ℤ θ) (↑d : 𝓞 K)}
have rw : Eq (α := ℕ) ((absNorm : (a : Ideal ℤ) → ℕ) (under ℤ (conductor ℤ θ)) : ℕ)
  (sInf {d : ℕ | 0 < d ∧ Membership.mem (γ := Ideal (𝓞 K)) (conductor ℤ θ) (↑d : 𝓞 K)} : ℕ)
Tactic: rw [exponent, Int.absNorm_under_eq_sInf]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind (goal)
Goal:
K : Type u_1
inst : Field K
θ : 𝓞 K
rw :
  Eq (α := ℕ) ((absNorm : (a : Ideal ℤ) → ℕ) (under ℤ (conductor ℤ θ)) : ℕ)
    (sInf {d : ℕ | 0 < d ∧ Membership.mem (γ := Ideal (𝓞 K)) (conductor ℤ θ) (↑d : 𝓞 K)} : ℕ)
⊢ exponent θ = sInf {d : ℕ | 0 < d ∧ Membership.mem (γ := Ideal (𝓞 K)) (conductor ℤ θ) (↑d : 𝓞 K)}
have rw₁ : Eq (α := ℕ) (sInf {d : ℕ | 0 < d ∧ Membership.mem (γ := Ideal (𝓞 K)) (conductor ℤ θ) (↑d : 𝓞 K)})
  (sInf {d : ℕ | 0 < d ∧ Membership.mem (γ := Ideal (𝓞 K)) (conductor ℤ θ) (↑d : 𝓞 K)})
Tactic: rw [exponent, Int.absNorm_under_eq_sInf]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
θ : 𝓞 K
p : ℕ
inst_2 : Fact (Nat.Prime p)
hp : ¬p ∣ exponent θ
Q : ℤ[X]
⊢ Eq (α := HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (span {(↑p : 𝓞 K)}))
    ((ZModXQuotSpanEquivQuotSpan hp :
          (a : (ZMod p)[X] ⧸ span {Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ θ)}) → 𝓞 K ⧸ span {(↑p : 𝓞 K)})
        ((Ideal.Quotient.mk (span {Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ θ)}) :
              (a : (ZMod p)[X]) → (ZMod p)[X] ⧸ span {Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ θ)})
            (Polynomial.map (Int.castRingHom (ZMod p)) Q) :
          HasQuotient.Quotient (ZMod p)[X] (B := Ideal (ZMod p)[X])
            (span {Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ θ)})) :
      HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (span {(↑p : 𝓞 K)}))
    ((Ideal.Quotient.mk (span {(↑p : 𝓞 K)}) : (a : 𝓞 K) → 𝓞 K ⧸ span {(↑p : 𝓞 K)}) ((aeval θ : (a : ℤ[X]) → 𝓞 K) Q) :
      HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (span {(↑p : 𝓞 K)}))
have simp : Eq (α := HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (span {(↑p : 𝓞 K)}))
  ((quotientEquivAlgOfEq ℤ sorry :
        (a : 𝓞 K ⧸ Ideal.map (Int.castRingHom (𝓞 K)) (span {(↑p : ℤ)})) → 𝓞 K ⧸ span {(↑p : 𝓞 K)})
      (((quotMapEquivQuotQuotMap sorry sorry).symm :
          (a : (ℤ ⧸ span {(↑p : ℤ)})[X] ⧸ span {Polynomial.map (Ideal.Quotient.mk (span {(↑p : ℤ)})) (minpoly ℤ θ)}) →
            𝓞 K ⧸ Ideal.map (Int.castRingHom (𝓞 K)) (span {(↑p : ℤ)}))
        ((Ideal.Quotient.mk (span {Polynomial.map (Ideal.Quotient.mk (span {(↑p : ℤ)})) (minpoly ℤ θ)}) :
              (a : (ℤ ⧸ span {(↑p : ℤ)})[X]) →
                (ℤ ⧸ span {(↑p : ℤ)})[X] ⧸ span {Polynomial.map (Ideal.Quotient.mk (span {(↑p : ℤ)})) (minpoly ℤ θ)})
            (Polynomial.map (Ideal.Quotient.mk (span {(↑p : ℤ)})) Q) :
          HasQuotient.Quotient (HasQuotient.Quotient ℤ (B := Ideal ℤ) (span {(↑p : ℤ)}))[X] (B :=
            Ideal (HasQuotient.Quotient ℤ (B := Ideal ℤ) (span {(↑p : ℤ)}))[X])
            (span {Polynomial.map (Ideal.Quotient.mk (span {(↑p : ℤ)})) (minpoly ℤ θ)}))) :
    HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (span {(↑p : 𝓞 K)}))
  ((Ideal.Quotient.mk (span {(↑p : 𝓞 K)}) : (a : 𝓞 K) → 𝓞 K ⧸ span {(↑p : 𝓞 K)}) ((aeval θ : (a : ℤ[X]) → 𝓞 K) Q) :
    HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (span {(↑p : 𝓞 K)}))
Tactic: simp only [ZModXQuotSpanEquivQuotSpan, algebraMap_int_eq,
    RingEquiv.trans_apply, AlgEquiv.coe_ringEquiv, quotientEquivAlgOfEq_mk,
    quotientEquiv_symm_apply, quotientMap_mk, RingHom.coe_coe, mapEquiv_symm_apply,
    Polynomial.map_map, Int.quotientSpanNatEquivZMod_comp_castRingHom]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind (goal)
Goal:
K : Type u_1
inst : Field K
θ_1 : 𝓞 K
inst_1 : NumberField K
θ : 𝓞 K
p : ℕ
inst_2 : Fact (Nat.Prime p)
hp : ¬p ∣ exponent θ
Q : ℤ[X]
hQ : Membership.mem (γ := Finset (ZMod p)[X]) (monicFactorsMod θ p) (Polynomial.map (Int.castRingHom (ZMod p)) Q)
h₀ : Ne (α := (ZMod p)[X]) (Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ θ)) 0
⊢ Eq (α := Ideal (ZMod p)[X]) (span {Polynomial.map (Int.castRingHom (ZMod p)) Q})
    (span {Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ θ)} ⊔
      span {Polynomial.map (Int.castRingHom (ZMod p)) Q})
have rw : Dvd.dvd (α := (ZMod p)[X]) (Polynomial.map (Int.castRingHom (ZMod p)) Q)
  (Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ θ))
Tactic: rw [← span_insert, span_pair_comm, span_pair_eq_span_left_iff_dvd.mpr]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind (hypothesis)
Goal:
K : Type u_1
inst : Field K
θ_1 : 𝓞 K
inst_1 : NumberField K
θ : 𝓞 K
p : ℕ
inst_2 : Fact (Nat.Prime p)
hp : ¬p ∣ exponent θ
Q : ℤ[X]
hQ : Membership.mem (γ := Finset (ZMod p)[X]) (monicFactorsMod θ p) (Polynomial.map (Int.castRingHom (ZMod p)) Q)
h₀ : Ne (α := (ZMod p)[X]) (Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ θ)) 0
⊢ Dvd.dvd (α := (ZMod p)[X]) (Polynomial.map (Int.castRingHom (ZMod p)) Q)
    (Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ θ))
have hQ₁ : Membership.mem (γ := Multiset (ZMod p)[X]) (normalizedFactors (Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ θ)))
  (Polynomial.map (Int.castRingHom (ZMod p)) Q)
Tactic: simp only [Multiset.mem_toFinset] at hQ
Cleared hypotheses: hQ